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