1a. A ----------------------- {A.B} ----------> S
 1b. A <---------------------- {B.Kb}_inv(Ks) -- S
 1c. A -- {Na.A}_Kb ----> B
 2a.                      B -- {B.A} ----------> S
 2b.                      B <- {A.Ka}_inv(Ks) -- S
 2c. A <- {Na.Nb.B}_Ka -- B
 3 . A -- {Nb}_Kb ------> B

• secrecy of na, nb
• strong authentication on alice_bob_nb
• strong authentication on bob_alice_na

role alice (A, B: agent,             
            Ka, Ks: public_key,  
            KeyRing: (agent.public_key) set,
            SND, RCV: channel(dy))
played_by A def=
        
  local State : nat,
        Na, Nb: text,
        Kb: public_key

  init State := 0

  transition

   % Start, if alice must request bob's public key from key server
   ask.    State  = 0 /\ RCV(start) /\ not(in(B.Kb', KeyRing))
       =|> State':= 1 /\ SND(A.B)

   % Receipt of response from key server
   learn.  State  = 1 /\ RCV({B.Kb'}_inv(Ks))
       =|> State':= 0 /\ KeyRing':=cons(B.Kb', KeyRing)
 
   % Start/resume, provided alice already knows bob's public key
   knows.  State  = 0 /\ RCV(start) /\ in(B.Kb', KeyRing)
       =|> State':= 4 /\ Na':=new() /\ SND({Na'.A}_Kb')
                      /\ secret(Na',na,{A,B})
                      /\ witness(A,B,bob_alice_na,Na')

   cont.   State  = 4 /\ RCV({Na.Nb'.B}_Ka) 
       =|> State':= 6 /\ SND({Nb'}_Kb)
                      /\ request(A,B,alice_bob_nb,Nb')

end role



role bob(A, B: agent,      
         Kb, Ks: public_key,  
         KeyRing: (agent.public_key) set,
         SND, RCV: channel(dy))
played_by B def=

  local State: nat,
        Na, Nb: text, 
        Ka: public_key

  init State := 2

  transition 

   % Start if bob must request alice's public key from key server
   ask.    State  = 2 /\ RCV({Na'.A}_Kb) /\ not(in(A.Ka', KeyRing))
       =|> State':= 3 /\ SND(B.A)

   % Receipt of response from key server
   learn.  State  = 3 /\ RCV({A.Ka'}_inv(Ks))
       =|> State':= 2 /\ KeyRing':=cons(A.Ka', KeyRing)

   % Start/resume, provided if bob knows alice's public key
   knows.  State  = 2 /\ RCV({Na'.A}_Kb) /\ in(A.Ka', KeyRing)
       =|> State':= 5 /\ Nb':=new() /\ SND({Na'.Nb'.B}_Ka')
                      /\ secret(Nb',nb,{A,B})
                      /\ witness(B,A,alice_bob_nb,Nb')

   cont.   State  = 5 /\ RCV({Nb}_Kb) 
       =|> State':= 7 /\ request(B,A,bob_alice_na,Na)

end role



role server(S: agent,
            Ks: public_key,
            KeyMap: (agent.public_key) set,
            SND, RCV: channel(dy))
played_by S def=

  local A, B: agent,
        State : nat,
        Kb: public_key

  init State := 8

  transition
   req1.   State = 8 /\ RCV(A'.B') /\ in(B'.Kb', KeyMap)
       =|> State':= 8 /\ SND({B'.Kb'}_inv(Ks))











end role


% The role representing a partial session between alice and bob

role nspk(SND, RCV: channel(dy),
          Ks: public_key,
          Instances: (agent.agent.public_key.public_key) set,
          KeySet: agent -> (agent.public_key) set)
def=

  local A, B: agent,
        Ka, Kb: public_key

  composition
     /\_{in(A.B.Ka.Kb,Instances)}
       (alice(A,B,Ka,Ks,KeySet(A),SND,RCV)
       /\ bob(A,B,Kb,Ks,KeySet(B),SND,RCV))

end role



role environment() def=

  local KeyMap: (agent.public_key) set,
        SND, RCV: channel(dy)

  const a,b,s,i: agent,
        ka, kb, ki, ks: public_key,
        na, nb, alice_bob_nb, bob_alice_na: protocol_id

  init KeyMap := {a.ka, b.kb, i.ki}

  intruder_knowledge = {a, b, ks, ka, kb, ki, inv(ki)}

  composition
        server(s,ks, KeyMap, SND, RCV)
     /\ nspk(SND, RCV,                  % channels
             ks,                        % public key of server
             {a.b.ka.kb,                % session instances 
              a.i.ka.ki,
              i.b.ki.kb
             },
             {a.{a.ka,b.kb},            % initial KeyRings
              b.{b.kb},
              i.{i.ki}})
end role



goal

  secrecy_of na, nb
  authentication_on alice_bob_nb
  authentication_on bob_alice_na

end goal



environment()