博客

%%1. A －> B : {A, Na}_KAS
%%2. B －> S : B, {
  {A, Na}_KAS, Nb}_KBS
%%3. S －> A : {B, KAB}_KAS ,{B,Na,Nb}_KAS, {A, KAB}_KBS
%%4. A －> B : {A, KAB}_KBS, {Nb}_KAB

role alice (A, S, B: agent,
		Kas : symmetric_key,
		SND_AB, RCV_SA, RCV_BA: channel(dy))
  played_by A def=
  
  local State : nat,
  Kab : symmetric_key,
	Na,Nb : text,
	X:{text}_symmetric_key

	
  init State := 0
  
  transition
	1. State  = 0 /\ RCV_BA(start) =|>
	   State':= 1 /\ Na':=new() /\ SND_AB({A.Na'}_Kas)
				/\ secret(Na',secret_na,{A,B,S})

	2. State  = 1 /\ RCV_SA({B.Kab'}_Kas.{B.Na.Nb'}_Kas.X') =|>
	   State':= 2 /\ SND_AB(X'.{Nb'}_Kab')
	              /\ witness(A,B,alice_bob_nb,Nb')
	              /\ witness(A,B,alice_bob_kab,Kab')
	              /\ secret(Kab',kab,{A,B,S})
	              /\ request(A,S,server_alice_na,Na)

end role