/* Otway and Ree's key exchange protocol */

/* Message 1: A->B  A,B,NonceA */
/* Message 2: B->S  A,B,NonceA,NonceB */
/* Event 1: S begins <A,B,KeyAB> */
/* Event 2: S begins <B,A,KeyAB> */
/* Message 3: S->B  {msg4(A,B,KeyAB,NonceA)}KeyAS,{msg3(A,B,KeyAB,NonceB)}KeyBS */
/* Event 3: B ends <B,A,KeyAB> */
/* Message 4: B->A  {msg4(A,B,KeyAB,NonceA)}KeyAS */
/* Event 4: A ends <A,B,KeyAB> */

(news db)
(news sender)
(news receiver)
(
 /*** server ***/
 (*net?msg4.
   split msg4 is (a,msg42) in
   split msg42 is (b,msg43) in
   split msg43 is (nonA,nonB) in
   (newSym keyAB)
   begin (a,(b,keyAB)).
   begin (b,(a,keyAB)).
   db??x.
   match x is (a, keyAS) in 
   db??y.
   match y is (b, keyBS) in
   net!({inl((a,(b,(keyAB,nonA))))}keyAS,{inr((a,(b,(keyAB,nonB))))}keyBS))
|
 (*sender??x.  /*** sender ***/
   split x is (a, keyA) in
   net?b.
   (new non)
   (net!(a,(b,non))
   |net?y.
    decrypt y is {m4}keyA in
    case m4 is inl(m4b).
                (match m4b is (a, m42) in
                 match m42 is (b, m43) in
                 split m43 is (keyAB, non2) in
                check non is non2 in
                end (a,(b,keyAB)))
             is inr(dummy).O))
|
 (*receiver??x.  /*** receiver ***/
   split x is (b, keyB) in
   net?msg3.
   split msg3 is (a,msg32) in
   match msg32 is (b,nonA) in
   (new nonB)
   (net!(a,(b,(nonA,nonB)))
   |net?ct.
    split ct is (ctxa,ctxb) in
    decrypt ctxb is {m3}keyB in
    case m3 is inl(dm1).O
     is inr(m3b).
         match m3b is (a, m3b2) in
         match m3b2 is (b, m3b3) in
         split m3b3 is (keyABb, nonB2) in
         check nonB is nonB2 in
         (end (b,(a,keyABb))|
         net!ctxa)))
|*(new p)(newSym keyP)  /*** infinitely participants of the protocol ***/
   (*net!p |
    *db!!(p,keyP) | 
    *sender!!(p,keyP) | 
    *receiver!!(p, keyP))
)