ElGamal Encryption and DDH Security

The ElGamal public-key encryption scheme over a cyclic group with explicit exponents, and its IND-CPA security under the Decisional Diffie–Hellman (DDH) assumption.

The cyclic-group interface CyclicGroup and the DDH games (DDH_real, DDH_ideal, DDH_Advantage) are reused from CatCryptCore.Examples.CyclicGroupDDH.

Overview

ElGamal encryption operates in a cyclic group G of prime order with generator g:

• Key generation: sample random x from Z_q, output (pk = g^x, sk = x).
• Encryption: for message m and randomness r, output (c₁ = g^r, c₂ = pk^r · m).
• Decryption: given (c₁, c₂) and sk = x, compute c₂ · c₁^(-x) = m.

Security

ElGamal is IND-CPA secure under the DDH assumption:

• DDH problem: distinguish (g^a, g^b, g^(ab)) from (g^a, g^b, g^c) for random a, b, c.
• Reduction: an IND-CPA adversary for ElGamal yields a DDH distinguisher.

The proof uses a game-based approach: define the ElGamal scheme, build the reduction from IND-CPA to DDH, and prove the security bound via message-independence of the ideal game (a bijection-coupling argument).

References

• [Taher ElGamal, A Public Key Cryptosystem and a Signature Scheme Based on Discrete Logarithms, 1985]
• [Boneh & Shoup, A Graduate Course in Applied Cryptography, Chapter 11]
• [SSProve: theories/Crypt/examples/PKE/ElGamal.v]

Decryption Correctness Identity

theorem CatCryptCore.Examples.ElGamalDDH.decrypt_correct {G : Type} [CG : CyclicGroupDDH.CyclicGroup G] (m : G) (sk r : CyclicGroupDDH.CyclicGroup.Exp G) : CyclicGroupDDH.CyclicGroup.mul (CyclicGroupDDH.CyclicGroup.mul m (CyclicGroupDDH.CyclicGroup.pow (CyclicGroupDDH.CyclicGroup.expMul sk r))) (CyclicGroupDDH.CyclicGroup.inv (CyclicGroupDDH.CyclicGroup.pow (CyclicGroupDDH.CyclicGroup.expMul sk r))) = m

Key algebraic identity underlying decryption: c₂ · c₁^(-sk) recovers the message when c₁ = g^r, c₂ = m · pk^r, pk = g^sk. That is m · g^(sk·r) · g^(-sk·r) = m.

ElGamal Encryption Scheme

structure CatCryptCore.Examples.ElGamalDDH.ElGamalScheme (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] : Type

ElGamal encryption scheme for a cyclic group G. The scheme is determined by the group, so the structure carries no configuration.

@[reducible, inline]

abbrev CatCryptCore.Examples.ElGamalDDH.ElGamalScheme.SecretKey (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] : Type

Secret key type: an exponent.

Equations

• CatCryptCore.Examples.ElGamalDDH.ElGamalScheme.SecretKey G = CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.Exp G

@[reducible, inline]

abbrev CatCryptCore.Examples.ElGamalDDH.ElGamalScheme.PublicKey (G : Type) [_CG : CyclicGroupDDH.CyclicGroup G] : Type

Public key type: a group element.

Equations

• CatCryptCore.Examples.ElGamalDDH.ElGamalScheme.PublicKey G = G

@[reducible, inline]

abbrev CatCryptCore.Examples.ElGamalDDH.ElGamalScheme.Message (G : Type) [_CG : CyclicGroupDDH.CyclicGroup G] : Type

Message type: a group element.

Equations

• CatCryptCore.Examples.ElGamalDDH.ElGamalScheme.Message G = G

@[reducible, inline]

abbrev CatCryptCore.Examples.ElGamalDDH.ElGamalScheme.Ciphertext (G : Type) [_CG : CyclicGroupDDH.CyclicGroup G] : Type

Ciphertext type: a pair of group elements (c₁, c₂).

Equations

• CatCryptCore.Examples.ElGamalDDH.ElGamalScheme.Ciphertext G = (G × G)

