Encrypted Key Exchange

Purpose

P is the password used as the symmetric key. Ka is randomly generated public key. R is randomly generated session key.

Informal Specification

  1. A -> B: E(P : Ka)
  2. B -> A: E(P : E(Ka : R))
  3. A -> B: E(R : Na)
  4. B -> A: E(R : Na, Nb)
  5. A -> B: E(R : Nb)

See Commonly Used Representations

MSR Specification

Click here to download 
--- Author: rishav
--- Date: 14 October 2007
--- Encrypted Key Exchange
---         A -> B: E(P : Ka)	
---         B -> A: E(P : E(Ka : R))
---         A -> B: E(R : Na)
---         B -> A: E(R : Na, Nb)
---         A -> B: E(R : Nb)
(reset)
(
module EKE
export * .

key : type.
stk : type.          stk <: msg.  stk <: key.
ltk : princ -> type.          ltk A <: msg.  ltk A <: key.
nonce : type.                     nonce  <: msg.

enc : key -> msg -> msg.

net : msg -> state.

initiator:
forall A : princ.
{
			exists LA1 : stk -> {A : princ} ltk A -> state.
			exists LA2 : nonce -> stk -> state.

EKERule1:
  forall P : stk.
    empty
  => exists Ka : ltk A. 
    net(enc P (Ka)), LA1 P A Ka.

EKERule3:
  forall R : stk.
  forall Ka : ltk A.
  forall P : stk.
   net(enc P (enc Ka R)), LA1 P A Ka
  => exists Na : nonce.
     net(enc R Na), LA2 NA R.

EKERule5:
  forall Na : nonce.
  forall Nb : nonce.
  forall R : stk.
  net(enc R (Na & Nb)), LA2 NA R
  => net(enc R Nb).

}

reciever:
forall B : princ.
{

			exists LB1 : stk -> state.
			exists LB2 : nonce -> stk -> state.	

EKERule2:
  forall Ka : ltk A.
  forall P : stk.
    net(enc P (Ka))
  => exists R : stk.
     net(enc P (enc Ka R)), LB1 R.

EKERule4:
  forall Na : nonce.
  forall R : stk.
  net(enc R Na), LB1 R
  => exists Nb : nonce.
     net(enc R (Na & Nb)), LB2 Nb R.

EKERule6:
   forall Nb : nonce.
   forall R : stk.
   net(enc R Nb), LB2 Nb R
  => empty.
}


)