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