noncomputable def CatCryptCore.Examples.ElGamalDDH.ElGamalScheme.keyGen (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] : CatCrypt.Core.SPComp (SecretKey G × PublicKey G)

Key generation: sample random x, output (sk = x, pk = g^x).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CatCryptCore.Examples.ElGamalDDH.ElGamalScheme.encrypt (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] (pk : PublicKey G) (m : Message G) : CatCrypt.Core.SPComp (Ciphertext G)

Encryption: Enc(pk, m) = (g^r, m · pk^r) for random r.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CatCryptCore.Examples.ElGamalDDH.ElGamalScheme.decrypt (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] (sk : SecretKey G) (ct : Ciphertext G) : CatCrypt.Core.SPComp (Option (Message G))

Decryption: Dec(sk, (c₁, c₂)) = c₂ · c₁^(-sk).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CatCryptCore.Examples.ElGamalDDH.ElGamalScheme.toEncScheme (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] : CatCrypt.Crypto.EncScheme

ElGamal presented as an EncScheme.

Equations

• One or more equations did not get rendered due to their size.

IND-CPA Security Game for ElGamal

The IND-CPA game for public-key encryption: the challenger generates (pk, sk), the adversary receives pk, chooses two messages m₀, m₁, and tries to guess which one was encrypted.

noncomputable def CatCryptCore.Examples.ElGamalDDH.ElGamal_INDCPA_real (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] (m0 _m1 : G) : CatCrypt.Core.SPComp (G × ElGamalScheme.Ciphertext G)

IND-CPA real game for ElGamal: encrypt m₀.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CatCryptCore.Examples.ElGamalDDH.ElGamal_INDCPA_ideal (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] (_m0 m1 : G) : CatCrypt.Core.SPComp (G × ElGamalScheme.Ciphertext G)

IND-CPA ideal game for ElGamal: encrypt m₁.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CatCryptCore.Examples.ElGamalDDH.ElGamal_INDCPA_Advantage (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] (m0 m1 : G) (A : G × ElGamalScheme.Ciphertext G → CatCrypt.Core.SPComp Bool) : ENNReal

IND-CPA advantage for ElGamal.

Equations

• One or more equations did not get rendered due to their size.

Security Reduction: IND-CPA to DDH

Given a DDH challenge (g^a, g^b, z), set pk = g^a and answer the encryption query for message m with (g^b, m · z). If z = g^(ab) this is a valid ElGamal ciphertext; if z = g^c it masks the message with an independent element.

noncomputable def CatCryptCore.Examples.ElGamalDDH.Reduction (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] (m : G) (A : G × ElGamalScheme.Ciphertext G → CatCrypt.Core.SPComp Bool) (challenge : CyclicGroupDDH.DDHTriple G) : CatCrypt.Core.SPComp Bool

The reduction from IND-CPA to DDH: given an IND-CPA adversary A, use the DDH challenge (g^a, g^b, z) to simulate the IND-CPA game with pk = g^a and ct = (g^b, m · z).

Equations

• CatCryptCore.Examples.ElGamalDDH.Reduction G m A (ga, gb, z) = A (ga, gb, CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.mul m z)

Main Security Theorem

theorem CatCryptCore.Examples.ElGamalDDH.keyGen_bind_eq (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] (m : G) : ElGamal_INDCPA_real G m m = (CatCrypt.Core.SPComp.sample (CyclicGroupDDH.CyclicGroup.Exp G)).bind fun (sk : CyclicGroupDDH.CyclicGroup.Exp G) => (ElGamalScheme.encrypt G (CyclicGroupDDH.CyclicGroup.pow sk) m).bind fun (ct : ElGamalScheme.Ciphertext G) => CatCrypt.Core.SPComp.pure (CyclicGroupDDH.CyclicGroup.pow sk, ct)

Simplify keyGen bind.

theorem CatCryptCore.Examples.ElGamalDDH.encrypt_eq (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] (m pk : G) : ElGamalScheme.encrypt G pk m = (CatCrypt.Core.SPComp.sample (CyclicGroupDDH.CyclicGroup.Exp G)).bind fun (r : CyclicGroupDDH.CyclicGroup.Exp G) => CatCrypt.Core.SPComp.pure (CyclicGroupDDH.CyclicGroup.pow r, CyclicGroupDDH.CyclicGroup.mul m (CyclicGroupDDH.CyclicGroup.elemPow pk r))

