Davis Swick Private Key Certificates

Purpose

T is a trusted translator. Kbt is shared key between B and T and Kat is between A and T.

Informal Specification

  1. B -> A : E(Kbt : A, msg)
  2. A -> T : E(Kbt : A, msg), B
  3. T -> A : E(kat : msg, B)

See Commonly Used Representations

MSR Specification

Click here to download 
--- Author: rishav
--- Date: 13 October 2007
--- Davis Swick Private Key Certificates
---     B -> A : E(Kbt : A, msg)
---     A -> T : E(Kbt : A, msg), B
---     T -> A : E(kat : msg, B)
(reset)
(
module DSP
export * .

translator : type.                         translator <: princ.
key : type.
ltk : princ -> princ -> type.          ltk A B <: key.
nonce : type.                           nonce  <: msg.

enc : key -> msg -> msg.

net : msg -> state.

initiator:
forall B : princ.
{
                          
DSPRule1:
 forall Kbt : ltk B T.
  empty => 
  exists mess : msg.
  net(enc Kbt (A & mess)).
}


receiver:
forall A : princ.
{
                          exists LA : msg -> state.
DSPRule2: 
   forall mess : msg.
   forall Kbt : ltk B T.
    net(enc Kbt (A & mess))
 =>  net(enc Kbt (A & mess) & B), LA mess.

ORRule4:
   forall mess : msg.
   forall Kat : ltk A T.
   net(enc Kat (mess & B)), LA mess
 => empty.

}


server:
forall T : translator.
{
DSPRule3:
   forall mess : msg.
   forall Kat : ltk A T.
   net(enc Kbt (A & mess) & B)
 => net(enc Kat (mess & B)).

}

)