Adv_O2H_Game1FO.qrhl

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

program Adv_O2H_Game1FO(query) := {
  (pk,sk) <- z';
  Hr <$ uniform UNIV;
  H0 <$ uniform UNIV;
  Hq <$ uniform UNIV;
  prfk <$ keygenPRF;
  mstar <$ uniform (msg_spaceT undefined);
  gin <- mstar;
  call ClassicalQueryG(query);
  cstar <- encr () pk mstar gout;
  Kstar <- Hq cstar;
  in_pk <- pk;
  in_cstar <- cstar;
  gin <- undefined;
  gout <- undefined;
  call Adv_INDCCA_encFO(query,queryH_Hq(query),decapsQuery1_G(query));
}.