Amended Needham Schroeder protocol

Purpose

Informal Specification

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

MSR Specification

--- Author: rishav
--- Date: 23 June 2007
--- Amended Needham Schroeder protocol
---     A -> B : A
---     B -> A : E(Kbs: A, Nb0)
---     A -> S : A, B, Na, E(Kbs: A, Nb0)
---     S -> A : E(Kas : A, Na, Kab, E(Kbs : A, Kab, Nb0))
---     A -> B : E(Kbs : A, Kab, Nb0)
---     B -> A : E(Kab : Nb)
---     A -> B : E(Kab : Nb-1)

(reset)
(
module ANS
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.
--- to decrement the nonce by one creating another nonce
dec : nonce -> nonce.

net : msg -> state.

initiator:
forall A : princ.
{
                    exists LA : state.
                    exists LA1 : nonce -> {B : princ} {S : server} ltk B S -> ltk A S -> state.
                    exists LA2 : {B : princ} stk A B -> state.
ANSRule1:
  empty
  => net A, LA.

ANSRule3:
   forall B : princ.
   forall S : server.
   forall Kas : ltk A S.
   forall Kbs : ltk B S.
   forall Nb0 : nonce.
    net (enc Kbs (A & Nb0)), LA
   => exists Na : nonce.
      net(A & B & Na & enc Kbs (A & Nb0)), LA1 Nb0 B S Kbs Kas.

ANSRule5:
   forall B : princ.
   forall S : server.
   forall Kas : ltk A S.
   forall Kbs : ltk B S.
   forall Kab : stk A B.
   forall Nb0 : nonce.
     net(enc Kas (Na & B & Kab & enc Kbs (A & Nb0 & Kab))), LA1 Nb0 B S Kbs Kas
   => net(enc Kbs (A & Nb0 & Kab)), LA2 B Kab.

ANSRule7:
   forall B : princ.
   forall Kab : stk A B.
   forall Nb : nonce.
    net(enc Kab Nb), LA2 B Kab
   => net(enc Kab (dec Nb)).
}

receiver:
forall B : princ.
{
                  exists LB1 : princ -> nonce -> {S : server} ltk B S -> state.
                  exists LB2 : nonce -> {A : princ} stk A B -> state.
ANSRule2:
    forall A : princ.
    forall S : server.
    forall Kbs : ltk B S. 
    net A
 => exists Nb0 : nonce.
   net (enc Kbs (A & Nb0)), LB1 A Nb0 S Kbs.

ANSRule6:
   forall A : princ.
   forall S : server.
   forall Kas : ltk A S.
   forall Kbs : ltk B S.
   forall Kab : stk A B.
   forall Nb0 : nonce.
     net(enc Kbs (A & Nb0 & Kab)), LB1 A Nb0 S Kbs
  => exists Nb : nonce.
     net(enc Kab Nb), LB2 Nb A Kab.

ANSRule8:
   forall A : princ.
   forall Kab : stk A B.
   forall Nb : nonce.
    net(enc Kab (dec Nb)), LB2 Nb A Kab
   => empty.

}


server:
---for S : server. if S is declared as global.
forall S : server.
{
ANSRule4:
   forall Kas : ltk A S.
   forall Kbs : ltk B S.
   forall Nb0 : nonce.
    net(A & B & Na & enc Kbs (A & Nb0))
     => exists Kab : stk A B.
        net(enc Kas (Na & B & Kab & enc Kbs (A & Nb0 & Kab))).
}


)

Findings