[Verifpal] Needham-Schroeder protocol

[Friedrich Wiemer]

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>
>>
>>
>