ElGamal and Hashed ElGamal encryption and IND-CPA security under DDH

Over a PrimeOrderGroupFamily, multiplicative ElGamal encryption ([BS23], Exercise 11.5, p. 459) uses a group description d, a secret exponent α : ZMod (F.order d), and the public key u = α • g. To encrypt a group element m : F.Carrier d with randomness β : ZMod (F.order d), the sender forms the ciphertext (v, e) = (β • g, β • u + m) = (β • g, (α * β) • g + m). Decryption recovers e - α • v = m, and the word-level operations encodeElGamalPublicKey, encodeElGamalEncrypt, and decodeElGamal compute public-key generation, encryption, and decryption in polynomial time from natural-number exponents and encoded group elements using F.generator, F.order, F.smul, and F.add.

We prove IND-CPA security under DDH in the following settings:

1. Shared typed-message ElGamal reduction (elGamalMsgCPAGameOn, elGamalMsgToDDHDistinguisher, advantage_elGamalMsgCPAGameOn_le, isPPTOn_elGamalMsgToDDHDistinguisher, DDH.negligible_elGamalMsgCPAGameOn). As in Encryption.gameOn, a challenge-pair admissibility predicate valid : ℕ → List Bool → Msg → Msg → Bool sees the security parameter and the public key, and an inadmissible pair makes the game output false in both experiments. The reduction needs valid to be computable in polynomial time and to admit only messages whose encodings are group elements (AdmitsGroupElements). It is instantiated for:
   • Bit ElGamal (elGamalCPAGame, elGamalINDCPA, DDH.elGamalINDCPA): false and true are embedded as 0 and g (bitElement, encodeBit), every pair is admissible, and Encryption.Adversary chooses two challenge bits.
   • Group-element ElGamal (Encryption.WordAdversary, elGamalGroupCPAGameOn, DDH.negligible_elGamalGroupCPAGameOn, [BS23], Exercise 11.5(a), p. 459): a two-stage word-message adversary chooses two words, and valid admits only encoded group elements, in Set.range (F.encode d). Replacing the Diffie–Hellman mask (α * β) • g with an independent uniform γ • g masks any admissible pair perfectly (uniform_smul_generator_add). A PrimeOrderGroupFamily has no membership test, so valid is a parameter; the tests instantiate it on Schnorr groups.
