PROTOCOL:
NSPK: Needham-Schroeder Public-Key Protocol

VARIANT:
original version (of 1978) without key server

PURPOSE:
Two-party mutual autentication
 

MODELER:
David von Oheimb, Siemens CT IC 3, January 2005
 

ALICE_BOB:

 1. A  - {Na.A}_Kb ----> B
 2. A <- {Na.Nb}_Ka ---  B
 3. A  - {Nb}_Kb ------> B
 

PROBLEMS:
3
 

CLASSIFICATION:
G1, G3, G12
 

ATTACKS:
Man-in-the-middle attack,
where in the first session Alice talks with the intruder as desired and in the second session Bob wants to talk with Alice but actually talks to the intruder. Therefore, also the nonce Nb gets leaked.
 1.1  A  - {Na.A}_Ki --> i   	
 2.1                     i(A)  - {Na.A}_Kb  -> B   	
 2.2                     i(A) <- {Na.Nb}_Ka -  B
 1.2  A <- {Na.Nb}_Ka -  i
 1.3  A  - {Nb}_Ki ----> i
 2.3                     i(A)  - {Nb}_Kb ----> B
 


HLPSL:

role alice (A, B: agent,             
            Ka, Kb: public_key,      
            SND, RCV: channel (dy)) 
played_by A def=

  local State : nat, 
        Na, Nb: text

  init State := 0

  transition  
   
    0.  State  = 0 /\ RCV(start) =|> 
        State':= 2 /\ Na' := new() /\ SND({Na'.A}_Kb)
                   /\ secret(Na',na,{A,B}) 
                   /\ witness(A,B,bob_alice_na,Na')

    2.  State  = 2 /\ RCV({Na.Nb'}_Ka) =|> 
        State':= 4 /\ SND({Nb'}_Kb) 
                   /\ request(A,B,alice_bob_nb,Nb')

end role


role bob(A, B: agent, Ka, Kb: public_key, SND, RCV: channel (dy)) played_by B def= local State : nat, Na, Nb: text init State := 1 transition 1. State = 1 /\ RCV({Na'.A}_Kb) =|> State':= 3 /\ Nb' := new() /\ SND({Na'.Nb'}_Ka) /\ secret(Nb',nb,{A,B}) /\ witness(B,A,alice_bob_nb,Nb') 3. State = 3 /\ RCV({Nb}_Kb) =|> State':= 5 /\ request(B,A,bob_alice_na,Na) end role
role session(A, B: agent, Ka, Kb: public_key) def= local SA, RA, SB, RB: channel (dy) composition alice(A,B,Ka,Kb,SA,RA) /\ bob (A,B,Ka,Kb,SB,RB) end role
role environment() def= const a, b : agent, ka, kb, ki : public_key, na, nb, alice_bob_nb, bob_alice_na : protocol_id intruder_knowledge = {a, b, ka, kb, ki, inv(ki)} composition session(a,b,ka,kb) /\ session(a,i,ka,ki) /\ session(i,b,ki,kb) end role
goal secrecy_of na, nb authentication_on alice_bob_nb authentication_on bob_alice_na end goal
environment()