VARIANT:
fix by Lowe (of 1995) 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.B}_Ka -  B
 3. A  - {Nb}_Kb ------> B
 

PROBLEMS:
3
 

ATTACKS:
None
 


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'.B}_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'.B}_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()