2. Hashed ElGamal (hashedElGamalEncrypt, hashedElGamalDecrypt, hashedElGamalCPAGame, DDH.negligible_hashedElGamalCPAGame, [BS23], Section 11.5, pp. 445–446, Remark 11.1, and Section 11.5.2, Attack Game 11.3, Definition 11.5, and Theorem 11.5, pp. 448–451): given a deterministic polynomial-time key-derivation hash function H : F.Desc × List Bool → List Bool, the sender masks a message word m with pad = H (d, encode (β • u)) via Cslib.BitString.listXor pad.length [pad, m] (the one-time pad specialization of the E'_EG variant of Remark 11.1). Security reduces to DDH together with key-derivation security (SecureKDF, Attack Game 11.3, p. 448, and Definition 11.5, p. 449: indistinguishability of H (d, encode (γ • g)) from a uniform msgLen n-bit key). The ciphertext length does not depend on the message, and hashedElGamalCPAGame admits every challenge pair, which is stronger than Attack Game 11.1's equal-length rule.

Limitations

In this module, key generation and challenge encryption in the security games sample exact uniform exponents in ZMod (F.order d) at the PMF level (PMF.uniformOfFintype (ZMod (F.order d))), because an odd prime order F.order d cannot be sampled with exact uniformity by a bounded-time fair-coin ProbComp machine; deterministic public-key computation (encodeElGamalPublicKey), encryption given randomness (encodeElGamalEncrypt, encodeHashedElGamalEncrypt), and decryption (decodeElGamal, decodeHashedElGamal) are certified polynomial time on words. Strict-PPT (IsPPTOn) key generation, KEM encapsulation/decapsulation, and encryption via ProbComp.sampleModNat (connecting to Encryption.KEMINDCPA, Encryption.INDCPAOn, Encryption.WordINDCPA, and Encryption.INDCPA) are provided in Complexity/Crypto/Computational/ElGamal/ProbComp.lean; non-degenerate SecureKDF instantiation (msgLen n > 0) via BitString.LinearHash and the leftover hash lemma is provided in Complexity/Crypto/Computational/ElGamal/KDF.lean.

Main definitions

• Cslib.Crypto.PrimeOrderGroupFamily.elGamalEncrypt, Cslib.Crypto.PrimeOrderGroupFamily.elGamalDecrypt: algebraic ElGamal encryption and decryption.
• Cslib.Crypto.PrimeOrderGroupFamily.encodeElGamalPublicKey, Cslib.Crypto.PrimeOrderGroupFamily.encodeElGamalEncrypt, Cslib.Crypto.PrimeOrderGroupFamily.decodeElGamal: polynomial-time public-key generation, encryption, and decryption on encoded group elements.
• Cslib.Crypto.PrimeOrderGroupFamily.elGamalMsgCPAGameOn, Cslib.Crypto.PrimeOrderGroupFamily.elGamalMsgToDDHDistinguisher, Cslib.Crypto.PrimeOrderGroupFamily.AdmitsGroupElements: shared typed-message ElGamal IND-CPA experiment with an admissibility predicate, DDH reduction, and the condition that the predicate admits only group elements ([BS23], Exercise 11.5(a), p. 459).
• Cslib.Crypto.PrimeOrderGroupFamily.bitElement, Cslib.Crypto.PrimeOrderGroupFamily.encodeBit: embedding and polynomial-time encoding of message bits as group elements.
• Cslib.Crypto.PrimeOrderGroupFamily.elGamalCPAGame, Cslib.Crypto.PrimeOrderGroupFamily.elGamalINDCPA, Cslib.Crypto.PrimeOrderGroupFamily.elGamalToDDHDistinguisher: bit ElGamal IND-CPA experiment, security property, and DDH distinguisher.
• Cslib.Crypto.PrimeOrderGroupFamily.elGamalGroupCPAGameOn, Cslib.Crypto.PrimeOrderGroupFamily.elGamalGroupToDDHDistinguisher: group-element ElGamal IND-CPA experiment and DDH reduction ([BS23], Exercise 11.5(a), p. 459).
• Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalEncrypt, Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalDecrypt, Cslib.Crypto.PrimeOrderGroupFamily.encodeHashedElGamalEncrypt, Cslib.Crypto.PrimeOrderGroupFamily.decodeHashedElGamal: algebraic and word-level Hashed ElGamal encryption and decryption ([BS23], Section 11.5, pp. 445–446, Remark 11.1).
• Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalCPAGame, Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalIdealDDHGame, Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalUniformPadGame, Cslib.Crypto.PrimeOrderGroupFamily.kdfRealGame, Cslib.Crypto.PrimeOrderGroupFamily.kdfIdealGame, Cslib.Crypto.PrimeOrderGroupFamily.SecureKDF, Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalToDDHDistinguisher, Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalToKDFDistinguisher: Hashed ElGamal IND-CPA experiments, hybrids, and reductions ([BS23], Section 11.5.2, Attack Game 11.3, Definition 11.5, and Theorem 11.5, pp. 448–451).

Main results

• Cslib.Crypto.PrimeOrderGroupFamily.elGamalDecrypt_elGamalEncrypt, Cslib.Crypto.PrimeOrderGroupFamily.encodeElGamalPublicKey_eq_encode, Cslib.Crypto.PrimeOrderGroupFamily.encodeElGamalEncrypt_encode, Cslib.Crypto.PrimeOrderGroupFamily.decodeElGamal_encode, Cslib.Crypto.PrimeOrderGroupFamily.decodeElGamal_elGamalEncrypt, Cslib.Crypto.PrimeOrderGroupFamily.decodeElGamal_encodeElGamalEncrypt: ElGamal correctness.
• Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_encodeElGamalPublicKey, Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_encodeElGamalEncrypt, Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_decodeElGamal: polynomial-time certificates for honest ElGamal operations.
• Cslib.Crypto.PrimeOrderGroupFamily.advantage_elGamalMsgCPAGameOn_le, Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_elGamalMsgToDDHDistinguisher, Cslib.Crypto.PrimeOrderGroupFamily.DDH.negligible_elGamalMsgCPAGameOn: shared typed-message ElGamal IND-CPA reduction to DDH.
• Cslib.Crypto.PrimeOrderGroupFamily.advantage_elGamalCPAGame_le, Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_elGamalToDDHDistinguisher, Cslib.Crypto.PrimeOrderGroupFamily.DDH.elGamalINDCPA: ElGamal IND-CPA security for bit messages under DDH ([BS23], Exercise 11.5(a), p. 459).
• Cslib.Crypto.PrimeOrderGroupFamily.advantage_elGamalGroupCPAGameOn_le, Cslib.Crypto.PrimeOrderGroupFamily.DDH.negligible_elGamalGroupCPAGameOn: ElGamal IND-CPA security for group-element messages under DDH ([BS23], Exercise 11.5(a), p. 459).
• Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalDecrypt_hashedElGamalEncrypt, Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_encodeHashedElGamalEncrypt, Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_decodeHashedElGamal, Cslib.Crypto.PrimeOrderGroupFamily.advantage_hashedElGamalCPAGame_le, Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_hashedElGamalToDDHDistinguisher, Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_hashedElGamalToKDFDistinguisher, Cslib.Crypto.PrimeOrderGroupFamily.DDH.negligible_hashedElGamalCPAGame: Hashed ElGamal correctness, polynomial-time certificates, and IND-CPA security under DDH and SecureKDF ([BS23], Section 11.5.2, Theorem 11.5, pp. 449–451).

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Section 11.5 (pp. 445–446, Remark 11.1), Section 11.5.2 (pp. 448–451, Attack Game 11.3, Definition 11.5, Theorem 11.5), and Exercise 11.5(a) (p. 459).

Group-element ElGamal encryption and decryption

def Cslib.Crypto.PrimeOrderGroupFamily.elGamalEncrypt (F : PrimeOrderGroupFamily) (d : F.Desc) (u m : F.Carrier d) (β : ZMod (F.order d)) : F.Carrier d × F.Carrier d

Algebraic ElGamal encryption of a group element m : F.Carrier d under public key u : F.Carrier d with randomness β : ZMod (F.order d).

theorem Cslib.Crypto.PrimeOrderGroupFamily.elGamalEncrypt_smul_generator (F : PrimeOrderGroupFamily) (d : F.Desc) (α β : ZMod (F.order d)) (m : F.Carrier d) : F.elGamalEncrypt d (α • F.generator d) m β = (β • F.generator d, (α * β) • F.generator d + m)

Under a genuine public key u = α • g, the second ciphertext component is (α * β) • g + m.

def Cslib.Crypto.PrimeOrderGroupFamily.elGamalDecrypt (F : PrimeOrderGroupFamily) (d : F.Desc) (α : ZMod (F.order d)) (ct : F.Carrier d × F.Carrier d) : F.Carrier d

Algebraic ElGamal decryption of a ciphertext pair (v, e) using secret key α : ZMod (F.order d).

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.elGamalDecrypt_elGamalEncrypt (F : PrimeOrderGroupFamily) (d : F.Desc) (α β : ZMod (F.order d)) (m : F.Carrier d) : F.elGamalDecrypt d α (F.elGamalEncrypt d (α • F.generator d) m β) = m

ElGamal decryption correctness: decrypting an encryption under u = α • g with secret key α recovers the message m.

def Cslib.Crypto.PrimeOrderGroupFamily.encodeElGamalPublicKey (F : PrimeOrderGroupFamily) (input : F.Desc × ℕ) : List Bool

Word-level ElGamal public-key computation: given (d, a), compute encode ((a : ZMod q) • g) as F.smul (d, a, F.encode d (F.generator d)).

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.encodeElGamalPublicKey_eq_encode (F : PrimeOrderGroupFamily) (d : F.Desc) (a : ℕ) : F.encodeElGamalPublicKey (d, a) = F.encode d (↑a • F.generator d)

encodeElGamalPublicKey computes the group encoding of (a : ZMod (F.order d)) • g.

theorem Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_encodeElGamalPublicKey (F : PrimeOrderGroupFamily) : Turing.MultiTapeTM.ComputableInPolyTime F.encodeElGamalPublicKey (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBits

Word-level ElGamal public-key computation is computable in polynomial time.

def Cslib.Crypto.PrimeOrderGroupFamily.encodeElGamalEncrypt (F : PrimeOrderGroupFamily) (input : F.Desc × List Bool × List Bool × ℕ) : List Bool × List Bool

Word-level ElGamal encryption: given (d, encode u, encode m, b), compute (encode (b • g), encode (b • u + m)).

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.encodeElGamalEncrypt_encode (F : PrimeOrderGroupFamily) (d : F.Desc) (u m : F.Carrier d) (b : ℕ) : F.encodeElGamalEncrypt (d, F.encode d u, F.encode d m, b) = (F.encode d (F.elGamalEncrypt d u m ↑b).1, F.encode d (F.elGamalEncrypt d u m ↑b).2)

encodeElGamalEncrypt evaluates elGamalEncrypt on encoded group elements.

theorem Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_encodeElGamalEncrypt (F : PrimeOrderGroupFamily) : Turing.MultiTapeTM.ComputableInPolyTime F.encodeElGamalEncrypt (Turing.MultiTapeTM.encPair F.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encNat))) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)

