role meter (SMi, NANGi, Sj : agent,
	 SKuisj : symmetric_key,
	 Snd,RCV :channel(dy))

played_by SMi
def=
 local State : nat,
	NIDi, MIDi, CIDi, RIDm, RIDs, Bj, Bi, Ai, Aj: text, 
	Vn, Vm, Hn, Hm, Csm, Cs, Cm, C1, C2, C3, C4: text, 
	T1, T2, T3, T4, W, Y, SKn, SKs, SKm, S, E, Qi, Qs: text,
	Ec, H0, H1, H2 : hash_func
	const subs1, subs2, subs3, smi_sj_w,smi_sj_T1, sj_smi_y, sj_smi_T2 : protocol_id
	
init State:=0
		transition
1. 		State=0 /\ RCV(start)=|>
		State':=1 /\ Bi':=new()
		/\Aj' := H0(MIDi, Bi')
% Send the registration request message
		/\ Snd({MIDi.Aj}_SKuisj)
% Keep X secret to Sj and PWi, B to Ui
		/\ secret({MIDi, Bi}, subs1, {SMi, NANGi})
		/\ secret({Bi}, subs2, NANGi)
		
		
% Receive the request from the Smart meter SMi
 2. State = 1 /\RCV({Ec(H0((H0((Ec((H0(s.e).H0(NIDi.Bj)))).NIDi)).(H0(MIDi.Bi))))}_SKuisj) =|>
 
% Login phase
 State':= 2 
			/\ W' := new()
			/\ T1' := new()
			/\ Qi' := Ec(W')
			/\ Csm' := xor(Qi', H0(Vm. MIDi))
			/\ CIDi' := xor(H1(Qi'. T1), Bi)
			/\ C1' := H1(CIDi', Bi, Qi')
			/\ Snd ({CIDi. T1. Csm. C1}_SKuisj)
			
			/\ secret({W}, subs3, {SMi, NANGi, Sj})

