[Verifpal] Trouble with simple naive DH handshake

[Nadim Kobeissi]

Dear Loup,

It’s not that authentication is broken in Verifpal. It’s rather that while the definition of authentication is operating as designed, that definition is too restricted and, as you show, very unrealistic, especially when it comes to detecting the potential for violations of message integrity.

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

I think you’re right and that Verifpal’s requirements for what constitute authentication must be expanded to be more considerate of violations to message integrity. I will work on this immediately and may have something for us to test perhaps today.

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

Again, the TLS 1.3 example here is very representative. Abortion simply means “something’s not right, stop everything,” which is what happens in TLS in the event of a bad transcript hash. Parties are free to attempt another session, of course. I’m perfectly fine with how this works and don’t see a reason for it to be changed (please feel free to argue otherwise.)

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

No, a nodding Verifpal doesn’t mean that:
	The message was authenticated despite Bob not reading it.
It means, rather, that:
	No scenario was found in which Bob reads an unauthenticated message.
So, in that sense, Verifpal’s output is perfectly sensible in this respect. This is a *critically* important distinction. I think I must make sure I clarify it in the User Manual. This sort of misunderstanding could be very misleading to users.

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

This is the heart of the problem. We do agree on this, but the way Verifpal currently captures this definition is, I think, not sufficient, as you successfully argue.

I’m making this my current top priority, will send an update soon.

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

> On Sep 2, 2019, at 1:02 AM, Loup Vaillant David <loup at loup-vaillant.fr> wrote:
> 
> 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.
> 
> 
>