%<pre>

needhamschroeder: CONTEXT =
BEGIN
  ids: TYPE = {a, b, e, X};

  participants: TYPE = {x: ids | x /= X};
  intruder(x: participants): BOOLEAN = x=e;

  intruders: TYPE = {x: participants | intruder(x)};
  principals: TYPE = {x: participants | NOT intruder(x)};
  nonces: TYPE = ids;
  nonce(a: participants): nonces = a;
  dmsg: TYPE = [ids, nonces, nonces];
  arb: dmsg = (X,X,X);

  emsg: TYPE = DATATYPE
    enc(key: ids, payload: dmsg)
  END;

  msg: TYPE = [# src: participants, dest: participants, em: emsg #];

  net: CONTEXT = network{msg;};

  dec(k: participants, m:emsg): dmsg = 
   IF key(m)=k THEN payload(m) ELSE arb ENDIF;
  states: TYPE = {sleeping, waiting, tentative, engaged, responding};

principal[i: principals]: MODULE =
BEGIN
  INPUT nstate: net!bufferstate, imsg: msg
  GLOBAL act: net!action, omsg: msg
  LOCAL pc: states, responder: participants
INITIALIZATION
  pc = sleeping;
  responder = i; 
TRANSITION
[
([] (j: participants): i /= j AND
  pc = sleeping AND nstate = net!empty -->
    pc' = waiting;
    responder' = j;
    omsg' = (# src := i, dest := j, em := enc(j, (i, nonce(i), X)) #);
    act' = net!write; 
)
[]
([] (j: participants): i /= j AND
     pc = sleeping AND nstate = net!full
     AND imsg.src = j AND imsg.dest = i AND dec(i, imsg.em).1=j  --> 
   responder' = j;
   pc' = tentative;
   act' = net!overwrite; 
   omsg' = (# src := i, dest := j, 
% following line is the bug
              em := enc(j, (X, dec(i,imsg.em).2, nonce(i))) #);
% To correct, replace by the following and add a check to the next rule
%              em := enc(j, (i, dec(i,imsg.em).2, nonce(i))) #);
)
[]
  pc = waiting AND nstate = net!full 
     AND imsg.src = responder AND imsg.dest = i
% Add this check to correct the bug
%     AND dec(i,imsg.em).1 = responder
     AND dec(i,imsg.em).2 = nonce(i) -->
   pc' = engaged;
   act' = net!overwrite; 
   omsg' = (# src := i, dest := responder, 
              em := enc(responder, (X, dec(i,imsg.em).3, X)) #);
[]
  pc = tentative AND nstate = net!full
     AND imsg.src = responder AND imsg.dest = i
     AND dec(i,imsg.em).3 = nonce(i) -->
   pc' = responding;
   act' = net!read;
[]
 ELSE --> 
]
END;

intruder[x:intruders]: MODULE =
BEGIN
  GLOBAL act: net!action, omsg: msg
  INPUT nstate: net!bufferstate, imsg: msg
  LOCAL  nmem, n1, n2: nonces, mmem: emsg
INITIALIZATION
  nmem = nonce(e);
%  n1 = nonce(e); n2 = nonce(e);
  mmem = enc(X,(X,X,X));
TRANSITION
[
 nstate = net!full AND imsg.dest = x  --> 
% this is too weak, but adequate to find the bug--see the discussion in the report.
   nmem' IN {dec(x,imsg.em).2, nmem};
% this is the stronger version
%   nmem' IN {dec(x,imsg.em).2, dec(x,imsg.em).3, dec(x,imsg.em).2, nmem};
   act' IN {net!read, net!copy};
[]
 nstate = net!full AND imsg.dest /= x --> 
   mmem' IN {imsg.em, mmem};
   act' IN {net!read, net!copy};
[]
([] (i: participants, j: principals): TRUE -->
   act' = IF nstate = net!empty THEN net!write ELSE net!overwrite ENDIF;
   omsg' = (# src := i, dest := j, em := mmem#);
)
[]
([] (i: participants, j: principals): TRUE -->
   act' = IF nstate = net!empty THEN net!write ELSE net!overwrite ENDIF;
   n1' IN {nmem, nonce(x)};
   n2' IN {nmem, nonce(x)};
   omsg' = (# src := i, dest := j, em := enc(j, (i, n1', n2')) #);
)
[]
  ELSE -->
]
END;

system: MODULE = (([] (id: principals): principal[id]) [] intruder[e])
   || (RENAME buffer TO imsg, inms TO omsg IN net!network);

prop: THEOREM system |- G((FORALL (x,y: principals): 
    (pc[x]=responding AND responder[x]=y) => 
         ((pc[y]=waiting OR pc[y]=engaged) AND responder[y]=x)));

test: THEOREM system |-  G(NOT (pc[a]=tentative AND pc[b]=tentative));

test2: THEOREM system |-  G(NOT (pc[a]=responding AND responder[a]=e));


END