[Verifpal] Needham-Schroeder protocol

Friedrich Wiemer friedrich.wiemer at rub.de
Thu Mar 12 10:25:06 CET 2020


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.

Dr. Friedrich Wiemer,
Research Assistant

Symmetric Cryptography
Horst Goertz Institute for IT-Security,
Ruhr-University Bochum,

-------------- next part --------------

principal Server[
    knows private k_sa
    knows private k_sb
    knows private k_ab
principal Alice[
    knows private k_sa
principal Bob[
    knows private k_sb

principal Alice[
    generates A
    generates B
    generates Na
Alice -> Server: A, B, Na

principal Server[
    m_bob = CONCAT(k_ab, A)
    e_bob = AEAD_ENC(k_sb, m_bob, nil)

    m_alice = CONCAT(k_ab, B, Na, e_bob)
    e_alice = AEAD_ENC(k_sa, m_alice, nil)
Server -> Alice: [e_alice]

principal Alice[
    e_alice_dec = AEAD_DEC(k_sa, e_alice, nil)?
    k_ab_dec_alice, B_dec, Na_dec, e_bob_dec = SPLIT(e_alice_dec)
Alice -> Bob: e_bob_dec

principal Bob[
    e_bob_decdec = AEAD_DEC(k_sb, e_bob_dec, nil)?
    k_ab_dec_bob, A_dec = SPLIT(e_bob_decdec)

    generates Nb
    eNb = AEAD_ENC(k_ab_dec_bob, Nb, nil)
Bob -> Alice: eNb

principal Alice[
    Nb_dec = AEAD_DEC(k_ab_dec_alice, eNb, nil)?
    Nb_minus_one = HASH(Nb_dec)
    eNb_minus_one = AEAD_ENC(k_ab_dec_alice, Nb_minus_one, nil)
Alice -> Bob: eNb_minus_one

principal Bob[
    Nb_minus_one_dec = AEAD_DEC(k_ab_dec_bob, eNb_minus_one, nil)?
    _ = ASSERT(Nb_minus_one_dec, HASH(Nb))?

    confidentiality? k_ab
    authentication? Alice -> Bob: eNb_minus_one
    authentication? Bob -> Alice: eNb
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 488 bytes
Desc: not available
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20200312/7805f5da/attachment.sig>

More information about the Verifpal mailing list