[Verifpal] I found a case where a broken protocol is not failing verification

Nadim Kobeissi nadim at symbolic.software
Wed Feb 5 09:54:33 CET 2020


Dear Tom,

Thank you very much for this.

This issue has been addressed here:
https://source.symbolic.software/verifpal/verifpal/commit/2c2c51e93b2b7f6cda07d61f7be34bdaea7859f3


A test has been added based on your model here:
https://source.symbolic.software/verifpal/verifpal/commit/7ebde2a2067e370a3d98317ddda31fd663b83b6c

The fix for this issue will be included in the Verifpal 0.10.2 update.

The issue stems from Verifpal trying to avoid (a bit too successfully)
including HKDF mutations in its analysis, since those are incredibly
expensive and slow down analysis greatly. As such, Verifpal will indeed be
a lot slower moving forward for many protocols (this is the only way to
resolve this issue).

Nadim Kobeissi
Symbolic Software • https://symbolic.software
Sent from office


On Wed, Feb 5, 2020 at 9:10 AM Tom Hacohen <tom at stosb.com> wrote:

> Hey,
>
> As the subject says, I found a case where a broken protocol is not
> failing verification. What makes it even more interesting is that a very
> small variation is. I tested this with both 0.9.2 and 0.10.1 and it
> behaves incorrectly in both cases.
>
> Consider the below:
>
>     attacker[active]
>
>     principal Alice[]
>     principal Bob[]
>
>     principal Alice[
>         // Encryption password
>         knows password a_pass
>         derived = PW_HASH(a_pass)
>
>         // Keypair
>         generates a
>         ga = G^a
>
>         // Collection key
>         generates collection_uid
>         collection_key = HKDF(collection_uid, derived, nil)
>     ]
>
>     Alice -> Bob: collection_uid
>
>     principal Bob[
>         // Keypair
>         generates b
>         gb = G^b
>     ]
>
>     Bob -> Alice: [gb]
>     principal Alice[
>         e_collection_key = PKE_ENC(gb, collection_key)
>     ]
>
>     Alice -> Bob: e_collection_key
>
>     principal Bob[
>         b_collection_key = PKE_DEC(b, e_collection_key)
>     ]
>
>     queries[
>         confidentiality? collection_key
>         authentication? Alice -> Bob: e_collection_key
>     ]
>
>
> This authentication query should fail because e_collection_key is not
> signed or otherwise authenticated, so Eve can just send whatever she
> wants, and Bob will use it. Even though it doesn't fail, a small
> adjustment, that shouldn't make a fail, does make it fail. Specifically,
> you just need to replace the first Alice block with this.
>
>     principal Alice[
>         // Encryption password
>         knows password a_pass
>         collection_pass = PW_HASH(a_pass)
>
>         // Keypair
>         generates a
>         ga = G^a
>
>         generates collection_uid
>     ]
>
> This change has nothing to do with the authentication of the message,
> just with the content of it, so I'm not sure why it makes a difference,
> though it definitely looks like a bug.
>
> Please let me know if you need any addition information.
>
> --
> Tom
>
> _______________________________________________
> 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/20200205/565806e7/attachment.htm>


More information about the Verifpal mailing list