% Ui has freshly generated the timestamp W for Sj
	/\ witness(SMi, Sj, smi_sj_w, W')
	/\ witness(SMi, Sj, smi_sj_T1, T1')
	
% Authentication phase
% Receive the authentication request message

3. State = 2 /\ RCV ({xor(Ec(Y'), H2(H0(Ec(H0((H0(s.e)).(H0(NIDi.Bj)))).NIDi))).T3.H2((H2(H2(Ec(Y'). Ec(W'). Bi. Bj). T3. Ec(Y'))).T4.xor(xor((xor(Ec(Y'), H2(H0(Ec(H0((H0(s.e)).(H0(NIDi.Bj)))).NIDi)))), (H0((Ec(H0((H0((Ec((H0(s.e).H0(NIDi.Bj)))).NIDi)).(H0(MIDi.Bi))))).MIDi))), H0((Ec(H0((H0(s.e)).(H0(NIDi.Bj))))).NIDi)).Bj).xor(xor((xor(Qs', H2(H0(Ec(H0((H0(s.e)).(H0(NIDi.Bj)))).NIDi)))), (H0((Ec(H0((H0((Ec((H0(s.e).H0(NIDi.Bj)))).NIDi)).(H0(MIDi.Bi))))).MIDi))), H0((Ec(H0((H0(s.e)).(H0(NIDi.Bj))))).NIDi)).T4.xor(H2(xor(xor((xor(Ec(Y'), H2(H0(Ec(H0((H0(s.e)).(H0(NIDi.Bj)))).NIDi)))), (H0((Ec(H0((H0((Ec((H0(s.e).H0(NIDi.Bj)))).NIDi)).(H0(MIDi.Bi))))).MIDi))), H0((Ec(H0((H0(s.e)).(H0(NIDi.Bj))))).NIDi)).(H0((Ec(H0((H0((Ec((H0(s.e).H0(NIDi.Bj)))).NIDi)).(H0(MIDi.Bi))))).MIDi))), Bj)}_SKuisj) =|>

 State' := 3 /\ Qs' := xor((xor(Ec(Y'), H2(H0(Ec(H0((H0(s.e)). (H0(NIDi.Bj)))).NIDi)))), H0(Ec(H0((H0(s.e)). (H0(NIDi.Bj)))). NIDi))
			/\ Cm' := xor(xor((xor(Qs', H2(H0((Ec(H0((H0(s.e)). (H0(NIDi.Bj))))).NIDi)))), (H0((Ec(H0((H0((Ec((H0(s.e).H0(NIDi.Bj)))).NIDi)).(H0(MIDi.Bi))))).MIDi))), H0(Ec(H0((H0(s.e)).(H0(NIDi.Bj)))).NIDi))
			/\RIDm' := xor(H2(Cm.(H0((Ec(H0((H0((Ec((H0(s.e).H0(NIDi.Bj)))).NIDi)).(H0(MIDi.Bi))))).MIDi))), Bj)
			/\ Bj' := xor(H1(Cm'.H0(Ec(H0(H0((Ec(H0((H0(s.e)).(H0(NIDi.Bj))))).NIDi).Aj)).MIDi)), RIDm')
			/\ SKm' := H2(Qs'. Qs'.Bi'.Bj')
			/\ C3' := H2(SKm.T3'.Qs')
			/\ C4' := H2(C3'.T4.Cm.Bj)

		/\ request(SMi, Sj, sj_smi_y, Y')
		/\ request(SMi, Sj, sj_smi_T2, T2')

	 end role 

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

role gateway (SMi, NANGi, Sj : agent,
	 SKuisj : symmetric_key,
	 Snd,RCV :channel(dy))

played_by NANGi
def=
 local State : nat,
	NIDi, MIDi, CIDi, RIDm, RIDs, Bj, Bi, Ai, Aj: text, 
	Vn, Vm, Hn, Hm, Csm, Cnan, Cs, Cm, C1, C2, C3, C4: text, 
	T1, T2, T3, T4, W, Y, SKn, SKs, SKm, S, E, Qi, Qs: text,
	Ec, H0, H1, H2 : hash_func
	const subs1, subs2, subs3, smi_sj_w,smi_sj_T1, sj_smi_y, sj_smi_T2 : protocol_id
		 
init State := 0
	transition
% Registration phase
% Receive the registration request message from the SMi

1. 		State=0 /\ RCV(start)=|>
		State':=1 /\ Bj':=new()
		/\Ai' := H0(NIDi, Bj')
		/\ Snd({NIDi.Ai}_SKuisj)
		

2. 	State=1 /\ RCV({Ec(H0((H0(s.e)).(H0(NIDi.Bj))))}_SKuisj)=|>
		State':=2 /\ secret({MIDi, Bi}, subs1, {SMi, NANGi})
				  /\ secret({Bi}, subs2, NANGi)
		
3. 		State=2 /\ RCV({MIDi.H0(MIDi.Bi)}_SKuisj)=|>
		State':=3 /\Hn' := H0((Ec(H0((H0(s.e)).(H0(NIDi.Bj))))).NIDi)
				/\Vm' := Ec(H0(Hn.Aj)) 
				/\Hm' := H0(Vm.MIDi)
				/\ Snd({Vm}_SKuisj)
				
4. 		State=3 /\ RCV({xor(H1(Ec(W). T1), Bi). T1. xor(Ec(W), H0((Ec(H0((H0((Ec((H0(s.e).H0(NIDi.Bj)))).NIDi)).(H0(MIDi.Bi))))). MIDi)). H1(xor(H1(Ec(W). T1), Bi). Bi. Ec(W))}_SKuisj)=|>

		State':=4 /\ Qi' := xor(xor(Ec(W'), H0((Ec(H0((H0((Ec((H0(s.e).H0(NIDi.Bj)))).NIDi)).(H0(MIDi.Bi))))). MIDi)), (H0((Ec(H0((H0((Ec((H0(s.e). H0(NIDi.Bj)))).NIDi)).(H0(MIDi.Bi))))).MIDi)))
				/\ Bi' := xor(H1(Qi'.T1), xor(H1(Qi'. T1), Bi'))
				/\Cnan' := xor(xor((xor(Ec(W'), H0((Ec(H0((H0((Ec((H0(s.e).H0(NIDi.Bj)))).NIDi)).(H0(MIDi.Bi))))). MIDi))), H0((Ec(H0((H0((Ec(H0((H0(s.e)).(H0(NIDi.Bj))))).NIDi)).(H0(MIDi.Bi)))) ).MIDi)), H0(Ec(H0((H0(s.e)).(H0(NIDi.Bj)))).NIDi))
				/\RIDs' := xor(H1(Cnan.H0((Ec(H0((H0(s.e)). (H0(NIDi.Bj))))).NIDi)), Bj)
				/\C2' := H1((H1((xor(H1(Qi'. T1), Bi)). Bi. Qi')).T2.Cnan.Bj)
				/\ Snd ({CIDi.C2.Cnan.RIDs.T2.T1}_SKuisj)
% Receive the Mutual authentication phase

5. 		State = 4 /\ RCV({H2((H2(Ec(Y'). Ec(W'). Bi'. Bj')). t3. (Ec(Y'))).xor(Ec(Y'), H2(H0(Ec(H0((H0(s.e)). (H0(NIDi.Bj)))).NIDi))).T3}_SKuisj) =|>
			State' := 5 /\ T4' := new() 
			/\Qs' := xor((xor(Ec(Y'), H2(H0(Ec(H0((H0(s.e)).(H0(NIDi.Bj)))).NIDi)))), H0(Ec(H0((H0(s.e)).(H0(NIDi.Bj)))).NIDi))
			/\ Cm' := xor(xor((xor(Qs', H2(H0((Ec(H0((H0(s.e)). (H0(NIDi.Bj))))).NIDi)))), (H0((Ec(H0((H0((Ec((H0(s.e).H0(NIDi.Bj)))).NIDi)).(H0(MIDi.Bi))))).MIDi))), H0(Ec(H0((H0(s.e)).(H0(NIDi.Bj)))).NIDi))
			/\RIDm' := xor(H2(Cm.(H0((Ec(H0((H0((Ec((H0(s.e).H0(NIDi.Bj)))).NIDi)).(H0(MIDi.Bi))))).MIDi))), Bj)
			/\SKn' := H2(Qs'. Qi'. Bi'. Bj')
			/\C4' := H2((H2(SKn. T3. Qs')).T4.Cm.Bj)	
