(* Encrypt-then-MAC example *)

param n.

type mkey [bounded].
type mkeyseed [fixed].
type key [fixed].
type keyseed [fixed].
type seed [fixed].
type macs [bounded].

fun k2b(key):bitstring [compos].

(* Shared-key encryption (CPA Stream cipher) *)

proba Penc.

expand IND_CPA_sym_enc(keyseed, key, bitstring, bitstring, seed, kgen, enc, dec, injbot, Z, Penc).

(* The function Z returns for each bitstring, a bitstring
   of the same length, consisting only of zeroes. *)
const Zk:bitstring.
forall y:key; 
	Z(k2b(y)) = Zk.

(* Mac *)

proba Pmac.

expand UF_CMA_mac(mkeyseed, mkey, bitstring, macs, mkgen, mac, verify, Pmac).

(* Queries *)

query secret1 k''.
query secret k''.

channel cA, cB, start, c.

let QA = 
	! i <= n 
	in(cA, ());
	new k' : key;
	new r'' : seed;
	let e = enc(k2b(k'), k, r'') in
	out(cA, (e, mac(e, mk))).

let QB =
	! i <= n 
	in(cB, (e':bitstring, ma:macs));
	if verify(e', mk, ma) then
	let injbot(k2b(k'':key)) = dec(e', k) in
	out(cB, ()).

process 
	in(start, ());
	new r: keyseed;
	let k = kgen(r) in
	new r': mkeyseed;
	let mk = mkgen(r') in
	out(c, ());
	(QA | QB)