fact: Definition IND_CCA2_G := [prikey, pubkey] <-$2 KeyGen; [r, _] <-$2 (A1 pubkey) _ _ (DecryptOracle prikey) tt; [p0, p1, a_state] <-3 r; b <-$ {0, 1}; pb <- if b then p0 else p1; c <-$ (Encrypt pb pubkey); [b', _] <-$2 A2 (c, a_state) _ _ (RestrictedDecryptOracle prikey c) tt; ret (eqb b b').
imports: FCF.FCF