VARIANT:
original version (of 1978) with key server

PURPOSE:
Two-party mutual autentication
 

MODELER:
LjV, INRIA, June 2005 and DvO, Siemens CT IC 3, July 2005
 

ALICE_BOB: 

 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}_Ka ---- B
 3 . A -- {Nb}_Kb ------> B
 

PROBLEMS:
3
 

ATTACKS:
Man-in-the-middle attack
 

HLPSL: 

% Role of the initiator:
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 knows bob's public key
   knows.  State  = 0 /\ Rcv(start) /\ in(B.Kb', KeyRing)
       =|> State':= 4 /\ Na':=new() /\ Snd({Na'.A}_Kb')
                      /\ secret(Na',sna,{A,B})
                      /\ witness(A,B,bob_alice_na,Na')

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

end role



% Role of the receiver:
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 bob knows alice's public key
   knows.  State  = 2 /\ Rcv({Na'.A}_Kb) /\ in(A.Ka', KeyRing)
       =|> State':= 5 /\ Nb':=new() /\ Snd({Na'.Nb'}_Ka')
                      /\ secret(Nb',snb,{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 of the key server:
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



% 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



% The main 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,
        sna, snb, 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



% Description of goal properties:
goal

  secrecy_of sna, snb
  authentication_on alice_bob_nb
  authentication_on bob_alice_na

end goal



% Call of the main role:
environment()