Woo and Lam authentication (Pi_f) protocol

Purpose

Kas is a long term symmetric key shared by A and S. Initially, A only knows Kas and the name of B, B only knows Kbs and S knows all shared keys, i.e. S knows the ``function'' shared.

Informal Specification

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

See Commonly Used Representations

MSR Specification

Click here to download 
--- Author: rishav
--- Date: 19 June 2007
--- Woo and Lam authentication (Pif) protocol
---     A -> B : A
---     B -> A : Nb
---     A -> B : E(Kas : B, Nb, A)
---     B -> S : E(Kbs : A, B, Nb, E(Kab : A, B, Nb)
---     S -> B : E(Kbs : A, B, Nb)

(reset)
(
module WLPf
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.
{
--- Couldnt find out a way to have L without parameters 
               exists LA : state.
PfRule1:
  empty
  => net A, LA.

PfRule3:
   forall Kas : ltk A S.
   forall Nb : nonce.
    net Nb, LA
   => net(enc Kas (A & B & Nb)).
}

receiver:
forall B : princ.
{
                  exists LB1 : princ -> nonce -> state.
                  exists LB2 : princ -> nonce -> state.
PfRule2:
    forall A : princ.
    net A
 => exists Nb : nonce.
   net Nb, LB1 A Nb.

PfRule4:
   forall A : princ.
   forall Kas : ltk A S.
   forall Kbs : ltk B S.
   forall Nb : nonce.
     net(enc Kas (A & B & Nb)), LB1 A Nb
  => net(enc Kbs (A & B & Nb & enc Kas (A & B & Nb))), LB2 A Nb. 


PfRule6:
   forall A : princ.
   forall Kbs : ltk B S.
   forall Nb : nonce.
    net(enc Kbs (A & Nb & B)), LB2 A Nb
   => empty.

}


server:
forall S : server.
{
PfRule5:
   forall Kas : ltk A S.
   forall Kbs : ltk B S.
   forall Nb : nonce.
    net(enc Kbs (A & B & Nb & enc Kas (A & B & Nb)))
     => net(enc Kbs (A & Nb & B)).
}


)