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

Friedrich Wiemer friedrich.wiemer at rub.de
Thu Oct 22 10:54:02 CEST 2020


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/20201022/1eac8ac6/attachment.htm>


More information about the Verifpal mailing list