Word-level ElGamal encryption is computable in polynomial time.

def Cslib.Crypto.PrimeOrderGroupFamily.decodeElGamal (F : PrimeOrderGroupFamily) (input : F.Desc × ℕ × List Bool × List Bool) : List Bool

Decryption on encoded group elements: given (d, a, encode v, encode e), compute encode (e - a • v) as F.add (d, encode e, F.smul (d, F.order d - a % F.order d, encode v)).

theorem Cslib.Crypto.PrimeOrderGroupFamily.decodeElGamal_encode (F : PrimeOrderGroupFamily) (d : F.Desc) (a : ℕ) (v e : F.Carrier d) : F.decodeElGamal (d, a, F.encode d v, F.encode d e) = F.encode d (F.elGamalDecrypt d ↑a (v, e))

decodeElGamal computes encode (elGamalDecrypt d a (v, e)) on encoded group elements.

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.decodeElGamal_elGamalEncrypt (F : PrimeOrderGroupFamily) (d : F.Desc) (a : ℕ) (β : ZMod (F.order d)) (m : F.Carrier d) : F.decodeElGamal (d, a, F.encode d (F.elGamalEncrypt d (↑a • F.generator d) m β).1, F.encode d (F.elGamalEncrypt d (↑a • F.generator d) m β).2) = F.encode d m

Encoded ElGamal decryption of an honest encryption recovers the encoded message.

theorem Cslib.Crypto.PrimeOrderGroupFamily.decodeElGamal_encodeElGamalEncrypt (F : PrimeOrderGroupFamily) (d : F.Desc) (a b : ℕ) (m : F.Carrier d) : F.decodeElGamal (d, a, (F.encodeElGamalEncrypt (d, F.encodeElGamalPublicKey (d, a), F.encode d m, b)).1, (F.encodeElGamalEncrypt (d, F.encodeElGamalPublicKey (d, a), F.encode d m, b)).2) = F.encode d m

Word-level ElGamal decryption of encodeElGamalEncrypt under encodeElGamalPublicKey recovers the encoded message.

theorem Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_decodeElGamal (F : PrimeOrderGroupFamily) : Turing.MultiTapeTM.ComputableInPolyTime F.decodeElGamal (Turing.MultiTapeTM.encPair F.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) Turing.MultiTapeTM.encBits

Encoded ElGamal decryption is computable in polynomial time.

Shared typed-message ElGamal IND-CPA reduction ([BS23], Exercise 11.5(a))

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.elGamalMsgCPAGameOn (F : PrimeOrderGroupFamily) {Msg : Type} (valid : ℕ → List Bool → Msg → Msg → Bool) (encodeMsg : F.Desc → Msg → List Bool) (setup : ℕ → PMF F.Desc) (adversary : Encryption.AdversaryOf Msg) (bit : Bool) (n : ℕ) : Game

The IND-CPA experiment for multiplicative ElGamal encryption over message type Msg via a word-level message encoder encodeMsg : F.Desc → Msg → List Bool, with challenge-pair admissibility predicate valid ([BS23], Exercise 11.5(a), p. 459, played in Attack Game 11.1, p. 436): draw d ← setup n and a uniform secret key α : ZMod (F.order d), and pass the encoded public key pk = (d, encode (α • g)) to adversary.choose. If valid n pk m₀ m₁ holds, encrypt the selected message m under a fresh uniform exponent β : ZMod (F.order d) via F.add (d, encode ((α * β) • g), encodeMsg d m) and pass the saved state and encoded ciphertext to adversary.guess; otherwise output false, in both experiments, as Encryption.gameOn does.

def Cslib.Crypto.PrimeOrderGroupFamily.elGamalMsgToDDHDistinguisher (F : PrimeOrderGroupFamily) {Msg : Type} (valid : ℕ → List Bool → Msg → Msg → Bool) (encodeMsg : F.Desc → Msg → List Bool) (adversary : Encryption.AdversaryOf Msg) (bit : Bool) (n : ℕ) (input : F.Desc × List Bool × List Bool × List Bool) : ProbComp Bool

The DDH distinguisher constructed from a typed-message ElGamal IND-CPA adversary ([BS23], Exercise 11.5(a), p. 459): given (d, u, v, w), pass pk = (d, u) as the public key; if valid n pk m₀ m₁ holds, mask the selected encoded message encodeMsg d m with w using F.add and return the adversary's guess, and otherwise return false.

theorem Cslib.Crypto.PrimeOrderGroupFamily.ddhRealGame_elGamalMsgToDDHDistinguisher (F : PrimeOrderGroupFamily) {Msg : Type} (valid : ℕ → List Bool → Msg → Msg → Bool) (encodeMsg : F.Desc → Msg → List Bool) (setup : ℕ → PMF F.Desc) (adversary : Encryption.AdversaryOf Msg) (bit : Bool) (n : ℕ) : F.ddhRealGame setup (F.elGamalMsgToDDHDistinguisher valid encodeMsg adversary bit) n = F.elGamalMsgCPAGameOn valid encodeMsg setup adversary bit n

In the real DDH game, elGamalMsgToDDHDistinguisher simulates elGamalMsgCPAGameOn exactly.

