Wide Mouthed Frog Protocol

Purpose

In this protocol A generates the session key. S checks if the timestamp is timely then it forwards the key to B with its own timestamp. B checks if the timestamp is later than any other message it has received form S.

Informal Specification

  1. A -> S : A, E(Kas: Ta, B, Kab)
  2. S -> B : E(Kbs: Ts, A, Kab)

See Commonly Used Representations
  Tx - Timestamp generated by X

MSR Specification

Click here to download 
--- Author: rishav
--- Date: 16 June 2007
--- Wide Mouthed Frog Protocol
---     A -> S : A, E(Kas: Ta, B, Kab)
---     S -> B : E(Kbs: Ts, A, Kab)

(reset)
(
module WMFprotocol
export * .

server : type.                         server <: princ.
key : type.
stk : princ -> princ -> type.          stk A B <: msg.  stk A B <: key.
ltk : princ -> princ -> type.          ltk A B <: key.
time : type.                           time <: msg.

enc : key -> msg -> msg.

net : msg -> state.

initiator:
forall A : princ.
{

WMFRule1:
--- forall B : princ.
--- forall Kas : ltk A S.
--- forall Ta : time.
  empty =>
  exists Kab : stk A B.
   net(A & enc Kas (Ta & B & Kab)).

}


receiver:
forall B : princ.
{

WMFRule3: 
---   forall Kab : stk A B.
  forall Kbs : ltk B S.
  forall Ts : time.
    net(enc Kbs (Ts & A & Kab))
 => empty.
}


server:
forall S : server.
{
WMFRule2:
   forall Kab : stk A B.
   forall Kas : ltk A S.
   forall Kbs : ltk B S.
   forall Ts : time.
   net(A & enc Kas (Ta & B & Kab)) 
 => net(enc Kbs (Ts & A & Kab)).
}

)
 

Findings

Reconstruction possible in most places. But in some places MSR does not allow reconstruction when it is possible.