[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 20:58:01 CEST 2020


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


More information about the Verifpal mailing list