(* Exam MPRI 2014-15 *)

param NA, NB.

type host [bounded].
type pkey [bounded].
type skey [bounded].
type pkeyseed [large,fixed].
type keyseed [large,fixed].
type spkey [bounded].
type sskey [bounded].
type skeyseed [large,fixed].
type signature [bounded].
type blocksize [fixed].
type key [fixed]. (* distributed key *)

fun concat(spkey, key, signature): blocksize [data].

(* Public-key encryption (IND-CCA2) *)

proba Penc.
proba Penccoll.

expand IND_CCA2_public_key_enc(pkeyseed, pkey, skey, blocksize, bitstring, skgen, pkgen, penc, pdec, pinjbot, pZ, Penc, Penccoll).

const Zb: blocksize.
equation forall x: blocksize; pZ(x) = Zb.

(* Signatures *)

proba Psign.
proba Psigncoll.

expand UF_CMA_proba_signature(skeyseed, spkey, sskey, key, signature, sskgen, spkgen, sign, check, Psign, Psigncoll).

(* Queries *)

channel c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, 
	start, finish.

query secret k'.
(* query secret k''. This query fails *)

let processA(pkA: spkey, skA: sskey, pkB: pkey) =
	in(c1, pkX: pkey);
	new k:key;
	let payload = concat(pkA, k, sign(k, skA)) in
        out(c2, penc(payload, pkX));
	(* Test for secrecy *)
	in(c5, ());
	if pkX = pkB then
	let k':key = k in
	yield.

let processB(skB: skey, pkA: spkey) =
	in(c3, m:bitstring);
	let pinjbot(concat(pkY, kB, s)) = pdec(m, skB) in
	if check(kB, pkY, s) then
	(* Test for secrecy *)
	if pkY = pkA then
	let k'': key = kB in
	yield.

process 
	in(start, ());
	new rkA: skeyseed;
	let pkA = spkgen(rkA) in
	let skA = sskgen(rkA) in
	new rkB: pkeyseed;
	let pkB = pkgen(rkB) in
	let skB = skgen(rkB) in
	out(c7, (pkA, pkB));
	((! NA processA(pkA, skA, pkB)) |
	 (! NB processB(skB, pkA)))

(* EXPECTED
RESULT Could not prove event inj:endB(x, y, k) ==> inj:beginA(x, y, k), secrecy of keyB.
0.290s (user 0.290s + system 0.000s), max rss 48432K
END *)