[Verifpal] Trouble with simple naive DH handshake

[Nadim Kobeissi]

Dear Loup,

I’m very excited to see the first critical analysis of Verifpal results on this list! Let’s dig into the puzzle that you are offering here.

1. Indeed, your model as initially communicated in the attachment `simple.pv` does not contradict any queries, since the guards are sufficient to prevent attacks. Therefore nothing unusual is happening here.

2. The query for the confidentiality of “plaintext_" can be removed, since it is somewhat identical for all practical purposes in this model to the query for the confidentiality of “plaintext”.

3. Regarding the query results, I am going to model two scenarios and explain the results.
	a. Unguard a_public only:
		In this model, only Alice encrypts only one message to Bob. When doing so, she is *always* using her correct private key, since it is local to her state, and she is *always* using Bob’s correct public key, since it is guarded. Since the attacker cannot obtain either Alice or Bob’s public key, the message retains confidentiality. Therefore, the results are within expectations.
	b. Unguard b_public only:
		In this model, only Alice encrypts only one message to Bob. When doing so, she is *always* using her correct private key, since it is local to her state, but she may encrypt to the attacker’s key thinking that it is Bob’s public key. Since the attacker can coerce Alice to encrypt to a public key for a private key that the attacker controls, a contradiction may be found for the confidentiality query. Therefore, the results are within expectations.

Now, let’s use the above information in order to address the points in your email directly.

> 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.

This is addressed by point 3.a.

> 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. 

That is not what checks do in Verifpal. According to the Verifpal User Manual, Section 2.4.4:
"In Verifpal, AEAD_DEC, HMACVERIF, and SIGNVERIF are “checkable” primitives: if you add a question mark (?) after one of these primitives, then model execution will abort should AEAD_DEC fail authenticated decryption, or should HMACVERIF fail to find its two provided inputs equal, or should SIGNVERIF fail to verify the signature against the provided message and public key.”

Checks instruct the principals to abort protocol execution if a check fails. This is similar, for example, to how TLS aborts the handshake setup phase if the transcript hashes do not match [0] and indeed the feature of checked primitives was inspired specifically by that real-world example.

Furthermore, whether or not the primitive is checked, “plaintext_” will only be rewritten to “plaintext_ = plaintext” if the rewrite pre-conditions are met. Otherwise “plaintext_ = AEAD_DEC(key_, ciphertext, ad)“.

Also, keep in mind that authentication queries test for authentication, which is a property of which integrity is a subset, and not an entirely clean subset at that. If you want to see what happens when authentication is broken, then allow the attacker to impersonate Alice — for example by leaking “a”. Does this design decision make it such that Verifpal is less intuitive? Should this be investigated more closely? That is possible, and I encourage you to pursue your critical thinking.

> 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.

Verifpal does perform these checks! :-) Try keeping AEAD_DEC checked and replace “key_" with some blatantly incorrect value (e.g. “a_public”) and see what happens.

If you keep challenging Verifpal with different models, especially at this early stage in development, I am certain that you will eventually find room for improvement in the verification output. Thanks again for this interesting and useful critical investigation! 

References:
[0] https://tls13.ulfheim.net/ (click on “Client Handshake Finished”)

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

> On Sep 1, 2019, at 6:31 PM, Loup Vaillant David <loup at loup-vaillant.fr> wrote:
> 
> 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.
> 
> <simple.vp>
> _______________________________________________
> Verifpal mailing list
> Verifpal at lists.symbolic.software
> https://lists.symbolic.software/mailman/listinfo/verifpal