Denning Sacco Key Distribution Protocol with Public Key

Purpose

A generates Kab and this protocol allows A to pass that key securely to B. S provides certificates to A and B.

Informal Specification

A -> S: A,B
S -> A: CertA, CertB
A -> B: CertA, CertB, E(Kb: E(Ka-1: Kab, Ta))

See Commonly Used Representations
CertX - Certificate for X
Ta - Timestamp

MSR Specification

--- Author: rishav
--- Date: 12 October 2007
--- Denning Sacco Key Distribution Protocol with Public Key
---      A -> S: A,B
---      S -> A: CertA, CertB
---      A -> B: CertA, CertB, E(Kb: E(Ka-1: Kab, Ta)) 
---
(reset)
(
module denningSacco
export * .

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

enc : key -> msg -> msg.

net : msg -> state.

initiator:
forall A : princ.
{

			exists LA : princ -> state.
DSDRule1:
  forall B : princ.
   empty =>  net(A & B), LA B.

DSDRule3:
   forall B :princ.
   forall CertB : msg.
   forall CertA : msg.
   forall Ka-1 : ltkpvt A.
   forall Kb : ltkpub B.
   forall Ta : time.
   net(CertA & CertB)
 => exists Kab : stk A B.
    net(CertA & CertB & enc Kb (enc Ka-1 (Kab & Ta))), LA B.
}

receiver: 
forall B : princ.
{

DSDRule4: 
   forall CertB : msg.
   forall CertA : msg.
   forall Ka-1 : ltkpvt A.
   forall Kb : ltkpub B.
   forall Kab : stk A B.
   forall Ta : time.
   net(CertA & CertB & enc Kb (enc Ka-1 (Kab & Ta)))
 => empty.
}

server:
forall S : server.
{
DSDRule2:
   forall A : princ.
   forall B : princ.
   forall Ks-1 : ltkpvt S.
   forall Ka  : ltkpub A.
   forall Kb  : ltkpub B.
   forall T : time.
   net(A & B)
 => net(enc Ks-1 (A & Ka & T) & enc Ks-1 (B & Kb & T)).

}

)

Findings

This is one more the cases where use of local state predicate doesn't allow complete reconstruction.