Needham-Schroeder Public Key Protocol

Purpose

Same as Needham Schroeder protocol but with public keys.

Informal Specification

  1. A -> S : A, B
  2. S -> A : E(Ks-1 : Kb, B)
  3. A -> B : E(Kb : Na, A)
  4. B -> S : B, A
  5. S -> B : E(Ks-1 : Ka, A)
  6. B -> A : E(Ka: Na, Nb)
  7. A -> B : E(Kb: Nb)

See Commonly Used Representations

MSR Specification

Click here to download 
--- Author: rishav
--- Date: 11 October 2007
--- Needham-Schroeder Public Key Protocol
---     A -> S : A, B
---     S -> A : E(Ks-1 : Kb, B) 
---     A -> B : E(Kb : Na, A)
---     B -> S : B, A
---     S -> B : E(Ks-1 : Ka, A)
---     B -> A : E(Ka: Na, Nb)
---     A -> B : E(Kb: Nb)
(reset)
(
module NSP
export * .

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

enc : key -> msg -> msg.

net : msg -> state.


initiator:
forall A : princ.
{
			exists LA : princ -> state.
			exists LA2 : nonce -> {B : princ} ltk B -> state.
NSPRule1:
  forall B : princ.
  empty
  => net(A & B), LA B.

NSPRule3:
   forall B : princ.
   forall Ks-1 : ltks S.
   forall Kb : ltk B.
   net(enc Ks-1 (B & Kb)), LA B
   => exists Na : nonce.
      net(enc Kb (A & Na)), LA2 Na B Kb.

NSPRule7:
    forall B : princ.
    forall Kb : ltk B.
    forall Ka : ltk A.
    forall Na : nonce.
    forall Nb : nonce.
      net(enc Ka (Nb & Na)), LA2 Na B Kb
    => net(enc Kb Nb).
}

receiver:
forall B : princ.
{
			exists LB : princ -> nonce -> state.
			exists LB2 : nonce -> state.
NSPRule4:
   forall A : princ.
   forall Na : nonce.
   forall Kb : ltk B.
     net(enc Kb (A & Na))
  => net(B & A), LB A Na.


NSPRule6:
   forall A : princ.
   forall Na : nonce.
   forall Ks-1 : ltks S.
   forall Ka : ltk A.
     net(enc Ks-1 (A & Ka)), LB A Na
   => exists Nb : nonce.
      net(enc Ka (Nb & Na)), LB2 Nb.


NSPRule8:
   forall Nb : nonce.
   forall Kb : ltk B.
    net(enc Kb Nb), LB2 Nb
  => empty.
}


server:
forall S : server.
{
			exists LS : princ -> princ -> state.
NSPRule2:
   forall A : princ.
   forall B : princ.
   forall Ks-1 : ltks S.
   forall Kb : ltk B.
   net(A & B)
     => net(enc Ks-1 (B & Kb)), LS A B.

NSPRule5:
   forall A : princ.
   forall B : princ.
   forall Ks-1 : ltks S.
   forall Ka : ltk A.
     net(B & A), LS A B
  => net(enc Ks-1 (A & Ka)).


}


)