General-Cipher Hashed ElGamal ([BS23], Section 11.5, Theorem 11.5)

This module generalizes Hashed ElGamal ([BS23], Section 11.5, pp. 445–446, Remark 11.1, and Section 11.5.2, Theorem 11.5, pp. 448–451) from the one-time pad specialization in Complexity/Crypto/Computational/ElGamal.lean to an arbitrary semantically secure symmetric cipher $\mathcal{E}_s$.

• Paraphrase of [BS23], Section 11.5 (p. 445) and Remark 11.1 (p. 446): over a cyclic group $G$ of prime order $q$ with generator $g$, a symmetric cipher $\mathcal{E}_s = (E_s, D_s)$ over $(\mathcal{K}, \mathcal{M}, \mathcal{C})$, and a key-derivation hash function $H$, key generation samples $\alpha \leftarrow \mathbb{Z}_q$ and outputs $(pk = \alpha \cdot g, sk = \alpha)$. In the $\mathcal{E}'_{\mathrm{EG}}$ variant of Remark 11.1 (which derives $k$ from $w = \beta \cdot u$ alone), encryption of $m \in \mathcal{M}$ under $pk = u$ samples $\beta \leftarrow \mathbb{Z}_q$, sets $v = \beta \cdot g$, $w = \beta \cdot u$, $k = H(w)$, $c \leftarrow E_s(k, m)$, and outputs $(v, c)$; decryption of $(v, c)$ under $sk = \alpha$ sets $w = \alpha \cdot v$, $k = H(w)$, and outputs $D_s(k, c)$.
• Paraphrase of [BS23], Section 11.5.2, Theorem 11.5 and Equation (11.14) (pp. 449–451): if DDH holds for $G$, $H$ is a secure KDF, and $\mathcal{E}_s$ is semantically secure, then Hashed ElGamal is semantically secure; for every CPA adversary $\mathcal{A}$ there exist elementary wrapper adversaries $\mathcal{B}_{\mathrm{ddh}}$, $\mathcal{B}_{\mathrm{kdf}}$, and $\mathcal{B}_s$ such that $\mathrm{SSadv}[\mathcal{A}, \mathcal{E}_{\mathrm{EG}}] \le 2 \cdot \mathrm{DDHadv}[\mathcal{B}_{\mathrm{ddh}}, G] + 2 \cdot \mathrm{KDFadv}[\mathcal{B}_{\mathrm{kdf}}, H] + \mathrm{SSadv}[\mathcal{B}_s, \mathcal{E}_s]$.

Main definitions

• Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalCipherEncrypt, Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalCipherDecrypt, Cslib.Crypto.PrimeOrderGroupFamily.encodeHashedElGamalCipherEncrypt, Cslib.Crypto.PrimeOrderGroupFamily.decodeHashedElGamalCipher: algebraic and word-level Hashed ElGamal encryption and decryption with a general symmetric cipher ([BS23], Section 11.5, pp. 445–446, Remark 11.1).
• Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalCipherCPAGameOn, Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalCipherCPAGame, Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalCipherIdealDDHGameOn, Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalCipherUniformKeyGameOn: PMF-level IND-CPA experiments and hybrids for general-cipher Hashed ElGamal ([BS23], Section 11.5.2, Theorem 11.5, pp. 449–451).
• Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalCipherToDDHDistinguisher, Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalCipherToDDHHiddenBitDistinguisher, Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalCipherToKDFDistinguisher, Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalCipherToKDFHiddenBitDistinguisher, Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalCipherToDEMAdversary, Cslib.Crypto.PrimeOrderGroupFamily.seededSetupProb: per-bit and hidden-bit DDH and KDF reductions, symmetric-cipher (DEMOneTimeINDCPAOn) reduction adversary, and executable seeded setup sampler for Theorem 11.5 ([BS23], Section 11.5.2, pp. 449–451).

Main results

• Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalCipherDecrypt_hashedElGamalCipherEncrypt, Cslib.Crypto.PrimeOrderGroupFamily.decodeHashedElGamalCipher_hashedElGamalCipherEncrypt: decryption correctness for general-cipher Hashed ElGamal.
• Cslib.Crypto.PrimeOrderGroupFamily.advantage_hashedElGamalCipherCPAGameOn_le, Cslib.Crypto.PrimeOrderGroupFamily.advantage_hashedElGamalCipherCPAGameOn_le_two_mul, Cslib.Crypto.PrimeOrderGroupFamily.advantage_hashedElGamalCipherUniformKeyGameOn_le_demGameOn, Cslib.Crypto.PrimeOrderGroupFamily.advantage_hashedElGamalCipherCPAGameOn_le_demGameOn: two-distinguisher and single hidden-bit distinguisher quantitative bounds for Theorem 11.5 (matching Equation (11.14) of [BS23], p. 449), together with the native approximate-sampling (sampleExp, adding 4 / 2 ^ n) bridge to standalone symmetric-cipher security (Encryption.demGameOn).
• Cslib.Crypto.PrimeOrderGroupFamily.DDH.negligible_hashedElGamalCipherCPAGameOn and its DEMOneTimeINDCPAOn / linearHashKDF specializations (negligible_hashedElGamalCipherCPAGameOn_of_demOneTimeINDCPAOn, negligible_hashedElGamalCipherCPAGameOn_linearHashKDF): Theorem 11.5 IND-CPA security in hashedElGamalCipherCPAGameOn from DDH, SecureKDF, and DEMOneTimeINDCPAOn, plus unconditional KDF instantiation via linearHashKDF.

References

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

Algebraic and word-level general-cipher Hashed ElGamal ([BS23], Section 11.5)

def Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalCipherEncrypt (F : PrimeOrderGroupFamily) {Msg Cipher : Type} (H : F.Desc × List Bool → List Bool) (encSym : List Bool → Msg → Cipher) (d : F.Desc) (u : F.Carrier d) (m : Msg) (β : ZMod (F.order d)) : F.Carrier d × Cipher

