(* Question 2: Encrypt-then-MAC is IND-CCA2 *)

param N, Nd.

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_proba_mac(mkey, bitstring, macs, mac, verify, Pmac).

(* Queries *)

query secret b.

channel start, c1, lr, c_dec.

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 LRenc(k: key, mk:mkey, b0: bool) =
       ! N
       in(lr, (m0: bitstring, m1: bitstring));
       if Z(m0) = Z(m1) then
       let ciphertext': bitstring = 
              enc'(k,mk, if b0 then m0 else m1)
       in
       out(lr, ciphertext').


let Odec(k: key, mk: mkey) =
       ! Nd
       in(c_dec, ciphertext: bitstring);
       find j <= N suchthat defined(ciphertext'[j]) && ciphertext'[j] = ciphertext then
           yield
       else
           out(c_dec, dec'(k, mk, ciphertext)).


process 
	in(start, ());
	new b: bool;
	new k: key;
	new mk: mkey;
	out(c1, ());
	LRenc(k,mk,b) | Odec(k,mk)