game1FO'_goodbad.qrhl

# Autogenerated file (by replacing game0FO -> game0FO', game1FO -> game1FO', etc. etc. in game1FO_goodbad.qrhl)

include "ClassicalQueryG.qrhl".
include "queryH_Hq.qrhl".
include "decapsQuery1_G.qrhl".
include "Adv_INDCCA_encFO.qrhl".
include "queryG.qrhl".

# Differences from game1FO':

# Instead of picking G uniformly, we do:
# Pick Ggood as a function that has only "good" outputs (good is defined via the constant Rbad and means that for that message, reencryption succeeds)
# Pick Gbad as a function that has only "bad" outputs.
# Pick S to contain the set of inputs for which G should return Gbad
# Construct G as the combination of Ggood and Gbad

# Everywhere: use queryG instead of G directly

# We don't pick from Rbad and -Rbad, but from Rbad',Rgood' because otherwise the uniform distribution might not exist

program game1FO'_goodbad := {
  Hr <$ uniform UNIV;
  H0 <$ uniform UNIV;
  Hq <$ uniform UNIV;
  (pk,sk) <$ keygenT undefined;
  prfk <$ keygenPRF;
  Ggood <$ uniform {G. ∀m. G m ∈ Rgood' pk sk m};
  Gbad <$ uniform {G. ∀m. G m ∈ Rbad' pk sk m};
  S <$ Rbad_select pk sk;
  G <- λm. if m ∈ S then Gbad m else Ggood m;
  mstar <$ uniform (msg_spaceT undefined);
  gin <- mstar;
  call ClassicalQueryG(queryG);
  cstar <- encr () pk mstar gout;
  Kstar <$ uniform UNIV;
  in_pk <- pk;
  in_cstar <- cstar;
  gin <- undefined;
  gout <- undefined;
  call Adv_INDCCA_encFO(queryG,queryH_Hq(queryG),decapsQuery1_G(queryG));
}.