*** 168 tests succeeded - MSR implementation self-test done ***

OCC libraries loaded, switching to MSR mode

Maude> in examples/needham-schroeder.msr
context reset
context extended: {pubK : princ -> type}%enum
context extended: {encrypt : {A | princ} pubK A -> msg -> msg}
context extended: {START-1 : princ -> princ -> state}
context extended: {START-2 : princ -> state}
context extended: {TERMINATED-1 : princ -> state}
context extended: {TERMINATED-2 : princ -> state}

role defined
initiator : forall A : princ . {
 exists L : princ -> nonce -> state .
 Init1 :
  forall B : princ .
  forall PKB : pubK B .
  START-1 A B
  => exists nA : nonce .
     N(princ-msg A & princ-msg B & encrypt PKB(nonce-msg nA & princ-msg A)),L B nA .
 Init2 :
  forall B : princ .
  forall PKA : pubK A .
  forall PKB : pubK B .
  forall nA : nonce .
  forall nB : nonce .
  N(princ-msg B & princ-msg A & encrypt PKA(nonce-msg nA & nonce-msg nB)),L B nA
  => N(princ-msg A & princ-msg B & encrypt PKB(nonce-msg nB)),TERMINATED-1 A .
}

role defined
responder : forall B : princ . {
 exists L : princ -> nonce -> state .
 Resp1 :
  forall A : princ .
  forall PKA : pubK A .
  forall PKB : pubK B .
  forall nA : nonce .
  START-2 B,N(princ-msg A & princ-msg B & encrypt PKB(nonce-msg nA & princ-msg A))
  => exists nB : nonce .
     N(princ-msg B & princ-msg A & encrypt PKA(nonce-msg nA & nonce-msg nB)),L A nB .
 Resp2 :
  forall A : princ .
  forall PKB : pubK B .
  forall nB : nonce .
  N(princ-msg A & princ-msg B & encrypt PKB(nonce-msg nB)),L A nB
  => TERMINATED-2 B .
}
context extended: {A : princ}
context extended: {B : princ}
context extended: {pkA : pubK A}
context extended: {pkB : pubK B}
config: START-1 A B,START-2 B
Maude>