Algebraic Hashed ElGamal encryption with a general deterministic symmetric cipher encSym ([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 m : Msg, and randomness β : ZMod (F.order d), derive k = H (d, encode (β • u)) and output (β • g, encSym k m).

theorem Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalCipherEncrypt_smul_generator (F : PrimeOrderGroupFamily) {Msg Cipher : Type} (H : F.Desc × List Bool → List Bool) (encSym : List Bool → Msg → Cipher) (d : F.Desc) (α β : ZMod (F.order d)) (m : Msg) : F.hashedElGamalCipherEncrypt H encSym d (α • F.generator d) m β = (β • F.generator d, encSym (H (d, F.encode d ((α * β) • F.generator d))) m)

Under a genuine public key u = α • g, hashedElGamalCipherEncrypt derives the symmetric key H (d, encode ((α * β) • g)).

def Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalCipherDecrypt (F : PrimeOrderGroupFamily) {Msg Cipher : Type} (H : F.Desc × List Bool → List Bool) (decSym : List Bool → Cipher → Msg) (d : F.Desc) (α : ZMod (F.order d)) (ct : F.Carrier d × Cipher) : Msg

Algebraic Hashed ElGamal decryption with a general symmetric cipher decSym ([BS23], Section 11.5, pp. 445–446, Remark 11.1): given secret key α : ZMod (F.order d) and ciphertext (v, c), derive k = H (d, encode (α • v)) and recover decSym k c.

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalCipherDecrypt_hashedElGamalCipherEncrypt (F : PrimeOrderGroupFamily) {Msg Cipher : Type} (H : F.Desc × List Bool → List Bool) (encSym : List Bool → Msg → Cipher) (decSym : List Bool → Cipher → Msg) (d : F.Desc) (α β : ZMod (F.order d)) {m : Msg} (hdec : have k := H (d, F.encode d ((α * β) • F.generator d)); decSym k (encSym k m) = m) : F.hashedElGamalCipherDecrypt H decSym d α (F.hashedElGamalCipherEncrypt H encSym d (α • F.generator d) m β) = m

General-cipher Hashed ElGamal decryption correctness: whenever decSym k (encSym k m) = m holds for the derived key k = H (d, encode ((α * β) • g)), decrypting an encryption under u = α • g with secret key α recovers m.

theorem Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalEncrypt_eq_hashedElGamalCipherEncrypt (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (d : F.Desc) (u : F.Carrier d) (m : List Bool) (β : ZMod (F.order d)) : F.hashedElGamalEncrypt H d u m β = F.hashedElGamalCipherEncrypt H (fun (pad msg : List Bool) => BitString.listXor pad.length [pad, msg]) d u m β

hashedElGamalEncrypt is the one-time pad specialization of hashedElGamalCipherEncrypt.

theorem Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalDecrypt_eq_hashedElGamalCipherDecrypt (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (d : F.Desc) (α : ZMod (F.order d)) (ct : F.Carrier d × List Bool) : F.hashedElGamalDecrypt H d α ct = F.hashedElGamalCipherDecrypt H (fun (pad c : List Bool) => BitString.listXor pad.length [pad, c]) d α ct

hashedElGamalDecrypt is the one-time pad specialization of hashedElGamalCipherDecrypt.

def Cslib.Crypto.PrimeOrderGroupFamily.encodeHashedElGamalCipherEncrypt (F : PrimeOrderGroupFamily) {Msg : Type} (H : F.Desc × List Bool → List Bool) (encSym : List Bool × Msg → List Bool) (input : F.Desc × List Bool × Msg × ℕ) : List Bool × List Bool

Word-level Hashed ElGamal encryption with a general symmetric cipher encSym: given (d, encode u, m, b), derive k = H (d, encode (b • u)) and compute (encode (b • g), encSym (k, m)).

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.encodeHashedElGamalCipherEncrypt_encode (F : PrimeOrderGroupFamily) {Msg : Type} (H : F.Desc × List Bool → List Bool) (encSym : List Bool × Msg → List Bool) (d : F.Desc) (u : F.Carrier d) (m : Msg) (b : ℕ) : F.encodeHashedElGamalCipherEncrypt H encSym (d, F.encode d u, m, b) = (F.encode d (F.hashedElGamalCipherEncrypt H (fun (k : List Bool) (msg : Msg) => encSym (k, msg)) d u m ↑b).1, (F.hashedElGamalCipherEncrypt H (fun (k : List Bool) (msg : Msg) => encSym (k, msg)) d u m ↑b).2)

encodeHashedElGamalCipherEncrypt evaluates hashedElGamalCipherEncrypt on encoded group elements.

theorem Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_encodeHashedElGamalCipherEncrypt (F : PrimeOrderGroupFamily) {Msg : Type} {encMsg : Msg ↪ List Bool} {H : F.Desc × List Bool → List Bool} {encSym : List Bool × Msg → List Bool} (hH : Turing.MultiTapeTM.ComputableInPolyTime H (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hencSym : Turing.MultiTapeTM.ComputableInPolyTime encSym (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits encMsg) Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (F.encodeHashedElGamalCipherEncrypt H encSym) (Turing.MultiTapeTM.encPair F.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair encMsg Turing.MultiTapeTM.encNat))) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)

Word-level general-cipher Hashed ElGamal encryption is computable in polynomial time whenever H and encSym are.

def Cslib.Crypto.PrimeOrderGroupFamily.decodeHashedElGamalCipher (F : PrimeOrderGroupFamily) {Msg : Type} (H : F.Desc × List Bool → List Bool) (decSym : List Bool × List Bool → Msg) (input : F.Desc × ℕ × List Bool × List Bool) : Msg

Word-level Hashed ElGamal decryption with a general symmetric cipher decSym: given (d, a, encode v, c), derive k = H (d, encode (a • v)) and compute decSym (k, c).

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.decodeHashedElGamalCipher_encode (F : PrimeOrderGroupFamily) {Msg : Type} (H : F.Desc × List Bool → List Bool) (decSym : List Bool × List Bool → Msg) (d : F.Desc) (a : ℕ) (v : F.Carrier d) (c : List Bool) : F.decodeHashedElGamalCipher H decSym (d, a, F.encode d v, c) = F.hashedElGamalCipherDecrypt H (fun (k ct : List Bool) => decSym (k, ct)) d ↑a (v, c)

decodeHashedElGamalCipher computes hashedElGamalCipherDecrypt on encoded group elements.

theorem Cslib.Crypto.PrimeOrderGroupFamily.decodeHashedElGamalCipher_hashedElGamalCipherEncrypt (F : PrimeOrderGroupFamily) {Msg : Type} (H : F.Desc × List Bool → List Bool) (encSym : List Bool × Msg → List Bool) (decSym : List Bool × List Bool → Msg) (d : F.Desc) (a : ℕ) (β : ZMod (F.order d)) {m : Msg} (hdec : have k := H (d, F.encode d ((↑a * β) • F.generator d)); decSym (k, encSym (k, m)) = m) : F.decodeHashedElGamalCipher H decSym (d, a, F.encode d (F.hashedElGamalCipherEncrypt H (fun (k : List Bool) (msg : Msg) => encSym (k, msg)) d (↑a • F.generator d) m β).1, (F.hashedElGamalCipherEncrypt H (fun (k : List Bool) (msg : Msg) => encSym (k, msg)) d (↑a • F.generator d) m β).2) = m

Word-level general-cipher Hashed ElGamal decryption of an honest encryption recovers m whenever decSym inverts encSym on the derived key.

theorem Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_decodeHashedElGamalCipher (F : PrimeOrderGroupFamily) {Msg : Type} {encMsg : Msg ↪ List Bool} {H : F.Desc × List Bool → List Bool} {decSym : List Bool × List Bool → Msg} (hH : Turing.MultiTapeTM.ComputableInPolyTime H (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hdecSym : Turing.MultiTapeTM.ComputableInPolyTime decSym (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) encMsg) : Turing.MultiTapeTM.ComputableInPolyTime (F.decodeHashedElGamalCipher H decSym) (Turing.MultiTapeTM.encPair F.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) encMsg

Word-level general-cipher Hashed ElGamal decryption is computable in polynomial time whenever H and decSym are.

PMF-level general-cipher Hashed ElGamal IND-CPA games and Theorem 11.5 reductions

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

The IND-CPA experiment for general-cipher Hashed ElGamal (Game 0, [BS23], Section 11.5, pp. 445–446, Remark 11.1, and Section 11.5.2, Theorem 11.5, Figure 11.4, pp. 449–450) with challenge-pair admissibility predicate valid: draw d ← setup n and a uniform secret key α : ZMod (F.order d), and pass 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) and derived symmetric key k = H (d, encode ((α * β) • g)) via c ← encryptSym n k m, and pass (encode (β • g), c) to adversary.guess; otherwise output false, in both experiments.

@[reducible, inline]

noncomputable abbrev Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalCipherCPAGame (F : PrimeOrderGroupFamily) {Msg : Type} (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : Encryption.AdversaryOf Msg) (bit : Bool) (n : ℕ) : Game

Unrestricted general-cipher Hashed ElGamal IND-CPA experiment: hashedElGamalCipherCPAGameOn with every challenge pair admissible.

theorem Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalCPAGame_eq_hashedElGamalCipherCPAGame (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (adversary : Encryption.WordAdversary) (bit : Bool) (n : ℕ) : F.hashedElGamalCPAGame setup H adversary bit n = F.hashedElGamalCipherCPAGame setup H (fun (x : ℕ) (pad m : List Bool) => pure (BitString.listXor pad.length [pad, m])) adversary bit n

hashedElGamalCPAGame is the specialization of hashedElGamalCipherCPAGame to one-time pad XOR encryption.

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

Game 1 for general-cipher Hashed ElGamal ([BS23], Section 11.5.2, proof of Theorem 11.5, p. 450): replace the Diffie–Hellman shared element (α * β) • g with an independent uniform group element γ • g.

@[reducible, inline]

noncomputable abbrev Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalCipherIdealDDHGame (F : PrimeOrderGroupFamily) {Msg : Type} (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : Encryption.AdversaryOf Msg) (bit : Bool) (n : ℕ) : Game

Unrestricted Game 1 for general-cipher Hashed ElGamal.

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

Game 2 for general-cipher Hashed ElGamal ([BS23], Section 11.5.2, proof of Theorem 11.5, p. 450): replace the derived key H (d, encode (γ • g)) with an independent uniform keyLen n-bit key k ← Cslib.BitString.uniformList (keyLen n).

@[reducible, inline]

noncomputable abbrev Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalCipherUniformKeyGame (F : PrimeOrderGroupFamily) {Msg : Type} (setup : ℕ → PMF F.Desc) (keyLen : ℕ → ℕ) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : Encryption.AdversaryOf Msg) (bit : Bool) (n : ℕ) : Game

Unrestricted Game 2 for general-cipher Hashed ElGamal.

theorem Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalCipherCPAGame_restrict (F : PrimeOrderGroupFamily) {Msg : Type} (valid : ℕ → List Bool → Msg → Msg → Bool) (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : Encryption.AdversaryOf Msg) (bit : Bool) (n : ℕ) : F.hashedElGamalCipherCPAGame setup H encryptSym (Encryption.AdversaryOf.restrict valid adversary) bit n = F.hashedElGamalCipherCPAGameOn valid setup H encryptSym adversary bit n

Running the unrestricted hashedElGamalCipherCPAGame on adversary.restrict valid has the same output distribution as running hashedElGamalCipherCPAGameOn valid on adversary.

theorem Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalCipherIdealDDHGame_restrict (F : PrimeOrderGroupFamily) {Msg : Type} (valid : ℕ → List Bool → Msg → Msg → Bool) (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : Encryption.AdversaryOf Msg) (bit : Bool) (n : ℕ) : F.hashedElGamalCipherIdealDDHGame setup H encryptSym (Encryption.AdversaryOf.restrict valid adversary) bit n = F.hashedElGamalCipherIdealDDHGameOn valid setup H encryptSym adversary bit n

Running the unrestricted hashedElGamalCipherIdealDDHGame on adversary.restrict valid has the same output distribution as running hashedElGamalCipherIdealDDHGameOn valid on adversary.

theorem Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalCipherUniformKeyGame_restrict (F : PrimeOrderGroupFamily) {Msg : Type} (valid : ℕ → List Bool → Msg → Msg → Bool) (setup : ℕ → PMF F.Desc) (keyLen : ℕ → ℕ) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : Encryption.AdversaryOf Msg) (bit : Bool) (n : ℕ) : F.hashedElGamalCipherUniformKeyGame setup keyLen encryptSym (Encryption.AdversaryOf.restrict valid adversary) bit n = F.hashedElGamalCipherUniformKeyGameOn valid setup keyLen encryptSym adversary bit n

Running the unrestricted hashedElGamalCipherUniformKeyGame on adversary.restrict valid has the same output distribution as running hashedElGamalCipherUniformKeyGameOn valid on adversary.

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

Per-bit DDH distinguisher constructed from a general-cipher Hashed ElGamal IND-CPA adversary ([BS23], Section 11.5.2, proof of Theorem 11.5, p. 450): given (d, u, v, w), pass pk = (d, u) to adversary.choose, encrypt the selected message m under k = H (d, w) via c ← encryptSym n k m, and return adversary.guess on (v, c).

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.ddhRealGame_hashedElGamalCipherToDDHDistinguisher (F : PrimeOrderGroupFamily) {Msg : Type} (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : Encryption.AdversaryOf Msg) (bit : Bool) (n : ℕ) : F.ddhRealGame setup (F.hashedElGamalCipherToDDHDistinguisher H encryptSym adversary bit) n = F.hashedElGamalCipherCPAGame setup H encryptSym adversary bit n

In the real DDH game, hashedElGamalCipherToDDHDistinguisher simulates hashedElGamalCipherCPAGame exactly.

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.ddhIdealGame_hashedElGamalCipherToDDHDistinguisher (F : PrimeOrderGroupFamily) {Msg : Type} (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : Encryption.AdversaryOf Msg) (bit : Bool) (n : ℕ) : F.ddhIdealGame setup (F.hashedElGamalCipherToDDHDistinguisher H encryptSym adversary bit) n = F.hashedElGamalCipherIdealDDHGame setup H encryptSym adversary bit n

In the ideal DDH game, hashedElGamalCipherToDDHDistinguisher simulates hashedElGamalCipherIdealDDHGame exactly.

theorem Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_hashedElGamalCipherToDDHDistinguisher (F : PrimeOrderGroupFamily) {Msg : Type} {encMsg : Msg ↪ List Bool} {H : F.Desc × List Bool → List Bool} {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)} {adversary : Encryption.AdversaryOf Msg} (hH : Turing.MultiTapeTM.ComputableInPolyTime H (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hencryptSym : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits encMsg)) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × Msg) => encryptSym p.1 p.2.1 p.2.2) (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.hashedElGamalCipherToDDHDistinguisher H encryptSym adversary bit input.1 input.2

hashedElGamalCipherToDDHDistinguisher is uniform strict PPT whenever H is polynomial time and encryptSym and adversary are uniform strict PPT.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalCipherToDDHHiddenBitDistinguisher (F : PrimeOrderGroupFamily) {Msg : Type} (H : F.Desc × List Bool → List Bool) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : Encryption.AdversaryOf Msg) (n : ℕ) (input : F.Desc × List Bool × List Bool × List Bool) : ProbComp Bool

