VARIANT:
EKE2 (with mutual authentication)

PURPOSE:
Encrypted key exchange with mutual authentication
 

REFERENCE:

http://citeseer.ist.psu.edu/bellare00authenticated.html  

MODELER:

 

ALICE_BOB: 

 1. A -> B : A.{exp(g,X)}_K(A,B)


     B computes master key MK
     MK = H(A,B,exp(g,X),exp(g,Y),exp(g,XY))


 2. B -> A : {exp(g,Y)}_K(A,B), H(MK,1)


      A computes master key MK


 3. A -> B : H(MK,2)


      Session key K = H(MK,0)


 H : hash function
 K(A,B): password (shared key)

 

LIMITATIONS:
None

 

PROBLEMS:
3

 

CLASSIFICATION:
G2 G12

 

ATTACKS:
None

 

NOTES:
For information, this protocol is an example of
the proposition done in http://citeseer.ist.psu.edu/bellare00authenticated.html showing that any secure AKE (Authentication Key Exchange) protocol can be easily improved to also provide MA (Mutual Authentication).  

HLPSL: 


role eke2_Init (A,B : agent,
                G: text,
                H: hash_func,
                Kab : symmetric_key,
                Snd,Rcv: channel(dy))
played_by A
def=

  local State     : nat, 
        X         : text, 
        GY        : message,
        MK_A,MK_B : message

  const two : text,
        sec_i_MK_A : protocol_id

  init  State := 0

  transition

   1. State = 0  /\ Rcv(start) =|> 
      State':= 1 /\ X' := new()
                 /\ Snd(A.{exp(G,X')}_Kab) 

   2. State = 1  /\ Rcv({GY'}_Kab.H(H(A.B.exp(G,X).GY'.exp(GY',X)).one)) =|> 
      State':= 2 /\ MK_A' := A.B.exp(G,X).GY'.exp(GY',X)
                 /\ MK_B' := MK_A'% Message authentication (G2)
                 /\ Snd(H(H(MK_A').two)) 
                 /\ secret(MK_A',sec_i_MK_A,{A,B})
                 /\ request(A,B,mk_a,MK_A')
                 /\ witness(A,B,mk_b,MK_B') 
end role




role eke2_Resp (B,A : agent,
                G: text,
                H: hash_func,
                Kab : symmetric_key,
                Snd,Rcv : channel(dy))
played_by B
def=% Message authentication (G2)

  local State     : nat, 
        Y         : text,
        GX        : message,
        MK_A,MK_B : message

  const one : text,
        sec_r_MK_B : protocol_id

  init  State := 0

  transition

   1. State = 0  /\ Rcv(A.{GX'}_Kab) =|> 
      State':= 1 /\ Y' := new()
                 /\ MK_B' := A.B.GX'.exp(G,Y').exp(GX',Y')
                 /\ MK_A' := MK_B'
                 /\ Snd({exp(G,Y')}_Kab.H(H(MK_B').one))
                 /\ secret(MK_B',sec_r_MK_B,{A,B})% Message authentication (G2)
                 /\ witness(B,A,mk_a,MK_A')

   2. State = 1  /\ Rcv(H(H(MK_B).two)) =|> 
      State':= 2 /\ request(B,A,mk_b,MK_B)

end role




role session (A,B: agent,
              G: text,
              H: hash_func,
              Kab: symmetric_key) def=

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

   composition

           eke2_Init(A,B,G,H,Kab,SA,RB)  /\
           eke2_Resp(B,A,G,H,Kab,SB,RA)

end role



role environment() def=

  const mk_a, mk_b  : protocol_id,
        a,b,c       : agent,
        kab,kai,kib : symmetric_key,
        g           : text,
        h           : hash_func

  intruder_knowledge  = {a,b,c,kai,kib}

  composition

        session(a,b,g,h,kab) /\
        session(a,i,g,h,kai) /\
        session(i,b,g,h,kib)

end role




goal

  % Confidentiality (G12)
  % secrecy_of MK
  secrecy_of sec_i_MK_A, sec_r_MK_B

  % Message authentication (G2)
  % Eke2_Init authenticates Eke2_Resp on mk_a
  authentication_on mk_a

  % Message authentication (G2)
  % Eke2_Resp authenticates Eke2_Init on mk_b
  authentication_on mk_b

end goal




environment()