proposition: Theorem ElGamal_IND_CPA_Advantage : (IND_CPA_Advantage ElGamalKeygen ElGamalEncrypt A1 A2) == (DDH_Advantage B).
proof: Proof. unfold IND_CPA_Advantage, DDH_Advantage, DiffieHellman.DDH_Advantage. eapply ratDistance_eqRat_compat. eapply ElGamal_IND_CPA0. rewrite <- ElGamal_G1_DDH1. rewrite ElGamal_G1_G2. symmetry. eapply ElGamal_G2_OneHalf. Qed.
imports: FCF RndGrpElem Encryption_PK DiffieHellman OTP