[Verifpal] Trouble with simple naive DH handshake

[Loup Vaillant David]

This is my first real question here. I have some trouble understanding
Verifpal's output for the trivial handshake: Alice and Bob know each
other's key, they do a DH exchange, which Alice uses to send a message
to Bob.

We assume an active attacker:

    attacker[active]


Alice and Bob pre-compute their static key:

    principal Alice[
        knows private a
        a_public = G^a
    ]
    principal Bob[
        knows private b
        b_public = G^b
    ]


Then they communicate their keys over a secure channel (hence the
guards):

    Alice -> Bob   : [a_public]
    Bob   -> Alice : [b_public]


Once that's done, Alice generates a message, computes the shared
secret, then sends the whole thing to Bob.

    principal Alice[
        generates plaintext
        generates ad
        ss         = b_public^a
        key        = HASH(ss)
        ciphertext = AEAD_ENC(key, plaintext, ad)
    ]
    Alice -> Bob : ad, ciphertext


Finally, Bob receives the message, and computes the plaintext back:


    principal Bob[
        ss_        = a_public^b
        key_       = HASH(ss_)
        plaintext_ = AEAD_DEC(key_, ciphertext, ad)?
    ]


To check it all works out, we check the confidentiality and integrity
of the message:

    queries[
        confidentiality? plaintext
        confidentiality? plaintext_
        authentication? Alice -> Bob : ciphertext
        authentication? Alice -> Bob : ad
    ]


Now when we run the analysis on all that, it looks like it comes clean.
I have some analysis, info, and deduction lines, but no result. So I
started to play with that model:

- What happens if we remove the check after AEAD_DEC()?
- What happens if we remove the guard around a_public?
- What happens if we remove the guard around b_public?

I expected something bad would have happened in all three cases. But
according to Verifpal, security is broken *only* when we remove the
guard around b_public. Which I found very odd.

If we remove the check after AEAD_DEC(), my intuition is that it should
have the same effect as an implementation that doesn't check the
relevant return value: no check, therefore no integrity. I expected a
"result!" telling me the integrity of ad and ciphertext was not
guaranteed. Worse, removing the AEAD_DEC() line *entirely* doesn't seem
to affect the integrity of ad and ciphertext. Intuitively, it should:
if Bob doesn't even look at ciphertext, there's no way its integrity is
preserved, is there?

If we remove the guard around a_public, my intuition is that it was not
transmitted over a secure channel, and may be modified by the attacker,
effectively impersonating Alice. The integrity of ad and ciphertext
should be compromised. But again, Verifpal seems to think everything is
all right.

If we remove the guard around b_public, then *at last* Verifpal catches
the problem, and tells me the attacker can break all security.

I get the feeling that I missed something. Was my model wrong, perhaps?


---

Another minor trouble I have is that I didn't find a way to check that
my protocol actually works. In this case, I want to be sure that
plaintext (encrypted by Alice) and plaintext_ (decrypted by Bob) are
the same value (assuming no attacker at all).  It would be nice if I
had a way to perform such basic checks.

Suggestion: an intuitive way to perform those checks could be to
actually allow users to use the same name for different constants.
Except Verifpal would check that all constants with the same name are
guaranteed to be equal if all goes well. This would help a great deal
with Diffie-Hellman exchanges, as well ass encryption and decryption:
we'd have some consistency checks almost for free, and we wouldn't have
to use different names for the same things.

A possible downside is worse error messages, but I'm not sure that's a
big issue. I feel that the readability of the model itself is more
important. I believe seeing the same name for different (but guaranteed
equal) constants would significantly improve that readability.

Loup.

-------------- next part --------------
attacker[active]

// initialisation
principal Alice[
    knows private a
    a_public = G^a
]
principal Bob[
    knows private b
    b_public = G^b
]
Alice -> Bob   : [a_public]
Bob   -> Alice : [b_public]


// Key exchange
principal Alice[
    generates plaintext
    generates ad
    ss         = b_public^a
    key        = HASH(ss)
    ciphertext = AEAD_ENC(key, plaintext, ad)
]
Alice -> Bob : ad, ciphertext

principal Bob[
    ss_        = a_public^b
    key_       = HASH(ss_)
    plaintext_ = AEAD_DEC(key_, ciphertext, ad)?
]

queries[
    confidentiality? plaintext
    confidentiality? plaintext_
    authentication? Alice -> Bob : ciphertext
    authentication? Alice -> Bob : ad
]