Single hidden-bit DDH distinguisher $\mathcal{B}_{\mathrm{ddh}}$ ([BS23], Section 11.5.2, proof of Theorem 11.5, Figure 11.4 and Equation (11.17), p. 450): sample a uniform challenge bit bit ← ProbComp.uniform Bool, run hashedElGamalCipherToDDHDistinguisher on bit, and output guess ^^ bit.

theorem Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_hashedElGamalCipherToDDHHiddenBitDistinguisher (F : PrimeOrderGroupFamily) {Msg : Type} {encMsg : Msg ↪ List Bool} {H : F.Desc × List Bool → List Bool} {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)} {adversary : Encryption.AdversaryOf Msg} (hH : Turing.MultiTapeTM.ComputableInPolyTime H (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hencryptSym : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits encMsg)) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × Msg) => encryptSym p.1 p.2.1 p.2.2) (hA : Encryption.AdversaryOf.IsPPT encMsg adversary) : 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.hashedElGamalCipherToDDHHiddenBitDistinguisher H encryptSym adversary input.1 input.2

hashedElGamalCipherToDDHHiddenBitDistinguisher is uniform strict PPT whenever H is polynomial time and encryptSym and adversary are uniform strict PPT.

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

Per-bit KDF distinguisher constructed from a general-cipher Hashed ElGamal IND-CPA adversary ([BS23], Section 11.5.2, proof of Theorem 11.5, pp. 450–451): given (d, u, v, k), pass pk = (d, u) to adversary.choose, encrypt the selected message m under k via c ← encryptSym n k m, and return adversary.guess on (v, c).

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.kdfRealGame_hashedElGamalCipherToKDFDistinguisher (F : PrimeOrderGroupFamily) {Msg : Type} (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : Encryption.AdversaryOf Msg) (bit : Bool) (n : ℕ) : F.kdfRealGame setup H (F.hashedElGamalCipherToKDFDistinguisher encryptSym adversary bit) n = F.hashedElGamalCipherIdealDDHGame setup H encryptSym adversary bit n

