Kehne Langendorfer Schoenwalder

Purpose

Informal Specification

1. A -> B : Na, A
2. B -> S : Na, Nb, A, B
3. S -> B : E(Kbs: Kab, Nb, A), E(Kas : B, Kab, Na)
4. B -> A : E(Kas : B, Kab, Na), E(Kbb : tb, A, Kab), Nc, E(Kab:Na))
5. A -> B : E(Kab : Nc)

MSR Specification

--- Author: rishav
--- Date: 9 September 2007
--- Kehne Langendorfer Schoenwalder
---     A -> B : Na, A
---     B -> S : Na, Nb, A, B
---     S -> B : E(Kbs: Kab, Nb, A), E(Kas : B, Kab, Na)
---     B -> A : E(Kas : B, Kab, Na), E(Kbb : tb, A, Kab), Nc, E(Kab:Na))
---     A -> B : E(Kab : Nc)

(reset)
(
module KLS
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.
ltks : princ -> type.                  ltks B <: key.
nonce : type.                           nonce <: msg.
time : type.                           time <: msg.

enc : key -> msg -> msg.

net : msg -> state.

initiator:
forall A : princ.
{
                exists LA : nonce -> state.
KLSRule1:
  empty
  => exists Na : nonce.
   net(A & Na), LA Na.

---tb is not recognised 
KLSRule5:
   forall tb : time.
   forall Kab : stk A B.
   forall Kas : ltk A S.
   forall Kbs : ltk B S.
   forall Kbb : ltks B.
   forall Na : nonce.
   forall Nb : nonce.
    net(enc Kas (B & Kab & Na) & Nc & enc Kbb (tb & A & Kab) & enc Kab Na), LA Na
   => net(enc Kab Nc).
}


receiver:
forall B : princ.
{
                  exists LB1 : nonce -> nonce -> state.
                  exists LB2 : nonce -> {A : princ} {B : princ} stk A B -> state.
KLSRule2:
   forall A : princ.
   forall Na : nonce.
    net(A & Na)
 => exists Nb : nonce.
   net(Nb & A & Na & B), LB1 Na Nb.

KLSRule4:
   forall A : princ.
   forall tb : time.
   forall Kab : stk A B.
   forall Kas : ltk A S.
   forall Kbs : ltk B S.
   forall Kbb : ltks B.
   forall Na : nonce.
   forall Nb : nonce.
     net(enc Kbs (A & Kab & Nb) & enc Kas (B & Kab & Na)), LB1 Na Nb
  => exists Nc : nonce.
     net(enc Kas (B & Kab & Na) & Nc & enc Kbb (tb & A & Kab) & enc Kab Na), LB2 Nc A B Kab.

KLSRule6:
   forall Kab : stk A B.
   forall Nc : nonce.
   net(enc Kab Nc), LB2 Nc A B Kab
   => empty.

}


server:
forall S : server.
{
KLSRule3:
   forall Kas : ltk A S.
   forall Kbs : ltk B S.
   forall Na : nonce.
   forall Nb : nonce.
    net(Nb & A & Na & B)
     => exists Kab : stk A B.
        net(enc Kbs (A & Kab & Nb) & enc Kas (B & Kab & Na)).
}

)