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