Yahalom

Purpose

The server generates the shared key Kab and sends it to A directly and B indirectly.

Informal Specification

A -> B : A,Na
B -> S : B,E(Kbs : A, Na, Nb)
S -> A : E(Kas : B, Kab, Na, Nb), E(Kbs: A, Kab)
A -> B : E(Kbs: A, Kab), E(Kab:Nb)

MSR Specification

--- Author: rishav
--- Date: 17 June 2007
---Yahalom
---     A -> B : A,Na
---     B -> S : B,E(Kbs : A, Na, Nb)
---     S -> A : E(Kas : B, Kab, Na, Nb), E(Kbs: A, Kab)
---     A -> B : E(Kbs: A, Kab), E(Kab:Nb)

(reset)
(
module yahalom
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.
nonce : type.                           nonce <: msg.

enc : key -> msg -> msg.

net : msg -> state.

initiator:
forall A : princ.
{
			 exists LA : nonce -> state.

YRule1:
  empty
  => exists Na : nonce.
   net(A & Na), LA Na.

YRule4:
   forall Kab : stk A B.
   forall Kas : ltk A S.
   forall Kbs : ltk B S.
   forall Na : nonce.
   forall Nb : nonce.
    net(enc Kas (B & Kab & Na & Nb) & enc Kbs (A & Kab)), LA Na
   => net(enc Kbs (A & Kab) & enc Kab Nb).
}


receiver:
forall B : princ.
{

                    exists LB : nonce -> nonce -> {S : server} ltk B S -> state.

YRule2:
  forall A : princ.
  forall S : server.
  forall Kbs : ltk B S.
  forall Na : nonce.
    net(A & Na)
 => exists Nb : nonce.
   net(B & enc Kbs (A & Na & Nb)), LB Na Nb S Kbs.

YRule5:
   forall S : server.
   forall Kab : stk A B.
   forall Kas : ltk A S.
   forall Kbs : ltk B S.
   forall Na : nonce.
   forall Nb : nonce.
    net(enc Kbs (A & Kab) & enc Kab Nb), LB Na Nb S Kbs
   => empty.

}


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

)