require import AllCore Int Real List Distr.
require import DList.
require (*..*) WeakPRP MACs RCPA_CMA CBC RCPA_pad.

(** Assume a permutation (P,Pinv) on block indexed by eK **)
type eK, block.

op d_eK: eK distr.

axiom d_eK_uffu: is_lossless d_eK /\ is_funiform d_eK.

op d_block: block distr.
axiom d_block_uffu: is_lossless d_block /\ is_funiform d_block.

op P : eK -> block -> block.
op Pi: eK -> block -> block.

axiom bijectiveP k:
     support d_eK k
  =>    cancel (P k) (Pi k)
     /\ cancel (Pi k) (P k).

(* Import definitions to consider (P,Pinv) as a weak PRP *)
clone import WeakPRP as PRPt with
  type K    <- eK,
  type D    <- block,
  op   dK   <- d_eK
proof * by smt (d_eK_uffu).

clone import ConcretePRP as PRPc with
  type K    <- eK,
  type D    <- block,
  op   dK   <- d_eK,
  op   P    <- P,
  op   Pi   <- Pi
proof * by smt (d_eK_uffu bijectiveP).

clone import IdealPRP as PRPi with
  type K    <- eK,
  type D    <- block,
  op   dK   <- d_eK,
  op   dD   <- d_block
rename "RandomPermutation" as "PRPi"
proof * by smt (d_eK_uffu d_block_uffu).

(** Assume a zmodule structure on block (for generality... we will instantiate it with {0,1}^k later on) *)
op zeros: block.
op (+): block -> block -> block.

axiom add0b (x : block)    : zeros + x = x.
axiom addbA (y x z : block): x + (y + z) = (x + y) + z.
axiom addbC (x y : block)  : x + y = y + x.
axiom addbK (x : block)    : x + x = zeros.

clone Ring.ZModule as Block with
  type t               <- block,
  op   zeror           <- zeros,
  op   (+)             <- (+),
  op   [-] (x : block) <- x
proof * by smt (add0b addbA addbC addbK).

(** Assume a (deterministic) MAC (mac,verify) with key in mK, message in msg and tag in tag **)
type mK, msg, tag.

op d_mK: mK distr.
axiom d_mK_uffu: is_lossless d_mK /\ is_funiform d_mK.

op mac: mK -> msg -> tag.

(* Import definitions to consider (mac,(fun k x t => mac k x = t)) a WUF-CMA MAC *)
clone import MACs as MACa with
  type mK  <- mK,
  type msg <- msg,
  type tag <- tag
proof * by smt ().
import WUF_CMA.

module MAC: MAC_Scheme = {
  proc keygen(): mK = {
    var k;

    k <$ d_mK;
    return k;
  }

  proc tag(k:mK,m:msg): tag = {
    return mac k m;
  }

  proc verify(k:mK,m:msg,t:tag): bool = {
    return mac k m = t;
  }
}.

(** Assume a well-formed padding function from msg to block list **)
(* morally, if "ptxt = octetstrings" and "block = fixed length octetstrings", "pad = extend and chunk" *)
op pad  : msg * tag -> block list.
op unpad: block list -> (msg * tag) option.

axiom can_unpad mt: unpad (pad mt) = Some mt.

axiom pad_tag m t0 t1: size (pad (m,t0)) = size (pad (m,t1)).

op leak: msg -> msg.
axiom leak_pad m t: size (pad (m,t)) = size (pad ((leak m),t)).

(** And construct MAC-then-Encode-then-Encrypt as a SKE scheme **)
op q: { int | 0 < q } as gt0_q. (* Number of queries to the lr oracle *)
op n: { int | 1 < n } as gt1_n. (* Max length of queries to the lr oracle (in blocks) *)

op valid_msg: msg -> bool.
axiom max_pad_n m t: valid_msg m => size (pad (m,t)) < n.

(* Import definitions to allow early type-checking *)
clone import SKE_INDR as SKEa with
  type eK              <- (eK * mK),
  type ptxt            <- msg,
  type ctxt            <- block list,
  type leaks           <- int,
  op   leak  (m : msg) <- size (pad (m,witness<:tag>)),
  op   dC    (l : int) <- dlist d_block (l + 1)
proof * by smt (dlist_ll d_block_uffu).
import RCPA PTXT.

module MEE(P:PRP,M:MAC_Scheme): Enc_Scheme = {
  proc keygen(): eK * mK = {
    var ek, mk;

    ek <@ P.keygen();
    mk <@ M.keygen();
    return (ek,mk);
  }

