(* Needham Schroeder-Lowe protocol. *)

(* set interactiveMode = true. *)

proof {
  show_game occ;
  insert 107 "if pkY = pkB then";
  insert 107 "if pkY = pkA then";
  insert 24 "if pkX = pkA then";
  insert 24 "if pkX = pkB then";
(*  crypto ind_cca2(enc) rkB;
  crypto ind_cca2(enc) rkA;
  success *)
  auto
}

param NA, NB.

type nonce [large,fixed].
type pkey [bounded].
type skey [bounded].
type keyseed [large,fixed].
type blocksize [fixed].

fun concat1(nonce, pkey):blocksize [data].
fun concat2(nonce, nonce, pkey):blocksize [data].
fun pad(nonce):blocksize [data].

equation forall z:nonce,t:nonce,u:pkey,y2:nonce,z2:pkey;
	concat2(z,t,u) <> concat1(y2,z2).
equation forall y:nonce,y2:nonce,z2:pkey;
	pad(y) <> concat1(y2,z2).
equation forall z:nonce,t:nonce,u:pkey,y2:nonce;
	concat2(z,t,u) <> pad(y2).

(* Public-key encryption (CCA2) *)

proba Penc.
proba Penccoll.

expand IND_CCA2_public_key_enc(keyseed, pkey, skey, blocksize, bitstring, skgen, pkgen, enc, dec, injbot, Z, Penc, Penccoll).

const Zblocksize: blocksize.
equation forall x: blocksize; Z(x) = Zblocksize.

(* Queries *)

channel c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, 
	c15, c16, c17, start, finish.

event beginA(pkey, pkey, nonce, nonce).
event endA(pkey, pkey, nonce, nonce).
event beginB(pkey, pkey, nonce, nonce).
event endB(pkey, pkey, nonce, nonce).

query x:pkey, y:pkey, na:nonce, nb:nonce;
	event(endA(x,y,na,nb)) ==> event(beginB(x,y,na,nb)).
query x:pkey, y:pkey, na:nonce, nb:nonce;
	event(endB(x,y,na,nb)) ==> event(beginA(x,y,na,nb)).
query x:pkey, y:pkey, na:nonce, nb:nonce;
	inj-event(endA(x,y,na,nb)) ==> inj-event(beginB(x,y,na,nb)).
query x:pkey, y:pkey, na:nonce, nb:nonce;
	inj-event(endB(x,y,na,nb)) ==> inj-event(beginA(x,y,na,nb)).


let processA(skA: skey, pkA: pkey, pkB: pkey) =
	in(c1, pkX: pkey);
	(* Message 1 *)
        new Na: nonce;
        out(c4, enc(concat1(Na, pkA), pkX));
	(* Message 2 *)
        in(c5, m: bitstring);
	let injbot(concat2(=Na, Nb, =pkX)) = dec(m, skA) in
	event beginA(pkA, pkX, Na, Nb);
	(* Message 3 *)
	out(c6, enc(pad(Nb), pkX));
	(* OK *)
	in(finish, ());
	if pkX = pkB then
	event endA(pkA, pkX, Na, Nb).

let processB(skB: skey, pkB: pkey, pkA: pkey) =
	(* Message 1 *)
	in(c7, m:bitstring);
	let injbot(concat1(Na, pkY)) = dec(m, skB) in
	(* Message 2 *)
	new Nb: nonce;
	event beginB(pkY, pkB, Na, Nb);
	out(c10, enc(concat2(Na, Nb, pkB), pkY));
	(* Message 3 *)
	in(c11, m3: bitstring);
	let injbot(pad(=Nb)) = dec(m3, skB) in
	(* OK *)
	if pkY = pkA then
	event endB(pkY, pkB, Na, Nb).

process 
	in(start, ());
	new rkA: keyseed;
	let pkA = pkgen(rkA) in
	let skA = skgen(rkA) in
	new rkB: keyseed;
	let pkB = pkgen(rkB) in
	let skB = skgen(rkB) in
	out(c15, (pkA, pkB));
	((! NA processA(skA, pkA, pkB)) |
	 (! NB processB(skB, pkB, pkA)))