In the real KDF game, hashedElGamalCipherToKDFDistinguisher simulates hashedElGamalCipherIdealDDHGame exactly.

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.kdfIdealGame_hashedElGamalCipherToKDFDistinguisher (F : PrimeOrderGroupFamily) {Msg : Type} (setup : ℕ → PMF F.Desc) (keyLen : ℕ → ℕ) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : Encryption.AdversaryOf Msg) (bit : Bool) (n : ℕ) : F.kdfIdealGame setup keyLen (F.hashedElGamalCipherToKDFDistinguisher encryptSym adversary bit) n = F.hashedElGamalCipherUniformKeyGame setup keyLen encryptSym adversary bit n

In the ideal KDF game, hashedElGamalCipherToKDFDistinguisher simulates hashedElGamalCipherUniformKeyGame exactly.

theorem Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_hashedElGamalCipherToKDFDistinguisher (F : PrimeOrderGroupFamily) {Msg : Type} {encMsg : Msg ↪ List Bool} {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)} {adversary : Encryption.AdversaryOf Msg} (hencryptSym : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits encMsg)) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × Msg) => encryptSym p.1 p.2.1 p.2.2) (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.hashedElGamalCipherToKDFDistinguisher encryptSym adversary bit input.1 input.2

hashedElGamalCipherToKDFDistinguisher is uniform strict PPT whenever encryptSym and adversary are.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalCipherToKDFHiddenBitDistinguisher (F : PrimeOrderGroupFamily) {Msg : Type} (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : Encryption.AdversaryOf Msg) (n : ℕ) (input : F.Desc × List Bool × List Bool × List Bool) : ProbComp Bool

Single hidden-bit KDF distinguisher $\mathcal{B}_{\mathrm{kdf}}$ ([BS23], Section 11.5.2, proof of Theorem 11.5, Equation (11.18), pp. 450–451): sample a uniform challenge bit bit ← ProbComp.uniform Bool, run hashedElGamalCipherToKDFDistinguisher on bit, and output guess ^^ bit.

theorem Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_hashedElGamalCipherToKDFHiddenBitDistinguisher (F : PrimeOrderGroupFamily) {Msg : Type} {encMsg : Msg ↪ List Bool} {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)} {adversary : Encryption.AdversaryOf Msg} (hencryptSym : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits encMsg)) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × Msg) => encryptSym p.1 p.2.1 p.2.2) (hA : Encryption.AdversaryOf.IsPPT encMsg adversary) : 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.hashedElGamalCipherToKDFHiddenBitDistinguisher encryptSym adversary input.1 input.2

