proposition: Theorem PRFE_IND_CPA_concrete : IND_CPA_SecretKey_Advantage PRFE_KeyGen PRFE_Encrypt A1 A2 _ <= PRF_Advantage ({0, 1}^eta) ({0, 1}^eta) f _ _ PRF_A' + (q1 / 2^eta + q2 / 2^eta).
proof: Proof. unfold IND_CPA_SecretKey_Advantage. rewrite G1_equiv. eapply ratDistance_le_trans. eapply eqRat_impl_leRat. eapply G1_G2_close. eapply leRat_trans. eapply ratDistance_le_trans. eapply G2_G3_close. eapply eqRat_impl_leRat. rewrite <- ratIdentityIndiscernables. rewrite G3_G4_equiv. rewrite G4_G5_equiv. eapply G5_one_half. eapply eqRat_impl_leRat. symmetry. eapply ratAdd_0_r. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime