(* Encrypt-then-MAC is IND-CCA2 *)
param qEnc.
param qDec.

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) =
  c <- enc(m, k);  
  concat(c, mac(c, mk)).

letfun full_dec(c: bitstring, k: key, mk: mkey) = 
  let concat(c1, mac1) = c in
  (
    if verify(c1, mk, mac1) then
      dec(c1, k)
    else 
      bottom
  )
  else
    bottom.

table ciphertexts(bitstring).

(* Queries *)
query secret b.

let QencLR(b0: bool, k: key, mk: mkey) = 
    	foreach ienc <= 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;
        cb <- full_enc(mb, k, mk);
        insert ciphertexts(cb);
	return(cb).

let Qdec(k: key, mk: mkey) =
  foreach idec <= qDec do
  Odec (c: bitstring) :=
  get ciphertexts(=c) in return(bottom) else
  return(???).

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