hashedElGamalCipherToKDFHiddenBitDistinguisher is uniform strict PPT whenever encryptSym and adversary are.

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_hashedElGamalCipherCPAGameOn_le (F : PrimeOrderGroupFamily) {Msg : Type} (valid : ℕ → List Bool → Msg → Msg → Bool) (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (keyLen : ℕ → ℕ) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : Encryption.AdversaryOf Msg) (n : ℕ) : (F.hashedElGamalCipherCPAGameOn valid setup H encryptSym adversary false n).advantage (F.hashedElGamalCipherCPAGameOn valid setup H encryptSym adversary true n) ≤ (F.ddhRealGame setup (F.hashedElGamalCipherToDDHDistinguisher H encryptSym (Encryption.AdversaryOf.restrict valid adversary) false) n).advantage (F.ddhIdealGame setup (F.hashedElGamalCipherToDDHDistinguisher H encryptSym (Encryption.AdversaryOf.restrict valid adversary) false) n) + (F.kdfRealGame setup H (F.hashedElGamalCipherToKDFDistinguisher encryptSym (Encryption.AdversaryOf.restrict valid adversary) false) n).advantage (F.kdfIdealGame setup keyLen (F.hashedElGamalCipherToKDFDistinguisher encryptSym (Encryption.AdversaryOf.restrict valid adversary) false) n) + (F.hashedElGamalCipherUniformKeyGameOn valid setup keyLen encryptSym adversary false n).advantage (F.hashedElGamalCipherUniformKeyGameOn valid setup keyLen encryptSym adversary true n) + (F.kdfRealGame setup H (F.hashedElGamalCipherToKDFDistinguisher encryptSym (Encryption.AdversaryOf.restrict valid adversary) true) n).advantage (F.kdfIdealGame setup keyLen (F.hashedElGamalCipherToKDFDistinguisher encryptSym (Encryption.AdversaryOf.restrict valid adversary) true) n) + (F.ddhRealGame setup (F.hashedElGamalCipherToDDHDistinguisher H encryptSym (Encryption.AdversaryOf.restrict valid adversary) true) n).advantage (F.ddhIdealGame setup (F.hashedElGamalCipherToDDHDistinguisher H encryptSym (Encryption.AdversaryOf.restrict valid adversary) true) n)

Quantitative reduction of general-cipher Hashed ElGamal IND-CPA to DDH, SecureKDF, and Game 2 via two per-bit distinguishers ([BS23], Section 11.5.2, Theorem 11.5, pp. 449–451): the IND-CPA advantage in hashedElGamalCipherCPAGameOn valid is bounded by the sum of the two per-bit DDH advantages, the two per-bit KDF advantages, and the Game 2 advantage in hashedElGamalCipherUniformKeyGameOn valid.

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_hashedElGamalCipherCPAGameOn_le_two_mul (F : PrimeOrderGroupFamily) {Msg : Type} (valid : ℕ → List Bool → Msg → Msg → Bool) (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (keyLen : ℕ → ℕ) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : Encryption.AdversaryOf Msg) (n : ℕ) : (F.hashedElGamalCipherCPAGameOn valid setup H encryptSym adversary false n).advantage (F.hashedElGamalCipherCPAGameOn valid setup H encryptSym adversary true n) ≤ 2 * (F.ddhRealGame setup (F.hashedElGamalCipherToDDHHiddenBitDistinguisher H encryptSym (Encryption.AdversaryOf.restrict valid adversary)) n).advantage (F.ddhIdealGame setup (F.hashedElGamalCipherToDDHHiddenBitDistinguisher H encryptSym (Encryption.AdversaryOf.restrict valid adversary)) n) + 2 * (F.kdfRealGame setup H (F.hashedElGamalCipherToKDFHiddenBitDistinguisher encryptSym (Encryption.AdversaryOf.restrict valid adversary)) n).advantage (F.kdfIdealGame setup keyLen (F.hashedElGamalCipherToKDFHiddenBitDistinguisher encryptSym (Encryption.AdversaryOf.restrict valid adversary)) n) + (F.hashedElGamalCipherUniformKeyGameOn valid setup keyLen encryptSym adversary false n).advantage (F.hashedElGamalCipherUniformKeyGameOn valid setup keyLen encryptSym adversary true n)

Quantitative reduction of general-cipher Hashed ElGamal IND-CPA to DDH, SecureKDF, and Game 2 via single hidden-bit distinguishers ([BS23], Section 11.5.2, Theorem 11.5, Equation (11.14), p. 449): $$\mathsf{SSadv}[\mathcal{A}, \mathcal{E}_{\mathrm{EG}}] \le 2 \cdot \mathsf{DDHadv}[\mathcal{B}_{\mathrm{ddh}}, \mathbb{G}] + 2 \cdot \mathsf{KDFadv}[\mathcal{B}_{\mathrm{kdf}}, H] + \mathsf{Adv}_{\mathrm{Game\,2}}[\mathcal{A}].$$

theorem Cslib.Crypto.PrimeOrderGroupFamily.DDH.negligible_hashedElGamalCipherCPAGameOn {F : PrimeOrderGroupFamily} {Msg : Type} {encMsg : Msg ↪ List Bool} {valid : ℕ → List Bool → Msg → Msg → Bool} {setup : ℕ → PMF F.Desc} {H : F.Desc × List Bool → List Bool} {keyLen : ℕ → ℕ} {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)} (hDDH : F.DDH setup) (hKDF : F.SecureKDF setup H keyLen) (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) (hH : Turing.MultiTapeTM.ComputableInPolyTime H (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hencryptSym : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits encMsg)) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × Msg) => encryptSym p.1 p.2.1 p.2.2) {adversary : Encryption.AdversaryOf Msg} (hA : Encryption.AdversaryOf.IsPPT encMsg adversary) (hSym : Negligible fun (n : ℕ) => (F.hashedElGamalCipherUniformKeyGameOn valid setup keyLen encryptSym adversary false n).advantage (F.hashedElGamalCipherUniformKeyGameOn valid setup keyLen encryptSym adversary true n)) : Negligible fun (n : ℕ) => (F.hashedElGamalCipherCPAGameOn valid setup H encryptSym adversary false n).advantage (F.hashedElGamalCipherCPAGameOn valid setup H encryptSym adversary true n)

