%% Here is a typical example of an HLPSL specification
%% ---------------------------------------------------

%% 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:
%%\begin{verbatim}
%% 1. A  - {Na.A}_Kb ----> B
%% 2. A <- {Na.Nb}_Ka ---  B
%% 3. A  - {Nb}_Kb ------> B
%%\end{verbatim}
%% 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.
%%\begin{verbatim}
%% 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
%%\end{verbatim}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%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)

end role

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

goal

  secrecy_of na, nb
  authentication_on alice_bob_nb
  authentication_on bob_alice_na

end goal

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

environment()