Hashed ElGamal Encryption

Hashed ElGamal masks the message with a hash of the Diffie-Hellman shared secret rather than a group element, so it encrypts messages of an arbitrary type (group elements or otherwise) and achieves IND-CPA security under the DDH assumption in the ROM.

Construction

Given a cyclic group G with generator g:

• keyGen: Sample sk ← Exp; output (sk, pk = g^sk)
• encrypt(pk, m): Sample r ← Exp; output (g^r, m ⊕ H(pk^r))
• decrypt(sk, (c₁, c₂)): Output c₂ ⊕ H(c₁^sk)

where H : G → {0,1}^n is a hash function and ⊕ is XOR.

Security

Under DDH + ROM: IND-CPA_Advantage ≤ DDH_Advantage

The reduction:

• Given DDH challenge (g^a, g^b, z)
• Set pk = g^a, c₁ = g^b
• If z = g^(ab): H(z) masks m correctly (real game)
• If z = g^c: H(z) is fresh random (ideal/OTP game)

References

• [Abdalla, Bellare & Rogaway, The Oracle Diffie-Hellman Assumptions, 2001]
• [Shoup, A Proposal for an ISO Standard for PKE, 2001]

Hash Function Type

structure CatCryptCore.Examples.HashedElGamal.HashFunc (G : Type) [CG : CyclicGroupDDH.CyclicGroup G] (PT : Type) : Type

A hash function from group elements to the plaintext space. In the ROM, this would be modeled as a random oracle.

• hash : G → PT

Hashed ElGamal Scheme

noncomputable def CatCryptCore.Examples.HashedElGamal.heg_keyGen {G : Type} [CG : CyclicGroupDDH.CyclicGroup G] : CatCrypt.Core.SPComp (CyclicGroupDDH.CyclicGroup.Exp G × G)

Hashed ElGamal key generation: sample secret key, compute public key.

Equations

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

noncomputable def CatCryptCore.Examples.HashedElGamal.heg_encrypt_bool {G : Type} [CG : CyclicGroupDDH.CyclicGroup G] (H : G → Bool) (pk : G) (m : Bool) : CatCrypt.Core.SPComp (G × Bool)

Hashed ElGamal encryption with XOR masking (for Bool plaintext).

encrypt(pk, m) = (g^r, m ⊕ H(pk^r)) for random r.

Here we use Bool as the plaintext type and xor as the masking operation.

Equations

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

noncomputable def CatCryptCore.Examples.HashedElGamal.heg_decrypt_bool {G : Type} [CG : CyclicGroupDDH.CyclicGroup G] (H : G → Bool) (sk : CyclicGroupDDH.CyclicGroup.Exp G) (ct : G × Bool) : Bool

Hashed ElGamal decryption for Bool plaintext.

decrypt(sk, (c₁, c₂)) = c₂ ⊕ H(c₁^sk)

Equations

• CatCryptCore.Examples.HashedElGamal.heg_decrypt_bool H sk (c₁, c₂) = (H (CatCryptCore.Examples.CyclicGroupDDH.CyclicGroup.elemPow c₁ sk) ^^ c₂)

Correctness

theorem CatCryptCore.Examples.HashedElGamal.heg_correct_bool {G : Type} [CG : CyclicGroupDDH.CyclicGroup G] (H : G → Bool) (sk : CyclicGroupDDH.CyclicGroup.Exp G) (m : Bool) (r : CyclicGroupDDH.CyclicGroup.Exp G) : have pk := CyclicGroupDDH.CyclicGroup.pow sk; have shared := CyclicGroupDDH.CyclicGroup.elemPow pk r; heg_decrypt_bool H sk (CyclicGroupDDH.CyclicGroup.pow r, H shared ^^ m) = m

Decryption inverts encryption: H(pk^r) ⊕ (H(pk^r) ⊕ m) = m.

Correctness relies on:

• pk^r = g^(sk·r) = (g^r)^sk = c₁^sk
• H is deterministic
• XOR is self-inverse

IND-CPA Security Game

noncomputable def CatCryptCore.Examples.HashedElGamal.heg_real {G : Type} [CG : CyclicGroupDDH.CyclicGroup G] (H : G → Bool) (m : Bool) : CatCrypt.Core.SPComp (G × Bool)

Real IND-CPA game for Hashed ElGamal: sample (sk, pk), sample r, return (g^r, H(pk^r) ⊕ m).

Equations

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

noncomputable def CatCryptCore.Examples.HashedElGamal.heg_ideal {G : Type} [CG : CyclicGroupDDH.CyclicGroup G] (m : Bool) : CatCrypt.Core.SPComp (G × Bool)

Ideal game (random mask): replace H(g^(sk·r)) with a random bit. This is the OTP game — perfectly secure.

Equations

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

DDH-based Security Reduction

noncomputable def CatCryptCore.Examples.HashedElGamal.heg_ddh_reduction {G : Type} (H : G → Bool) (m : Bool) (A : G × Bool → CatCrypt.Core.SPComp Bool) (challenge : CyclicGroupDDH.DDHTriple G) : CatCrypt.Core.SPComp Bool

DDH distinguisher from a Hashed ElGamal IND-CPA adversary.

Given DDH challenge (g^a, g^b, z):

• pk := g^a, c₁ := g^b
• If z = g^(ab): encrypt = (g^b, H(g^(ab)) ⊕ m) = real game
• If z = g^c: encrypt = (g^b, H(g^c) ⊕ m) with independent H(g^c)

Equations

• CatCryptCore.Examples.HashedElGamal.heg_ddh_reduction H m A (_ga, gb, z) = A (gb, H z ^^ m)