General-cipher Hashed ElGamal IND-CPA security from DDH, SecureKDF, and Game 2 indistinguishability ([BS23], Section 11.5.2, Theorem 11.5, pp. 449–451): whenever H and valid are polynomial-time computable, encryptSym is uniform strict PPT, and every uniform strict PPT adversary has negligible advantage in Game 2 (hashedElGamalCipherUniformKeyGameOn), every uniform strict PPT adversary has negligible advantage in hashedElGamalCipherCPAGameOn valid.

Reduction from Game 2 (hashedElGamalCipherUniformKeyGameOn) to DEMOneTimeINDCPAOn

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalCipherToDEMAdversary (F : PrimeOrderGroupFamily) {Msg : Type} (setupProb : ℕ → ProbComp F.Desc) (adversary : Encryption.AdversaryOf Msg) : Encryption.AdversaryOf Msg

One-time symmetric-cipher reduction adversary $\mathcal{B}_s$ for general-cipher Hashed ElGamal ([BS23], Section 11.5.2, proof of Theorem 11.5, p. 451): given an efficiently samplable group-description generator setupProb : ℕ → ProbComp F.Desc and a PKE adversary adversary, choose n _ samples d ← setupProb n and a, b ← F.sampleExp n d, sets u = encode (a • g) and v = encode (b • g), runs choice ← adversary.choose n (d, u), and saves (v, choice.2); guess n state ctSym unpacks (v, st) and runs adversary.guess n st (v, ctSym).

theorem Cslib.Crypto.PrimeOrderGroupFamily.isPPT_hashedElGamalCipherToDEMAdversary (F : PrimeOrderGroupFamily) {Msg : Type} {encMsg : Msg ↪ List Bool} {setupProb : ℕ → ProbComp F.Desc} (hsetup : Probability.IsPPTOn Turing.MultiTapeTM.encUnary F.encDesc setupProb) {adversary : Encryption.AdversaryOf Msg} (hA : Encryption.AdversaryOf.IsPPT encMsg adversary) : Encryption.AdversaryOf.IsPPT encMsg (F.hashedElGamalCipherToDEMAdversary setupProb adversary)

hashedElGamalCipherToDEMAdversary setupProb adversary is an admissible uniform strict PPT Encryption.AdversaryOf Msg whenever setupProb and adversary are.

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_hashedElGamalCipherUniformKeyGameOn_demGameOn_le (F : PrimeOrderGroupFamily) {Msg : Type} (valid validSym : ℕ → List Bool → Msg → Msg → Bool) (setupProb : ℕ → ProbComp F.Desc) (keyLen : ℕ → ℕ) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : Encryption.AdversaryOf Msg) (bit : Bool) (n : ℕ) (hkeyLen : keyLen n = n) (hvalid_imp : ∀ (d : F.Desc) (u : List Bool) (m₀ m₁ : Msg), valid n ((Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) (d, u)) m₀ m₁ = true → validSym n [] m₀ m₁ = true) : (F.hashedElGamalCipherUniformKeyGameOn valid (fun (m : ℕ) => (setupProb m).eval) keyLen encryptSym adversary bit n).advantage (Encryption.demGameOn validSym encryptSym (F.hashedElGamalCipherToDEMAdversary setupProb (Encryption.AdversaryOf.restrict valid adversary)) bit n).eval ≤ 2 / 2 ^ n

For each bit bit : Bool, the Game 2 distribution hashedElGamalCipherUniformKeyGameOn over fun m => ProbComp.eval (setupProb m) with keyLen n = n is within 2 / 2 ^ n in Game.advantage of the standalone one-time symmetric experiment Encryption.demGameOn on hashedElGamalCipherToDEMAdversary setupProb (adversary.restrict valid) (two approximate exponent draws via sampleExp, each within 1 / 2 ^ n of uniform).

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_hashedElGamalCipherUniformKeyGameOn_le_demGameOn (F : PrimeOrderGroupFamily) {Msg : Type} (valid validSym : ℕ → List Bool → Msg → Msg → Bool) (setupProb : ℕ → ProbComp F.Desc) (keyLen : ℕ → ℕ) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : Encryption.AdversaryOf Msg) (n : ℕ) (hkeyLen : keyLen n = n) (hvalid_imp : ∀ (d : F.Desc) (u : List Bool) (m₀ m₁ : Msg), valid n ((Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) (d, u)) m₀ m₁ = true → validSym n [] m₀ m₁ = true) : (F.hashedElGamalCipherUniformKeyGameOn valid (fun (m : ℕ) => (setupProb m).eval) keyLen encryptSym adversary false n).advantage (F.hashedElGamalCipherUniformKeyGameOn valid (fun (m : ℕ) => (setupProb m).eval) keyLen encryptSym adversary true n) ≤ Game.advantage (Encryption.demGameOn validSym encryptSym (F.hashedElGamalCipherToDEMAdversary setupProb (Encryption.AdversaryOf.restrict valid adversary)) false n).eval (Encryption.demGameOn validSym encryptSym (F.hashedElGamalCipherToDEMAdversary setupProb (Encryption.AdversaryOf.restrict valid adversary)) true n).eval + 4 / 2 ^ n