% Send the authentication request message
	/\ Snd({Cs.T3.C4.Cm.T4.RIDm}_SKuisj)
 
end role
%%%%%%%%%%%%%%%%%%%%%%%
role server (SMi, NANGi, Sj : agent,
	 SKuisj : symmetric_key,
	 Snd,RCV :channel(dy))

played_by Sj
def=
 local State : nat,
	NIDi, MIDi, CIDi, RIDm, RIDs, Bj, Bi, Ai, Aj: text, 
	Vn, Vm, Hn, Hm, Csm, Cnan, Mi, Cs, Cm, C1, C2, C3, C4: text, 
	T1, T2, T3, W, Y, SKn, SKs, SKm, S, E, Qi, Qs: text,
	Ec, H0, H1, H2 : hash_func
	const subs1, subs2, subs3, smi_sj_w, smi_sj_T1, sj_smi_y, sj_smi_T2 : protocol_id
init State:=0
		transition
1. 		State=0 /\ RCV({NIDi.H0(NIDi.Bj)}_SKuisj)=|>
		State':=1 /\ E':=new()
					/\Mi' := H0(s.e)
					/\Vn' := Ec(H0(Mi.(H0(NIDi.Bj)))) 
					/\Hn' := H0(Vn.NIDi)
% Send the registration request message
		/\ Snd({Vn}_SKuisj)
			
 2. State = 1 /\RCV({xor(H1(Ec(W'). T1), Bi).H1((H1((xor(H1(Ec(W'). T1), Bi)). Bi. Ec(W))).T2.xor(xor((xor(Ec(W'), H0((Ec(H0((H0((Ec((H0(s.e).H0(NIDi.Bj)))).NIDi)).(H0(MIDi.Bi))))). MIDi))), H0((Ec(H0((H0((Ec(H0((H0(s.e)).(H0(NIDi.Bj))))).NIDi)).(H0(MIDi.Bi)))) ).MIDi)), H0(Ec(H0((H0(s.e)).(H0(NIDi.Bj)))).NIDi)).Bj).xor(xor((xor(Ec(W'), H0((Ec(H0((H0((Ec((H0(s.e).H0(NIDi.Bj)))).NIDi)).(H0(MIDi.Bi))))). MIDi))), H0((Ec(H0((H0((Ec(H0((H0(s.e)).(H0(NIDi.Bj))))).NIDi)).(H0(MIDi.Bi)))) ).MIDi)), H0(Ec(H0((H0(s.e)).(H0(NIDi.Bj)))).NIDi)).xor(H1(Cnan.H0((Ec(H0((H0(s.e)).(H0(NIDi.Bj))))).NIDi)), Bj).T2.T1}_SKuisj) =|>
 