Simplify encrypt.

theorem CatCryptCore.Examples.ElGamalDDH.ElGamal_INDCPA_real_simplified (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] (m : G) : ElGamal_INDCPA_real G m m = do let sk ← CatCrypt.Core.SPComp.sample (CyclicGroupDDH.CyclicGroup.Exp G) let r ← CatCrypt.Core.SPComp.sample (CyclicGroupDDH.CyclicGroup.Exp G) CatCrypt.Core.SPComp.pure (CyclicGroupDDH.CyclicGroup.pow sk, CyclicGroupDDH.CyclicGroup.pow r, CyclicGroupDDH.CyclicGroup.mul m (CyclicGroupDDH.CyclicGroup.pow (CyclicGroupDDH.CyclicGroup.expMul sk r)))

Fully simplified form of ElGamal_INDCPA_real.

theorem CatCryptCore.Examples.ElGamalDDH.reduction_real_lhs_eq (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] (m : G) (A : G × ElGamalScheme.Ciphertext G → CatCrypt.Core.SPComp Bool) : (CyclicGroupDDH.DDH_real G).bind (Reduction G m A) = (CatCrypt.Core.SPComp.sample (CyclicGroupDDH.CyclicGroup.Exp G)).bind fun (a : CyclicGroupDDH.CyclicGroup.Exp G) => (CatCrypt.Core.SPComp.sample (CyclicGroupDDH.CyclicGroup.Exp G)).bind fun (b : CyclicGroupDDH.CyclicGroup.Exp G) => A (CyclicGroupDDH.CyclicGroup.pow a, CyclicGroupDDH.CyclicGroup.pow b, CyclicGroupDDH.CyclicGroup.mul m (CyclicGroupDDH.CyclicGroup.pow (CyclicGroupDDH.CyclicGroup.expMul a b)))

Simplify the LHS of the reduction to explicit samples and application.

theorem CatCryptCore.Examples.ElGamalDDH.reduction_real_rhs_eq (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] (m : G) (A : G × ElGamalScheme.Ciphertext G → CatCrypt.Core.SPComp Bool) : (ElGamal_INDCPA_real G m m).bind A = (CatCrypt.Core.SPComp.sample (CyclicGroupDDH.CyclicGroup.Exp G)).bind fun (a : CyclicGroupDDH.CyclicGroup.Exp G) => (CatCrypt.Core.SPComp.sample (CyclicGroupDDH.CyclicGroup.Exp G)).bind fun (b : CyclicGroupDDH.CyclicGroup.Exp G) => A (CyclicGroupDDH.CyclicGroup.pow a, CyclicGroupDDH.CyclicGroup.pow b, CyclicGroupDDH.CyclicGroup.mul m (CyclicGroupDDH.CyclicGroup.pow (CyclicGroupDDH.CyclicGroup.expMul a b)))

Simplify the RHS of the reduction to explicit samples and application.

theorem CatCryptCore.Examples.ElGamalDDH.reduction_real_eq_indcpa_real (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] (m : G) (A : G × ElGamalScheme.Ciphertext G → CatCrypt.Core.SPComp Bool) : (CyclicGroupDDH.DDH_real G).bind (Reduction G m A) = (ElGamal_INDCPA_real G m m).bind A

The DDH real game with the reduction equals the IND-CPA real game with the adversary.

theorem CatCryptCore.Examples.ElGamalDDH.reduction_ideal_indep_message (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] (m0 m1 : G) (A : G × ElGamalScheme.Ciphertext G → CatCrypt.Core.SPComp Bool) : (CyclicGroupDDH.DDH_ideal G).bind (Reduction G m0 A) = (CyclicGroupDDH.DDH_ideal G).bind (Reduction G m1 A)

When z = g^c for random c, the ciphertext is independent of the message: for any messages m₀, m₁, the DDH ideal game composed with the reduction gives the same distribution. The map m · g^c is a bijection for fixed m, so m · g^c is uniform, and the two games are coupled by the induced exponent bijection.

