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

Tom Hacohen tom at stosb.com
Wed Feb 5 09:10:39 CET 2020


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


More information about the Verifpal mailing list