[Verifpal] Needham-Schroeder protocol

Nadim Kobeissi nadim at symbolic.software
Tue May 19 20:28:55 CEST 2020


Hello everyone,

Verifpal 0.3.15 will fix an issue where Verifpal failed to detect Gavin
Lowe's attack
on the public-key variant of Needham-Schroeder.

In order for this attack to be detected, it should be only necessary to
model standard Needham-Schroeder and to unguard Bob's public key, while
leaving Alice's guarded. However, Verifpal would in this scenario did not
detect the attack if Alice were to used a checked ASSERT in order to
verify that the message she received from Bob did indeed contain her
correct nonce on top of Bob's nonce. This is incorrect behavior.

The issue lay with the fact that the Verifpal mutation map did not
actually include a fully resolved expression of the original un-mutated
value by default, but only a pristine copy of the non-resolved
expression.

A new test has been added that shows that Verifpal can correctly detect
Lowe's attack in a standard Needham-Schroeder model with all the correct
checked ASSERTs and no undue "nudging" of Verifpal. A subsequent commit
will also contain a test that shows that Lowe's proposed fix for the
attack does indeed fix the attack in Verifpal.

Incidentally, the fix for this issue also dramatically speeds up
Verifpal's performance, cutting integration test run times by half.

It is now the case that Verifpal can detect Gavin Lowe's attack with only
Bob's
public key being unguarded (and Alice's remaining guarded), even if Alice
checks
to see if nonces match always:

https://source.symbolic.software/verifpal/verifpal/-/blob/master/examples/test/needham-schroeder-pk.vp


Lowe's fix is modeled here:
https://source.symbolic.software/verifpal/verifpal/-/blob/master/examples/test/needham-schroeder-pk-withfix.vp

Verifpal 0.13.5 will contain these fixes.

Nadim Kobeissi
Symbolic Software • https://symbolic.software
Sent from office


On Wed, Mar 18, 2020 at 10:36 AM Friedrich Wiemer <friedrich.wiemer at rub.de>
wrote:

> Dear Nadim,
>
> I wasn't aware that replay attacks are currently not detected. That's
> good to know (and maybe I just missed the paragraph in the documentation).
>
> Regarding the second point: I guess my experience with formal
> verification is not enough to be a help in this discussion. Anyway
> thanks for the detailed explanation. Looking forward to the development :)
>
> Best,
> Friedrich
>
> Am 17.03.2020 um 22:21 schrieb Nadim Kobeissi:
> > Dear Friedrich,
> >
> > Thank you very much for bringing the classic Needham-Schroeder case
> scenario into view.
> >
> > I’ve modeled both symmetric and classical Needham Schroeder in Verifpal
> and added these models to the `example` folder in the master branch. I have
> some interesting things to remark here:
> >
> > Symmetric Needham-Schroeder:
> > Verifpal currently does not detect replay attacks. This is a known
> limitation and is slated as a to-do item for this year. So indeed, there is
> nothing surprising here. However...
> >
> > Public-Key Needham-Schroeder:
> > Gavin Lowe’s 1995 attack will only be detected if Alice and Bob’s keys
> are unguarded. I wonder if this is fair, and think it might not be. There
> should be a more intuitive way to capture that even if Alice and Bob
> communicate to each other with pre-authenticated public keys, it is still
> the case that Alice may in parallel set up a session with a compromised
> Carol, without this being explicitly written down in the model or
> unguarding Alice and Bob’s public keys (doing either will immediately
> reveal Gavin Lowe’s attack in current Verifpal versions.)
> >
> > I think therefore that serious thought needs to be given as to whether
> we want to automatically capture and illustrate Gavin Lowe’s attack even if
> we have a model where Alice only talks to Bob and both their public keys
> are guarded. To me this is the real question that arises here from looking
> at Needham-Schroeder, and is more important than replay attack detection
> for the time being. Indeed it’s a fundamental question regarding the
> expectations we can impose on Verifpal’s eventual analysis given what is
> initially described in the model.
> >
> > Nadim Kobeissi
> > Symbolic Software • https://symbolic.software
> >
> >> On 12 Mar 2020, at 10:25 AM, Friedrich Wiemer via Verifpal
> <verifpal at lists.symbolic.software> wrote:
> >>
> >> Signed PGP part
> >> Hi,
> >>
> >> I have thought a bit more about my Needham-Schroeder protocol model and
> >> I think the solution using guards should be fine to model the protocol
> >> (at least I do not see how this would change any of its properties).
> >>
> >> That beeing said, I think verifpal is missing an attack here. For
> >> reference, I'm following the protocol description from "Protocols for
> >> Authentication and Key Establishment" by Boyd and Mathuria (in
> >> particular Figs. 1.7 and 1.8 on pages 10f).
> >>
> >>
> >> The protocol works as follows:
> >>
> >> A -> S: A, B, Na
> >> (two identifiers of the parties that whish to communicate and a nonce)
> >>
> >> S -> A: {Kab, B, Na, {Kab, A}_Kbs}_Kas
> >> (a message encrypted under the long-term secret key of A and S,
> >> containing the session key Kab, identifier B, nonce Na, and a message
> >> encrypted under the long-term secret key of B and S containing the
> >> session key Kab and identifier A)
> >>
> >> A -> B: {Kab, A}_Kbs
> >> B -> A: {Nb}_Kab
> >> A -> B: {hash(Nb)}_Kab
> >>
> >>
> >> However, there exists a reply attack on the protocol, where an
> >> adversary can impersonate A in the last three protocol messages:
> >>
> >> C -> B: {K'ab, A}_Kbs
> >> B -> C: {Nb}_K'ab
> >> C -> B: {hash(Nb)}_K'ab
> >>
> >> (the attack is due to Denning and Sacco).
> >>
> >>
> >> So in my understanding, verifpal should not verify the protocol - or
> >> maybe my modeling is wrong. Attached is the verifpal model I'm using.
> >>
> >> Thanks in advance for the support.
> >> Best,
> >> Friedrich
> >>
> >> --
> >> Dr. Friedrich Wiemer,
> >> Research Assistant
> >>
> >> Symmetric Cryptography
> >> Horst Goertz Institute for IT-Security,
> >> Ruhr-University Bochum,
> >>
> >> orcid.org/0000-0003-2998-6777
> >> <needham-schroeder.vp>
> >>
> >>
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20200519/150d5262/attachment.htm>


More information about the Verifpal mailing list