CCITT X.509

Purpose

This is the classic description of three protocols, either message 1 or message 1 and 2 or all three.

Informal Specification

  1. A -> B : A, E(Ka-1: Ta, Na, B, Xa, E(Kb : Ya))
  2. B -> A : B, E(Kb-1: Tb, Nb, A, Na, Xb, E(Ka : Yb))
  3. A -> B : A, E(Ka-1 : Nb)

See Commonly Used Representations
  Xa,Xb,Ya,Yb - user data

MSR Specification

Click here to download 
--- Author: rishav
--- Date: 13 October 2007
---  CCITT X.509
---     A -> B : A, E(Ka-1: Ta, Na, B, Xa, E(Kb : Ya))
---     B -> A : B, E(Kb-1: Tb, Nb, A, Na, Xb, E(Ka : Yb)) 
---     A -> B : A, E(Ka-1 : Nb)

(reset)
(
module CCITT
export * .

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

enc : key -> msg -> msg.

net : msg -> state.

initiator:
forall A : princ.
{
               exists LA : nonce -> {A : princ} ltks A -> state.
CCRule1:
  forall B : princ.
  forall Ka-1 : ltks A.
  forall Kb : ltk B.
  forall Ta : msg.
  forall Xa : msg.
  forall Ya : msg.
  empty
  => exists Na : nonce.
     net (A & enc Ka-1 (Ta & Na & B & Xa & enc Kb Ya)), LA Na A Ka-1.

CCRule3:
   forall B : princ.
   forall Nb : nonce.
   forall Na : nonce.
   forall Kb-1 : ltks B.
   forall Ka-1 : ltks A.
   forall Ka : ltk A.
   forall Tb : msg.
   forall Xb : msg.
   forall Yb : msg.
    net (B & enc Kb-1 (Tb & Nb & A & Na & Xb & enc Ka Yb)), LA Na A Ka-1
   => net(enc Ka-1 Nb).
}

receiver:
forall B : princ.
{
                  exists LB : nonce -> {A : princ} ltks A -> state.
CCRule2:
  forall A : princ.
  forall Na : nonce.
  forall Ka-1 : ltks A.
  forall Kb-1 : ltks B.
  forall Kb : ltk B.
  forall Ka : ltk A.
  forall Ta : msg.
  forall Xa : msg.
  forall Ya : msg.
  forall Tb : msg.
  forall Xb : msg.
  forall Yb : msg.
   net (A & enc Ka-1 (Ta & Na & B & Xa & enc Kb Ya))
 => exists Nb : nonce.
    net (B & enc Kb-1 (Tb & Nb & A & Na & Xb & enc Ka Yb)), LB Nb A Ka-1.

CCRule4:
   forall A : princ.
   forall Ka-1 : ltks A.
   forall Nb : nonce.
     net(enc Ka-1 Nb), LB Nb A Ka-1
  => empty.

}


)