PROTOCOL:
EKE: Encrypted Key Exchange

VARIANT:
basic

PURPOSE:
Encrypted key exchange
 

REFERENCE:

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

MODELER:

 

ALICE_BOB: 

 A -> B : {Ea}_Kab        |    Key exchange part
 B -> A : {{K}_Ea}_Kab    |
 A -> B : {Ca}_K          |
 B -> A : {Ca,Cb}_K       |    Challenge/Response
 A -> B : {Cb}_K          |    Authentication part

 

LIMITATIONS:
None

 

PROBLEMS:
3

 

CLASSIFICATION:
G2 G12

 

ATTACKS: 

 i -> (a,3): start
 (a,3) -> i: {Ea(1)}_kab
 i -> (a,6): {Ea(1)}_kab
 (a,6) -> i: {{K(2)}_Ea(1)}_kab 
 i -> (a,3): {{K(2)}_Ea(1)}_kab
 (a,3) -> i: {Na(3)}_K(2) witness(a,b,na,Na(3))
 i -> (a,6): {Na(3)}_K(2)
 (a,6) -> i: {Na(3),Nb(4)}_K(2) witness(a,b,nb,Nb(4))
 i -> (a,3): {Na(3),Nb(4)}_K(2)
 (a,3) -> i: {Nb(4)}_K(2)  request(a,b,nb,Nb(4))

Parallel session attack, man-in-the-middle between A as initiator and A as responder, attacker masquerades as B, but no secret nonces are exposed.

 


HLPSL: 


role eke_Init (A,B: agent,
               Kab: symmetric_key,
               Snd,Rcv: channel(dy))
played_by A
def=

  local State   : nat,
        Ea      : public_key,
        Na,Nb,K : text

  const sec_k1 : protocol_id

  init  State := 0

  transition

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

   2. State = 1
      /\ Rcv({{K'}_Ea}_Kab)
      =|> 
      State' := 2
      /\ Na' := new()
      /\ Snd({Na'}_K') 
      /\ secret(K',sec_k1,{A,B})
      /\ witness(A,B,na,Na')

   3. State = 2
      /\ Rcv({Na.Nb'}_K) 
      =|> 
      State' := 3
      /\ Snd({Nb'}_K) 
      /\ request(A,B,nb,Nb')

end role




role eke_Resp (B,A: agent,
               Kab: symmetric_key,
               Snd,Rcv: channel(dy))
played_by B
def=

  local State   : nat,
        Na,Nb,K : text,
        Ea      : public_key

  const sec_k2 : protocol_id

  init  State := 0

  transition

   1. State = 0 /\ Rcv({Ea'}_Kab)
      =|> 
      State' := 1
      /\ K' := new()
      /\ Snd({{K'}_Ea'}_Kab) 
      /\ secret(K',sec_k2,{A,B})

   2. State = 1 /\ Rcv({Na'}_K)
      =|> 
      State' := 2
      /\ Nb' := new()
      /\ Snd({Na'.Nb'}_K)
      /\ witness(B,A,nb,Nb')

   3. State = 2
      /\ Rcv({Nb}_K)
      =|> 
      State' := 3
      /\ request(B,A,na,Na)

end role




role session(A,B: agent,
             Kab: symmetric_key)
def=

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

  composition
     eke_Init(A,B,Kab,SA,RA)
  /\ eke_Resp(B,A,Kab,SB,RB)

end role





role environment()
def=

  const a, b   : agent,
        kab    : symmetric_key,
        na, nb : protocol_id

  intruder_knowledge={a,b}

  composition
      session(a,b,kab)
   /\ session(b,a,kab)
 
end role




goal

 % Confidentiality (G12)
 secrecy_of sec_k1, sec_k2

 % Message authentication (G2)
 % EKE_Init authenticates EKE_Resp on nb
 authentication_on nb

 % Message authentication (G2)
 % EKE_Resp authenticates EKE_Init on na
 authentication_on na

end goal




environment()