proposition: Theorem ElGamalDecrypt_correct : forall (pubkey msg : GroupElement)(prikey : nat)(ct : GroupElement * GroupElement), In (prikey, pubkey) (getSupport ElGamalKeygen) -> In ct (getSupport (ElGamalEncrypt msg pubkey)) -> ElGamalDecrypt prikey ct = msg.
proof: Proof. unfold ElGamalKeygen, ElGamalEncrypt, ElGamalDecrypt. intuition. repeat simp_in_support. rewrite <- associativity. repeat rewrite groupExp_mult. rewrite Nat.mul_comm. rewrite left_inverse. apply left_identity. Qed.
imports: FCF RndGrpElem Encryption_PK DiffieHellman OTP