theorem CatCryptCore.Examples.HashedElGamal.heg_real_bind_eq {G : Type} [CG : CyclicGroupDDH.CyclicGroup G] (H : G → Bool) (m : Bool) (A : G × Bool → CatCrypt.Core.SPComp Bool) : (heg_real H m).bind A = (CatCrypt.Core.SPComp.sample (CyclicGroupDDH.CyclicGroup.Exp G)).bind fun (sk : CyclicGroupDDH.CyclicGroup.Exp G) => (CatCrypt.Core.SPComp.sample (CyclicGroupDDH.CyclicGroup.Exp G)).bind fun (r : CyclicGroupDDH.CyclicGroup.Exp G) => A (CyclicGroupDDH.CyclicGroup.pow r, H (CyclicGroupDDH.CyclicGroup.pow (CyclicGroupDDH.CyclicGroup.expMul sk r)) ^^ m)

LHS normal form: heg_real.bind A as explicit double-sample.

theorem CatCryptCore.Examples.HashedElGamal.ddh_real_bind_red_eq {G : Type} [CG : CyclicGroupDDH.CyclicGroup G] (H : G → Bool) (m : Bool) (A : G × Bool → CatCrypt.Core.SPComp Bool) : (CyclicGroupDDH.DDH_real G).bind (heg_ddh_reduction H 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 b, H (CyclicGroupDDH.CyclicGroup.pow (CyclicGroupDDH.CyclicGroup.expMul a b)) ^^ m)

RHS normal form: DDH_real.bind reduction as explicit double-sample.

theorem CatCryptCore.Examples.HashedElGamal.heg_real_eq_ddh_real {G : Type} [CG : CyclicGroupDDH.CyclicGroup G] (H : G → Bool) (m : Bool) (A : G × Bool → CatCrypt.Core.SPComp Bool) : (heg_real H m).bind A = (CyclicGroupDDH.DDH_real G).bind (heg_ddh_reduction H m A)

Program equality: the real Hashed ElGamal game composed with adversary A equals the DDH real game composed with the DDH reduction.

theorem CatCryptCore.Examples.HashedElGamal.heg_indcpa_le_ddh {G : Type} [CG : CyclicGroupDDH.CyclicGroup G] (H : G → Bool) (m₀ m₁ : Bool) (A : G × Bool → CatCrypt.Core.SPComp Bool) [DecidableEq G] (h_ideal_indep : (CyclicGroupDDH.DDH_ideal G).bind (heg_ddh_reduction H m₀ A) = (CyclicGroupDDH.DDH_ideal G).bind (heg_ddh_reduction H m₁ A)) : CatCrypt.Crypto.AdvantageA (heg_real H m₀) (heg_real H m₁) A ≤ CyclicGroupDDH.DDH_Advantage G (heg_ddh_reduction H m₀ A) + CyclicGroupDDH.DDH_Advantage G (heg_ddh_reduction H m₁ A)

Hashed ElGamal IND-CPA advantage is bounded by DDH advantage.

The hypothesis h_ideal_indep captures the key property that in the DDH ideal world (where z = g^c for random c independent of a, b), the distinguisher's view is independent of the encrypted message m.

This holds when H is modeled as a random oracle: H(g^c) for random c acts as a fresh random mask, making xor(H(g^c), m) independent of m. It also holds for any hash function H such that H ∘ pow maps uniform exponents to uniform bits (e.g., a universal hash function).

The proof follows the standard DDH reduction:

1. Real game = DDH_real ∘ reduction (program equality)
2. Triangle: |Adv(real m₀, real m₁)| ≤ DDH(red m₀) + |ideal m₀ vs ideal m₁| + DDH(red m₁)
3. Middle term = 0 by h_ideal_indep
4. Conclusion: ≤ DDH(red m₀) + DDH(red m₁)

Perfect Security with Random Oracle

When H is a truly random function (perfect hash), the encryption mask is uniformly random regardless of the shared secret, giving perfect IND-CPA security.

theorem CatCryptCore.Examples.HashedElGamal.heg_ideal_mask_indep {G : Type} (c₁ : G) (m : Bool) : ((CatCrypt.Core.SPComp.sample Bool).bind fun (mask : Bool) => CatCrypt.Core.SPComp.pure (c₁, mask ^^ m)) = (CatCrypt.Core.SPComp.sample Bool).bind fun (mask : Bool) => CatCrypt.Core.SPComp.pure (c₁, mask)

OTP core: with a uniform mask, (c₁, mask ⊕ m) has the same distribution as (c₁, mask) — the message m is masked away. This is the one-time-pad bijection (boolXorBij m) applied inside the sampled mask, giving perfect secrecy of the ideal Hashed ElGamal game.

theorem CatCryptCore.Examples.HashedElGamal.heg_ideal_indep {G : Type} [CG : CyclicGroupDDH.CyclicGroup G] (m₀ m₁ : Bool) : heg_ideal m₀ = heg_ideal m₁

Perfect secrecy of the ideal game: the two ideal games for distinct messages are the same distribution. Only the innermost mask depends on the message, and the OTP bijection removes that dependence.

theorem CatCryptCore.Examples.HashedElGamal.heg_perfect_hash_security {G : Type} [CG : CyclicGroupDDH.CyclicGroup G] (m₀ m₁ : Bool) (A : G × Bool → CatCrypt.Core.SPComp Bool) : CatCrypt.Crypto.AdvantageA (heg_ideal m₀) (heg_ideal m₁) A = 0

With a perfect random oracle, Hashed ElGamal has zero IND-CPA advantage: the two ideal games are the same distribution (heg_ideal_indep), so every adversary distinguishes them with advantage 0. This is the OTP/perfect-secrecy endpoint the DDH reduction (heg_indcpa_le_ddh) targets.