ElGamal Public-Key Encryption: IND-CPA Security from DDH #
ElGamal encryption over an abstract prime-order group, and its reduction to the Decisional Diffie–Hellman assumption. Following Rosulek, The Joy of Cryptography (ElGamal / DDH).
We work in the group P.G₁ of a PairingGroup P — an abstract cyclic group of
prime order P.p with generator g₁ and ZMod P.p-exponentiation x ^ᵍ a. No
concrete curve is used.
The scheme #
- Secret key
sk : ZMod p, public keypk = g₁ ^ᵍ sk. Enc(sk, m)samplesr ← ZMod pand outputs(g₁ ^ᵍ r, (g₁ ^ᵍ sk) ^ᵍ r · m).Dec(sk, (c₁, c₂)) = c₂ · (c₁ ^ᵍ sk)⁻¹.
Messages are group elements (Plaintext = P.G₁), ciphertexts are pairs
(Ciphertext = P.G₁ × P.G₁).
The reduction (Rosulek) #
The DDH structure elgamalDDH : DDHDef P.G₁ samples s ← ZMod p and publishes
g₁ ^ᵍ s, with ecdh (g₁ ^ᵍ a) (g₁ ^ᵍ b) = g₁ ^ᵍ (a·b) (the true shared secret,
defined through the discrete-log bijection expEquiv : ZMod p ≃ G₁).
Given a fixed message m, the reduction adversary elgamalReduction m A turns a
DDH triple (g^a, g^b, Z) into the ciphertext (g^b, Z · m) and runs the IND-CPA
distinguisher A on it. When Z = g^{ab} this is a real ElGamal encryption of m
under pk = g^a with randomness r = b; when Z is uniform, Z · m is uniform
and independent of m.
The classic three-hop argument (real m₀ → uniform → real m₁, the middle games
coinciding because multiplication by m is a bijection of the uniform mask) yields
the bound INDCPA_Adv ≤ DDH_Advantage(m₀) + DDH_Advantage(m₁).
Main results #
elgamalDDH/elgamalEnc— the DDH structure and the encryption scheme.elgamalEnc_correct— decryption inverts encryption.elgamal_real₀_eq/elgamal_real₁_eq— each IND-CPA game equals a real DDH game composed with the reduction adversary (exact distribution equalities).elgamal_ideal_eq— the two ideal DDH games coincide (the mask absorbs the message).elgamal_indcpa_le_ddh— the headline: for every message pair and every distinguisher,INDCPA_Adv elgamalEnc m₀ m₁ A ≤DDH_Advantage elgamalDDH (elgamalReduction m₀ A) + DDH_Advantage elgamalDDH (elgamalReduction m₁ A).
References #
- [Rosulek, The Joy of Cryptography, §15 (ElGamal / DDH)]
- [Boneh & Shoup, A Graduate Course in Applied Cryptography, §11.4]
CatCryptCore.Crypto.Assumptions.DDHfor the DDH game and advantage.CatCryptCore.Crypto.PairingGroupfor the abstract prime-order group.
Sampleability of the group #
P.G₁ is a sampleable type (finite, nonempty, decidable equality, inhabited):
everything but the inhabitant comes from the PairingGroup instances.
Equations
- One or more equations did not get rendered due to their size.
Discrete-log bijection #
s ↦ g₁ ^ᵍ s is injective (trivial kernel) and, since |ZMod p| = p = |G₁|,
bijective. Its inverse is the (noncomputable) discrete log, which we use to give
ecdh its intended meaning g^a, g^b ↦ g^{ab}.
The discrete-log equivalence ZMod p ≃ G₁, a ↦ g₁ ^ᵍ a.
Equations
Instances For
Discrete log of g₁ ^ᵍ a is a.
The ElGamal DDH structure #
ElGamal's Diffie–Hellman operation: ecdh X Y = g₁ ^ᵍ (dlog X · dlog Y), i.e.
ecdh (g^a) (g^b) = g^{ab}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
On honest key pairs, ecdh computes the true shared secret.
ElGamal key generation: sample s, publish g₁ ^ᵍ s (as both key components).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The DDH group underlying ElGamal, over the abstract prime-order group P.G₁.
Equations
- CatCrypt.Examples.ElGamal.elgamalDDH P = { ecdh := CatCrypt.Examples.ElGamal.elgamalEcdh, keygen := CatCrypt.Examples.ElGamal.elgamalKeygen, keygen_isPure := ⋯ }
Instances For
The ElGamal encryption scheme #
ElGamal as a core EncScheme over P.G₁.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Correctness (algebraic core): for every secret key, randomness, and message, the ElGamal decryption formula inverts the encryption formula.
The reduction adversary #
The Rosulek reduction: on a DDH triple (g^a, g^b, Z), form the ciphertext
(g^b, Z · m) and run the IND-CPA distinguisher A.
Instances For
Game equalities #
The real IND-CPA game encrypting m₀ (the true branch), post-composed with the
distinguisher, is exactly the real DDH game with the m₀-reduction.
The real IND-CPA game encrypting m₁ (the false branch) equals the real DDH
game with the m₁-reduction.
The two ideal DDH games (with the m₀- and m₁-reductions) coincide: after the
mask is absorbed, neither depends on the message.
The IND-CPA → DDH reduction bound #
ElGamal is IND-CPA secure under DDH. For every message pair m₀, m₁ and
every distinguisher A, the IND-CPA advantage against ElGamal is bounded by the
sum of the DDH advantages of the two reduction adversaries:
INDCPA_Adv elgamalEnc m₀ m₁ A ≤
DDH_Advantage elgamalDDH (elgamalReduction m₀ A)
+ DDH_Advantage elgamalDDH (elgamalReduction m₁ A).
This is the standard three-hop reduction of Rosulek, The Joy of Cryptography:
the two real games are DDH-real games (elgamal_real₀_eq, elgamal_real₁_eq),
the two ideal games coincide (elgamal_ideal_eq), and the triangle inequality
for Advantage glues the hops.
ElGamal one-time real-or-random secrecy is EXACTLY a single DDH advantage.
This is the tight analog of SSProve-Rocq's OT_CPA_elgamal
(AdvOf (OT_CPA elgamal) A = AdvOf (LDDH G) (A ∘ RED)), whose OT_CPA game is a
real-or-random one-time-secrecy game: the true branch is a genuine encryption of
m₀, the false branch is a ciphertext whose second component is uniformly random
and independent of the message.
The left game is a real ElGamal encryption of m₀ post-composed with the
distinguisher; the right game is the ideal (random-ciphertext) game. Their
distinguishing advantage equals — with NO factor 2 and NO two-term sum — the DDH
advantage of the single reduction elgamalReduction m₀ A:
Advantage (bind (INDCPA_Game ⋯ m₀ m₁ true) A) (DDH_Game_Ideal ⋯ (elgamalReduction m₁ A))
= DDH_Advantage (elgamalDDH P) (elgamalReduction m₀ A).
The ideal game on the left is built from the m₁-reduction, yet the advantage is
exactly the m₀-reduction's DDH advantage: this is precisely because the two ideal
games coincide (elgamal_ideal_eq) — the uniform mask absorbs the message. The proof
is the exact-equality core underlying the looser elgamal_indcpa_le_ddh bound:
the real game is a real DDH game (elgamal_real₀_eq) and the ideal is
message-independent (elgamal_ideal_eq).
Note: the two-message left-or-right INDCPA_Adv (encrypt m₀ vs encrypt m₁) is a
different quantity; it genuinely requires the two-term bound elgamal_indcpa_le_ddh
(the real encryption of m₁ is not the ideal random ciphertext). SSProve's exact
result — reproduced here — is the real-or-random one, which is the single-DDH-term
statement.