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

Nadim Kobeissi nadim at symbolic.software
Wed Feb 5 15:36:23 CET 2020


Verifpal 0.10.3, to be released shortly, will provide heuristic-powered speedups to counter the slowdown introduced by HKDF mutations.

Nadim Kobeissi
Symbolic Software • https://symbolic.software

> On 5 Feb 2020, at 12:22 PM, Tom Hacohen <tom at stosb.com> wrote:
> 
> 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: Message signed with OpenPGP
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20200205/c14cb5b5/attachment.sig>


More information about the Verifpal mailing list