Bilateral Key Exchange with Public Key

Purpose

The two principals exchange their public key while encrypting the nonce of the other protocol to verify.

Informal Specification

  1. B -> A: B, E(Ka: Nb,B)
  2. A -> B: E(Kb: f(Nb),Na,A,K)
  3. B -> A: E(Kb: f(Na))

See Commonly Used Representations

MSR Specification

Click here to download 
--- Author: Rishav Bhowmick
--- Date: 4 Oct 2007
--- Bilateral Key Exchange with Public Key
---
---	  B -> A: B, E(Ka: Nb,B)
---       A -> B: E(Kb: f(Nb),Na,A,K)
---       B -> A: E(Kb: f(Na))
(reset)
(
module BKEPL
export * .

key : type.
skey : princ -> princ -> type.         skey A B <: key.          skey A B <: msg.
pubk : princ -> type.          pubk A <: key.
nonce: type.                           nonce  <: msg.

enc : key -> msg -> msg. 
f : nonce -> msg.

net : msg -> state.


initiator:
forall B : princ.
{
			exists LB : {A: princ} pubk A -> nonce -> state. 
  BKRule1:
  forall A : princ.
  forall Ka : pubk A.
    empty
  => exists Nb : nonce.
    net(B & enc Ka (Nb & B)), LB A Ka Nb.

  BKRule3:
  forall A : princ.
  forall Nb : nonce.
  forall Na : nonce.
  forall Kb : pubk B.
  forall Ka : pubk A.
  forall K : skey A B.
     net(enc Kb ((f Nb) & Na & A & K)), LB A Ka Nb
  => net(enc K (f Na)).
}



reciever:
forall A : princ.
{

			exists LA : {B : princ} skey A B -> nonce -> nonce -> state.
  BKRule2:
  forall B : princ.
  forall Nb : nonce.
  forall Kb : pubk B.
  forall Ka : pubk A.
   net(B & enc Ka (Nb & B))
  => exists Na : nonce.
     exists K : skey A B.
    net(enc Kb ((f Nb) & Na & A & K)), LA B K Na Nb.

  BKRule4:
  forall B : princ.
  forall Nb : nonce.
  forall Na : nonce.
  forall K : skey A B.
    net(enc K (f Na)), LA B K Na Nb
  => empty.
}
)