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

Tom Hacohen tom at stosb.com
Wed Feb 5 12:22:33 CET 2020


Hey,

With pleasure, and thanks for the super quick fix!

I know nothing about formal verification, and even less about verifpal,
though I have a question that's related to the fix.

The problem, as I see it, is not with the KDF or anything about the KDF.
It's about collection_key being a secret, no matter how it was created,
and that secret being leaked. What I'm asking essentially, is why does
it matter how collection_key was created for the analysis if
collection_key is only used as the content of the message? Wouldn't this
lead to similar bugs using other ways to create this value? Also, this
therefore shouldn't make a lot of a difference when it comes to
performance, because the attacker is (still) only able to modify what's
being sent, doesn't matter how that something was created.

Thanks again for the quick turn-around on this.

--
Tom

On 05/02/2020 10:54, Nadim Kobeissi wrote:
> 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
> <mailto: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
> 


More information about the Verifpal mailing list