Quantitative bridge from Game 2 (hashedElGamalCipherUniformKeyGameOn) to standalone symmetric-cipher security (Encryption.demGameOn): the Game 2 advantage is bounded by the Encryption.demGameOn advantage of hashedElGamalCipherToDEMAdversary setupProb (adversary.restrict valid) plus 4 / 2 ^ n.

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_hashedElGamalCipherCPAGameOn_le_demGameOn (F : PrimeOrderGroupFamily) {Msg : Type} (valid validSym : ℕ → List Bool → Msg → Msg → Bool) (setupProb : ℕ → ProbComp F.Desc) (H : F.Desc × List Bool → List Bool) (keyLen : ℕ → ℕ) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) (adversary : Encryption.AdversaryOf Msg) (n : ℕ) (hkeyLen : keyLen n = n) (hvalid_imp : ∀ (d : F.Desc) (u : List Bool) (m₀ m₁ : Msg), valid n ((Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) (d, u)) m₀ m₁ = true → validSym n [] m₀ m₁ = true) : (F.hashedElGamalCipherCPAGameOn valid (fun (m : ℕ) => (setupProb m).eval) H encryptSym adversary false n).advantage (F.hashedElGamalCipherCPAGameOn valid (fun (m : ℕ) => (setupProb m).eval) H encryptSym adversary true n) ≤ 2 * (F.ddhRealGame (fun (m : ℕ) => (setupProb m).eval) (F.hashedElGamalCipherToDDHHiddenBitDistinguisher H encryptSym (Encryption.AdversaryOf.restrict valid adversary)) n).advantage (F.ddhIdealGame (fun (m : ℕ) => (setupProb m).eval) (F.hashedElGamalCipherToDDHHiddenBitDistinguisher H encryptSym (Encryption.AdversaryOf.restrict valid adversary)) n) + 2 * (F.kdfRealGame (fun (m : ℕ) => (setupProb m).eval) H (F.hashedElGamalCipherToKDFHiddenBitDistinguisher encryptSym (Encryption.AdversaryOf.restrict valid adversary)) n).advantage (F.kdfIdealGame (fun (m : ℕ) => (setupProb m).eval) keyLen (F.hashedElGamalCipherToKDFHiddenBitDistinguisher encryptSym (Encryption.AdversaryOf.restrict valid adversary)) n) + Game.advantage (Encryption.demGameOn validSym encryptSym (F.hashedElGamalCipherToDEMAdversary setupProb (Encryption.AdversaryOf.restrict valid adversary)) false n).eval (Encryption.demGameOn validSym encryptSym (F.hashedElGamalCipherToDEMAdversary setupProb (Encryption.AdversaryOf.restrict valid adversary)) true n).eval + 4 / 2 ^ n

Native approximate-sampling version of Equation (11.14) for Theorem 11.5 via DDH, SecureKDF, and standalone symmetric-cipher security (Encryption.demGameOn) ([BS23], Section 11.5.2, Theorem 11.5, Equation (11.14), p. 449): combining the exact PMF-level Equation (11.14) bound advantage_hashedElGamalCipherCPAGameOn_le_two_mul with the sampleExp Game 2 bridge advantage_hashedElGamalCipherUniformKeyGameOn_le_demGameOn adds 4 / 2 ^ n for the two approximate exponent draws per branch: $$\mathsf{SSadv}[\mathcal{A}, \mathcal{E}_{\mathrm{EG}}] \le 2 \cdot \mathsf{DDHadv}[\mathcal{B}_{\mathrm{ddh}}, \mathbb{G}] + 2 \cdot \mathsf{KDFadv}[\mathcal{B}_{\mathrm{kdf}}, H] + \mathsf{SSadv}[\mathcal{B}_s, \mathcal{E}_s] + \frac{4}{2^n}.$$

theorem Cslib.Crypto.PrimeOrderGroupFamily.negligible_hashedElGamalCipherUniformKeyGameOn_of_demOneTimeINDCPAOn (F : PrimeOrderGroupFamily) {Msg : Type} {encMsg : Msg ↪ List Bool} {valid validSym : ℕ → List Bool → Msg → Msg → Bool} {setupProb : ℕ → ProbComp F.Desc} {keyLen : ℕ → ℕ} {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)} (hDEM : Encryption.DEMOneTimeINDCPAOn validSym encMsg encryptSym) (hsetup : Probability.IsPPTOn Turing.MultiTapeTM.encUnary F.encDesc setupProb) (hkeyLen : ∀ (n : ℕ), keyLen n = n) (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) (hvalid_imp : ∀ (n : ℕ) (d : F.Desc) (u : List Bool) (m₀ m₁ : Msg), valid n ((Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) (d, u)) m₀ m₁ = true → validSym n [] m₀ m₁ = true) {adversary : Encryption.AdversaryOf Msg} (hA : Encryption.AdversaryOf.IsPPT encMsg adversary) : Negligible fun (n : ℕ) => (F.hashedElGamalCipherUniformKeyGameOn valid (fun (m : ℕ) => (setupProb m).eval) keyLen encryptSym adversary false n).advantage (F.hashedElGamalCipherUniformKeyGameOn valid (fun (m : ℕ) => (setupProb m).eval) keyLen encryptSym adversary true n)

One-time symmetric IND-CPA security (Encryption.DEMOneTimeINDCPAOn) implies negligibility of the Game 2 advantage (hashedElGamalCipherUniformKeyGameOn) whenever the setup law is efficiently samplable (setupProb : ℕ → ProbComp F.Desc), keyLen n = n, and valid implies validSym.

theorem Cslib.Crypto.PrimeOrderGroupFamily.DDH.negligible_hashedElGamalCipherCPAGameOn_of_demOneTimeINDCPAOn {F : PrimeOrderGroupFamily} {Msg : Type} {encMsg : Msg ↪ List Bool} {valid validSym : ℕ → List Bool → Msg → Msg → Bool} {setupProb : ℕ → ProbComp F.Desc} {H : F.Desc × List Bool → List Bool} {keyLen : ℕ → ℕ} {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)} (hDDH : F.DDH fun (n : ℕ) => (setupProb n).eval) (hKDF : F.SecureKDF (fun (n : ℕ) => (setupProb n).eval) H keyLen) (hDEM : Encryption.DEMOneTimeINDCPAOn validSym encMsg encryptSym) (hsetup : Probability.IsPPTOn Turing.MultiTapeTM.encUnary F.encDesc setupProb) (hkeyLen : ∀ (n : ℕ), keyLen n = n) (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) (hvalid_imp : ∀ (n : ℕ) (d : F.Desc) (u : List Bool) (m₀ m₁ : Msg), valid n ((Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) (d, u)) m₀ m₁ = true → validSym n [] m₀ m₁ = true) (hH : Turing.MultiTapeTM.ComputableInPolyTime H (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hencryptSym : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits encMsg)) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × Msg) => encryptSym p.1 p.2.1 p.2.2) {adversary : Encryption.AdversaryOf Msg} (hA : Encryption.AdversaryOf.IsPPT encMsg adversary) : Negligible fun (n : ℕ) => (F.hashedElGamalCipherCPAGameOn valid (fun (n : ℕ) => (setupProb n).eval) H encryptSym adversary false n).advantage (F.hashedElGamalCipherCPAGameOn valid (fun (n : ℕ) => (setupProb n).eval) H encryptSym adversary true n)

