[Verifpal] Trouble with simple naive DH handshake

[Loup Vaillant David]

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.