role alice(
	A,B     : agent,
    	K       : symmetric_key,
    	Hash    : hash_func,
    	SND,RCV : channel(dy))
  played_by A def=
    local
      State   : nat,
      Na,Nb   : text,
      K1      : message
    init
      State := 0
transition
    1. State  = 0 /\ RCV(start) =|>
       State’:= 2 /\ Na’ := new()
                  /\ SND({Na’}_K)
    2. State  = 2 /\ RCV({Nb’}_K) =|>
       State’:= 4 /\ K1’ := Hash(Na.Nb’)
                  /\ SND({Nb’}_K1’)
                  /\ witness(A,B,bob_alice_nb,Nb’)
end role

role bob(
      A,B     : agent,
      K       : symmetric_key,
      Hash    : hash_func,
      SND,RCV : channel(dy))
  played_by B def=
    local
	State   : nat,
	Nb,Na   : text,
	K1      : message
	init
  State := 1
transition
1. State  = 1 /\ RCV({Na’}_K) =|>
   State’:= 3 /\ Nb’ := new()
              /\ SND({Nb’}_K)
              /\ K1’:= Hash(Na’.Nb’)
              /\ secret(K1’,k1,{A,B})
2. State  = 3 /\ RCV({Nb}_K1) =|>
   State’:= 5 /\ request(B,A,bob_alice_nb,Nb)
end role


  role session(
      A,B  : agent,
      K    : symmetric_key,
      Hash : hash_func)
  def=
    local SA, SB, RA, RB : channel (dy)
    composition
       alice(A,B,K,Hash,SA,RA)
    /\ bob  (A,B,K,Hash,SB,RB)
end role

 role environment()
  def=
const
  bob_alice_nb,
  k1          : protocol_id,
  kab,kai,kib : symmetric_key,
  a,b         : agent,
  h           : hash_func
intruder_knowledge = {a,b,h,kai,kib}
composition
   session(a,b,kab,h)
/\ session(a,i,kai,h)
/\ session(i,b,kib,h)
end role

 goal
    secrecy_of k1
    authentication_on bob_alice_nb
end goal

 environment()