require import AllCore List Distr DBool DInterval.
require (*--*) IND_CCA2_hybrid IND_CCA2 LibExt.
import LibExt.RMap.

import Distr.MRat.

(* This file provides games for the Real/Ideal variant of
IND-CCA2. The Real game provides the adversary with access to an
encryption oracle, in the Ideal game the encryption oracle always
encrypts the same (fixed) message.

Unlike Oracle_PKE, we do not work with an abstract [Scheme]
module. Instead, we require distributions [dkeyseed, dencseed] and
operators that allow implementing a [Scheme] module *)

(* FIXME: We use an inner theory to avoid the name-clash with the Real theory. *)
theory CCA.

type pkey, skey, plaintext, ciphertext, encseed, keyseed.

op [lossless] dkeyseed : keyseed distr.
op [lossless] dencseed : encseed distr.


op Ndec : int.
op Nenc : { int | 0 < Nenc } as Nenc_gt0.

op enc   : plaintext * pkey * encseed -> ciphertext.
op dec   : ciphertext * skey -> plaintext option.
op pkgen : keyseed -> pkey.
op skgen : keyseed -> skey.
op m0    : plaintext.

axiom encK (k : keyseed) (m : plaintext) (e : encseed) :
  dec (enc(m, pkgen k, e), skgen k) = Some m.

op Gen = dmap dkeyseed (fun ks => (pkgen ks, skgen ks)).
op Enc = fun (x : pkey * plaintext) => dmap dencseed (fun es => enc(x.`2,x.`1,es)).
op Dec = fun (x : skey * ciphertext) => dec(x.`2, x.`1).

clone import IND_CCA2_hybrid as PKE with
  type pkey       <- pkey,
  type skey       <- skey,
  type plaintext  <- plaintext,
  type ciphertext <- ciphertext,
  op Gen          <- Gen,
  op Enc          <- Enc,
  op Dec          <- Dec
proof*.
realize Gen_ll by apply/dmap_ll/dkeyseed_ll.
realize Enc_ll by move =>*; apply/dmap_ll/dencseed_ll.
realize kg_ll by islossless.
realize enc_ll by islossless.
realize dec_ll by islossless.

clone import IND_CCA2 as C with
  op Ndec        <- Ndec,
  op Nenc        <- Nenc,
  axiom Nenc_gt0 <- Nenc_gt0
  proof*.

module type Oracle = {
  proc pk ()                 : pkey
  proc enc (_ : plaintext)   : ciphertext
  proc dec (_ : ciphertext)  : plaintext option
}.

module type Oracle_i = {
  include Oracle
  proc init() : unit
}.

(* "Real" oracle, enc encrypts the given message *)
module Real : Oracle = {
  var pk : pkey
  var sk : skey

  proc init() : unit = {
    var ks;

    ks <$ dkeyseed;
    pk <- pkgen ks;
    sk <- skgen ks;
  }

  proc pk () = { return pk; }

  proc enc (m : plaintext) : ciphertext = {
    var e;

    e <$ dencseed;
    return enc(m, pk, e);
  }

  proc dec (c : ciphertext) : plaintext option = {
    return dec(c, sk);
  }
}.

(* Ideal orcale, discards m and always encrypts m0

In the case of a ciphertext collision (e.g. a collision in dencseed),
the last given message is returned *)

module Ideal : Oracle = {
  include var Real[pk]
  var cs : (ciphertext, plaintext) rmap

  proc init() : unit = {
    Real.init();
    cs <- [];
  }

  proc enc (m : plaintext) : ciphertext = {
    var e, c;

    e  <$ dencseed;
    c  <- enc(m0, pk, e);
    cs <- cs.[c <- m];
    return c;
  }

  proc dec (c : ciphertext) : plaintext option = {
    var m;

    m <- assoc cs c;
    if (m = None) {
      m <- dec(c, sk);
    }
    return m;
  }
}.

(* Same as above, but in the case of a ciphertext collision, the
message returned by decryption is chosen randomly. *)

module IdealS : Oracle = {
  import var Real
  include var Ideal [-dec]

  proc dec (c : ciphertext) : plaintext option = {
    var m;

    if (c \in cs) {
      m <$ cs.[c];
    } else {
      m <- dec(c, sk);
    }
    return m;
  }
}.

