/*********************************************************************/
/* Otway-Rees, version 1                                             */
/* A_{i} != B_{i}, KA_{i} != KB_{i}.                                 */
/*             Time-stamp: <04-10-06 Christoffer Rosenkilde Nielsen> */
/*********************************************************************/

let X subset NATURAL3 in
(new_{i in X} KA_{i})(
(new_{j in X} KB_{j})(

/* Initiator - A */
(|_{i in X} |_{j in  X union ZERO} !(new NA_{i,j})
  <A_{i}, B_{j}, M_{i,j}, A_{i}, B_{j}, {A_{i}, B_{j}, M_{i,j}, NA_{i,j}} : KA_{i} [at a1_{i,j} dest {s1_{i,j}}]>.
  (B_{j}, A_{i}, M_{i,j}; x1_{i,j}).
  decrypt x1_{i,j} as {NA_{i,j}; xk_{i,j}} : KA_{i} [at a2_{i,j} orig {s3_{i,j}}] in 
    (B_{j}, A_{i}; x2_{i,j}).
    decrypt x2_{i,j} as {; xmsg_{i,j}} : xk_{i,j} [at a3_{i,j} orig {b3_{i,j}}] in 0)

|

/* Responder - B */
(|_{j in X} |_{i in X union ZERO} !(new NB_{i,j})
  (A_{i}, B_{j}, M_{i,j}, A_{i}, B_{j}; y1_{i,j}).
  <B_{j}, S, M_{i,j}, A_{i}, B_{j}, y1_{i,j}, {A_{i}, B_{j}, M_{i,j}, NB_{i,j}} : KB_{j} [at b1_{i,j} dest {s2_{i,j}}]>.
  (S, B_{j}, M_{i,j}; y2_{i,j}, y3_{i,j}).
  decrypt y3_{i,j} as {NB_{i,j}; yk_{i,j}} : KB_{j} [at b2_{i,j} orig {s4_{i,j}}] in 
    <B_{j}, A_{i}, M_{i,j}, y2_{i,j}>.
    (new MSG_{i,j})
    <B_{j},A_{i}, {MSG_{i,j}} : yk_{i,j} [at b3_{i,j} dest {a3_{i,j}}]>.0)
  	
|

/* Server - S */
(|_{i in X union ZERO} |_{j in X union ZERO} !
  (B_{j}, S, M_{i,j}, A_{i}, B_{j}; z1_{i,j}, z2_{i,j}).
  decrypt z1_{i,j} as {A_{i}, B_{j}, M_{i,j}; zna_{i,j}} : KA_{i} [at s1_{i,j} orig {a1_{i,j}}] in 
    decrypt z2_{i,j} as {A_{i}, B_{j}, M_{i,j}; znb_{i,j}} : KB_{j} [at s2_{i,j} orig {b1_{i,j}}] in 
      (new K_{i,j})
      <S, B_{j}, M_{i,j}, {zna_{i,j}, K_{i,j}} : KA_{i} [at s3_{i,j} dest {a2_{i,j}}], 
                          {znb_{i,j}, K_{i,j}} : KB_{j} [at s4_{i,j} dest {b2_{i,j}}]>.0)
))