Denning Sacco Protocol

Purpose

Denning and Sacco suggested the use of time stamps to remove the freshness flaw in Needham Schroeder protocol. It cut shorts the size of Needham Schroeder protocol too.

Informal Specification

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

See Commonly Used Representations

MSR Specification

Click here to download 
--- Author: rishav
--- Date: 10 June 2007
--- Denning Sacco Protocol
---      A -> S: A,B
---      S -> A: E(Kas: B, Kab, T, E(Kbs: A, Kab, T))
---      A -> B: E(Kbs: A, Kab, T) 
---
(reset)
(
module denningSacco
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.
{

DSRule1:
   empty =>  net(A & B).

DSRule3:
   forall KAS : ltk A S.
   forall KAB : stk A B.
   forall KBS : ltk B S.
   net(enc KAS (B & KAB & T & enc KBS (A & KAB & T)))
 => net(enc KBS (A & KAB & T)).
}

receiver: 
forall B : princ.
{

DSRule4: 
   forall KAB : stk A B.
   forall KBS : ltk B S.
   net(enc KBS (A & KAB & T))
 => empty.
}

server:
forall S : server.
{
DSRule2:
   forall KAS : ltk A S.
   forall KBS : ltk B S.
   net(A & B)
 => exists KAB : stk A B.
    net(enc KAS (B & KAB & T & enc KBS (A & KAB & T))).

}

)