--- The Needham-Schroeder protocol for two parties implemented in MSR
--- Author: Stefan Reich

(reset)
in ../lib/native.msr
(
module needham-schroeder2
import native * .
export * .

--- Key types

pubK: princ -> type. %enum

encrypt: pubK A -> msg -> msg.

--- auxiliary start tags to limit role instantiation
START-1: princ -> state.
START-2: princ -> state.

--- tags to mark succesful role termination
--- 1st argument is active principal, 2nd/3rd argument is other party and its session nonce 
TERMINATED-1, TERMINATED-2: princ -> princ -> nonce -> state.

--- Initiator's role with all declarations explicit:

initiator :
forall A: princ.
{
  exists L: princ -> nonce -> state.
  
  Init1:
  forall B: princ.
  forall PKB: pubK B.
     START-1 A
  => exists nA: nonce.
     A & B & encrypt PKB (nA & A),
     L B nA
     ***( if not(eq_princ A B) ) --- doesn't work because inequality not decidable
     .

  Init2:
  forall B: princ.
  forall PKA: pubK A.
  forall PKB: pubK B.
  forall nA: nonce.
  forall nB: nonce.
     B & A & encrypt PKA (nA & nB),
     L B nA
  => A & B & encrypt PKB nB,
     TERMINATED-1 A B nB.
}

--- Responder's role with all declarations explicit:

responder :
forall B: princ.
{
  exists L: princ -> nonce -> nonce -> state.
  
  Resp1:
  forall A: princ.
  forall PKA: pubK A.
  forall PKB: pubK B.
  forall nA: nonce.
     START-2 B,
     A & B & encrypt PKB (nA & A)
  => exists nB: nonce.
     B & A & encrypt PKA (nA & nB),
     L A nA nB.
     
  Resp2:
  forall A: princ.
  forall PKB: pubK B.
  forall nA: nonce.
  forall nB: nonce.
     A & B & encrypt PKB nB,
     L A nA nB
  => TERMINATED-2 B A nA.
}

A, B: princ.
pkA: pubK A.
pkB: pubK B.

config START-1 A, START-2 B.

)