[Verifpal] Trouble with simple naive DH handshake

[Loup Vaillant David]

Okay, I'll compile the master branch and begin testing starting
tomorrow evening (err, today by my clock, I'm a little late to bed). If
I find some time and courage, I'll even take a look at the source code.

I *need* Verifpal, I promise I won't let go until it works.

See you soon,
Loup.


On Mon, 2019-09-02 at 23:44 +0200, Nadim Kobeissi wrote:
> 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.
> > 
> > 
> 
>