/*  nsl-with-secret-optimized(NSL with secret, avoiding encryption of the second nonce response) */ 

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

(news chE)(news chD)
(
  /* the process of A */

  *chD??cmsg.
   split cmsg is (a,dka) in
   chE??cmsg2.
   split cmsg2 is (b,ekb) in
   (new nonceA)
   (net!{{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 (m,text4) in
                 split text4 is (nonceA2,nonceB2) in
                 check nonceA is nonceA2 in
                 (end (b,(a,m)) |
                  begin (a,b).net!nonceB2)
                 )
    )

   |
     /* the process of B */
   
   *chD??cmsg3.
    split cmsg3 is (b,dkb) in
    chE??cmsg4.
    split cmsg4 is (a,eka) in
    net?ctext2.
    (new msg)
    (new nonceB)
    decrypt ctext2 is {{text5}}dkb in
    case text5 is inl(text6).
                  (match text6 is (a,nonceA2) in
                   begin (b,(a,msg)).net!{{inr((b,(msg,(nonceA2,nonceB))))}}eka |
                   net?nonceB2.
                   check nonceB is nonceB2 in
                   end (a,b) 
                  )
               is inr(d).O

    |

    *(new p)(newAsym ekp,dkp)
     (*net!p |*net!ekp |
      *chE!!(p,ekp) |
      *chD!!(p,dkp)
     )
)