module type Adversary (G : Oracle) = {
  proc main () : bool
}.

module Game (O : Oracle_i, A : Adversary) = {

  proc main() = {
    var r;

    O.init();
    r <@ A(O).main();
    return r;
  }
}.

(*-------------------------------*)

module CountICCA (O : Oracle) = {
  import var C.CountCCA
  (* var ndec, nenc : int *)

  proc init () : unit = {
    ndec <- 0;
    nenc <- 0;
  }

  proc pk = O.pk

  proc enc (m : plaintext) : ciphertext = {
    var c;

    c    <@ O.enc(m);
    nenc <- nenc + 1;
    return c;
  }

  proc dec (c : ciphertext) : plaintext option = {
    var m;

    m    <@ O.dec(c);
    ndec <- ndec + 1;
    return m;
  }
}.

module CountAdv (A : Adversary) (O : Oracle) = {
  proc main() = {
    var b;

    CountICCA(O).init();
    b <@ A(CountICCA(O)).main();
    return b;
  }
}.

(* Adversary for the bound |Real - Ideal| < |CCA_L - CCA_R| *)
(* We need to keep a log, because the CCA_Oracle will only decrypt
ciphertexts that were not generated by the l_or_r oracle *)
module B (A : Adversary) (O : CCA_Oracle) = {
  var cs : (ciphertext * plaintext) list
  var pk : pkey

  module O' : Oracle = {

    proc init (p : pkey) = { pk <- p; }

    proc pk () = { return pk; }

    proc enc (m : plaintext) = {
      var c;

      c  <@ O.l_or_r(m, m0);
      cs <- (c, m) :: cs;
      return c;
    }

    proc dec (c : ciphertext) = {
      var m;

      m <- assoc cs c;
      if (m = None) {
        m <@ O.dec(c);
      }
      return m;
    }
  }

  proc main (pk : pkey) : bool = {
    var r;

    cs <- [];
    O'.init(pk);
    r  <@ A(O').main();
    return r;
  }
}.

(* Adversary for the bound |Real - IdealS| < |CCA_L - CCA_R| *)
module BS (A : Adversary) (O : CCA_Oracle) = {
  import var B

  module O' : Oracle = {

    proc init (p : pkey) = { pk <- p; }

    proc pk () = { return pk; }

    proc enc (m : plaintext) = {
      var c;

      c  <@ O.l_or_r(m, m0);
      cs <- (c, m) :: cs;
     return c;
    }

    proc dec (c : ciphertext) : plaintext option = {
      var m;

      if (c \in cs) {
        m <$ cs.[c];
      } else {
        m <@ O.dec(c);
      }
      return m;
    }
  }

  proc main (pk : pkey) : bool = {
    var r;

    cs <- [];
    O'.init(pk);
    r  <@ A(O').main();
    return r;
  }
}.

(* more natural formulation of the scheme using seed operators *)
module S : Scheme = {
  proc kg () : pkey * skey = {
    var ks, pk, sk;

    ks <$ dkeyseed;
    pk <- pkgen ks;
    sk <- skgen ks;
    return (pk, sk);
  }

  proc enc (pk : pkey, m : plaintext) : ciphertext = {
    var e, c;

    e <$ dencseed;
    c <- enc (m, pk, e);
    return c;
  }

  proc dec(sk : skey, c : ciphertext) : plaintext option = {
    var m;

    m <- dec (c, sk);
    return m;
  }
}.

equiv eq_S (D <: SchemeDist) :
  D(S).distinguish ~ D(PKE.S).distinguish : ={glob D} ==> ={glob D,res}.
proof.
proc (true) => //; proc.
- rnd: *0 *0; auto => />; progress; try by rewrite(dmap_id). smt().
- rnd: *0 *0; auto => />; progress; by rewrite(dmap_id).
- by auto.
qed.

section.

declare module A <: Adversary {-Real, -Ideal, -IdealS,
                              -C.CCA_Oracle, -B, -BS, -CountCCA, -CountICCA}.