def Cslib.Crypto.PrimeOrderGroupFamily.AdmitsGroupElements (F : PrimeOrderGroupFamily) {Msg : Type} (encodeMsg : F.Desc → Msg → List Bool) (valid : ℕ → List Bool → Msg → Msg → Bool) : Prop

The admissibility predicate valid admits only group elements under encodeMsg: at every public key (d, u), an admissible pair (m₀, m₁) has both encodeMsg d m₀ and encodeMsg d m₁ in Set.range (F.encode d).

theorem Cslib.Crypto.PrimeOrderGroupFamily.ddhIdealGame_elGamalMsgToDDHDistinguisher_false_eq_true (F : PrimeOrderGroupFamily) {Msg : Type} (valid : ℕ → List Bool → Msg → Msg → Bool) (encodeMsg : F.Desc → Msg → List Bool) (setup : ℕ → PMF F.Desc) (adversary : Encryption.AdversaryOf Msg) (n : ℕ) (hsound : F.AdmitsGroupElements encodeMsg valid) : F.ddhIdealGame setup (F.elGamalMsgToDDHDistinguisher valid encodeMsg adversary false) n = F.ddhIdealGame setup (F.elGamalMsgToDDHDistinguisher valid encodeMsg adversary true) n

When valid admits only group elements under encodeMsg, the uniform element γ • g of the ideal DDH game perfectly masks both admissible candidate messages, so the experiments for bit = false and bit = true are identical.

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_elGamalMsgCPAGameOn_le (F : PrimeOrderGroupFamily) {Msg : Type} (valid : ℕ → List Bool → Msg → Msg → Bool) (encodeMsg : F.Desc → Msg → List Bool) (setup : ℕ → PMF F.Desc) (adversary : Encryption.AdversaryOf Msg) (n : ℕ) (hsound : F.AdmitsGroupElements encodeMsg valid) : (F.elGamalMsgCPAGameOn valid encodeMsg setup adversary false n).advantage (F.elGamalMsgCPAGameOn valid encodeMsg setup adversary true n) ≤ (F.ddhRealGame setup (F.elGamalMsgToDDHDistinguisher valid encodeMsg adversary false) n).advantage (F.ddhIdealGame setup (F.elGamalMsgToDDHDistinguisher valid encodeMsg adversary false) n) + (F.ddhRealGame setup (F.elGamalMsgToDDHDistinguisher valid encodeMsg adversary true) n).advantage (F.ddhIdealGame setup (F.elGamalMsgToDDHDistinguisher valid encodeMsg adversary true) n)

Quantitative reduction of typed-message ElGamal IND-CPA to DDH ([BS23], Exercise 11.5(a), p. 459): when valid admits only group elements under encodeMsg, the IND-CPA distinguishing advantage of adversary is bounded by the sum of the DDH advantages of elGamalMsgToDDHDistinguisher valid encodeMsg adversary false and elGamalMsgToDDHDistinguisher valid encodeMsg adversary true.

theorem Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_elGamalMsgToDDHDistinguisher (F : PrimeOrderGroupFamily) {Msg : Type} {encMsg : Msg ↪ List Bool} {valid : ℕ → List Bool → Msg → Msg → Bool} (hvalid : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × Msg × Msg) => valid p.1 p.2.1 p.2.2.1 p.2.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair encMsg encMsg))) Turing.MultiTapeTM.encBool) {encodeMsg : F.Desc → Msg → List Bool} (hencMsg : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : F.Desc × Msg) => encodeMsg p.1 p.2) (Turing.MultiTapeTM.encPair F.encDesc encMsg) Turing.MultiTapeTM.encBits) {adversary : Encryption.AdversaryOf Msg} (hA : Encryption.AdversaryOf.IsPPT encMsg adversary) (bit : Bool) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair F.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)))) Turing.MultiTapeTM.encBool fun (input : ℕ × F.Desc × List Bool × List Bool × List Bool) => F.elGamalMsgToDDHDistinguisher valid encodeMsg adversary bit input.1 input.2

elGamalMsgToDDHDistinguisher is uniform strict PPT whenever valid and encodeMsg are computable in polynomial time and adversary is uniform strict PPT.

theorem Cslib.Crypto.PrimeOrderGroupFamily.DDH.negligible_elGamalMsgCPAGameOn {F : PrimeOrderGroupFamily} {setup : ℕ → PMF F.Desc} {Msg : Type} {encMsg : Msg ↪ List Bool} {valid : ℕ → List Bool → Msg → Msg → Bool} {encodeMsg : F.Desc → Msg → List Bool} (hDDH : F.DDH setup) (hvalid : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × Msg × Msg) => valid p.1 p.2.1 p.2.2.1 p.2.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair encMsg encMsg))) Turing.MultiTapeTM.encBool) (hsound : F.AdmitsGroupElements encodeMsg valid) (hencMsg : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : F.Desc × Msg) => encodeMsg p.1 p.2) (Turing.MultiTapeTM.encPair F.encDesc encMsg) Turing.MultiTapeTM.encBits) {adversary : Encryption.AdversaryOf Msg} (hA : Encryption.AdversaryOf.IsPPT encMsg adversary) : Negligible fun (n : ℕ) => (F.elGamalMsgCPAGameOn valid encodeMsg setup adversary false n).advantage (F.elGamalMsgCPAGameOn valid encodeMsg setup adversary true n)

Typed-message ElGamal encryption is IND-CPA secure under the DDH assumption ([BS23], Exercise 11.5(a), p. 459): for a polynomial-time admissibility predicate valid that admits only group elements under encodeMsg, every uniform strict PPT adversary has negligible advantage in elGamalMsgCPAGameOn valid encodeMsg.

Bit encryption and IND-CPA security under DDH

def Cslib.Crypto.PrimeOrderGroupFamily.bitElement (F : PrimeOrderGroupFamily) (d : F.Desc) (b : Bool) : F.Carrier d

Embed a message bit b : Bool into F.Carrier d as 0 (for false) or g (for true).

theorem Cslib.Crypto.PrimeOrderGroupFamily.bitElement_injective (F : PrimeOrderGroupFamily) (d : F.Desc) : Function.Injective (F.bitElement d)

Distinct message bits map to distinct group elements.

def Cslib.Crypto.PrimeOrderGroupFamily.encodeBit (F : PrimeOrderGroupFamily) (d : F.Desc) (b : Bool) : List Bool