theorem CatCryptCore.Examples.ElGamalDDH.INDCPA_real_ignores_m1 (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] (m0 m1 m1' : G) : ElGamal_INDCPA_real G m0 m1 = ElGamal_INDCPA_real G m0 m1'

ElGamal_INDCPA_real ignores the second message argument.

theorem CatCryptCore.Examples.ElGamalDDH.INDCPA_ideal_eq_real_m1 (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] (m0 m1 : G) : ElGamal_INDCPA_ideal G m0 m1 = ElGamal_INDCPA_real G m1 m1

ElGamal_INDCPA_ideal equals ElGamal_INDCPA_real with the second message.

theorem CatCryptCore.Examples.ElGamalDDH.elgamal_indcpa_security (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] (m0 m1 : G) (A : G × ElGamalScheme.Ciphertext G → CatCrypt.Core.SPComp Bool) : ElGamal_INDCPA_Advantage G m0 m1 A ≤ CyclicGroupDDH.DDH_Advantage G (Reduction G m0 A) + CyclicGroupDDH.DDH_Advantage G (Reduction G m1 A)

ElGamal IND-CPA security reduces to DDH: for any adversary A and messages m₀, m₁, the IND-CPA advantage is bounded by the sum of the DDH advantages of the reductions using m₀ and m₁.

The proof hops through: IND-CPA real (encrypt m₀) = DDH real reduction with m₀; DDH ideal reduction with m₀ = DDH ideal reduction with m₁ (message independence); DDH real reduction with m₁ = IND-CPA ideal (encrypt m₁).

Correctness of ElGamal

theorem CatCryptCore.Examples.ElGamalDDH.elgamal_correct (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] (sk : CyclicGroupDDH.CyclicGroup.Exp G) (m : G) : have _pk := CyclicGroupDDH.CyclicGroup.pow sk; ∀ (r : CyclicGroupDDH.CyclicGroup.Exp G), have _c1 := CyclicGroupDDH.CyclicGroup.pow r; have c2 := CyclicGroupDDH.CyclicGroup.mul m (CyclicGroupDDH.CyclicGroup.pow (CyclicGroupDDH.CyclicGroup.expMul sk r)); have decrypted := CyclicGroupDDH.CyclicGroup.mul c2 (CyclicGroupDDH.CyclicGroup.inv (CyclicGroupDDH.CyclicGroup.pow (CyclicGroupDDH.CyclicGroup.expMul sk r))); decrypted = m

ElGamal correctness: decryption recovers the original message. For secret key sk and message m, encrypting with c₁ = g^r and c₂ = m · g^(sk·r) and then decrypting via c₂ · (g^(sk·r))⁻¹ returns m.

Bijection Lemmas for the Security Proof

theorem CatCryptCore.Examples.ElGamalDDH.pow_bijective (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] : Function.Bijective CyclicGroupDDH.CyclicGroup.pow

g^(-) is a bijection from Exp to G.

theorem CatCryptCore.Examples.ElGamalDDH.mul_pow_bijective (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] (m : G) : Function.Bijective fun (b : CyclicGroupDDH.CyclicGroup.Exp G) => CyclicGroupDDH.CyclicGroup.mul m (CyclicGroupDDH.CyclicGroup.pow b)

For any m : G, the map b ↦ m · g^b is a bijection: multiplication by m is a bijection and g^b is a bijection. This couples m₀ · g^c and m₁ · g^c' to the same distribution when c and c' are coupled.

noncomputable def CatCryptCore.Examples.ElGamalDDH.powEquiv (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] : CyclicGroupDDH.CyclicGroup.Exp G ≃ G

Equivalence from Exp to G via pow, for coupling arguments.

Equations

• CatCryptCore.Examples.ElGamalDDH.powEquiv G = Equiv.ofBijective CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.pow ⋯

noncomputable def CatCryptCore.Examples.ElGamalDDH.mulPowEquiv (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] (m : G) : CyclicGroupDDH.CyclicGroup.Exp G ≃ G

Equivalence from Exp to G via b ↦ m · g^b, for coupling arguments.

Equations

• One or more equations did not get rendered due to their size.