[Verifpal] Needham-Schroeder protocol

Nadim Kobeissi nadim at symbolic.software
Tue Mar 17 22:21:27 CET 2020

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 --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: Message signed with OpenPGP
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20200317/fb599238/attachment.sig>

More information about the Verifpal mailing list