token_authentication.hlpsl

role role_Requester(Requester:agent,Device:agent,Kab:symmetric_key,SND,RCV:channel(dy))
played_by Requester
def=
	local
		State:nat,NDevice:text,AA:text, Salt:text
	init
		State := 0
	transition
		1. State=0 /\ RCV(start) =|> State' := 1 /\ Salt' := new() /\ AA' := new()  /\ 
                        secret(Salt'.AA',sec_1,{Requester,Device}) /\ SND({Requester.Device.Salt'.AA'}_Kab)

		2. State=1 /\ RCV({Device.Requester.NDevice'}_Kab) =|> 
                   State':=2 /\ SND({Requester.Device.NDevice'}_Kab) /\ witness(Requester, Device, auth_1, NDevice')
                   
end role

role role_Device(Device:agent,Requester:agent,Kab:symmetric_key,SND,RCV:channel(dy))
played_by Device
def=
	local
		State:nat,NDevice:text,AA:text, Salt:text
	init
		State := 0
	transition
		1. State=0 /\ RCV({Requester.Device.Salt'.AA'}_Kab) =|> 
                   State':=1 /\  NDevice' := new() /\ SND({Device.Requester.NDevice'}_Kab)

		2. State = 1 /\ RCV({Requester.Device.NDevice'}_Kab) =|> State' := 2 /\ request(Device, Requester, auth_1, NDevice')

end role

role session(Requester:agent,Device:agent,Kab:symmetric_key)
def=
	local
		SND2,RCV2,SND1,RCV1:channel(dy)
	composition
		role_Device(Device,Requester,Kab,SND2,RCV2) /\ role_Requester(Requester,Device,Kab,SND1,RCV1)
end role

role environment()
def=
	const
		kab:symmetric_key,
        requester,device:agent,
        sec_1, auth_1:protocol_id
	intruder_knowledge = {requester,device}
	composition
		session(requester,device,kab) /\ session(requester,i,kab) /\ session(i,requester,kab)
end role

goal
	secrecy_of sec_1
        authentication_on auth_1
end goal

environment()