The ElGamal encryption scheme has been proposed several years ago and is one of the few probabilistic encryption schemes. However, its security has never been concretely proven based on clearly understood and accepted primitives. Here we show directly that the decision Diffie-Hellman assumption implies the security of the original ElGamal encryption scheme (with messages from a subgroup) without modification. In addition, we show that the opposite direction holds, i.e., the semantic security of the ElGamal encryption is actually equivalent to the decision Diffie-Hellman problem. We also present an exact analysis of the efficiency of the reduction. Next we present additions on ElGamal encryption which result in nonmalleability under adaptive chosen plaintext attacks. Non-malleability is equivalent to the decision Diffie-Hellman assumption, the existence of a random oracle (in practice a secure hash function) or a trusted beacon (as needed for the Fiat-Shamir argument), and one assumptio...