Encode a message bit b : Bool as an encoded element of F.Carrier d using F.smul.

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.encodeBit_eq_encode_bitElement (F : PrimeOrderGroupFamily) (d : F.Desc) (b : Bool) : F.encodeBit d b = F.encode d (F.bitElement d b)

encodeBit computes the group encoding of bitElement.

theorem Cslib.Crypto.PrimeOrderGroupFamily.admitsGroupElements_encodeBit (F : PrimeOrderGroupFamily) : F.AdmitsGroupElements F.encodeBit fun (x : ℕ) (x_1 : List Bool) (x_2 x_3 : Bool) => true

Every pair of bit messages encodes group elements, so the always-true predicate admits only group elements under encodeBit.

theorem Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_encodeBit (F : PrimeOrderGroupFamily) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : F.Desc × Bool) => F.encodeBit p.1 p.2) (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBool) Turing.MultiTapeTM.encBits

encodeBit is computable in polynomial time from the group description and the bit.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.elGamalCPAGame (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (adversary : Encryption.Adversary) (bit : Bool) (n : ℕ) : Game

The IND-CPA experiment for ElGamal bit encryption ([BS23], Exercise 11.5, p. 459): draw d from setup n and a uniform secret key α : ZMod (F.order d), pass the encoded public key (d, encode (α • g)) to adversary.choose, encrypt the selected challenge bit under a fresh uniform exponent β : ZMod (F.order d), and pass the saved state and encoded ciphertext to adversary.guess.

theorem Cslib.Crypto.PrimeOrderGroupFamily.elGamalCPAGame_eq_elGamalMsgCPAGameOn (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (adversary : Encryption.Adversary) (bit : Bool) (n : ℕ) : F.elGamalCPAGame setup adversary bit n = F.elGamalMsgCPAGameOn (fun (x : ℕ) (x_1 : List Bool) (x_2 x_3 : Bool) => true) F.encodeBit setup adversary bit n

elGamalCPAGame is the unrestricted encodeBit specialization of elGamalMsgCPAGameOn.

def Cslib.Crypto.PrimeOrderGroupFamily.elGamalINDCPA (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) : Prop

IND-CPA security of ElGamal bit encryption over F for a setup law setup: every uniform strict PPT Encryption.Adversary has negligible distinguishing advantage between challenge bit false and challenge bit true.

@[reducible, inline]

abbrev Cslib.Crypto.PrimeOrderGroupFamily.elGamalToDDHDistinguisher (F : PrimeOrderGroupFamily) (adversary : Encryption.Adversary) (bit : Bool) (n : ℕ) (input : F.Desc × List Bool × List Bool × List Bool) : ProbComp Bool

The DDH distinguisher constructed from an IND-CPA adversary ([BS23], proof of Exercise 11.5(a), p. 459): given (d, u, v, w), pass (d, u) as the public key, encrypt the selected challenge bit by masking with w, and return the adversary's guess.

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.ddhRealGame_elGamalToDDHDistinguisher (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (adversary : Encryption.Adversary) (bit : Bool) (n : ℕ) : F.ddhRealGame setup (F.elGamalToDDHDistinguisher adversary bit) n = F.elGamalCPAGame setup adversary bit n

In the real DDH game, elGamalToDDHDistinguisher simulates elGamalCPAGame exactly.

theorem Cslib.Crypto.PrimeOrderGroupFamily.ddhIdealGame_elGamalToDDHDistinguisher_false_eq_true (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (adversary : Encryption.Adversary) (n : ℕ) : F.ddhIdealGame setup (F.elGamalToDDHDistinguisher adversary false) n = F.ddhIdealGame setup (F.elGamalToDDHDistinguisher adversary true) n

In the ideal DDH game, the uniform element γ • g perfectly masks the challenge bit, so the experiments for bit = false and bit = true are identical.

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_elGamalCPAGame_le (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (adversary : Encryption.Adversary) (n : ℕ) : (F.elGamalCPAGame setup adversary false n).advantage (F.elGamalCPAGame setup adversary true n) ≤ (F.ddhRealGame setup (F.elGamalToDDHDistinguisher adversary false) n).advantage (F.ddhIdealGame setup (F.elGamalToDDHDistinguisher adversary false) n) + (F.ddhRealGame setup (F.elGamalToDDHDistinguisher adversary true) n).advantage (F.ddhIdealGame setup (F.elGamalToDDHDistinguisher adversary true) n)

Quantitative reduction of ElGamal IND-CPA to DDH ([BS23], Exercise 11.5(a), p. 459): the IND-CPA distinguishing advantage of adversary is bounded by the sum of the DDH advantages of elGamalToDDHDistinguisher adversary false and elGamalToDDHDistinguisher adversary true.

theorem Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_elGamalToDDHDistinguisher (F : PrimeOrderGroupFamily) {adversary : Encryption.Adversary} (hA : adversary.IsPPT) (bit : Bool) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair F.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)))) Turing.MultiTapeTM.encBool fun (input : ℕ × F.Desc × List Bool × List Bool × List Bool) => F.elGamalToDDHDistinguisher adversary bit input.1 input.2

elGamalToDDHDistinguisher is uniform strict PPT whenever adversary is.

theorem Cslib.Crypto.PrimeOrderGroupFamily.DDH.elGamalINDCPA {F : PrimeOrderGroupFamily} {setup : ℕ → PMF F.Desc} (hDDH : F.DDH setup) : F.elGamalINDCPA setup

ElGamal bit encryption is IND-CPA secure under the DDH assumption ([BS23], Exercise 11.5(a), p. 459).

Group-element ElGamal IND-CPA security under DDH

@[reducible, inline]

noncomputable abbrev Cslib.Crypto.PrimeOrderGroupFamily.elGamalGroupCPAGameOn (F : PrimeOrderGroupFamily) (valid : ℕ → List Bool → List Bool → List Bool → Bool) (setup : ℕ → PMF F.Desc) (adversary : Encryption.WordAdversary) (bit : Bool) (n : ℕ) : Game

The IND-CPA experiment for group-element ElGamal encryption with challenge-pair admissibility predicate valid ([BS23], Exercise 11.5(a), p. 459): specialization of elGamalMsgCPAGameOn to word messages (Encryption.WordAdversary) with identity message encoding. The message space of Exercise 11.5 is the group, so valid is meant to admit only encoded group elements (AdmitsGroupElements (fun _ m => m) valid).

@[reducible, inline]

abbrev Cslib.Crypto.PrimeOrderGroupFamily.elGamalGroupToDDHDistinguisher (F : PrimeOrderGroupFamily) (valid : ℕ → List Bool → List Bool → List Bool → Bool) (adversary : Encryption.WordAdversary) (bit : Bool) (n : ℕ) (input : F.Desc × List Bool × List Bool × List Bool) : ProbComp Bool

The DDH distinguisher constructed from a group-element ElGamal IND-CPA adversary ([BS23], Exercise 11.5(a), p. 459): specialization of elGamalMsgToDDHDistinguisher to identity message encoding.

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_elGamalGroupCPAGameOn_le (F : PrimeOrderGroupFamily) (valid : ℕ → List Bool → List Bool → List Bool → Bool) (setup : ℕ → PMF F.Desc) (adversary : Encryption.WordAdversary) (n : ℕ) (hsound : F.AdmitsGroupElements (fun (x : F.Desc) (m : List Bool) => m) valid) : (F.elGamalGroupCPAGameOn valid setup adversary false n).advantage (F.elGamalGroupCPAGameOn valid setup adversary true n) ≤ (F.ddhRealGame setup (F.elGamalGroupToDDHDistinguisher valid adversary false) n).advantage (F.ddhIdealGame setup (F.elGamalGroupToDDHDistinguisher valid adversary false) n) + (F.ddhRealGame setup (F.elGamalGroupToDDHDistinguisher valid adversary true) n).advantage (F.ddhIdealGame setup (F.elGamalGroupToDDHDistinguisher valid adversary true) n)

Quantitative reduction of group-element ElGamal IND-CPA to DDH ([BS23], Exercise 11.5(a), p. 459): when valid admits only encoded group elements, the IND-CPA distinguishing advantage of adversary is bounded by the sum of the DDH advantages of elGamalGroupToDDHDistinguisher valid adversary false and elGamalGroupToDDHDistinguisher valid adversary true.

theorem Cslib.Crypto.PrimeOrderGroupFamily.DDH.negligible_elGamalGroupCPAGameOn {F : PrimeOrderGroupFamily} {setup : ℕ → PMF F.Desc} {valid : ℕ → List Bool → List Bool → List Bool → Bool} (hDDH : F.DDH setup) (hvalid : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool × List Bool) => valid p.1 p.2.1 p.2.2.1 p.2.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) Turing.MultiTapeTM.encBool) (hsound : F.AdmitsGroupElements (fun (x : F.Desc) (m : List Bool) => m) valid) {adversary : Encryption.WordAdversary} (hA : adversary.IsPPT) : Negligible fun (n : ℕ) => (F.elGamalGroupCPAGameOn valid setup adversary false n).advantage (F.elGamalGroupCPAGameOn valid setup adversary true n)

