Untitled

%%% Key exchange protocol 
%%% 1. Alice
%%% 2. Bob
%%% 3. Third Party Agent

role role_A(A:agent,B:agent,T:agent,Kat:symmetric_key,SND,RCV:channel(dy))
played_by A
def=
	local
		State:nat,
                Kab:symmetric_key
	init
		State := 0
	transition
		1. State=0 /\ RCV(start) =|> State':=1 
		/\ Kab':=new() /\ SND({Kab'}_Kat) 
		/\ secret(Kab',sec_1,{A,B,T})
		/\ SND(Kab') 
end role

role role_T(T:agent,A:agent,B:agent,Kat,Kbt:symmetric_key,SND,RCV:channel(dy))
played_by T
def=
	local
		State:nat,
                Kab:symmetric_key
	init
		State := 0
	transition
		1. State=0 /\ RCV({Kab'}_Kat) =|> State':=1 /\ SND({Kab'}_Kbt)

end role

role role_B(B:agent,A:agent,T:agent,Kbt:symmetric_key,SND,RCV:channel(dy))
played_by B
def=
	local
		State:nat,
                Kab:symmetric_key
	init
		State := 0
	transition
		1. State=0 /\ RCV({Kab'}_Kbt) =|> State':=1 
end role



role session(A:agent,B:agent,T:agent,Kat,Kbt:symmetric_key)
def=
	local
		SND3,RCV3,SND2,RCV2,SND1,RCV1:channel(dy)
	composition
                		role_A(A,B,T,Kat,SND1,RCV1) /\
		role_B(B,A,T,Kbt,SND2,RCV2) /\ 
                		role_T(T,A,B,Kat,Kbt,SND3,RCV3) 
end role

role environment()
def=
	const
		kat,kbt,kit:symmetric_key,
                		alice,bob,trusted:agent,
               		sec_1,auth_1:protocol_id
	intruder_knowledge = {alice,bob, kit}
	composition
		session(alice,bob,trusted,kat,kbt)/\session(alice,i,trusted,kat,kit)
end role

goal
	secrecy_of sec_1
end goal

environment()