Diffie Hellman Exchange

Purpose

In this protocol two numbers are publicly agreed by the communicating principals A and B. After the messages are exchangd, A computes k = Yxmod N and B computes k = Xymod N where X = Gxmod N and Y = Gymod N. The result of the two calculations is the same and equal new session key.

Informal Specification

  1. A -> B: Gxmod N
  2. B -> A: Gymod N

See Commonly Used Representations

MSR Specification

Click here to download 
--- Author: rishav
--- Date: 7 October 2007
--- Diffie Hellman Exchange
---
---	  A -> B: X=G^xmod N
---	  B -> A: Y=G^ymod N

(
module DHE
export * .
key : type.                             key <: msg.
random : type.                          random  <: msg.
enc : key -> msg -> msg.
expm : random -> random -> random -> msg.
DHpar: random -> random -> state.
--- calculation performed to get key K by both A and B
dh : msg -> random -> random -> key -> state.

net : msg -> state.

initiator:
forall A : princ.
{
			exists LA1 : random -> random -> random -> state.
 			exists LA2 : key -> state.
  DHERule1:
  forall G : random.
  forall N : random.
    empty
  => exists x : random.
     net (expm x G N), LA1 G N x if DHpar G N.


  DHERule3:
  forall Y : msg. 
  forall G : random.
  forall N : random.
  forall x : random.
   net(Y), LA1 G N x
  => exists K : key.
     LA2 K if dh Y x N K.


}

receiver:
forall B : princ.
{
			exists LB1 : random -> random -> random -> state.
 			exists LB2 : key -> state.

  DHERule2: 
  forall G : random.
  forall N : random.
    empty
  => exists y : random.
     net (expm y G N), LB1 G N y if DHpar G N.


  DHERule4:
  forall X : msg. 
  forall G : random.
  forall N : random.
  forall y : random.
   net(X), LB1 G N y
  => exists K : key.
     LB2 K if dh X y N K.


}

)