[Verifpal] Crash when sending an already known value within concat and checking it with assert
Friedrich Wiemer
friedrich.wiemer at rub.de
Sun Nov 1 20:51:21 CET 2020
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>
More information about the Verifpal
mailing list