Boneh–Shoup Theorem 11.5 from DDH, SecureKDF, and Encryption.DEMOneTimeINDCPAOn ([BS23], Section 11.5.2, Theorem 11.5, pp. 449–451): for any efficiently samplable setup setupProb : ℕ → ProbComp F.Desc (setup n = ProbComp.eval (setupProb n)), keyLen n = n, and admissibility predicate valid implying validSym, if F.DDH, F.SecureKDF, and Encryption.DEMOneTimeINDCPAOn validSym encMsg encryptSym hold, then every uniform strict PPT adversary has negligible advantage in hashedElGamalCipherCPAGameOn valid.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.seededSetupProb (F : PrimeOrderGroupFamily) (setupProb : ℕ → ProbComp F.Desc) (seedLen : ℕ → F.Desc → ℕ) (n : ℕ) : ProbComp F.withSeed.Desc

Executable ProbComp sampler for F.seededSetup: sample d ← setupProb n, then conditional on d, sample a uniform seed s ← Cslib.BitString.sampleList (seedLen n d) and output (d, s).

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.eval_seededSetupProb (F : PrimeOrderGroupFamily) (setupProb : ℕ → ProbComp F.Desc) (seedLen : ℕ → F.Desc → ℕ) (n : ℕ) : (F.seededSetupProb setupProb seedLen n).eval = F.seededSetup (fun (m : ℕ) => (setupProb m).eval) seedLen n

ProbComp.eval (F.seededSetupProb setupProb seedLen n) equals F.seededSetup (fun m => ProbComp.eval (setupProb m)) seedLen n.

theorem Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_seededSetupProb (F : PrimeOrderGroupFamily) {setupProb : ℕ → ProbComp F.Desc} {seedLen : ℕ → F.Desc → ℕ} (hsetup : Probability.IsPPTOn Turing.MultiTapeTM.encUnary F.encDesc setupProb) (hseed : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × F.Desc) => seedLen p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary F.encDesc) Turing.MultiTapeTM.encUnary) : Probability.IsPPTOn Turing.MultiTapeTM.encUnary F.withSeed.encDesc (F.seededSetupProb setupProb seedLen)

F.seededSetupProb setupProb seedLen is uniform strict PPT whenever setupProb is uniform strict PPT and seedLen is computable in polynomial time in unary.

theorem Cslib.Crypto.PrimeOrderGroupFamily.DDH.negligible_hashedElGamalCipherCPAGameOn_linearHashKDF {F : PrimeOrderGroupFamily} {Msg : Type} {encMsg : Msg ↪ List Bool} {valid validSym : ℕ → List Bool → Msg → Msg → Bool} {setupProb : ℕ → ProbComp F.Desc} {keyLen bound : F.Desc → ℕ} {qMin : ℕ → ℕ} {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)} (hDDH : F.DDH fun (n : ℕ) => (setupProb n).eval) (hDEM : Encryption.DEMOneTimeINDCPAOn validSym encMsg encryptSym) (hsetup : Probability.IsPPTOn Turing.MultiTapeTM.encUnary F.encDesc setupProb) (hkey_poly : Turing.MultiTapeTM.ComputableInPolyTime keyLen F.encDesc Turing.MultiTapeTM.encUnary) (hbound_poly : Turing.MultiTapeTM.ComputableInPolyTime bound F.encDesc Turing.MultiTapeTM.encUnary) (hq0 : ∀ (n : ℕ), 0 < qMin n) (hkey : ∀ (n : ℕ), ∀ d ∈ (setupProb n).eval.support, keyLen d = n) (hbound : ∀ (n : ℕ), ∀ d ∈ (setupProb n).eval.support, ∀ (x : F.Carrier d), (F.encode d x).length ≤ bound d) (hq : ∀ (n : ℕ), ∀ d ∈ (setupProb n).eval.support, qMin n ≤ F.order d) (hneg : Negligible fun (n : ℕ) => 2 ^ n / ↑(qMin n)) (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) (hvalid_imp : ∀ (n : ℕ) (d : F.withSeed.Desc) (u : List Bool) (m₀ m₁ : Msg), valid n ((Turing.MultiTapeTM.encPair F.withSeed.encDesc Turing.MultiTapeTM.encBits) (d, u)) m₀ m₁ = true → validSym n [] m₀ m₁ = true) (hencryptSym : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits encMsg)) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × Msg) => encryptSym p.1 p.2.1 p.2.2) {adversary : Encryption.AdversaryOf Msg} (hA : Encryption.AdversaryOf.IsPPT encMsg adversary) : Negligible fun (n : ℕ) => (F.withSeed.hashedElGamalCipherCPAGameOn valid (F.seededSetup (fun (m : ℕ) => (setupProb m).eval) (F.linearHashSeedLen (fun (n : ℕ) => n) bound)) (F.linearHashKDF keyLen bound) encryptSym adversary false n).advantage (F.withSeed.hashedElGamalCipherCPAGameOn valid (F.seededSetup (fun (m : ℕ) => (setupProb m).eval) (F.linearHashSeedLen (fun (n : ℕ) => n) bound)) (F.linearHashKDF keyLen bound) encryptSym adversary true n)

General-cipher Hashed ElGamal IND-CPA security with linearHashKDF from DDH and Encryption.DEMOneTimeINDCPAOn alone ([BS23], Section 8.10.4, Theorem 8.11, p. 334, and Section 11.5.2, Theorem 11.5, pp. 449–451): combining DDH.withSeed, secureKDF_linearHashKDF, isPPTOn_seededSetupProb, and DDH.negligible_hashedElGamalCipherCPAGameOn_of_demOneTimeINDCPAOn yields IND-CPA security of general-cipher Hashed ElGamal instantiated with linearHashKDF under F.DDH and Encryption.DEMOneTimeINDCPAOn alone, with no separate KDF assumption.