Needham-Schroeder Signature Protocol

Purpose

A has a one way function that creates a digest CS of the message and sends it to S using shared key Kas. S sends back the digest and A to A using its own prrivate key Kss. A then passes this on to B who then sends it back to S. S checks if the digest is equal.

Informal Specification

  1. A -> S : A, E(Kas : CS)
  2. S -> A : E(Kss : A, CS)
  3. A -> B : Message, E(Kss : A, CS)
  4. B -> S : B, E(Kss : A, CS)
  5. S -> B : E(Kbs : A, CS)

See Commonly Used Representations

MSR Specification

Click here to download 
--- Author: rishav
--- Date: 6 August 2007
--- Needham-Schroeder Signature Protocol
---     A -> S : A, E(Kas : CS)
---     S -> A : E(Kss : A, CS) 
---     A -> B : Message, E(Kss : A, CS)
---     B -> S : B, E(Kss : A, CS)
---     S -> B : E(Kbs : A, CS)

(reset)
(
module NSS
export * .

server : type.                         server <: princ.
key : type.
ltk : princ -> princ -> type.          ltk A B <: key.
ltks : princ -> type.		       ltks S <: key.
digest : type.                         digest <: msg.
dig : msg -> digest.

enc : key -> msg -> msg.

net : msg -> state.


initiator:
forall A : princ.
{
			exists LA : msg -> state.
NSSRule1:
  forall Kas : ltk A S.
  forall mess : msg.
  empty
  => net(A & enc Kas (dig mess)), LA mess.

NSSRule3:
   forall Kss : ltks S.
   forall mess : msg.
   net(enc Kss (A & dig mess))
   => net(mess & enc Kss (A & dig mess)), LA mess.
}

receiver:
forall B : princ.
{
			exists LB : msg -> princ -> state.
NSSRule4:
   forall A : princ.
   forall Kss : ltks S.
   forall mess : msg.
     net(mess & enc Kss (A & dig mess))
  => net(B & enc Kss (A & dig mess)), LB mess A.


NSSRule6:
   forall A : princ.
   forall Kbs : ltk B S.
   forall mess : msg.
    net(enc Kbs (A & dig mess)), LB mess A
   => empty.

}


server:
forall S : server.
{
			exists LB : msg -> {S : server} ltks S -> state.
NSSRule2:
   forall S : server.
   forall Kas : ltk A S.
   forall Kss : ltks S.
   forall mess : msg.
   net(A & enc Kas (dig mess))
     => net(enc Kss (A & dig mess)), LB mess S Kss.

NSSRule5:
   forall S : server.
   forall Kss : ltks S.
   forall Kbs : ltk B S.
   forall mess : msg.
     net(B & enc Kss (A & dig mess)), LB mess S Kss
  => net(enc Kbs (A & dig mess)).


}


)