(* --------------------------------------------------------------------
 * Copyright (c) - 2012--2016 - IMDEA Software Institute
 * Copyright (c) - 2012--2021 - Inria
 * Copyright (c) - 2012--2021 - Ecole Polytechnique
 *
 * Distributed under the terms of the CeCILL-B-V1 license
 * -------------------------------------------------------------------- *)

require import Bool Core FSet.
require (*--*) DBool NewSKE.

clone include NewSKE.

module type CCA = {
  proc enc(p: plain): cipher option
  proc dec(c: cipher): plain option
}.

module type Adv_CCA (O : CCA) = {
  proc choose(): plain * plain
  proc guess(c: cipher): bool
}.

module IND_CCA ( S : SKE, A : Adv_CCA) = {
  module O = Wrap(S)
  module A = A(O)

  proc main(): bool = {
    var b, b', c, p0, p1, p;

    O.init();
    (p0,p1) <@ A.choose();
    b       <$ {0,1};
    p       <- b ? p1 : p0; (* FIXME: need to check whether plaintexts are both valid or both invalid *)
    c       <@ O.enc(p);
    b'      <@ A.guess(oget c);
    return (b = b' /\ !mem Wrap.dqs (oget c)); (* Penalty-style *)
  }
}.