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

Nadim Kobeissi nadim at symbolic.software
Wed Oct 21 23:16:35 CEST 2020


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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20201021/d1c866a6/attachment-0001.htm>


More information about the Verifpal mailing list