%% PROTOCOL*: NSPK: Needham-Schroeder Public-Key Protocol
%% VARIANT: fix by Lowe (of 1995) without key server
%% PURPOSE: Two-party mutual authentication
%% MODELER: David von Oheimb, Siemens CT IC 3, January 2005
%% ALICE_BOB:
%%\begin{verbatim}
%% 1. A  - {Na.A}_Kb ----> B
%% 2. A <- {Na.Nb.B}_Ka -  B
%% 3. A  - {Nb}_Kb ------> B
%%\end{verbatim}
%% 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')

    2.  State  = 2 /\ RCV({Na.Nb'.B}_Ka) =|> 
	State':= 4 /\ 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')

%We do not need the code below anymore.
%    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
  %We no longer want this goal achieved.
  %authentication_on alice_bob_nb
  authentication_on bob_alice_na

end goal

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

environment()