Group-element ElGamal encryption is IND-CPA secure under the DDH assumption ([BS23], Exercise 11.5(a), p. 459): for a polynomial-time admissibility predicate valid that admits only encoded group elements, every uniform strict PPT Encryption.WordAdversary has negligible advantage in elGamalGroupCPAGameOn valid.

Hashed ElGamal encryption and IND-CPA security ([BS23], Section 11.5)

def Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalEncrypt (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (d : F.Desc) (u : F.Carrier d) (m : List Bool) (β : ZMod (F.order d)) : F.Carrier d × List Bool

Algebraic Hashed ElGamal encryption ([BS23], Section 11.5, pp. 445–446, Remark 11.1): given key-derivation hash function H : F.Desc × List Bool → List Bool, public key u : F.Carrier d, message word m : List Bool, and randomness β : ZMod (F.order d), derive pad = H (d, encode (β • u)) and output (β • g, Cslib.BitString.listXor pad.length [pad, m]).

theorem Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalEncrypt_smul_generator (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (d : F.Desc) (α β : ZMod (F.order d)) (m : List Bool) : F.hashedElGamalEncrypt H d (α • F.generator d) m β = have pad := H (d, F.encode d ((α * β) • F.generator d)); (β • F.generator d, BitString.listXor pad.length [pad, m])

Under a genuine public key u = α • g, Hashed ElGamal masks m with pad = H (d, encode ((α * β) • g)) via Cslib.BitString.listXor pad.length [pad, m].

def Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalDecrypt (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (d : F.Desc) (α : ZMod (F.order d)) (ct : F.Carrier d × List Bool) : List Bool

Algebraic Hashed ElGamal decryption ([BS23], Section 11.5, pp. 445–446, Remark 11.1): given secret key α : ZMod (F.order d) and ciphertext (v, c), derive pad = H (d, encode (α • v)) and recover Cslib.BitString.listXor pad.length [pad, c].

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalDecrypt_hashedElGamalEncrypt (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (d : F.Desc) (α β : ZMod (F.order d)) {m : List Bool} (hlen : m.length = (H (d, F.encode d ((α * β) • F.generator d))).length) : F.hashedElGamalDecrypt H d α (F.hashedElGamalEncrypt H d (α • F.generator d) m β) = m

Hashed ElGamal decryption correctness: when the message word m has the same length as the derived pad H (d, encode ((α * β) • g)), decrypting an encryption under u = α • g with secret key α recovers m.

def Cslib.Crypto.PrimeOrderGroupFamily.encodeHashedElGamalEncrypt (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (input : F.Desc × List Bool × List Bool × ℕ) : List Bool × List Bool

Word-level Hashed ElGamal encryption: given (d, encode u, m, b), derive pad = H (d, encode (b • u)) and compute (encode (b • g), Cslib.BitString.listXor pad.length [pad, m]).

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.encodeHashedElGamalEncrypt_encode (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (d : F.Desc) (u : F.Carrier d) (m : List Bool) (b : ℕ) : F.encodeHashedElGamalEncrypt H (d, F.encode d u, m, b) = (F.encode d (F.hashedElGamalEncrypt H d u m ↑b).1, (F.hashedElGamalEncrypt H d u m ↑b).2)

encodeHashedElGamalEncrypt evaluates hashedElGamalEncrypt on encoded group elements.

theorem Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_encodeHashedElGamalEncrypt (F : PrimeOrderGroupFamily) {H : F.Desc × List Bool → List Bool} (hH : Turing.MultiTapeTM.ComputableInPolyTime H (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (F.encodeHashedElGamalEncrypt H) (Turing.MultiTapeTM.encPair F.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encNat))) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)

Word-level Hashed ElGamal encryption is computable in polynomial time whenever H is.

def Cslib.Crypto.PrimeOrderGroupFamily.decodeHashedElGamal (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (input : F.Desc × ℕ × List Bool × List Bool) : List Bool

Word-level Hashed ElGamal decryption: given (d, a, encode v, c), derive pad = H (d, encode (a • v)) and compute Cslib.BitString.listXor pad.length [pad, c].

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.decodeHashedElGamal_encode (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (d : F.Desc) (a : ℕ) (v : F.Carrier d) (c : List Bool) : F.decodeHashedElGamal H (d, a, F.encode d v, c) = F.hashedElGamalDecrypt H d ↑a (v, c)

decodeHashedElGamal computes hashedElGamalDecrypt on encoded group elements.

theorem Cslib.Crypto.PrimeOrderGroupFamily.decodeHashedElGamal_hashedElGamalEncrypt (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (d : F.Desc) (a : ℕ) (β : ZMod (F.order d)) {m : List Bool} (hlen : m.length = (H (d, F.encode d ((↑a * β) • F.generator d))).length) : F.decodeHashedElGamal H (d, a, F.encode d (F.hashedElGamalEncrypt H d (↑a • F.generator d) m β).1, (F.hashedElGamalEncrypt H d (↑a • F.generator d) m β).2) = m

Word-level Hashed ElGamal decryption of an honest encryption recovers m whenever m has the same length as the derived pad.

theorem Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_decodeHashedElGamal (F : PrimeOrderGroupFamily) {H : F.Desc × List Bool → List Bool} (hH : Turing.MultiTapeTM.ComputableInPolyTime H (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (F.decodeHashedElGamal H) (Turing.MultiTapeTM.encPair F.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) Turing.MultiTapeTM.encBits

Word-level Hashed ElGamal decryption is computable in polynomial time whenever H is.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalCPAGame (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (adversary : Encryption.WordAdversary) (bit : Bool) (n : ℕ) : Game

The IND-CPA experiment for Hashed ElGamal encryption ([BS23], Section 11.5, pp. 445–446, Remark 11.1, and Section 11.5.2, Theorem 11.5, pp. 449–451): draw d ← setup n and a uniform secret key α : ZMod (F.order d), pass the encoded public key (d, encode (α • g)) to adversary.choose, encrypt the selected message word m under a fresh uniform exponent β : ZMod (F.order d) by masking with pad = H (d, encode ((α * β) • g)) via Cslib.BitString.listXor pad.length [pad, m], and pass the saved state and encoded ciphertext to adversary.guess.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalIdealDDHGame (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (adversary : Encryption.WordAdversary) (bit : Bool) (n : ℕ) : Game

Hybrid 1 for Hashed ElGamal ([BS23], Section 11.5.2, proof of Theorem 11.5, pp. 449–451): replace the Diffie–Hellman shared element (α * β) • g with an independent uniform group element γ • g.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalUniformPadGame (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (msgLen : ℕ → ℕ) (adversary : Encryption.WordAdversary) (bit : Bool) (n : ℕ) : Game

Hybrid 2 for Hashed ElGamal ([BS23], Section 11.5.2, proof of Theorem 11.5, pp. 449–451): replace the derived key H (d, encode (γ • g)) with an independent uniform msgLen n-bit key pad ← Cslib.BitString.uniformList (msgLen n).

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.kdfRealGame (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (distinguisher : ℕ → F.Desc × List Bool × List Bool × List Bool → ProbComp Bool) (n : ℕ) : Game

The real key-derivation security experiment ([BS23], Section 11.5.2, Attack Game 11.3, Experiment 0, p. 448): draw d ← setup n and independent uniform α, β, γ : ZMod (F.order d), and give the distinguisher (d, encode (α • g), encode (β • g), H (d, encode (γ • g))).

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.kdfIdealGame (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (msgLen : ℕ → ℕ) (distinguisher : ℕ → F.Desc × List Bool × List Bool × List Bool → ProbComp Bool) (n : ℕ) : Game

The ideal key-derivation security experiment ([BS23], Section 11.5.2, Attack Game 11.3, Experiment 1, p. 448): draw d ← setup n, independent uniform α, β : ZMod (F.order d), and an independent uniform msgLen n-bit key pad ← Cslib.BitString.uniformList (msgLen n), and give the distinguisher (d, encode (α • g), encode (β • g), pad).

def Cslib.Crypto.PrimeOrderGroupFamily.SecureKDF (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (msgLen : ℕ → ℕ) : Prop

Secure key derivation for H over F ([BS23], Section 11.5.2, Attack Game 11.3, p. 448, and Definition 11.5, p. 449): every uniform strict PPT distinguisher has negligible advantage between kdfRealGame and kdfIdealGame. No nondegenerate SecureKDF instance (msgLen n > 0, e.g., via the leftover hash lemma) is constructed in this module.

def Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalToDDHDistinguisher (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (adversary : Encryption.WordAdversary) (bit : Bool) (n : ℕ) (input : F.Desc × List Bool × List Bool × List Bool) : ProbComp Bool

The DDH distinguisher constructed from a Hashed ElGamal IND-CPA adversary ([BS23], Section 11.5.2, proof of Theorem 11.5, pp. 449–451): given (d, u, v, w), pass (d, u) as the public key, mask the selected message word with pad = H (d, w) via Cslib.BitString.listXor pad.length [pad, m], and return the adversary's guess.

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.ddhRealGame_hashedElGamalToDDHDistinguisher (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (adversary : Encryption.WordAdversary) (bit : Bool) (n : ℕ) : F.ddhRealGame setup (F.hashedElGamalToDDHDistinguisher H adversary bit) n = F.hashedElGamalCPAGame setup H adversary bit n

In the real DDH game, hashedElGamalToDDHDistinguisher simulates hashedElGamalCPAGame exactly.

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.ddhIdealGame_hashedElGamalToDDHDistinguisher (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (adversary : Encryption.WordAdversary) (bit : Bool) (n : ℕ) : F.ddhIdealGame setup (F.hashedElGamalToDDHDistinguisher H adversary bit) n = F.hashedElGamalIdealDDHGame setup H adversary bit n

In the ideal DDH game, hashedElGamalToDDHDistinguisher simulates hashedElGamalIdealDDHGame exactly.

theorem Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_hashedElGamalToDDHDistinguisher (F : PrimeOrderGroupFamily) {H : F.Desc × List Bool → List Bool} (hH : Turing.MultiTapeTM.ComputableInPolyTime H (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) {adversary : Encryption.WordAdversary} (hA : adversary.IsPPT) (bit : Bool) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair F.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)))) Turing.MultiTapeTM.encBool fun (input : ℕ × F.Desc × List Bool × List Bool × List Bool) => F.hashedElGamalToDDHDistinguisher H adversary bit input.1 input.2

hashedElGamalToDDHDistinguisher is uniform strict PPT whenever H is polynomial time and adversary is uniform strict PPT.

def Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalToKDFDistinguisher (F : PrimeOrderGroupFamily) (adversary : Encryption.WordAdversary) (bit : Bool) (n : ℕ) (input : F.Desc × List Bool × List Bool × List Bool) : ProbComp Bool

The KDF distinguisher constructed from a Hashed ElGamal IND-CPA adversary ([BS23], Section 11.5.2, proof of Theorem 11.5, pp. 449–451): given (d, u, v, pad), pass (d, u) as the public key, mask the selected message word with pad via Cslib.BitString.listXor pad.length [pad, m], and return the adversary's guess.

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.kdfRealGame_hashedElGamalToKDFDistinguisher (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (adversary : Encryption.WordAdversary) (bit : Bool) (n : ℕ) : F.kdfRealGame setup H (F.hashedElGamalToKDFDistinguisher adversary bit) n = F.hashedElGamalIdealDDHGame setup H adversary bit n

In the real KDF game, hashedElGamalToKDFDistinguisher simulates hashedElGamalIdealDDHGame exactly.

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.kdfIdealGame_hashedElGamalToKDFDistinguisher (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (msgLen : ℕ → ℕ) (adversary : Encryption.WordAdversary) (bit : Bool) (n : ℕ) : F.kdfIdealGame setup msgLen (F.hashedElGamalToKDFDistinguisher adversary bit) n = F.hashedElGamalUniformPadGame setup msgLen adversary bit n

In the ideal KDF game, hashedElGamalToKDFDistinguisher simulates hashedElGamalUniformPadGame exactly.

theorem Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_hashedElGamalToKDFDistinguisher (F : PrimeOrderGroupFamily) {adversary : Encryption.WordAdversary} (hA : adversary.IsPPT) (bit : Bool) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair F.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)))) Turing.MultiTapeTM.encBool fun (input : ℕ × F.Desc × List Bool × List Bool × List Bool) => F.hashedElGamalToKDFDistinguisher adversary bit input.1 input.2

hashedElGamalToKDFDistinguisher is uniform strict PPT whenever adversary is.

theorem Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalUniformPadGame_false_eq_true (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (msgLen : ℕ → ℕ) (adversary : Encryption.WordAdversary) (n : ℕ) : F.hashedElGamalUniformPadGame setup msgLen adversary false n = F.hashedElGamalUniformPadGame setup msgLen adversary true n

In hashedElGamalUniformPadGame, the uniform msgLen n-bit pad masks any challenge message word perfectly via Cslib.BitString.listXor pad.length [pad, m], so the experiments for bit = false and bit = true are identical.

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_hashedElGamalCPAGame_le (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (msgLen : ℕ → ℕ) (adversary : Encryption.WordAdversary) (n : ℕ) : (F.hashedElGamalCPAGame setup H adversary false n).advantage (F.hashedElGamalCPAGame setup H adversary true n) ≤ (F.ddhRealGame setup (F.hashedElGamalToDDHDistinguisher H adversary false) n).advantage (F.ddhIdealGame setup (F.hashedElGamalToDDHDistinguisher H adversary false) n) + (F.kdfRealGame setup H (F.hashedElGamalToKDFDistinguisher adversary false) n).advantage (F.kdfIdealGame setup msgLen (F.hashedElGamalToKDFDistinguisher adversary false) n) + (F.kdfRealGame setup H (F.hashedElGamalToKDFDistinguisher adversary true) n).advantage (F.kdfIdealGame setup msgLen (F.hashedElGamalToKDFDistinguisher adversary true) n) + (F.ddhRealGame setup (F.hashedElGamalToDDHDistinguisher H adversary true) n).advantage (F.ddhIdealGame setup (F.hashedElGamalToDDHDistinguisher H adversary true) n)

Quantitative reduction of Hashed ElGamal IND-CPA to DDH and SecureKDF ([BS23], Section 11.5.2, Theorem 11.5, pp. 449–451): the IND-CPA distinguishing advantage of adversary is bounded by the sum of the two DDH advantages of hashedElGamalToDDHDistinguisher and the two KDF advantages of hashedElGamalToKDFDistinguisher.

theorem Cslib.Crypto.PrimeOrderGroupFamily.DDH.negligible_hashedElGamalCPAGame {F : PrimeOrderGroupFamily} {setup : ℕ → PMF F.Desc} {H : F.Desc × List Bool → List Bool} {msgLen : ℕ → ℕ} (hDDH : F.DDH setup) (hKDF : F.SecureKDF setup H msgLen) (hH : Turing.MultiTapeTM.ComputableInPolyTime H (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) {adversary : Encryption.WordAdversary} (hA : adversary.IsPPT) : Negligible fun (n : ℕ) => (F.hashedElGamalCPAGame setup H adversary false n).advantage (F.hashedElGamalCPAGame setup H adversary true n)

Hashed ElGamal encryption is IND-CPA secure under DDH and SecureKDF ([BS23], Section 11.5.2, Theorem 11.5, pp. 449–451): when H is computable in polynomial time, every uniform strict PPT Encryption.WordAdversary has negligible IND-CPA distinguishing advantage. Note that SecureKDF is assumed as a hypothesis; no nondegenerate SecureKDF instance (msgLen n > 0) is constructed in this module.