/* nsl(Lowe's fix, 3-message version) */

/* Message 1: A -> B : {{msg1(A,Na)}}pkB */
/* Event 1:  B begins  "b authenticating to a" */
/* Message 2: B -> A : {{msg2(B,Na,Nb)}}pkA */
/* Event 2:  A ends    "b authenticating to a" */
/* Event 3:  A begins  "a authenticating to b" */
/* Message 3: A -> B : {{msg3(Nb)}}pkB */
/* Event 4:  B ends    "a authenticating to b" */


(news db)(news roleA)(news roleB)(news db_untrusted)
(
  /* the process of A */

  *roleA??cmsg.
   split cmsg is (a,dka) in 
   db??cmsg2.
   split cmsg2 is (b,ekb) in 
   (new nonceA)
   (net!{{inl(inl((a,nonceA)))}}ekb |
    net?ctext.
    decrypt ctext is {{text}}dka in
    case text is inl(c).O
              is inr(text2).
                (match text2 is (b,text3) in
                 split text3 is (nonceA2,nonceB2) in
                 (check nonceA is nonceA2 in
                  end (b,a) |
                  begin (a,b).net!{{inl(inr(nonceB2))}}ekb)
                 )
    )

   | /* A talking to an intruder */
  *roleA??cmsg.
   split cmsg is (a,dka) in 
   db_untrusted??cmsg2.
   split cmsg2 is (b,ekb) in 
   (new nonceA)
   (net!{{inl(inl((a,nonceA)))}}ekb |
    net?ctext.
    decrypt ctext is {{text}}dka in
    case text is inl(c).O
              is inr(text2).
                (match text2 is (b,text3) in
                 split text3 is (nonceA2,nonceB2) in
                 (check nonceA is nonceA2 in
                 /*  end (b,a) | */
                  begin (a,b).net!{{inl(inr(nonceB2))}}ekb)
                 )
    )

   |
     /* the process of B */
   
   *roleB??cmsg3.
    split cmsg3 is (b,dkb) in 
    db??cmsg4.
    split cmsg4 is (a,eka) in 
    net?ctext2.
    (new nonceB)
    (new msg)
    decrypt ctext2 is {{text0}}dkb in
    case text0 is inl(text4).
                  (case text4 is inl(text5).
                                 (match text5 is (a,nonceA2) in
                                  (begin (b,a).
                                   net!{{inr((b,(nonceA2,nonceB)))}}eka |
                                   net?ctext3.
                                   decrypt ctext3 is {{text6}}dkb in
                                   case text6 is inl(text7).
                                                (case text7 is inl(f).O
                                                            is inr(nonceB2).
                                                                (check nonceB is nonceB2 in
                                                                 end (a,b)
                                                                 )
                                                 )
                                              is inr(g).O
                                   )
                                  )
                               is inr(e).O 
                  )
                is inr(d).O

   |
     /* B talking to an intruder  */
   
   *roleB??cmsg3.
    split cmsg3 is (b,dkb) in 
    db_untrusted??cmsg4.
    split cmsg4 is (a,eka) in 
    net?ctext2.
    (new nonceB)
    (new msg)
    decrypt ctext2 is {{text0}}dkb in
    case text0 is inl(text4).
                  (case text4 is inl(text5).
                                 (match text5 is (a,nonceA2) in
                                  (begin (b,a).
                                   net!{{inr((b,(nonceA2,nonceB)))}}eka |
                                   net?ctext3.
                                   decrypt ctext3 is {{text6}}dkb in
                                   case text6 is inl(text7).
                                                (case text7 is inl(f).O
                                                            is inr(nonceB2).
                                                                (check nonceB is nonceB2 in O
                                                               /*  end (a,b) */
                                                                 )
                                                 )
                                              is inr(g).O
                                   )
                                  )
                               is inr(e).O 
                  )
                is inr(d).O

    |

    *(new p)(newAsym ekp,dkp)
     (*net!p |*net!ekp |
      *db!!(p,ekp) |
      *roleA!!(p,dkp) |
      *roleB!!(p,dkp)
     )
    | /* intruders using their own keys */
    *(new intruder)(newAsym ekap,dkap)
     (*net!intruder | *net!ekap | *net!dkap
     |  *db_untrusted!!(intruder,ekap)  
     )
)