(* Encrypt-then-MAC example *)

param n.

type mkey [fixed].
type key [fixed].
type macs [bounded].

fun k2b(key):bitstring [data].

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

proba Penc.

expand IND_CPA_sym_enc(key, bitstring, bitstring, 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.
equation forall y:key; 
	Z(k2b(y)) = Zk.

(* Mac *)

proba Pmac.

expand SUF_CMA_det_mac(mkey, bitstring, macs, mac, verify, Pmac).

(* Queries *)

query secret k'' [onesession].
query secret k''.

letfun enc'(k: key, mk:mkey, m: bitstring) =
      let e = enc(m,k) in
      (e, mac(e,mk)).

letfun dec'(k: key, mk: mkey, c: bitstring) =
      let (e: bitstring, m: macs) = c in
      (
         if verify(e, mk, m) then
            dec(e, k)
         else
            bottom
      )
      else
         bottom.

let QA(k: key, mk: mkey) = 
	foreach i <= n do
	OA() :=
	k' <-R key;
	return(enc'(k, mk, k2b(k'))).

let QB(k: key, mk: mkey) =
	foreach i' <= n do
	OB(e':bitstring) :=
	let injbot(k2b(k'':key)) = dec'(k, mk, e') in
	return().

process 
	Ostart() :=
	k <-R key;
	mk <-R mkey;
	return;
	(run QA(k,mk) | run QB(k,mk))