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. Abort. Theorem ElGamal_IND_CPA0 : Pr[IND_CPA_G ElGamalKeygen ElGamalEncrypt A1 A2] == Pr[DDH0 B]. unfold IND_CPA_G, DDH0, DiffieHellman.DDH0, ElGamalKeygen, ElGamalEncrypt, B. inline_first. comp_skip. comp_at dist_inline rightc 1%nat. comp_swap rightc. comp_skip. destruct x0. destruct p. comp_at dist_inline rightc 1%nat. comp_swap rightc. comp_skip. comp_inline leftc. comp_skip. comp_inline rightc. comp_skip. rewrite groupExp_mult; intuition. comp_simp. intuition. Qed.
imports: FCF RndGrpElem Encryption_PK DiffieHellman OTP