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()