  proc enc(key:eK * mK,p:msg): block list = {
    var ek, mk;
    var t, p', s, i, pi, c;

    (ek,mk) <- key;
    (* compute tag *)
    t       <@ M.tag(mk,p);
    (* pad (produce block list from plain and tag) *)
    p'      <- pad (p,t);
    (* compute CBC$ encryption *)
    s       <$ d_block;
    c       <- [s];
    i       <- 0;
    while (i < size p') {
      pi <- nth witness p' i;
      s  <@ P.f(ek,s + pi);
      c  <- c ++ [s];
      i  <- i + 1;
    }
    return c;
  }

  proc dec(key:eK * mK,c:block list): msg option = {
    var ek, mk;
    var t, s, i, ci, pi, padded, pt, p', b;
    var p <- None;

    (ek,mk) <- key;
    (* compute CBC decryption (first block is iv) *)
    s       <- head witness c;
    c       <- behead c;
    padded  <- [];
    i       <- 0;
    while (i < size c) {
      ci     <- nth witness c i;
      pi     <@ P.fi(ek,ci);
      padded <- padded ++ [s + pi];
      s      <- ci;
      i      <- i + 1;
    }
    (* strip padding *)
    pt      <- unpad padded;
    (* check MAC *)
    if (pt <> None) {
      (p',t) <- oget pt;
      b      <@ M.verify(mk,p',t);
      p      <- b ? Some p' : None;
    }
    return p;
  }
}.

module RCPA_QueryBounder (A : RCPA_Adversary, O : RCPA_Oracles) = {
  var qC : int

  module O' = {
    proc enc(p:msg): block list = {
      var i;
      var c <- witness;

      if (qC < q /\ size (pad (p,witness)) <= n) {
        c  <@ O.enc(p);
        qC <- qC + 1;
      } else {
        c <- [];
        i <- 0;
        while (i <= size (pad (p,witness))) {
          c <- c ++ [witness];
          i <- i + 1;
        }
      }
      return c;
    }
  }

  proc distinguish(): bool = {
    var b;

    qC <- 0;
    b  <@ A(O').distinguish();
    return b;
  }
}.

(* From the MAC and a CPA adversary against MtE, we construct an adversary against the PRP *)
module Weak_PRPa (M : MAC_Scheme, A : RCPA_Adversary, P : WeakPRP_Oracles) = {
  var qC: int
  var mk: mK

  module O = {
    proc enc(p:msg): block list = {
      var i, s, t, padded, pi;
      var c <- witness;

      if (qC < q /\ size (pad (p,witness)) <= n) {
        t = M.tag(mk,p);
        padded = pad(p,t);
        s <$ d_block;
        c <- [s];
        i <- 0;
        while (i < size padded) {
          pi <- nth witness padded i;
          s  <@ P.f(s + pi);
          c  <- c ++ [s];
          i  <- i + 1;
        }
        qC <- qC + 1;
      } else {
        c <- [];
        i <- 0;
        while (i <= size (pad (p,witness))) {
          c <- c ++ [witness];
          i <- i + 1;
        }
      }
      return c;
    }
  }

  proc distinguish(): bool = {
    var b;

    qC <- 0;
    mk <@ M.keygen();
    b  <@ A(O).distinguish();
    return b;
  }
}.

section RCPA.
  declare module A : RCPA_Adversary { PRPi, WeakPRP_Wrap, RCPA_Wrap, RCPA_QueryBounder, Weak_PRPa }.
  axiom A_distinguish_ll (O <: RCPA_Oracles { A }):
    islossless O.enc => islossless A(O).distinguish.

  local clone import CBC as CBCa with
    op   q       <- q,
    op   ell     <- n,
    type key     <- eK,
    op   dKey    <- d_eK,
    type block   <- block,
    op   dBlock  <- d_block,
    op   zeros   <- zeros,
    op   (+)     <- (+),
    op   P       <- P,
    op   Pi      <- Pi
  proof *.
  realize gt0_q       by exact/gt0_q.
  realize gt0_ell     by smt (gt1_n).
  realize dKey_uffu   by smt(@Distr d_eK_uffu).
  realize dBlock_uffu by smt(@Distr d_block_uffu).
  realize add0b       by exact/add0b.
  realize addbA       by exact/addbA.
  realize addbC       by exact/addbC.
  realize addbK       by exact/addbK.
  realize bijective_P. by move=> k; apply/bijectiveP; smt(@Distr d_eK_uffu). qed.

  (** We really want to clone only MtE, but since RCPA_CPA is
      abstract, its inner theories don't exist until cloned...
      Unintended side-effect or intended behaviour? **)
  local clone RCPA_CMA as CPA_CMA with
    type MtE.mK              <- mK,
    type MtE.eK              <- eK,
    type MtE.ptxt            <- msg,
    type MtE.ctxt            <- block list,
    type MtE.tag             <- tag,
    type MtE.leaks           <- msg,
    op   MtE.leak  (m : msg) <- leak m,
    op   MtE.dC    (m : msg) <- CBCa.dBlocks (size (pad (m,witness<:tag>)) + 1)
  proof MtE.* by smt (dlist_ll d_block_uffu).
  import CPA_CMA.MtE.

  local clone import RCPA_pad as PtE with
    type key                     <- eK,
    type ptxt                    <- block list,
    type ctxt                    <- block list,
    type msg                     <- msg * tag,
    type leaks_m                 <- msg,
    type leaks_p                 <- int,
    op   leak_m (mt : msg * tag) <- leak mt.`1,
    op   leak_p                  <- size<:block>,
    op   pad                     <- pad,
    op   unpad                   <- unpad,
    op   dC_m          (m : msg) <- CBCa.dBlocks (size (pad (m,witness<:tag>)) + 1),
    op   dC_p          (l : int) <- CBCa.dBlocks (l + 1)
  proof * by smt (dlist_ll d_block_uffu can_unpad leak_pad pad_tag).

  local lemma MEE_unfold &m:
    Pr[INDR_CPA(MEE(PRPr,MAC),RCPA_QueryBounder(A)).main() @ &m: res]
    = Pr[INDR_CPA(MacThenEncrypt(PadThenEncrypt(IV_Wrap(CBC(PRPr))),MAC),RCPA_QueryBounder(A)).main () @ &m: res].
  proof.
    byequiv (_: ={glob A} ==> ={res})=> //=; proc; inline *.
    wp; call (_: ={glob RCPA_QueryBounder, glob RCPA_Wrap})=> //=.
      proc; inline*; sp; if=> //=; sim.
      by auto.
    by auto.
  qed.

  (** We bound the RCPA advantage of A against MEE(P,M) **)
  local lemma MtE_security &m:
    `|Pr[INDR_CPA(MacThenEncrypt(PadThenEncrypt(IV_Wrap(CBC(PRPr))),MAC),RCPA_QueryBounder(A)).main() @ &m: res]
      - Pr[INDR_CPA(Ideal,RCPA_QueryBounder(A)).main() @ &m: res]|
    = `|Pr[SKEa.RCPA.INDR_CPA(PadThenEncrypt(IV_Wrap(CBC(PRPr))),RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A))).main() @ &m: res]
        - Pr[SKEa.RCPA.INDR_CPA(SKEa.RCPA.Ideal,RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A))).main() @ &m: res]|.
  proof.
    (* Unfortunately, we have several copies of the modules and
       alpha conversion does not work at module level, so we need
       to prove that it implies semantic equality. This is easy. *)
    rewrite -(RCPA_WUF_RCPA.RCPA_preservation (<: PadThenEncrypt(IV_Wrap(CBC(PRPr)))) MAC (<: RCPA_QueryBounder(A)) &m _ _).
      by proc; rnd predT; auto=> />; smt (d_mK_uffu).
      by proc.
    do !congr.
      by byequiv=> //=; sim.
    byequiv=> //=. proc; inline *; wp; call (_: ={glob RCPA_QueryBounder}).
      proc; inline *; sp; if=> //=; auto; [smt (leak_pad pad_tag)|sim].
    by auto.
  qed.

  local lemma PtE_security &m:
    `|Pr[SKEa.RCPA.INDR_CPA(PadThenEncrypt(IV_Wrap(CBC(PRPr))),RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A))).main() @ &m: res] - Pr[SKEa.RCPA.INDR_CPA(SKEa.RCPA.Ideal,RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A))).main() @ &m: res]|
    = `|Pr[CoreDefs.RCPA.INDR_CPA(IV_Wrap(CBC(PRPr)),RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A)))).main() @ &m: res] - Pr[CoreDefs.RCPA.INDR_CPA(CoreDefs.RCPA.Ideal,RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A)))).main() @ &m: res]|.
  proof.
    (* The same issue arises here *)
    rewrite -(RCPA_preservation (<: IV_Wrap(CBC(PRPr))) (<: RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A))) &m).
    do !congr.
      by byequiv=> //=; sim.
    byequiv=> //=; proc; inline *.
    wp; call (_: ={glob RCPA_QueryBounder, glob RCPA_WUF_RCPA.RCPAa}).
      by proc; inline *; sp; if=> //=; sim.
    by auto.
  qed.

  local lemma CBC_security &m:
    `|Pr[CoreDefs.RCPA.INDR_CPA(IV_Wrap(CBC(PRPr)),RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A)))).main () @ &m: res]
      - Pr[CoreDefs.RCPA.INDR_CPA(CoreDefs.RCPA.Ideal,RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A)))).main () @ &m: res]|
    = `|Pr[CBCa.SKEa.RCPA.INDR_CPA(IV_Wrap(CBC(PRPr)),QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A)))).main() @ &m: res]
              - Pr[CBCa.SKEa.RCPA.INDR_CPA(CBCa.SKEa.RCPA.Ideal,QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A)))).main() @ &m: res]|.
  proof.
    (* We have the same issue PLUS we need to move the QueryBounder around.
       A much better way of doing this would be to make sure that each library
       defines its own QueryCounter and QueryBounder and to make sure that
       abstract security results come in both bounded and unbounded (when
       possible) flavours. This is TODO when we rework the crypto libraries    *)
    have PushQueryBounder: forall (O <: CBCa.SKEa.RCPA.RCPA_Oracles { A, RCPA_QueryBounder, OracleBounder, RCPA_WUF_RCPA.RCPAa }),
      equiv [QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A)),O).distinguish
             ~ RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A)),O).distinguish
             : ={arg, glob A, glob O} ==> ={res}].
        move=> O; proc; inline *.
        wp; call (_:    ={glob O, glob RCPA_WUF_RCPA.RCPAa}
                     /\ ={qC}(OracleBounder,RCPA_QueryBounder)).
          proc; inline *.
          case ((RCPA_QueryBounder.qC < q /\ size (pad (p,witness)) <= n){2}).
            rcondt{2} 2; 1:by auto.
            rcondt{1} 8; 1:by auto; smt (pad_tag).
            wp; call (_: true).
            by auto.
          rcondf{2} 2; 1:by auto.
          rcondf{1} 8; 1:by auto; smt (pad_tag).
          wp; while (   ={i, p}
                     /\ r{1} = c{2}
                     /\ p0{1} = pad (p,t){1}).
            by auto; smt (pad_tag).
          by auto; smt (max_pad_n pad_tag).
        by auto.
      have ->: Pr[CBCa.SKEa.RCPA.INDR_CPA(IV_Wrap(CBC(PRPr)),QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A)))).main() @ &m: res]
               = Pr[CBCa.SKEa.RCPA.INDR_CPA(IV_Wrap(CBC(PRPr)),RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A)))).main() @ &m: res].
        byequiv=> //=; proc.
        call (PushQueryBounder (CBCa.SKEa.RCPA.RCPA_Wrap(IV_Wrap(CBC(PRPr))))).
        by call (_: true); auto.
      have ->: Pr[CBCa.SKEa.RCPA.INDR_CPA(CBCa.SKEa.RCPA.Ideal,QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A)))).main() @ &m: res]
               = Pr[CBCa.SKEa.RCPA.INDR_CPA(CBCa.SKEa.RCPA.Ideal,RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A)))).main() @ &m: res].
        byequiv=> //=; proc.
        call (PushQueryBounder (CBCa.SKEa.RCPA.RCPA_Wrap(CBCa.SKEa.RCPA.Ideal))).
        by call (_: true); auto.
    do !congr.
      by byequiv=> //=; sim.
    byequiv=> //=; proc.
    inline *; wp.
    call (_:    ={glob RCPA_QueryBounder, glob RCPA_WUF_RCPA.RCPAa}
             /\ ={k}(CoreDefs.RCPA.RCPA_Wrap,CBCa.SKEa.RCPA.RCPA_Wrap)).
      by proc; inline *; sp; if=> //=; sim.
    by auto.
  qed.

  local lemma local_conclusion &m:
    `|Pr[INDR_CPA(MacThenEncrypt(PadThenEncrypt(IV_Wrap(CBC(PRPr))),MAC),RCPA_QueryBounder(A)).main () @ &m: res]
      - Pr[INDR_CPA(Ideal,RCPA_QueryBounder(A)).main() @ &m: res]|
    <= `|Pr[WeakPRP_IND(WeakPRP_Wrap(PRPr), PRPF_Adv(QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A))))).main() @ &m : res]
         - Pr[WeakPRP_IND(PRPi, PRPF_Adv(QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A))))).main() @ &m : res]|
       + 2%r * ((q * n) ^ 2)%r * mu d_block (pred1 witness).
  proof.
    have := Conclusion (<: RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A))) &m _.
      move=> O O_enc_ll.
      proc; inline *.
      wp; call (_: true); 1:exact/A_distinguish_ll.
        by proc; inline *; wp; call O_enc_ll; auto.
      by wp; rnd predT; auto; smt (d_mK_uffu).
    rewrite (MtE_security &m) (PtE_security &m) (CBC_security &m).
    (* Here again, we have to tell EasyCrypt that alpha equality implies semantic equality *)
    have ->: Pr[PRPt.WeakPRP_IND(PRPt.WeakPRP_Wrap(PRPr.PRPr), PRPF_Adv(QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A))))).main() @ &m: res]
             = Pr[WeakPRP_IND(WeakPRP_Wrap(PRPr),PRPF_Adv(QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A))))).main() @ &m: res].
      by byequiv=> //=; sim.
    have ->: Pr[PRPt.WeakPRP_IND(PRPi.PRPi, PRPF_Adv(QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A))))).main() @ &m: res]
             = Pr[WeakPRP_IND(PRPi,PRPF_Adv(QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A))))).main() @ &m: res].
      by byequiv=> //=; sim.
    have ->: Pr[CBCa.SKEa.RCPA.INDR_CPA(IV_Wrap(CBC(PRPr.PRPr)),QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A)))).main() @ &m: res]
             = Pr[CBCa.SKEa.RCPA.INDR_CPA(IV_Wrap(CBC(PRPr)),QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A)))).main() @ &m: res].
      by byequiv=> //=; sim.
    have ->: Pr[CBCa.SKEa.RCPA.INDR_CPA(Random,QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A)))).main() @ &m: res]
             = Pr[CBCa.SKEa.RCPA.INDR_CPA(Random,QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A)))).main() @ &m: res].
      by byequiv=> //=; sim.
    (* And we conclude by proving the equivalence of the Random module and the Ideal module used in IND$-CPA *)
    have ->: Pr[CBCa.SKEa.RCPA.INDR_CPA(Random,QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A)))).main() @ &m: res]
             = Pr[CBCa.SKEa.RCPA.INDR_CPA(CBCa.SKEa.RCPA.Ideal,QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A)))).main() @ &m: res].
      byequiv=> //=; proc; inline *; wp.
      call (_: ={glob OracleBounder, glob RCPA_WUF_RCPA.RCPAa}).
        proc.
        call (_: ={glob OracleBounder}).
          call (_: ={glob OracleBounder}).
            sp; if=> //=; 2:by sim.
            wp; call (_: true)=> //=.
            by call Random_Ideal=> //=.
          by auto.
        by call (_: true); auto.
      by auto.
    done.
  qed.

  local lemma CleanupAdversary (P <: WeakPRP { A, Weak_PRPa, OracleBounder, RCPA_WUF_RCPA.RCPAa }) &m:
    Pr[WeakPRP_IND(P,Weak_PRPa(MAC,A)).main() @ &m: res]
    = Pr[WeakPRP_IND(P, PRPF_Adv(QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A))))).main() @ &m : res].
  proof.
    byequiv (_: ={glob P, glob A} ==> ={res})=> //=; proc; inline *; wp.
    call (_:    ={glob P}
             /\ ={qC}(Weak_PRPa,OracleBounder)
             /\ Weak_PRPa.mk{1} = RCPA_WUF_RCPA.RCPAa.mk{2})=> //=.
      proc; inline *; sp.
      if; 1:smt (max_pad_n pad_tag).
      + by sim; auto.
      wp; while (   ={i}
                 /\ size (pad (p,witness)){1} = size p0{2}
                 /\ c{1} = r{2});
        1:by auto=> /#.
      by auto; smt (pad_tag).
    by auto; call (_: true).
  qed.

  lemma RCPA_security &m:
    `|Pr[INDR_CPA(MEE(PRPr,MAC),RCPA_QueryBounder(A)).main() @ &m: res]
      - Pr[INDR_CPA(Ideal,RCPA_QueryBounder(A)).main() @ &m: res]|
    <= `|Pr[WeakPRP_IND(WeakPRP_Wrap(PRPr), Weak_PRPa(MAC,A)).main() @ &m : res]
         - Pr[WeakPRP_IND(PRPi, Weak_PRPa(MAC,A)).main() @ &m: res]|
       + 2%r * ((q * n) ^ 2)%r * mu d_block (pred1 witness).
  proof.
    rewrite (MEE_unfold &m) (CleanupAdversary (<: WeakPRP_Wrap(PRPr)) &m) (CleanupAdversary PRPi &m).
    exact/(local_conclusion &m).
  qed.
end section RCPA.

(* From the PRP and a PTXT adversary against MtE, we construct a WUF-CMA adversary against the MAC *)
module CMAa (P : PRP, A : PTXT_Adversary, M : CMA_Oracles) = {
  var ek: eK

  module O = {
    proc enc(m:msg): block list = {
      var i, s, t, padded, pi;
      var c <- witness;

      t <@ M.tag(m);
      padded = pad(m,t);
      s <$ d_block;
      c <- [s];
      i <- 0;
      while (i < size padded) {
        pi <- nth witness padded i;
        s  <@ P.f(ek,s + pi);
        c  <- c ++ [s];
        i  <- i + 1;
      }
      return c;
    }

    proc verify(c:block list): bool = {
      var pt, pi, padded, b, s, i, ci;

      b <- false;
      (* compute CBC decryption (first block is iv) *)
      s       <- head witness c;
      c       <- behead c;
      padded  <- [];
      i       <- 0;
      while (i < size c) {
        ci     <- nth witness c i;
        pi     <@ P.fi(ek,ci);
        padded <- padded ++ [s + pi];
        s      <- ci;
        i      <- i + 1;
      }
      (* strip padding *)
      pt      <- unpad padded;
      (* check MAC *)
      if (pt <> None) {
        b     <@ M.verify(oget pt);
      }
      return b;
    }
  }

  proc forge(): unit = {
    ek <@ P.keygen();
          A(O).forge();
  }
}.

section PTXT.
  declare module A : PTXT_Adversary { WUF_Wrap, PTXT_Wrap, CMAa }.
  axiom A_forge_ll (O <: PTXT_Oracles { A }):
    islossless O.enc => islossless O.verify => islossless A(O).forge.

  (** TODO: this is not useful apart from avoiding having to define
      the part of the scheme that we don't care about **)
  local clone import CBC as CBCb (* FIXME *) with
    op   q       <- q,
    op   ell     <- n,
    type key     <- eK,
    op   dKey    <- d_eK,
    type block   <- block,
    op   dBlock  <- d_block,
    op   zeros   <- zeros,
    op   (+)     <- (+),
    op   P       <- P,
    op   Pi      <- Pi
  proof *.
  realize gt0_q       by exact/gt0_q.
  realize gt0_ell     by smt (gt1_n).
  realize dKey_uffu   by smt(@Distr d_eK_uffu).
  realize dBlock_uffu by smt(@Distr d_block_uffu).
  realize add0b       by exact/add0b.
  realize addbA       by exact/addbA.
  realize addbC       by exact/addbC.
  realize addbK       by exact/addbK.
  realize bijective_P. by move=> k; apply/bijectiveP; smt(@Distr d_eK_uffu). qed.

  (** TODO: ditto **)
  local clone import RCPA_pad as PtEb (* FIXME *) with
    type key                     <- eK,
    type ptxt                    <- block list,
    type ctxt                    <- block list,
    type msg                     <- msg * tag,
    type leaks_m                 <- msg,
    type leaks_p                 <- int,
    op   leak_m (mt : msg * tag) <- leak mt.`1,
    op   leak_p                  <- size<:block>,
    op   pad                     <- pad,
    op   unpad                   <- unpad,
    op   dC_m          (m : msg) <- CBCa.dBlocks (size (pad (m,witness<:tag>)) + 1),
    op   dC_p          (l : int) <- CBCa.dBlocks (l + 1)
  proof * by smt (dlist_ll d_block_uffu can_unpad leak_pad pad_tag).

  (** See comment in CPA proof **)
  local clone import RCPA_CMA as MtEb (* FIXME *) with
    type MtE.mK              <- mK,
    type MtE.eK              <- eK,
    type MtE.ptxt            <- msg,
    type MtE.ctxt            <- block list,
    type MtE.tag             <- tag,
    type MtE.leaks           <- msg,
    op   MtE.leak  (m : msg) <- leak m,
    op   MtE.dC    (m : msg) <- CBCa.dBlocks (size (pad (m,witness<:tag>)) + 1)
  proof MtE.* by smt (dlist_ll d_block_uffu).
  import MtEb.MtE.

  local lemma MEE_unfold &m:
    Pr[INT_PTXT(MEE(PRPr,MAC),A).main() @ &m: res]
    = Pr[INT_PTXT(MacThenEncrypt(PadThenEncrypt(IV_Wrap(CBC(PRPr))),MAC),A).main () @ &m: res].
  proof.
    byequiv (_: ={glob A} ==> ={res})=> //=; proc; inline *.
    wp; call (_: ={glob PTXT_Wrap})=> //=.
      by proc; inline *; sim; auto.
      proc; inline *; sim.
      by wp=> //=; sim.
    by auto.
  qed.

  (** We bound the PTXT advantage of A against MEE(P,M) **)
  local lemma local_conclusion &m:
    Pr[INT_PTXT(MacThenEncrypt(PadThenEncrypt(IV_Wrap(CBC(PRPr))),MAC),A).main () @ &m: res]
    <= Pr[MACa.WUF_CMA.WUF_CMA(MAC,RCPA_WUF_PTXT.CMAa(PadThenEncrypt(IV_Wrap(CBC(PRPr))),A)).main() @ &m: res].
  proof.
    have ->: Pr[INT_PTXT(MacThenEncrypt(PadThenEncrypt(IV_Wrap(CBC(PRPr))),MAC),A).main() @ &m: res]
             = Pr[Sec.PTXT.INT_PTXT(MacThenEncrypt(PadThenEncrypt(IV_Wrap(CBC(PRPr))),MAC),A).main() @ &m: res].
      by byequiv=> //=; proc; inline *; sim.
    apply/(RCPA_WUF_PTXT.PTXT_security (<: PadThenEncrypt(IV_Wrap(CBC(PRPr)))) MAC A _ _ _ _ _ _ _ &m).
      by proc; wp; rnd predT; auto; smt (d_eK_uffu).
      proc; inline *; wp; while (0 <= i <= size p0) (size p0 - i).
        by move=> z; auto=> /#.
      by wp; rnd predT; auto; smt (d_block_uffu size_ge0).
      proc; inline *; wp; while (0 <= i <= size c1) (size c1 - i).
        by move=> z; auto=> /#.
      by auto; smt (size_ge0).
      by proc; rnd predT; skip; smt (d_mK_uffu).
      by proc.
      by proc.
      by move=> O O_enc_ll O_verify_ll; apply (A_forge_ll O). (* types are different but the same *)
  qed.

  local lemma CleanupAdversary &m:
    Pr[MACa.WUF_CMA.WUF_CMA(MAC,RCPA_WUF_PTXT.CMAa(PadThenEncrypt(IV_Wrap(CBC(PRPr))),A)).main() @ &m: res]
    = Pr[WUF_CMA(MAC,CMAa(PRPr,A)).main() @ &m: res].
  proof.
    byequiv=> //=; proc; inline *; wp.
    call (_:    ={ek}(RCPA_WUF_PTXT.CMAa,CMAa)
             /\ ={s,k,win}(MACa.WUF_CMA.WUF_Wrap,WUF_Wrap)).
      by proc; inline *; wp;
         while (   ={i, s}
                /\ c2{1} = c{2}
                /\ p1{1} = padded{2}
                /\ key0{1} = CMAa.ek{2});
         auto.
      by proc; inline *; wp;
         while (   ={i, s}
                /\ c2{1} = c{2}
                /\ p2{1} = padded{2}
                /\ key0{1} = CMAa.ek{2});
         auto.
    by auto.
  qed.

  lemma PTXT_security &m:
    Pr[INT_PTXT(MEE(PRPr,MAC),A).main () @ &m: res]
    <= Pr[WUF_CMA(MAC,CMAa(PRPr,A)).main() @ &m: res].
  proof.
    rewrite (MEE_unfold &m) -(CleanupAdversary &m).
    exact/(local_conclusion &m).
  qed.
end section PTXT.