[Verifpal] Trouble with simple naive DH handshake

[Nadim Kobeissi]

Dear Loup,

I’m very happy to be able to get back to you with an update today as promised.

The main weakness with Verifpal’s existing understanding of authentication was that it authenticated the message itself only — so if the attacker tampered with the message, then Verifpal would consider it as different from that which it was responsible for authenticating. This is really quite unrealistic and I’m glad we are moving away from it.

I just pushed to GitHub a !!!HIGHLY EXPERIMENTAL!!! set of changes, which I *think* will allow the attacker better ability to detect tamper-vulnerable messages. Furthermore, the resolution logic that Verifpal used for certain elements was subpar and I have now improved it.

The results I’ve gotten from limited testing thus far are encouraging, but:
1. I am 70% sure we will run into missed attacks, as I’m not sure my extensions to the methodology are sufficiently complete and sound and have so far had little time to perform rigorous testing.
2. I am 10% sure I’ve broken some thing or another while implementing this.

Loup, what I would really appreciate for you to do is just go to town and just test the heck out of Verifpal. Act as a human fuzzer. Produce strange models that explicitly attempt to trick Verifpal towards incorrect, misleading or unintuitive results, and let me know what you find. Hopefully it will be less easy than it was this time.

Please keep me updated, and thanks again. I will join you in testing some time tomorrow or later in the week, but I’m afraid that this week is full of work and teaching for me, so any assistance is very much appreciated.

I very sincerely appreciate your collaboration, and will make sure to mail you some Verifpal stickers as well as a hardcover, full-color print of the User Manual as a thank-you.

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

> On Sep 2, 2019, at 11:13 AM, Loup Vaillant David <loup at loup-vaillant.fr> wrote:
> 
> Thanks, I'm looking forward to trying the next version.
> 
> 
>> 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.)
> 
> I'll need to study a bit more before I can argue anything. I'll take a
> closer look at the TLS 1.3 example. Right now I don't understand what
> design decision lead to what result exactly, so I'd rather be cautious.
> 
> 
>> 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.
> 
> Okay, that explains a lot. And I can see how useful that could be: if
> Bob doesn't read the message, who cares it's not authenticated? It's
> not even part of the attack surface.
> 
> On the other hand, the user supposedly wrote the query for a reason. If
> we care about the authentication of the message, doesn't it mean Bob
> (the real Bob, when we implement the actual software) is supposed to
> read it eventually?
> 
> Maybe we could add a warning? If the user is making an authentication
> query, they presumably care about it. If the model is such that this
> authentication does not even matter, I believe this means the user made
> a mistake in most cases: either they really don't care about
> authenticating that message, or they forgot to have it read by the
> recipient.
> 
> Loup.
> 
>