VARIANT:
with XOR

PURPOSE:
Two-party mutual autentication
 

MODELER:
Mathieu Turuani, INRIA, May 2005
 

ALICE_BOB:

 A --> B: {Na,A}_Kb
 B --> A: {Nb,xor(Na,B)}_Ka
 A --> B: {Nb}_Kb
 

PROBLEMS:
3
 


HLPSL:


role alice (A,B     : agent, 
            Ka,Kb   : public_key,  
            Snd,Rcv : channel (dy)) played_by A def=

  local 
     State  : nat, 
     Na     : message, 
     Nb     : text

  init 
     State:=0

  transition 
    1. State=0 /\ Rcv(start) =|>
          State':=1
       /\ Na':=new()
       /\ Snd({Na'.A}_Kb)
       /\ witness(A,B,bob_alice_na,Na')
       /\ secret(Na',na,{A,B})


    2. State=1 /\ Rcv({Nb'.xor(Na,B)}_Ka) =|>
          State':=2
       /\ Snd({Nb'}_Kb)
       /\ wrequest (A,B,alice_bob_nb,Nb')

end role


role bob (B,A : agent, Kb,Ka : public_key, Snd,Rcv : channel (dy)) played_by B def= local State : nat, Na : message, Nb : text init State:=0 transition 1. State=0 /\ Rcv({Na'.A}_Kb) =|> State':=1 /\ Nb':=new() /\ Snd({Nb'.xor(Na',B)}_Ka) /\ witness(B,A,alice_bob_nb,Nb') /\ secret(Nb',nb,{A,B}) 2. State=1 /\ Rcv({Nb}_Kb) =|> State':=2 /\ wrequest(B,A,bob_alice_na,Na) end role
role session (A,B: agent, Ka, Kb: public_key, SND, RCV: channel(dy) ) def= composition alice(A,B,Ka,Kb,SND,RCV) /\ bob(B,A,Kb,Ka,SND,RCV) end role
role environment() def= local Snd, Rcv: channel(dy) const a, b, i: agent, ka, kb, ki: public_key, na, nb, alice_bob_nb, bob_alice_na: protocol_id intruder_knowledge = {a,b,i,ka,kb,ki,inv(ki)} composition session(a,b,ka,kb,Snd,Rcv) /\ session(a,i,ka,ki,Snd,Rcv) end role
goal weak_authentication_on alice_bob_nb weak_authentication_on bob_alice_na secrecy_of na, nb end goal
environment()