PROTOCOL:
SHARE
SHARE enables two principals to obtain a shared key, assuming that initially each knows the public key of the other.

 

PURPOSE:

Key establishment protocol  

REFERENCE:

Martin Abadi, Two Facets of Authentication
Technical Report, Digital Systems Research Centre,
March 18, 1998  

MODELER:

Haykal Tej, Siemens CT IC 3, 2003 and
Luca Compagna et al, AI-Lab DIST University of Genova, November 2004

 

ALICE_BOB: 

   1. A -> B: {Na}_Kb
   2. B -> A: {Nb}_Ka
   3. A -> B: {zero,Msg}_(Na,Nb)
   4. B -> A: {one,Msg}_(Na,Nb)
 

PROBLEMS:
3
 

ATTACKS:

The responder B believes to talk with the initiator A, while it is talking to the intruder. The attack trace looks like: 
   i       -> (a,6)    :  start
   (a,6)   -> i        :  {na(a,6)}ki
   i       -> (b,4)    :  {na(a,6)}kb
   (b,4)   -> i        :  {nb(b,4)}ka
   i       -> (a,6)    :  {nb(b,4)}ka
   (a,6)   -> i        :  {zero,msg(a,6)}(na(a,6),nb(b,4))
   i       -> (b,4)    :  {zero,msg(a,6)}(na(a,6),nb(b,4))
   (b,4)   -> i        :  {one,msg(a,6)}(na(a,6),nb(b,4))

 

NOTES:

Such a protocol exploits the compound types feature by simply imposing that the variable {\texttt{K}} can be only instantiated with a pair of nonces.

 


HLPSL: 

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

  local  State   : nat,
         Na, Msg : text,
         Nb      : text,
         K       : text.text

  init   State := 0
  accept State = 3

  transition

   1. State  = 0 /\ Rcv(start) =|> 
      State':= 1 /\ Na':= new()
                 /\ Snd({Na'}_Kb)

   2. State  = 1 /\ Rcv({Nb'}_Ka) =|> 
      State':= 2 /\ Msg':= new()
                 /\ Snd({zero.Msg'}_(Na.Nb')) 
                 /\ K':= Na.Nb'
                 /\ secret(Na.Nb',nanb,{A,B})
                 /\ witness(A,B,k2,Na.Nb')

   3. State  = 2 /\ Rcv({one.Msg}_K) =|> 
      State':= 3 /\ wrequest(A,B,k1,K)

end role




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

  local State   : nat,
        Nb      : text,
        Msg, Na : text,
        K       : text.text

  init   State := 0
  accept State = 2 

  transition

   1. State  = 0 /\ Rcv({Na'}_Kb) =|> 
      State':= 1 /\ Nb':= new()
                 /\ Snd({Nb'}_Ka)
                 /\ K':= Na'.Nb'
                 /\ witness(B,A,k1,Na'.Nb')
                 /\ secret(Na'.Nb',nanb,{A,B})

   2. State  = 1 /\ Rcv({zero.Msg'}_K) =|> 
      State':= 2 /\ Snd({one.Msg'}_K)
                 /\ wrequest(B,A,k2,K)

end role




role session(A, B           : agent,
             Ka, Kb         : public_key) def=

  local  SA, RA, SB, RB : channel (dy)

  composition
    share_Init(A,B,Ka,Kb,SA,RA) /\
    share_Resp(B,A,Kb,Ka,SB,RB)

end role




role environment() def=
 
 const zero, one    : text,
       a, b, i      : agent,
       ka, kb, ki   : public_key,
       k1, k2, nanb : protocol_id

 intruder_knowledge = {a,b,ka,kb,ki,i,inv(ki),zero,one}

 composition

        session(a,b,ka,kb) 
    /\  session(a,i,ka,ki) 

end role




goal


    secrecy_of nanb


    weak_authentication_on k1


    weak_authentication_on k2

end goal




environment()