[Verifpal] Trouble with simple naive DH handshake

[Loup Vaillant David]

Hi, thanks for your response.

Confidentiality is not the issue here. That part is okay.
Authentication however is broken. Possibly by my own misunderstanding,
but the end result is the same: I have broken protocols, and Verifpal
gave me the green light anyway. To me, that feels like Verifpal *missed
attacks*.


When I write this:

    authentication? Alice -> Bob : ciphertext

I expect Verifpal to check that completing the protocol means Bob was
able to ascertain that `ciphertext` indeed came from Alice, unmodified.
More specifically:

- If Bob doesn't even read an incoming message, that message is not
  authenticated to him.
- If Bob doesn't put the message through a checkable primitive, whose
  return value is checked (that would be the question mark), then that
  message is not authenticated to him.
- If Bob cannot ascertain the origin of a key, messages authenticated
  with that key may not come from Alice.

And yet:

- Verifpal gave me the green light even when Bob did not check the 
  return value of AEAD_DEC(). (Removing the question mark)
- Verifpal gave me the green light even when Bob did not even read
  `ciphertext`. (Removing the entire AEAD_DEC() line.)
- Verifpal gave me the green light even when Bob could not tell whether
  he has Alice's key, or the attacker's. (Removing the guard around
  `a_public`.)

I strongly believe Verifpal should not give the green light in these
cases.

Why does it anyway?  Is there a way to correct that problem?

---

About a couple specific points:


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

That only addresses confidentiality. Not authentication. If a_public is
not guarded, Bob has no way to tell if he got the right public key. He
has no way to distinguish Alice from the attacker.


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

I believe you didn't address the authentication part.


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

Well, yeah, the manual refers here to an execution model only you
really know.  As a user, I'm not really sure what "aborting a protocol"
really means. For instance, does aborting a protocol also means the
party that aborted it has an "aborted, don't trust" flag? Or does it
mean we just stopped?

Even then, removing the line entirely has the same effect: Verifpal
still sees no problem. Bob does not even *read* the message and
Verifpal still nods when I ask whether that message is authenticated.
It's obviously not: if I don't read a message, I cannot possibly
ascertain its provenance.


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

Err… well… Do we agree that authentication means the recipient can tell
where the message came from (depending on the notion of identity) *and*
the message was not tampered with?


> If you want to see what happens when authentication is broken, then
> allow the attacker to impersonate Alice — for example by leaking “a”.

That's the thing: allowing `a_public` to be transmitted over a channel
under the control of an active attacker *does* allow that attacker to
impersonate Alice. I don't understand why Verifpal doesn't agree with
me.

Loup.