% Login phase
 State':= 2 
		   /\Cnan' := xor(xor((xor(Ec(W'), H0((Ec(H0((H0((Ec((H0(s.e).H0(NIDi.Bj)))).NIDi)).(H0(MIDi.Bi))))). MIDi))), H0((Ec(H0((H0((Ec(H0((H0(s.e)).(H0(NIDi.Bj))))).NIDi)).(H0(MIDi.Bi)))) ).MIDi)), H0(Ec(H0((H0(s.e)).(H0(NIDi.Bj)))).NIDi))
		   /\Hn' := H0(Ec(H0((H0(s.e)).(H0(NIDi.Bj)))).NIDi)
		   /\ Qi':=xor(Cnan, Hn)
			/\ Bi' := xor(H1(Qi'.T1), xor(H1(Qi'. T1), Bi))
			/\ Bj' := xor(H1(Cnan.Hn), (xor(H1(Cnan.H0((Ec(H0((H0(s.e)).(H0(NIDi.Bj))))).NIDi)), Bj)))
			/\ C1' := H1((xor(H1(Ec(W'). T1), Bi)).Bi'.Qi')
			/\C2' := H1(C1'.T2.Cnan.Bj')
%Mutual authentication begins
			/\ Y' := new()
			/\ Qs' := Ec(Y')
			/\Cs' := xor(Qs', H2(Hn))
			/\SKs' := H2(Qs'. Qi'. Bi'. Bj') 
			/\C3' := H2(SKs'. T3. Qs')
		   
		   /\ Snd ({C3.Cs.T3}_SKuisj)

		   /\ witness(SMi, Sj, sj_smi_y, Y')
		   /\ witness(SMi, Sj, sj_smi_T2, T2')
		
		/\ request(SMi, Sj, smi_sj_w, W')
		/\ request(SMi, Sj, smi_sj_T1, T1')

	 end role 

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

role session(SMi, NANGi, Sj : agent,
	 SKuisj : symmetric_key)
def=
local Send1, Send2, Send3, Recv1, Recv2,Recv3: channel (dy)
composition
	meter(SMi, NANGi, Sj, SKuisj, Send1, Recv1)
	/\gateway(SMi, NANGi, Sj, SKuisj, Send2, Recv2)
	/\server(SMi, NANGi, Sj, SKuisj, Send3, Recv3)
end role 
%%%%%%%%%%%%%%%%%%%
role environment()
def=
const smi, nangi, sj: agent,
skuisj : symmetric_key,
nidi,midi,cidi,ridm,rids,bj,bi,ai,aj:text,
vn,vm,hn,hm,csm,cs,cm,c1,c2,c3,c4,t1,t2,t3,t4:text,
w,y,skn,sks,skm,s,e,qi,qs:text,
ec,h0,h1,h2:hash_func,
subs1, subs2, subs3, smi_sj_w,smi_sj_T1, sj_smi_y, sj_smi_T2 : protocol_id

intruder_knowledge = {smi, nangi, sj, ec, h0, h1, h2, c1, c2, c3, t1, t2, t3, t4, cidi, ridm, rids}
composition
session(smi, nangi, sj, skuisj)
/\session(smi, nangi, sj, skuisj)
/\session(smi, nangi, sj, skuisj)
end role
goal
secrecy_of subs1, subs2, subs3
authentication_on smi_sj_w, smi_sj_T1, sj_smi_y, sj_smi_T2
end goal
environment() 
%%%%%%%%%%%%%%%%%%%%%%%%