private fun kxs/1; (* kxs(X) is the private key shared between X and S. *)

proc dolev_yao_intruder (pub_channel, initial_knowledge) =
     new id;
     !(	out (pub_channel, initial_knowledge)
	| out (pub_channel, id)
	| in (pub_channel, M); out (pub_channel, M); out (pub_channel, M)
	| new N; out (pub_channel, N)
	| dy_synthesizer (pub_channel, pub_channel)
	| dy_analyzer (pub_channel, pub_channel)
	);

proc alice (to_s, from_s, to_b, from_b, A, B, Kas) =
   new Na; out (to_s, A, B, Na);
   in (from_s, {=Na, =B, Kab, M} Kas);
   out (to_b, M);
   in (from_b, {Nb} Kab);
   out (to_b, {s (Nb)} Kab);

proc bob (to_a, from_a, Kbs) =
   in (from_a, {Kab, A} Kbs);
   new Nb; out (to_a, {Nb} Kab);
   in (from_a, {=s (Nb)} Kab);

proc server (from_a, to_a) =
   in (from_a, A, B, Na);
   new Kab; out (to_a, {Na, B, Kab, {Kab, A} kxs(B)} kxs(A));

proc main = new c_pub; new a; new b; new Kas; new Kbs;
   ( dolev_yao_intruder (c_pub, 0)
   | ![a_no] ![b_no] let A = (a, a_no) in
                     let B = (b, b_no) in
                     ( alice (c_pub, c_pub, c_pub, c_pub, A, B, kxs (A))
                     | bob (c_pub, c_pub, kxs (B)))
   | !server (c_pub, c_pub)
   );