\||||||||||||||||||/
                   --- Welcome to Maude ---
                     /||||||||||||||||||\
            Maude alpha84c built: Jun 22 2004 15:35:45
             Copyright 1997-2004 SRI International
                   Fri Oct 15 20:04:31 2004
                   
*** 168 tests succeeded - MSR implementation self-test done ***

OCC libraries loaded, switching to MSR mode

Maude> in examples/otway-rees.msr
context extended: {shK : princ -> princ -> type}
context extended: {ltK : princ -> princ -> type}%enum
context extended: {stK : princ -> princ -> type}
context extended: {ltK-shK : {A | princ} {B | princ} ltK A B <: shK A B}
context extended: {stK-shK : {A | princ} {B | princ} stK A B <: shK A B}
context extended: {stK-msg : {A | princ} {B | princ} stK A B <: msg}
context extended: {encrypt : {A | princ} {B | princ} shK A B -> msg -> msg}
context extended: {START-1 : princ -> princ -> state}
context extended: {START-2 : princ -> state}
context extended: {START-3 : princ -> state}
context extended: {TERMINATED-1 : princ -> state}
context extended: {TERMINATED-2 : princ -> state}
context extended: {TERMINATED-3 : princ -> state}
context extended: {S : princ}

role defined
initiator : forall A : princ . {
 exists L : princ -> princ -> nonce -> nonce -> state .
 Init1 :
  forall B : princ .
  forall kAS : ltK A S .
  START-1 A B
  => exists n : nonce . exists nA : nonce .
     N(nonce-msg n & princ-msg A & princ-msg B & encrypt(ltK-shK kAS)(nonce-msg nA & nonce-msg n & princ-msg A & princ-msg
    B)),L A B n nA .
 Init2 :
  forall B : princ .
  forall kAS : ltK A S .
  forall n : nonce .
  forall nA : nonce .
  forall kAB : stK A B .
  N(nonce-msg n & encrypt(ltK-shK kAS)(nonce-msg nA & stK-msg kAB)),L A B n nA
  => TERMINATED-1 A .
}

role defined
responder : forall B : princ . {
 exists L : {B : princ} princ -> nonce -> nonce -> ltK B S -> state .
 Resp1 :
  forall n : nonce .
  forall A : princ .
  forall X : msg .
  forall kBS : ltK B S .
  START-2 B,N(nonce-msg n & princ-msg A & princ-msg B & X)
  => exists nB : nonce .
     N(nonce-msg n & princ-msg A & princ-msg B & X & encrypt(ltK-shK kBS)(nonce-msg nB & nonce-msg n & princ-msg A &
    princ-msg B)),L B A n nB kBS .
 Resp2 :
  forall n : nonce .
  forall A : princ .
  forall Y : msg .
  forall kBS : ltK B S .
  forall nB : nonce .
  forall kAB : stK A B .
  N(nonce-msg n & Y & encrypt(ltK-shK kBS)(nonce-msg nB & stK-msg kAB)),L B A n nB kBS
  => N(nonce-msg n & Y),TERMINATED-2 B .
}

role defined
server : for S . {
 Server1 :
  forall n : nonce .
  forall A : princ .
  forall kAS : ltK A S .
  forall B : princ .
  forall kBS : ltK B S .
  forall nA : nonce .
  forall nB : nonce .
  START-3 S,N(nonce-msg n & princ-msg A & princ-msg B & encrypt(ltK-shK kAS)(nonce-msg nA & nonce-msg n & princ-msg A &
    princ-msg B)& encrypt(ltK-shK kBS)(nonce-msg nB & nonce-msg n & princ-msg A & princ-msg B))
  => exists kAB : stK A B .
     N(nonce-msg n & encrypt(ltK-shK kAS)(nonce-msg nA & stK-msg kAB)& encrypt(ltK-shK kBS)(nonce-msg nB & stK-msg kAB)),
    TERMINATED-3 S .
}
context extended: {A : princ}
context extended: {B : princ}
context extended: {kAS : ltK A S}
context extended: {kBS : ltK B S}
config: START-1 A B,START-2 B,START-3 S
Maude> (rew)
TERMINATED-1 A,TERMINATED-2 B,TERMINATED-3 S