[Verifpal] Crash when sending an already known value within concat and checking it with assert

[Friedrich Wiemer]

Hi Nadim,

I finally found time to look into this again. The model does not produce any crash anymore. Don't know what has happened here. I guess we can close this issue.

Best, 
Friedrich


On October 22, 2020 8:58:01 PM GMT+02:00, Friedrich Wiemer via Verifpal <verifpal at lists.symbolic.software> wrote:
>Dear Nadim,
>
>I tried to reproduce the crash on my private laptop and it works as
>expected. I also tried both versions 0.19.2 and 0.19.3 with the same
>result.
>
>Will try again on my work laptop tomorrow, to see if I missed something
>or so.
>
>Best,
>Friedrich
>
>Am 22/10/2020 um 10:54 schrieb Friedrich Wiemer via Verifpal:
>> Thanks for checking. I'll have another look later. I tried to reduce
>the
>> model as much as possible and the crash appeared and disappeared
>> somewhat arbitrarily looking for me.
>> 
>> On October 21, 2020 11:16:35 PM GMT+02:00, Nadim Kobeissi
>> <nadim at symbolic.software> wrote:
>> 
>>     Dear Friedrich,
>> 
>>     I cannot reproduce this crash on the current version of Verifpal
>>     (0.19.3) by running your model. Are you sure you've sent the
>correct
>>     model?
>> 
>>     Here are the analysis results successfully on Verifhub as
>evidence:
>>     https://verifhub.verifpal.com/d742e895968823096abc5249382c13e1
>> 
>>     Nadim Kobeissi
>>     Symbolic Software • https://symbolic.software
>>     Sent from office
>> 
>> 
>>     On Wed, Oct 21, 2020 at 10:19 PM Friedrich Wiemer via Verifpal
>>     <verifpal at lists.symbolic.software> wrote:
>> 
>>         Here is another crashing model:
>> 
>>         attacker[active]
>> 
>>         principal Client[
>>             generates skc
>>             pkc = G^skc
>>         ]
>>         principal Server[
>>             generates sks
>>             pks = G^sks
>>         ]
>>         Server -> Client: [pks]
>>         principal Client[
>>             generates nc
>>             mcs = CONCAT(pkc, nc, pks)
>>         ]
>>         Client -> Server: pkc, mcs
>>         principal Server[
>>             pkc_recv, nc_recv, pks_recv = SPLIT(mcs)
>>             _ = ASSERT(pks, pks_recv)?
>>             generates ns
>>         ]
>>         Server -> Client: ns
>>         principal Client[ kcs = HASH(ns) ]
>> 
>>         queries[
>>             authentication? Client -> Server: mcs
>>             authentication? Server -> Client: ns
>>             confidentiality? kcs
>>         ]
>> 
>>         This seems to be related to sending the already known value
>>         'pkS' to the server and then having the server check
>>         'ASSERT(pks, pks_recv)'. Note that sending the already known
>>         value only works, because its "hidden" inside the concat.
>Maybe
>>         this should be handled similarly to sending the values
>directly,
>>         or does that not make sense?
>> 
>>         Best,
>>         Friedrich
>
>-- 
>Dr. Friedrich Wiemer,
>orcid.org/0000-0003-2998-6777
>
>_______________________________________________
>Verifpal mailing list
>Verifpal at lists.symbolic.software
>https://lists.symbolic.software/mailman/listinfo/verifpal

--
Dr. Friedrich Wiemer,
orcid.org/0000-0003-2998-6777 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20201101/16345f21/attachment.htm>