(* Encrypt-and-MAC is IND-CPA *)
param qEnc.

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

(* Shared-key encryption (CPA Stream cipher) *)
proba Penc.
expand IND_CPA_sym_enc(key, bitstring, bitstring, enc, dec, injbot, Z, Penc).

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

fun concat(bitstring, macs): bitstring [data].

letfun full_enc(m: bitstring, k: key, mk: mkey) =
  enc(m, k).

(* Queries *)
query secret b.

let QencLR(b0: bool, k: key, mk: mkey) = 
    	foreach i <= qEnc do
	Oenc (m0: bitstring, m1: bitstring) :=
	if Z(m0) = Z(m1) then (* m0 and m1 have the same length *)
	mb <- if b0 then m0 else m1;
	return(full_enc(mb, k, mk)).

process 
	Ostart() :=
	b <-R bool;
	k <-R key;
	mk <-R mkey;
	return;
	run QencLR(b, k, mk)