declare axiom A_bound (O <: Oracle {-A, -CountICCA}) :
  hoare [CountAdv(A, O).main :
    true ==> CountCCA.ndec <= Ndec /\ CountCCA.nenc <= Nenc].

equiv AB_bound (O <: CCA_Oracle{-CountCCA, -A, -B}) :
  C.CountAdv(B(A), O).main ~ CountAdv(A, B(A, O).O').main :
  ={glob A, glob O} /\ B.cs{2} = [] /\ arg{1} = B.pk{2} ==>
  CountCCA.ndec{1} <= CountCCA.ndec{2} /\ CountCCA.nenc{1} = CountCCA.nenc{2}.
proof.
proc. inline*; sp; auto.
call (: ={glob O, glob B} /\ CountCCA.ndec{1} <= CountCCA.ndec{2} /\
        CountCCA.nenc{1} = CountCCA.nenc{2}) => //.
- by proc; auto.
- by proc; inline *; sp; auto; call (: true); auto => /> /#.
- proc; inline *; sp; auto.
  if; auto => />; 2: by smt().
  by sp; call (: true); auto => /> /#.
qed.

lemma B_bound (O <: CCA_Oracle{-CountCCA, -CountCCA, -A, -B}) :
  hoare [C.CountAdv(B(A), O).main :
    true ==> CountCCA.ndec <= Ndec /\ CountCCA.nenc <= Nenc].
proof.
by conseq (AB_bound (<: O)) (A_bound (<: B(A, O).O')) => // /#.
qed.

local equiv Real_CCA_L :
  Game(Real, A).main ~ CCA_L(S, B(A)).main : ={glob A} ==> ={res}.
proof.
proc; inline*; wp.
call (: ={pk,sk}(Real,CCA_Oracle) /\ B.pk{2} = Real.pk{1}
  /\ (exists ks, (Real.pk, Real.sk){1} = (pkgen ks, skgen ks))
  /\ (unzip1 B.cs= CCA_Oracle.cs){2}
  /\ (forall m c, assoc B.cs c = Some m => dec(c,CCA_Oracle.sk) = Some m){2}).
- proc; inline*; auto.
- proc; inline*; auto => /> &m ks Hcs es ? m c.
  rewrite assoc_cons; smt(encK).
- proc; inline*; auto => /> &m ks Hcs.
  split; smt(assocTP). (* split is necessary!? *)
by auto => /> /#.
qed.

local equiv Ideal_CCA_R :
  Game(Ideal, A).main ~ CCA_R(S, B(A)).main : ={glob A} ==> ={res}.
proof.
proc; inline *; wp.
call (: ={pk, sk}(Real, CCA_Oracle) /\ unzip1 Ideal.cs{1} = CCA_Oracle.cs{2} /\
        (forall c m,
           assoc Ideal.cs c = Some m => dec(c, Real.sk) = Some m0){1} /\
        (exists ks, (CCA_Oracle.pk, CCA_Oracle.sk){2} = (pkgen ks, skgen ks)) /\
        Ideal.cs{1} = B.cs{2} /\ B.pk{2} = CCA_Oracle.pk{2}).
- by proc; inline *; auto => />.
- proc; inline *; auto => /> &m1 &m2 Hcs ks ? ? e _ c m'.
  by rewrite assoc_cons; case : (c = enc (m0, pkgen ks, e)) => />; smt(encK).
- proc; inline *; auto => /> &m1 &m2 Hcs ks ? ?.
  by rewrite -assocTP.
- by wp; rnd; skip => /> /#.
qed.

lemma ICCA_CCALR &m :
  Pr[Game(Real, A).main() @ &m : res] - Pr[Game(Ideal, A).main() @ &m : res] =
  Pr[CCA_L(S, B(A)).main() @ &m : res] - Pr[CCA_R(S, B(A)).main() @ &m : res].
proof.
have -> : Pr[Game(Real, A).main() @ &m : res] = Pr[CCA_L(S, B(A)).main() @ &m : res].
  by byequiv Real_CCA_L.
have -> : Pr[Game(Ideal, A).main() @ &m : res] = Pr[CCA_R(S, B(A)).main() @ &m : res].
  by byequiv Ideal_CCA_R.
smt().
qed.

(* Variation of the above, chosing a random preimage, if there are multiple *)

equiv AB_bound' (O <: CCA_Oracle{-CountCCA, -CountCCA, -A, -B}) :
  C.CountAdv(BS(A), O).main ~ CountAdv(A, BS(A, O).O').main :
  ={glob A, glob O} /\ B.cs{2} = [] /\ arg{1} = B.pk{2} ==>
  CountCCA.ndec{1} <= CountCCA.ndec{2} /\ CountCCA.nenc{1} = CountCCA.nenc{2}.
proof.
proc. inline*; sp; auto.
call (: ={glob O, glob B} /\ CountCCA.ndec{1} <= CountCCA.ndec{2} /\
        CountCCA.nenc{1} = CountCCA.nenc{2}) => //.
- by proc; auto.
- by proc; inline *; sp; auto; call (: true); auto => /> /#.
- proc; inline *; sp; auto.
  if; auto => />; 1: smt().
  by sp; call (: true); auto => /> /#.
qed.

lemma B_bound' (O <: CCA_Oracle{-CountCCA, -CountCCA, -A, -B}) :
  hoare [C.CountAdv(BS(A), O).main :
    true ==> CountCCA.ndec <= Ndec /\ CountCCA.nenc <= Nenc].
proof.
by conseq (AB_bound' (<: O)) (A_bound (<: BS(A, O).O')) => // /#.
qed.

local equiv Real_CCA_L' :
  Game(Real, A).main ~ CCA_L(S, BS(A)).main : ={glob A} ==> ={res}.
proof.
proc; inline*; wp.
call (: ={pk,sk}(Real,CCA_Oracle) /\ B.pk{2} = Real.pk{1}
  /\ (exists ks, (Real.pk, Real.sk){1} = (pkgen ks, skgen ks))
  /\ (unzip1 B.cs= CCA_Oracle.cs){2}
  /\ (forall m c, (c,m) \in B.cs => dec(c,CCA_Oracle.sk) = Some m){2}).
- by proc; auto.
- proc; inline*; auto => />; smt(encK).
- proc; inline*; sp; conseq />.
  if{2}; first by auto => /> 4?; smt(get_valid get_ll).
  by auto => />; smt(domP mapP).
by auto => /> /#.
qed.

equiv IdealS_CCA_R :
  Game(IdealS, A).main ~ CCA_R(S, BS(A)).main : ={glob A} ==> ={res}.
proof.
proc; inline *; wp.
call (: ={pk, sk}(Real, CCA_Oracle) /\ unzip1 Ideal.cs{1} = CCA_Oracle.cs{2} /\
        (forall c m, (c, m) \in Ideal.cs => dec(c, Real.sk) = Some(m0)){1} /\
        (* (forall c m, (c, m) \in List.filter (fun p => fst p = c) *)
        (*                                            Ideal.cs => *)
        (*                dec(c, Real.sk) = Some m0){1} /\ *)
        (exists ks, (CCA_Oracle.pk, CCA_Oracle.sk){2} = (pkgen ks, skgen ks)) /\
        Ideal.cs{1} = B.cs{2} /\ B.pk{2} = CCA_Oracle.pk{2}).
- by proc; inline *; auto => />.
- proc; inline *; auto => /> &m1 &m2 Hcs ks skP ? e _ c m'; smt(encK).
- proc; inline *; sp; auto; if; auto => /> &m1 &m2 5?; smt(domP mapP).
- by wp; rnd; skip => /> /#.
qed.

lemma ICCA_CCALR' &m :
  Pr[Game(Real, A).main() @ &m : res] - Pr[Game(IdealS, A).main() @ &m : res] =
  Pr[CCA_L(S, BS(A)).main() @ &m : res] - Pr[CCA_R(S, BS(A)).main() @ &m : res].
proof.
have -> : Pr[Game(Real, A).main() @ &m : res] =
          Pr[CCA_L(S, BS(A)).main() @ &m : res].
- by byequiv Real_CCA_L'.
have -> : Pr[Game(IdealS, A).main() @ &m : res] =
          Pr[CCA_R(S, BS(A)).main() @ &m : res]; 2: by smt().
by byequiv IdealS_CCA_R.
qed.

end section.

end CCA.