From a21be084e6467a16625a49ecb9b165540581b96a Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Mon, 26 Oct 2026 17:30:35 -0400 Subject: [PATCH 1/2] feat(Crypto/ElGamal): non-degenerate SecureKDF and strict-PPT ElGamal --- Complexity.lean | 2 + Complexity/Crypto/Computational/ElGamal.lean | 25 +- .../Crypto/Computational/ElGamal/KDF.lean | 579 ++++++++++++++ .../Computational/ElGamal/ProbComp.lean | 747 ++++++++++++++++++ ComplexityTests/Crypto/DiffieHellman.lean | 144 ++++ ROADMAP.md | 5 +- 6 files changed, 1486 insertions(+), 16 deletions(-) create mode 100644 Complexity/Crypto/Computational/ElGamal/KDF.lean create mode 100644 Complexity/Crypto/Computational/ElGamal/ProbComp.lean diff --git a/Complexity.lean b/Complexity.lean index 78506ce6d..8991553e2 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1533,6 +1533,8 @@ public import Complexity.Crypto.Computational.DiffieHellman.MultiDDH public import Complexity.Crypto.Computational.DiscreteLog public import Complexity.Crypto.Computational.DiscreteLog.SchnorrGroup public import Complexity.Crypto.Computational.ElGamal +public import Complexity.Crypto.Computational.ElGamal.KDF +public import Complexity.Crypto.Computational.ElGamal.ProbComp public import Complexity.Crypto.Computational.Encryption.Authenticated public import Complexity.Crypto.Computational.Encryption.Basic public import Complexity.Crypto.Computational.Encryption.CCA diff --git a/Complexity/Crypto/Computational/ElGamal.lean b/Complexity/Crypto/Computational/ElGamal.lean index 80a7329a4..21df3d90a 100644 --- a/Complexity/Crypto/Computational/ElGamal.lean +++ b/Complexity/Crypto/Computational/ElGamal.lean @@ -63,19 +63,18 @@ We prove IND-CPA security under DDH in the following settings: ## Limitations -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. Because exponent -sampling in key generation and encapsulation is at the `PMF` level rather than a `ProbComp` -machine (see the `ROADMAP.md` item for efficient key generation and encryption), Hashed ElGamal -security is proved via a direct three-hop `PMF` chain (`hashedElGamalCPAGame`, -`hashedElGamalIdealDDHGame`, `hashedElGamalUniformPadGame`) rather than through the `ProbComp`-level -`KEMINDCPA.hybrid_otpWordEncrypt_indcpa` combinator. The Diffie–Hellman and key-derivation security -assumptions (`DDH`, `SecureKDF`) are hypotheses, not theorems; no nondegenerate `SecureKDF` -instance (`msgLen n > 0`, e.g., via the leftover hash lemma) is constructed in this module. +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 diff --git a/Complexity/Crypto/Computational/ElGamal/KDF.lean b/Complexity/Crypto/Computational/ElGamal/KDF.lean new file mode 100644 index 000000000..7bbe41ab9 --- /dev/null +++ b/Complexity/Crypto/Computational/ElGamal/KDF.lean @@ -0,0 +1,579 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Padding +public import Complexity.Crypto.Computational.DiffieHellman.EncodingBounds +public import Complexity.Crypto.Computational.ElGamal +public import Complexity.Languages.Probabilistic.LinearHash +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString +import Complexity.Computability.Probabilistic.LinearHash +import Complexity.Computability.Probabilistic.Sampling +import Complexity.Crypto.Game.Statistical +import Complexity.Crypto.Negligible.Basic +import Complexity.Probability.Collision +import Complexity.Tactic.PPT + +/-! +# Unconditionally Secure Key Derivation for Hashed ElGamal via the Leftover Hash Lemma + +In [BonehShoup2023], Section 8.10.4 (Theorem 8.11, p. 334) and Section 11.5.2 (p. 449), a universal +hash function whose key is placed in the public system parameter yields an unconditionally secure +key derivation function (`SecureKDF`, Attack Game 11.3, pp. 448–449, and Definition 11.5, p. 449) +via the Leftover Hash Lemma, without any computational assumptions on the hash family. + +* **Paraphrase of [BonehShoup2023], Section 8.10.4, Theorem 8.11 (p. 334, Leftover Hash Lemma):** + for a $(1 + \alpha)/N$-universal keyed hash function $H$ over $(\mathcal{K}, \mathcal{S}, + \mathcal{T})$ with $N = |\mathcal{T}|$, if $k$ is uniform on $\mathcal{K}$ and $s_1, \dots, s_m$ + are independent of $k$ and of each other with guessing/collision probability at most $\gamma$, + the statistical distance $\delta$ between $(k, H(k, s_1), \dots, H(k, s_m))$ and the uniform + distribution on $\mathcal{K} \times \mathcal{T}^m$ satisfies + $\delta \le \frac{1}{2} m \sqrt{N \gamma + \alpha}$. +* **Paraphrase of [BonehShoup2023], Section 11.5.2, Attack Game 11.3 and Definition 11.5 + (pp. 448–449):** for $F : \mathcal{X} \times \mathcal{Y} \to \mathcal{Z}$, Experiment $b$ samples + $x \leftarrow \mathcal{X}$, $y \leftarrow \mathcal{Y}$, sets $z_0 = F(x, y)$, samples uniform + $z_1 \leftarrow \mathcal{Z}$, and passes $(x, z_b)$ to $\mathcal{A}$; $F$ is a secure KDF if + $|\Pr[W_0] - \Pr[W_1]|$ is negligible for every efficient adversary $\mathcal{A}$. As noted on + p. 449: + > One may even build a secure KDF without making any assumptions at all: the construction in + > Section 8.10.4 based on a universal hash function and the leftover hash lemma yields an + > unconditionally secure KDF. + +To formalize this over an arbitrary `PrimeOrderGroupFamily`: +1. `PrimeOrderGroupFamily.withSeed` augments the public group description `d : F.Desc` with a public + bit-string seed `s : List Bool`, giving `F.withSeed.Desc = F.Desc × List Bool`. Under + `PrimeOrderGroupFamily.seededSetup`, `s` is sampled uniformly from `{0, 1}^{seedLen n d}` + independently of the group description `d ← setup n`. When `seedLen` is polynomial-time + computable in unary, `DDH.withSeed` transfers the `DDH` assumption from `(F, setup)` to + `(F.withSeed, F.seededSetup setup seedLen)`. +2. `PrimeOrderGroupFamily.linearHashKDF` pads the encoded group element `w : List Bool` to the fixed + self-delimiting width `2 * bound d + 1` via `Cslib.BitString.padWord (bound d) w` and hashes it + with the public Boolean matrix seed `s` via `Cslib.BitString.LinearHash.wordHash (keyLen d) s`. + Because `padWord` is injective on words of length at most `bound d` + (`Cslib.BitString.word_eq_of_paddedBits_eq`) and `F.encode d` is injective on `F.Carrier d`, a + uniform group element `γ • g` maps injectively into `BitString (2 * bound d + 1)` with collision + probability `(F.order d)⁻¹`. +3. Applying the Leftover Hash Lemma for two-universal binary matrix hashing + (`Cslib.BitString.LinearHash.isTwoUniversal_flat` and `IsTwoUniversal.leftover_hash`), + `advantage_kdfGame_linearHashKDF_le` bounds the distinguishing advantage between `kdfRealGame` + and `kdfIdealGame` for *every* (even computationally unbounded) distinguisher by + `NNReal.sqrt ((2 : ℝ≥0) ^ (msgLen n) / (qMin : ℝ≥0)) / 2`. Consequently, + `secureKDF_linearHashKDF`, `secureKDF_linearHashKDF_const`, `exists_secureKDF_withSeed`, and + `DDH.negligible_hashedElGamalCPAGame_linearHashKDF` yield non-degenerate `SecureKDF` and Hashed + ElGamal instantiations for arbitrary positive key lengths `msgLen n > 0` whenever + `2 ^ (msgLen n) / q` is negligible. + +## Main definitions + +* `Cslib.Crypto.PrimeOrderGroupFamily.withSeed`: prime-order group family with a public hash seed in + the description. +* `Cslib.Crypto.PrimeOrderGroupFamily.seededSetup`: setup distribution augmenting `setup n` with an + independent uniform bit-string seed. +* `Cslib.Crypto.PrimeOrderGroupFamily.seededDDHDistinguisher`: DDH reduction that samples the public + seed internally. +* `Cslib.Crypto.PrimeOrderGroupFamily.linearHashKDF`: polynomial-time key-derivation function built + from `Cslib.BitString.padWord` and `Cslib.BitString.LinearHash.wordHash`. +* `Cslib.Crypto.PrimeOrderGroupFamily.linearHashSeedLen`: seed length + `msgLen n * (2 * bound d + 1)` for `linearHashKDF`. + +## Main results + +* `Cslib.Crypto.PrimeOrderGroupFamily.DDH.withSeed`: `DDH` is preserved under `seededSetup` when + `seedLen` is polynomial-time computable in unary. +* `Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_linearHashKDF`: `linearHashKDF` is + computable in polynomial time when `keyLen` and `bound` are polynomial-time computable in unary. +* `Cslib.Crypto.PrimeOrderGroupFamily.advantage_kdfGame_linearHashKDF_le`: unconditional Leftover + Hash Lemma bound on `Game.advantage` between `kdfRealGame` and `kdfIdealGame` + ([BonehShoup2023], Section 8.10.4, Theorem 8.11, p. 334, and Section 11.5.2, p. 449). +* `Cslib.Crypto.PrimeOrderGroupFamily.secureKDF_linearHashKDF`, + `Cslib.Crypto.PrimeOrderGroupFamily.secureKDF_linearHashKDF_const`, + `Cslib.Crypto.PrimeOrderGroupFamily.exists_secureKDF_withSeed`, + `Cslib.Crypto.PrimeOrderGroupFamily.DDH.negligible_hashedElGamalCPAGame_linearHashKDF`: + non-degenerate `SecureKDF` and Hashed ElGamal IND-CPA instantiations via `linearHashKDF`. + +## References + +* [D. Boneh, V. Shoup, *A Graduate Course in Applied Cryptography*, + Version 0.6][BonehShoup2023], Section 8.10.4 (Theorem 8.11, p. 334) and Section 11.5.2 + (Attack Game 11.3, Definition 11.5, and Theorem 11.5, pp. 448–451). +-/ + +@[expose] public section + +namespace Cslib.Crypto.PrimeOrderGroupFamily + +open Probability Probability.PMF Turing.MultiTapeTM +open scoped ENNReal NNReal Cslib.Probability.PMF + +variable (F : PrimeOrderGroupFamily) + +/-! ### Prime-order group family with a public seed in the description -/ + +/-- Augment a `PrimeOrderGroupFamily` with a public bit-string seed in the group description +(`Desc := F.Desc × List Bool`), as in [BonehShoup2023], Section 8.10.4 (p. 334), where the +universal-hash key is part of the public system parameter. All group operations act on the +underlying group description `d.1 : F.Desc`. -/ +abbrev withSeed : PrimeOrderGroupFamily where + Desc := F.Desc × List Bool + encDesc := encPair F.encDesc encBits + order d := F.order d.1 + prime_order d := F.prime_order d.1 + Carrier d := F.Carrier d.1 + addCommGroup d := F.addCommGroup d.1 + module d := F.module d.1 + generator d := F.generator d.1 + card_carrier d := F.card_carrier d.1 + generator_ne_zero d := F.generator_ne_zero d.1 + encode d := F.encode d.1 + encode_injective d := F.encode_injective d.1 + add input := F.add (input.1.1, input.2) + add_encode d x y := F.add_encode d.1 x y + smul input := F.smul (input.1.1, input.2) + smul_encode d a x := F.smul_encode d.1 a x + computableInPolyTime_order := + F.computableInPolyTime_order.comp (by fun_prop) + computableInPolyTime_generator := + F.computableInPolyTime_generator.comp (by fun_prop) + computableInPolyTime_add := + F.computableInPolyTime_add.comp + ((by fun_prop : ComputableInPolyTime + (fun input : (F.Desc × List Bool) × List Bool × List Bool => input.1.1) + (encPair (encPair F.encDesc encBits) (encPair encBits encBits)) F.encDesc).prod + (by fun_prop)) + computableInPolyTime_smul := + F.computableInPolyTime_smul.comp + ((by fun_prop : ComputableInPolyTime + (fun input : (F.Desc × List Bool) × ℕ × List Bool => input.1.1) + (encPair (encPair F.encDesc encBits) (encPair encNat encBits)) F.encDesc).prod + (by fun_prop)) + +/-- Setup distribution for `F.withSeed`: draw `d ← setup n` and an independent uniform seed +`s ← Cslib.BitString.uniformList (seedLen n d)`, and return `(d, s)`. -/ +noncomputable def seededSetup (setup : ℕ → PMF F.Desc) (seedLen : ℕ → F.Desc → ℕ) + (n : ℕ) : PMF F.withSeed.Desc := do + let d ← setup n + let s ← Cslib.BitString.uniformList (seedLen n d) + return (d, s) + +/-- Given a DDH distinguisher for `F.withSeed`, construct a DDH distinguisher for `F` by sampling +a fresh uniform seed `s ← Cslib.BitString.sampleList (seedLen n d)` and passing +`((d, s), u, v, w)` to `distinguisher`. -/ +noncomputable def seededDDHDistinguisher (seedLen : ℕ → F.Desc → ℕ) + (distinguisher : ℕ → F.withSeed.Desc × List Bool × List Bool × List Bool → ProbComp Bool) + (n : ℕ) (input : F.Desc × List Bool × List Bool × List Bool) : ProbComp Bool := do + let s ← Cslib.BitString.sampleList (seedLen n input.1) + distinguisher n ((input.1, s), input.2) + +/-- In `ddhRealGame`, `seededDDHDistinguisher` simulates `F.withSeed.ddhRealGame` under +`seededSetup`. -/ +@[simp] theorem ddhRealGame_seededDDHDistinguisher (setup : ℕ → PMF F.Desc) + (seedLen : ℕ → F.Desc → ℕ) + (distinguisher : ℕ → F.withSeed.Desc × List Bool × List Bool × List Bool → ProbComp Bool) + (n : ℕ) : + F.ddhRealGame setup (F.seededDDHDistinguisher seedLen distinguisher) n = + F.withSeed.ddhRealGame (F.seededSetup setup seedLen) distinguisher n := by + simp only [ddhRealGame, seededDDHDistinguisher, seededSetup, withSeed, ProbComp.eval_bind, + Cslib.BitString.eval_sampleList, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.bind_bind, + PMF.pure_bind] + congr 1; funext d + change _ = + (Cslib.BitString.uniformList (seedLen n d)).bind fun a => + (PMF.uniformOfFintype (ZMod (F.order d))).bind fun α => + (PMF.uniformOfFintype (ZMod (F.order d))).bind fun β => + ProbComp.eval (distinguisher n + ((d, a), F.encode d (α • F.generator d), F.encode d (β • F.generator d), + F.encode d ((α * β) • F.generator d))) + conv_rhs => rw [PMF.bind_comm] + congr 1; funext α + conv_rhs => rw [PMF.bind_comm] + +/-- In `ddhIdealGame`, `seededDDHDistinguisher` simulates `F.withSeed.ddhIdealGame` under +`seededSetup`. -/ +@[simp] theorem ddhIdealGame_seededDDHDistinguisher (setup : ℕ → PMF F.Desc) + (seedLen : ℕ → F.Desc → ℕ) + (distinguisher : ℕ → F.withSeed.Desc × List Bool × List Bool × List Bool → ProbComp Bool) + (n : ℕ) : + F.ddhIdealGame setup (F.seededDDHDistinguisher seedLen distinguisher) n = + F.withSeed.ddhIdealGame (F.seededSetup setup seedLen) distinguisher n := by + simp only [ddhIdealGame, seededDDHDistinguisher, seededSetup, withSeed, ProbComp.eval_bind, + Cslib.BitString.eval_sampleList, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.bind_bind, + PMF.pure_bind] + congr 1; funext d + change _ = + (Cslib.BitString.uniformList (seedLen n d)).bind fun a => + (PMF.uniformOfFintype (ZMod (F.order d))).bind fun α => + (PMF.uniformOfFintype (ZMod (F.order d))).bind fun β => + (PMF.uniformOfFintype (ZMod (F.order d))).bind fun γ => + ProbComp.eval (distinguisher n + ((d, a), F.encode d (α • F.generator d), F.encode d (β • F.generator d), + F.encode d (γ • F.generator d))) + conv_rhs => rw [PMF.bind_comm] + congr 1; funext α + conv_rhs => rw [PMF.bind_comm] + congr 1; funext β + conv_rhs => rw [PMF.bind_comm] + +/-- `seededDDHDistinguisher` is uniform strict PPT whenever `seedLen` is polynomial-time computable +in unary and `distinguisher` is uniform strict PPT. -/ +theorem isPPTOn_seededDDHDistinguisher {seedLen : ℕ → F.Desc → ℕ} + (hseed : ComputableInPolyTime (fun p : ℕ × F.Desc => seedLen p.1 p.2) + (encPair encUnary F.encDesc) encUnary) + {distinguisher : ℕ → F.withSeed.Desc × List Bool × List Bool × List Bool → ProbComp Bool} + (hD : IsPPTOn + (encPair encUnary (encPair F.withSeed.encDesc (encPair encBits (encPair encBits encBits)))) + encBool (fun input => distinguisher input.1 input.2)) : + IsPPTOn (encPair encUnary (encPair F.encDesc (encPair encBits (encPair encBits encBits)))) + encBool (fun input => F.seededDDHDistinguisher seedLen distinguisher input.1 input.2) := by + let EIn := encPair encUnary (encPair F.encDesc (encPair encBits (encPair encBits encBits))) + have hprep : ComputableInPolyTime + (fun input : ℕ × F.Desc × List Bool × List Bool × List Bool => (input.1, input.2.1)) + EIn (encPair encUnary F.encDesc) := by fun_prop + have hlen : ComputableInPolyTime + (fun input : ℕ × F.Desc × List Bool × List Bool × List Bool => seedLen input.1 input.2.1) + EIn encUnary := hseed.comp hprep + have hsample : IsPPTOn EIn encBits + (fun input : ℕ × F.Desc × List Bool × List Bool × List Bool => + Cslib.BitString.sampleList (seedLen input.1 input.2.1)) := + ComputableInPolyTime.sampleList hlen + unfold seededDDHDistinguisher + refine hsample.bind_with ?_ + change IsPPTOn (encPair EIn encBits) encBool + (fun p : (ℕ × F.Desc × List Bool × List Bool × List Bool) × List Bool => + distinguisher p.1.1 ((p.1.2.1, p.2), p.1.2.2)) + refine hD.preprocess + (prepare := fun p : (ℕ × F.Desc × List Bool × List Bool × List Bool) × List Bool => + (p.1.1, ((p.1.2.1, p.2), p.1.2.2))) ?_ + change ComputableInPolyTime + (fun p : (ℕ × F.Desc × List Bool × List Bool × List Bool) × List Bool => + (p.1.1, ((p.1.2.1, p.2), p.1.2.2))) + (encPair EIn encBits) + (encPair encUnary + (encPair (encPair F.encDesc encBits) + (encPair encBits (encPair encBits encBits)))) + fun_prop + +/-- **Preservation of `DDH` under public-seed augmentation**: if `F.DDH setup` holds and +`seedLen` is polynomial-time computable in unary, then `F.withSeed.DDH (F.seededSetup setup +seedLen)` holds. -/ +theorem DDH.withSeed {F : PrimeOrderGroupFamily} {setup : ℕ → PMF F.Desc} + {seedLen : ℕ → F.Desc → ℕ} (hDDH : F.DDH setup) + (hseed : ComputableInPolyTime (fun p : ℕ × F.Desc => seedLen p.1 p.2) + (encPair encUnary F.encDesc) encUnary) : + F.withSeed.DDH (F.seededSetup setup seedLen) := by + intro distinguisher hD + simpa only [F.ddhRealGame_seededDDHDistinguisher, F.ddhIdealGame_seededDDHDistinguisher] using + hDDH (F.seededDDHDistinguisher seedLen distinguisher) + (F.isPPTOn_seededDDHDistinguisher hseed hD) + +/-! ### Binary Linear-Hash Key Derivation and Leftover Hash Lemma -/ + +/-- Binary linear-hash key derivation function ([BonehShoup2023], Section 8.10.4, Theorem 8.11, +p. 334, and Section 11.5.2, p. 449): given a seeded group description `(d, s) : F.withSeed.Desc` +and an encoded group element `w : List Bool`, pad `w` to the self-delimiting width +`2 * bound d + 1` via `Cslib.BitString.padWord (bound d) w` and hash with the public seed `s` +via `Cslib.BitString.LinearHash.wordHash (keyLen d) s`. -/ +def linearHashKDF (keyLen bound : F.Desc → ℕ) + (input : F.withSeed.Desc × List Bool) : List Bool := + Cslib.BitString.LinearHash.wordHash (keyLen input.1.1) input.1.2 + (Cslib.BitString.padWord (bound input.1.1) input.2) + +/-- `linearHashKDF` always outputs a word of length `keyLen input.1.1`. -/ +@[simp] theorem length_linearHashKDF (keyLen bound : F.Desc → ℕ) + (input : F.withSeed.Desc × List Bool) : + (F.linearHashKDF keyLen bound input).length = keyLen input.1.1 := by + simp [linearHashKDF] + +/-- `linearHashKDF` is computable in polynomial time whenever `keyLen` and `bound` are computable +in polynomial time in unary from the group description `d : F.Desc`. -/ +theorem computableInPolyTime_linearHashKDF {keyLen bound : F.Desc → ℕ} + (hkey : ComputableInPolyTime keyLen F.encDesc encUnary) + (hbound : ComputableInPolyTime bound F.encDesc encUnary) : + ComputableInPolyTime (F.linearHashKDF keyLen bound) + (encPair F.withSeed.encDesc encBits) encBits := by + let EIn := encPair (encPair F.encDesc encBits) encBits + have hd : ComputableInPolyTime + (fun input : (F.Desc × List Bool) × List Bool => input.1.1) EIn F.encDesc := by fun_prop + have hkeyIn : ComputableInPolyTime + (fun input : (F.Desc × List Bool) × List Bool => keyLen input.1.1) EIn encUnary := + hkey.comp hd + have hboundIn : ComputableInPolyTime + (fun input : (F.Desc × List Bool) × List Bool => bound input.1.1) EIn encUnary := + hbound.comp hd + change ComputableInPolyTime + (fun input : (F.Desc × List Bool) × List Bool => + Cslib.BitString.LinearHash.wordHash (keyLen input.1.1) input.1.2 + (Cslib.BitString.padWord (bound input.1.1) input.2)) + EIn encBits + fun_prop + +/-- The matrix seed length required by `linearHashKDF` for output length `msgLen n` and encoding +length bound `bound d`: `msgLen n * (2 * bound d + 1)` bits. -/ +def linearHashSeedLen (msgLen : ℕ → ℕ) (bound : F.Desc → ℕ) (n : ℕ) (d : F.Desc) : ℕ := + msgLen n * (2 * bound d + 1) + +/-- `linearHashSeedLen` is computable in polynomial time in unary whenever `msgLen` and `bound` +are computable in polynomial time in unary. -/ +theorem computableInPolyTime_linearHashSeedLen {msgLen : ℕ → ℕ} {bound : F.Desc → ℕ} + (hmsg : ComputableInPolyTime msgLen encUnary encUnary) + (hbound : ComputableInPolyTime bound F.encDesc encUnary) : + ComputableInPolyTime (fun p : ℕ × F.Desc => F.linearHashSeedLen msgLen bound p.1 p.2) + (encPair encUnary F.encDesc) encUnary := by + have hmsgIn : ComputableInPolyTime (fun p : ℕ × F.Desc => msgLen p.1) + (encPair encUnary F.encDesc) encUnary := hmsg.comp (by fun_prop) + have hboundIn : ComputableInPolyTime (fun p : ℕ × F.Desc => bound p.2) + (encPair encUnary F.encDesc) encUnary := hbound.comp (by fun_prop) + unfold linearHashSeedLen + fun_prop + +/-- Self-delimiting padded bit-string encoding of `γ • g` in `BitString (2 * bound d + 1)`. -/ +def paddedGeneratorMultiple (bound : F.Desc → ℕ) (d : F.Desc) + (γ : ZMod (F.order d)) : BitString (2 * bound d + 1) := + Cslib.BitString.ofList (2 * bound d + 1) + (Cslib.BitString.padWord (bound d) (F.encode d (γ • F.generator d))) + +/-- When every encoded group element in `F.Carrier d` has bit-length at most `bound d`, +`List.ofFn (F.paddedGeneratorMultiple bound d γ)` recovers the padded word +`Cslib.BitString.padWord (bound d) (F.encode d (γ • F.generator d))`. -/ +theorem ofFn_paddedGeneratorMultiple {bound : F.Desc → ℕ} {d : F.Desc} + (hbound : ∀ x : F.Carrier d, (F.encode d x).length ≤ bound d) + (γ : ZMod (F.order d)) : + List.ofFn (F.paddedGeneratorMultiple bound d γ) = + Cslib.BitString.padWord (bound d) (F.encode d (γ • F.generator d)) := + Cslib.BitString.ofFn_ofList + (Cslib.BitString.length_padWord (hbound (γ • F.generator d))) + +/-- When every encoded group element in `F.Carrier d` has bit-length at most `bound d`, +`paddedGeneratorMultiple bound d` is injective on `ZMod (F.order d)`. -/ +theorem paddedGeneratorMultiple_injective {bound : F.Desc → ℕ} {d : F.Desc} + (hbound : ∀ x : F.Carrier d, (F.encode d x).length ≤ bound d) : + Function.Injective (F.paddedGeneratorMultiple bound d) := by + intro γ₁ γ₂ h + unfold paddedGeneratorMultiple at h + have hpad : F.encode d (γ₁ • F.generator d) = F.encode d (γ₂ • F.generator d) := + Cslib.BitString.word_eq_of_paddedBits_eq + (hbound (γ₁ • F.generator d)) (hbound (γ₂ • F.generator d)) h + exact F.smul_generator_injective d (F.encode_injective d hpad) + +/-- **Unconditional Leftover Hash Lemma bound for `linearHashKDF`** ([BonehShoup2023], +Section 8.10.4, Theorem 8.11, p. 334, and Section 11.5.2, p. 449): for every (even computationally +unbounded) distinguisher, when every `d ∈ (setup n).support` satisfies `keyLen d = msgLen n`, +`∀ x, (F.encode d x).length ≤ bound d`, and `qMin ≤ F.order d` with `0 < qMin`, the distinguishing +advantage between `kdfRealGame` and `kdfIdealGame` under `F.seededSetup` and `F.linearHashKDF` is at +most `NNReal.sqrt ((2 : ℝ≥0) ^ (msgLen n) / (qMin : ℝ≥0)) / 2`. -/ +theorem advantage_kdfGame_linearHashKDF_le (setup : ℕ → PMF F.Desc) + (keyLen bound : F.Desc → ℕ) (msgLen : ℕ → ℕ) + (distinguisher : ℕ → F.withSeed.Desc × List Bool × List Bool × List Bool → ProbComp Bool) + (n qMin : ℕ) (hq0 : 0 < qMin) + (hkey : ∀ d ∈ (setup n).support, keyLen d = msgLen n) + (hbound : ∀ d ∈ (setup n).support, ∀ x : F.Carrier d, (F.encode d x).length ≤ bound d) + (hq : ∀ d ∈ (setup n).support, qMin ≤ F.order d) : + Game.advantage + (F.withSeed.kdfRealGame (F.seededSetup setup (F.linearHashSeedLen msgLen bound)) + (F.linearHashKDF keyLen bound) distinguisher n) + (F.withSeed.kdfIdealGame (F.seededSetup setup (F.linearHashSeedLen msgLen bound)) + msgLen distinguisher n) ≤ + NNReal.sqrt ((2 : ℝ≥0) ^ (msgLen n) / (qMin : ℝ≥0)) / 2 := by + simp only [kdfRealGame, kdfIdealGame, seededSetup, withSeed, PMF.monad_bind_eq_bind, + PMF.monad_pure_eq_pure, PMF.bind_bind, PMF.pure_bind] + refine Game.advantage_bind_le_of_support (setup n) _ _ fun d hd => ?_ + change Game.advantage + ((Cslib.BitString.uniformList (F.linearHashSeedLen msgLen bound n d)).bind fun a => + (PMF.uniformOfFintype (ZMod (F.order d))).bind fun α => + (PMF.uniformOfFintype (ZMod (F.order d))).bind fun β => + (PMF.uniformOfFintype (ZMod (F.order d))).bind fun γ => + ProbComp.eval (distinguisher n + ((d, a), F.encode d (α • F.generator d), F.encode d (β • F.generator d), + F.linearHashKDF keyLen bound ((d, a), F.encode d (γ • F.generator d))))) + ((Cslib.BitString.uniformList (F.linearHashSeedLen msgLen bound n d)).bind fun a => + (PMF.uniformOfFintype (ZMod (F.order d))).bind fun α => + (PMF.uniformOfFintype (ZMod (F.order d))).bind fun β => + (Cslib.BitString.uniformList (msgLen n)).bind fun pad => + ProbComp.eval (distinguisher n + ((d, a), F.encode d (α • F.generator d), F.encode d (β • F.generator d), + pad))) ≤ _ + rw [Game.advantage_bind_comm] + refine Game.advantage_bind_le_nnreal (PMF.uniformOfFintype (ZMod (F.order d))) _ _ fun α => ?_ + rw [Game.advantage_bind_comm] + refine Game.advantage_bind_le_nnreal (PMF.uniformOfFintype (ZMod (F.order d))) _ _ fun β => ?_ + let m := msgLen n + let W := 2 * bound d + 1 + let source : PMF (BitString W) := + (PMF.uniformOfFintype (ZMod (F.order d))).map (F.paddedGeneratorMultiple bound d) + let test : BitString (m * W) × BitString m → Game := fun pair => + ProbComp.eval (distinguisher n + ((d, List.ofFn pair.1), F.encode d (α • F.generator d), F.encode d (β • F.generator d), + List.ofFn pair.2)) + have hreal : + (Cslib.BitString.uniformList (F.linearHashSeedLen msgLen bound n d)).bind (fun s => + (PMF.uniformOfFintype (ZMod (F.order d))).bind fun γ => + ProbComp.eval (distinguisher n + ((d, s), F.encode d (α • F.generator d), F.encode d (β • F.generator d), + F.linearHashKDF keyLen bound ((d, s), F.encode d (γ • F.generator d))))) = + (seededHash (PMF.uniformOfFintype (BitString (m * W))) source + (fun seed => + Cslib.BitString.LinearHash.hash + (Cslib.BitString.blocksEquiv (m := m) (k := W) seed))).bind test := by + simp only [linearHashSeedLen, Cslib.BitString.uniformList, seededHash_eq_bind, source, test, + PMF.bind_map, PMF.bind_bind, Function.comp_def] + conv_rhs => rw [PMF.bind_comm] + congr 1; funext seed + congr 1; funext γ + have hpad := F.ofFn_paddedGeneratorMultiple (hbound d hd) γ + have hhash : + F.linearHashKDF keyLen bound ((d, List.ofFn seed), F.encode d (γ • F.generator d)) = + List.ofFn (Cslib.BitString.LinearHash.hash + (Cslib.BitString.blocksEquiv (m := m) (k := W) seed) + (F.paddedGeneratorMultiple bound d γ)) := by + simp only [linearHashKDF, hkey d hd, ← hpad, Cslib.BitString.LinearHash.wordHash_eq_ofFn, + Cslib.BitString.ofList_ofFn, Cslib.BitString.blocksEquiv_apply] + rw [hhash] + have hideal : + (Cslib.BitString.uniformList (F.linearHashSeedLen msgLen bound n d)).bind (fun s => + (Cslib.BitString.uniformList m).bind fun pad => + ProbComp.eval (distinguisher n + ((d, s), F.encode d (α • F.generator d), F.encode d (β • F.generator d), pad))) = + ((PMF.uniformOfFintype (BitString (m * W))).bind fun seed => + (PMF.uniformOfFintype (BitString m)).map (seed, ·)).bind test := by + simp only [linearHashSeedLen, Cslib.BitString.uniformList, test, + PMF.bind_map, PMF.bind_bind, Function.comp_def] + rfl + rw [hreal, hideal, Game.advantage_eq_nndist, ← NNReal.coe_le_coe, coe_nndist] + have hlhl := (Cslib.BitString.LinearHash.isTwoUniversal_flat W m).leftover_hash source + have hcoll : collisionProbability source = (F.order d : ℝ)⁻¹ := by + simp only [source, + collisionProbability_map_of_injective _ _ (F.paddedGeneratorMultiple_injective (hbound d hd)), + collisionProbability_uniform, ZMod.card] + have hcard : (Fintype.card (BitString m) : ℝ) = (2 : ℝ) ^ m := by + simp [BitString] + have hord_le : (F.order d : ℝ)⁻¹ ≤ (qMin : ℝ)⁻¹ := + inv_anti₀ (by exact_mod_cast hq0) (by exact_mod_cast hq d hd) + calc dist + ((seededHash (PMF.uniformOfFintype (BitString (m * W))) source + (fun seed => + Cslib.BitString.LinearHash.hash + (Cslib.BitString.blocksEquiv (m := m) (k := W) seed))).bind test) + (((PMF.uniformOfFintype (BitString (m * W))).bind fun seed => + (PMF.uniformOfFintype (BitString m)).map (seed, ·)).bind test) + ≤ dist + (seededHash (PMF.uniformOfFintype (BitString (m * W))) source + (fun seed => + Cslib.BitString.LinearHash.hash + (Cslib.BitString.blocksEquiv (m := m) (k := W) seed))) + ((PMF.uniformOfFintype (BitString (m * W))).bind fun seed => + (PMF.uniformOfFintype (BitString m)).map (seed, ·)) := + dist_bind_le _ _ _ + _ ≤ Real.sqrt (Fintype.card (BitString m) * collisionProbability source) / 2 := hlhl + _ = Real.sqrt ((2 : ℝ) ^ m * (F.order d : ℝ)⁻¹) / 2 := by rw [hcard, hcoll] + _ ≤ Real.sqrt ((2 : ℝ) ^ m * (qMin : ℝ)⁻¹) / 2 := by + gcongr + _ = ↑(NNReal.sqrt ((2 : ℝ≥0) ^ m / (qMin : ℝ≥0)) / 2) := by + push_cast + rw [← div_eq_mul_inv] + +/-- **Unconditional `SecureKDF` instantiation via `linearHashKDF`** ([BonehShoup2023], +Section 8.10.4, Theorem 8.11, p. 334, and Section 11.5.2, Definition 11.5, p. 449): when `keyLen` +matches `msgLen n` on `(setup n).support`, `bound` bounds the encoded group element length, and +`2 ^ (msgLen n) / qMin n` is negligible, `linearHashKDF keyLen bound` satisfies `SecureKDF` over +`F.withSeed` and `F.seededSetup setup (F.linearHashSeedLen msgLen bound)`. -/ +theorem secureKDF_linearHashKDF (setup : ℕ → PMF F.Desc) + (keyLen bound : F.Desc → ℕ) (msgLen : ℕ → ℕ) {qMin : ℕ → ℕ} + (hq0 : ∀ n, 0 < qMin n) + (hkey : ∀ n, ∀ d ∈ (setup n).support, keyLen d = msgLen n) + (hbound : ∀ n, ∀ d ∈ (setup n).support, ∀ x : F.Carrier d, (F.encode d x).length ≤ bound d) + (hq : ∀ n, ∀ d ∈ (setup n).support, qMin n ≤ F.order d) + (hneg : Negligible fun n => (2 : ℝ≥0) ^ (msgLen n) / (qMin n : ℝ≥0)) : + F.withSeed.SecureKDF (F.seededSetup setup (F.linearHashSeedLen msgLen bound)) + (F.linearHashKDF keyLen bound) msgLen := by + intro distinguisher _ + have hsqrt : Negligible fun n => NNReal.sqrt ((2 : ℝ≥0) ^ (msgLen n) / (qMin n : ℝ≥0)) / 2 := by + have h1 : Negligible fun n => + (2⁻¹ : ℝ≥0) * NNReal.sqrt ((2 : ℝ≥0) ^ (msgLen n) / (qMin n : ℝ≥0)) := + (Negligible.sqrt hneg).const_mul (2⁻¹ : ℝ≥0) + simpa only [div_eq_inv_mul] using h1 + exact negligible_of_le hsqrt fun n => + F.advantage_kdfGame_linearHashKDF_le setup keyLen bound msgLen distinguisher n (qMin n) + (hq0 n) (hkey n) (hbound n) (hq n) + +/-- **Unconditional `SecureKDF` instantiation for any constant key length `k : ℕ`** (including all +non-degenerate `k > 0`, e.g., `k = 128` as in [BonehShoup2023], Section 8.10.4, p. 334): when +`1 / qMin n` is negligible, `linearHashKDF (fun _ => k) bound` is a `SecureKDF` with output length +`fun _ => k`. -/ +theorem secureKDF_linearHashKDF_const (setup : ℕ → PMF F.Desc) + (bound : F.Desc → ℕ) (k : ℕ) {qMin : ℕ → ℕ} + (hq0 : ∀ n, 0 < qMin n) + (hbound : ∀ n, ∀ d ∈ (setup n).support, ∀ x : F.Carrier d, (F.encode d x).length ≤ bound d) + (hq : ∀ n, ∀ d ∈ (setup n).support, qMin n ≤ F.order d) + (hneg : Negligible fun n => (1 / qMin n : ℝ≥0)) : + F.withSeed.SecureKDF (F.seededSetup setup (F.linearHashSeedLen (fun _ => k) bound)) + (F.linearHashKDF (fun _ => k) bound) (fun _ => k) := by + refine F.secureKDF_linearHashKDF setup (fun _ => k) bound (fun _ => k) hq0 + (fun _ _ _ => rfl) hbound hq ?_ + have hk : Negligible fun n => (2 : ℝ≥0) ^ k * (1 / qMin n : ℝ≥0) := + hneg.const_mul ((2 : ℝ≥0) ^ k) + simpa only [div_eq_mul_inv, one_mul] using hk + +/-- **Existence of a polynomial-time non-degenerate `SecureKDF` for any `PrimeOrderGroupFamily`** +with super-polynomial group order: using the canonical polynomial encoding-length bound from +`F.exists_length_encode_le`, for every key length `k : ℕ` (in particular any `k > 0`) there exist a +unary polynomial-time seed-length function `seedLen` and a polynomial-time hash function +`H : F.withSeed.Desc × List Bool → List Bool` such that `F.withSeed.SecureKDF +(F.seededSetup setup seedLen) H (fun _ => k)` holds whenever `1 / qMin n` is negligible. -/ +theorem exists_secureKDF_withSeed (setup : ℕ → PMF F.Desc) (k : ℕ) {qMin : ℕ → ℕ} + (hq0 : ∀ n, 0 < qMin n) + (hq : ∀ n, ∀ d ∈ (setup n).support, qMin n ≤ F.order d) + (hneg : Negligible fun n => (1 / qMin n : ℝ≥0)) : + ∃ (seedLen : ℕ → F.Desc → ℕ) (H : F.withSeed.Desc × List Bool → List Bool), + ComputableInPolyTime (fun p : ℕ × F.Desc => seedLen p.1 p.2) + (encPair encUnary F.encDesc) encUnary ∧ + ComputableInPolyTime H (encPair F.withSeed.encDesc encBits) encBits ∧ + (∀ ds w, (H (ds, w)).length = k) ∧ + F.withSeed.SecureKDF (F.seededSetup setup seedLen) H (fun _ => k) := by + obtain ⟨c, e, hce⟩ := F.exists_length_encode_le + let bound : F.Desc → ℕ := fun d => c * ((F.encDesc d).length + 1) ^ e + have hbound_poly : ComputableInPolyTime bound F.encDesc encUnary := by + dsimp [bound] + fun_prop + have hkey_poly : ComputableInPolyTime (fun _ : F.Desc => k) F.encDesc encUnary := by fun_prop + have hmsg_poly : ComputableInPolyTime (fun _ : ℕ => k) encUnary encUnary := by fun_prop + refine ⟨F.linearHashSeedLen (fun _ => k) bound, F.linearHashKDF (fun _ => k) bound, + F.computableInPolyTime_linearHashSeedLen hmsg_poly hbound_poly, + F.computableInPolyTime_linearHashKDF hkey_poly hbound_poly, + fun ds w => F.length_linearHashKDF (fun _ => k) bound (ds, w), + F.secureKDF_linearHashKDF_const setup bound k hq0 (fun _ d _ x => hce d x) hq hneg⟩ + +/-- **Hashed ElGamal with `linearHashKDF` is IND-CPA secure under `F.DDH setup` alone** +([BonehShoup2023], 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`, and +`DDH.negligible_hashedElGamalCPAGame`, no computational hypothesis on the key-derivation hash is +needed when `2 ^ (msgLen n) / qMin n` is negligible. -/ +theorem DDH.negligible_hashedElGamalCPAGame_linearHashKDF {F : PrimeOrderGroupFamily} + {setup : ℕ → PMF F.Desc} {keyLen bound : F.Desc → ℕ} {msgLen qMin : ℕ → ℕ} + (hDDH : F.DDH setup) + (hkey_poly : ComputableInPolyTime keyLen F.encDesc encUnary) + (hbound_poly : ComputableInPolyTime bound F.encDesc encUnary) + (hmsg_poly : ComputableInPolyTime msgLen encUnary encUnary) + (hq0 : ∀ n, 0 < qMin n) + (hkey : ∀ n, ∀ d ∈ (setup n).support, keyLen d = msgLen n) + (hbound : ∀ n, ∀ d ∈ (setup n).support, ∀ x : F.Carrier d, (F.encode d x).length ≤ bound d) + (hq : ∀ n, ∀ d ∈ (setup n).support, qMin n ≤ F.order d) + (hneg : Negligible fun n => (2 : ℝ≥0) ^ (msgLen n) / (qMin n : ℝ≥0)) + {adversary : Encryption.WordAdversary} (hA : adversary.IsPPT) : + Negligible fun n => + Game.advantage + (F.withSeed.hashedElGamalCPAGame + (F.seededSetup setup (F.linearHashSeedLen msgLen bound)) + (F.linearHashKDF keyLen bound) adversary false n) + (F.withSeed.hashedElGamalCPAGame + (F.seededSetup setup (F.linearHashSeedLen msgLen bound)) + (F.linearHashKDF keyLen bound) adversary true n) := + (hDDH.withSeed (F.computableInPolyTime_linearHashSeedLen hmsg_poly hbound_poly)) + |>.negligible_hashedElGamalCPAGame + (F.secureKDF_linearHashKDF setup keyLen bound msgLen hq0 hkey hbound hq hneg) + (F.computableInPolyTime_linearHashKDF hkey_poly hbound_poly) hA + +end Cslib.Crypto.PrimeOrderGroupFamily diff --git a/Complexity/Crypto/Computational/ElGamal/ProbComp.lean b/Complexity/Crypto/Computational/ElGamal/ProbComp.lean new file mode 100644 index 000000000..236dd315e --- /dev/null +++ b/Complexity/Crypto/Computational/ElGamal/ProbComp.lean @@ -0,0 +1,747 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Crypto.Computational.ElGamal +public import Complexity.Crypto.Computational.Encryption.Hybrid +public import Complexity.Languages.Probabilistic.UniformNat +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.BinaryDiv +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain +import Complexity.Computability.Probabilistic.Sampling +import Complexity.Computability.Probabilistic.UniformNat +import Complexity.Crypto.Game.Statistical +import Complexity.Crypto.Negligible.Basic +import Complexity.Probability.PMF +import Complexity.Probability.PMF.Event +import Complexity.Probability.StatisticalDistance +import Complexity.Tactic.PolyTime +import Complexity.Tactic.PPT + +/-! +# Strict-PPT ElGamal Key Generation, KEM Encapsulation, and `Encryption.INDCPAOn` Bridges + +This module defines uniform strict-PPT (`IsPPTOn`) key generation, encapsulation, decapsulation, +and encryption for multiplicative ElGamal and Hashed ElGamal ([BonehShoup2023], Section 11.5, +pp. 445–446, Remark 11.1, Section 11.5.2, Theorem 11.5, pp. 449–451, Exercise 11.5(a), p. 459, and +Exercise 11.9, pp. 460–461) using `ProbComp.sampleModNat`, and connects the PMF-level ElGamal games +in `Complexity/Crypto/Computational/ElGamal.lean` directly to `Encryption.KEMINDCPA`, +`Encryption.INDCPAOf`, `Encryption.INDCPAOn`, and `Encryption.INDCPA`. + +* **Paraphrase of [BonehShoup2023], Section 11.5 (p. 445) and Remark 11.1 (p. 446):** 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, encapsulation/encryption + samples $\beta \leftarrow \mathbb{Z}_q$, sets $v = \beta \cdot g$ and $w = \beta \cdot u$, + derives the symmetric key $k = H(w)$, and encrypts $m$ under $k$; decapsulation/decryption + computes $w = \alpha \cdot v$, recovers $k = H(w)$, and decrypts $c$ under $k$. +* **Paraphrase of [BonehShoup2023], Exercise 11.5(a) (p. 459) and Exercise 11.9 (pp. 460–461):** + multiplicative ElGamal encrypts a group element $m \in G$ as $(\beta \cdot g, \beta \cdot u + m)$ + and is IND-CPA secure under DDH; Hashed ElGamal acts as an IND-CPA secure KEM under DDH and + `SecureKDF`, and composing it with any one-time semantically secure DEM yields an IND-CPA secure + public-key encryption scheme. + +## Main definitions + +* `Cslib.Crypto.PrimeOrderGroupFamily.sampleElGamalExp`: approximate uniform exponent sampling + modulo `F.order d` via `ProbComp.sampleModNat` with statistical distance at most `1 / 2 ^ n`. +* `Cslib.Crypto.PrimeOrderGroupFamily.elGamalKeyGenProb`: uniform strict-PPT ElGamal key + generation. +* `Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalEncapsProb`, + `Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalDecaps`: uniform strict-PPT Hashed ElGamal KEM + encapsulation and deterministic polynomial-time decapsulation. +* `Cslib.Crypto.PrimeOrderGroupFamily.kemToDDHDistinguisher`, + `Cslib.Crypto.PrimeOrderGroupFamily.kemToKDFDistinguisher`: DDH and KDF reductions from a KEM + distinguisher. +* `Cslib.Crypto.PrimeOrderGroupFamily.elGamalEncryptProb`, + `Cslib.Crypto.PrimeOrderGroupFamily.elGamalDecryptDet`: uniform strict-PPT multiplicative ElGamal + encryption and deterministic polynomial-time decryption. + +## Main results + +* `Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalDecaps_hashedElGamalEncapsProb`, + `Cslib.Crypto.PrimeOrderGroupFamily.elGamalDecryptDet_elGamalEncryptProb`: support-level + decapsulation and decryption correctness. +* `Cslib.Crypto.PrimeOrderGroupFamily.advantage_kemGame_hashedElGamalEncapsProb_le`, + `Cslib.Crypto.PrimeOrderGroupFamily.DDH.kemINDCPA_hashedElGamalEncapsProb`: quantitative KEM + advantage bound and `Encryption.KEMINDCPA` security of Hashed ElGamal under `DDH` and + `SecureKDF`. +* `Cslib.Crypto.PrimeOrderGroupFamily.DDH.indcpaOf_hybrid_hashedElGamal`, + `Cslib.Crypto.PrimeOrderGroupFamily.DDH.indcpaOn_hybrid_hashedElGamal`, + `Cslib.Crypto.PrimeOrderGroupFamily.DDH.wordINDCPA_hybrid_hashedElGamal`: Theorem 11.5 via + `Encryption.INDCPAOf`, `Encryption.INDCPAOn`, and `Encryption.WordINDCPA` for any one-time + semantically secure symmetric cipher (`Encryption.DEMOneTimeINDCPAOf` / + `Encryption.DEMOneTimeINDCPAOn` / `Encryption.DEMOneTimeWordINDCPA`). +* `Cslib.Crypto.PrimeOrderGroupFamily.DDH.indcpaOn_elGamalEncryptProb`, + `Cslib.Crypto.PrimeOrderGroupFamily.DDH.indcpa_elGamalBitEncryptProb`: multiplicative and bit + ElGamal satisfy `Encryption.INDCPAOn` and `Encryption.INDCPA` under `DDH`. + +## References + +* [D. Boneh, V. Shoup, *A Graduate Course in Applied Cryptography*, + Version 0.6][BonehShoup2023], Section 11.5 (pp. 445–446, Remark 11.1), Section 11.5.2 + (pp. 448–451, Theorem 11.5), Exercise 11.5(a) (p. 459), and Exercise 11.9 (pp. 460–461). +-/ + +@[expose] public section + +namespace Cslib.Crypto.PrimeOrderGroupFamily + +open Probability Turing.MultiTapeTM Encryption Game +open scoped ENNReal NNReal + +variable (F : PrimeOrderGroupFamily) + +private theorem negligible_const_div_two_pow (c : ℕ) : + Negligible (fun n => (c : ℝ≥0) / 2 ^ n) := by + have h : (fun n => (c : ℝ≥0) / 2 ^ n) = + fun n => (c : ℝ≥0) * (1 / 2 : ℝ≥0) ^ n := by + funext n + rw [div_eq_mul_inv, one_div, inv_pow] + rw [h] + exact (negligible_geometric (ratio := (1 / 2 : ℝ≥0)) (by norm_num)).polynomiallyBounded_mul + (by fun_prop) + +private theorem dropFrame_encPair_encBits {α : Type} (e : α ↪ List Bool) (a : α) + (s : List Bool) : dropFrame (encPair e encBits (a, s)) = s := by + simp [encPair_apply] + +private theorem unframe_encPair_encBits (p : List Bool × List Bool) : + unframe (encPair encBits encBits p) = p.1 := by + simp [encPair_apply] + +private theorem dropFrame_encPair_encBits_pair (p : List Bool × List Bool) : + dropFrame (encPair encBits encBits p) = p.2 := by + simp [encPair_apply] + +/-- Sample one approximate uniform exponent modulo `F.order d` using `n + |encNat (F.order d)|` +fair coins via `ProbComp.sampleModNat`, within statistical distance `1 / 2 ^ n` of exact uniform on +`ZMod (F.order d)`. -/ +noncomputable def sampleElGamalExp (n : ℕ) (d : F.Desc) : ProbComp ℕ := + ProbComp.sampleModNat (n + (encNat (F.order d)).length) (F.order d) + +private theorem isPPTOn_sampleElGamalExp {γ : Type} {encIn : γ ↪ List Bool} + {n : γ → ℕ} {d : γ → F.Desc} + (hn : ComputableTidilyInPolyTime n encIn encUnary) + (hd : ComputableTidilyInPolyTime d encIn F.encDesc) : + IsPPTOn encIn encNat (fun a => F.sampleElGamalExp (n a) (d a)) := by + have hord : ComputableTidilyInPolyTime (fun a => F.order (d a)) encIn encNat := + F.computableInPolyTime_order.tidy.comp hd + have hlen : ComputableTidilyInPolyTime + (fun a => (encNat (F.order (d a))).length) encIn encUnary := + (ComputableTidilyInPolyTime.encoding_length encNat).comp hord + have hadd : ComputableTidilyInPolyTime (fun p : ℕ × ℕ => p.1 + p.2) + (encPair encUnary encUnary) encUnary := by fun_prop + have hwidth : ComputableTidilyInPolyTime + (fun a => n a + (encNat (F.order (d a))).length) encIn encUnary := + hadd.comp (hn.prod hlen) + exact isPPTOn_sampleModNat (.of_tidy hwidth) (.of_tidy hord) + +/-- Replacing one `sampleElGamalExp n d` draw by an exact uniform draw on `ZMod (F.order d)` +changes `Game.advantage` by at most `1 / 2 ^ n`. -/ +theorem advantage_bind_sampleElGamalExp_le (n : ℕ) (d : F.Desc) + (k : ZMod (F.order d) → Game) : + Game.advantage + ((ProbComp.eval (F.sampleElGamalExp n d)).bind fun s => k (s : ZMod (F.order d))) + ((PMF.uniformOfFintype (ZMod (F.order d))).bind k) ≤ + 1 / 2 ^ n := by + open scoped Cslib.Probability.PMF in + have hmap : + ((ProbComp.eval (F.sampleElGamalExp n d)).bind fun s => k (s : ZMod (F.order d))) = + ((ProbComp.eval (F.sampleElGamalExp n d)).map + (Nat.cast : ℕ → ZMod (F.order d))).bind k := + (PMF.bind_map _ _ _).symm + have hlt : F.order d < 2 ^ (encNat (F.order d)).length := by + simpa only [encNat_apply, ← Nat.size_eq_bits_len] using Nat.lt_size_self (F.order d) + have hord_le : (F.order d : ℝ) ≤ 2 ^ (encNat (F.order d)).length := by + exact_mod_cast hlt.le + rw [← NNReal.coe_le_coe, hmap, Game.advantage_eq_nndist, coe_nndist] + refine (PMF.dist_bind_le _ _ k).trans ?_ + refine (ProbComp.dist_map_natCast_eval_sampleModNat_le + (n + (encNat (F.order d)).length) (F.order d)).trans ?_ + rw [Nat.add_comm n, pow_add, ← div_div] + have hdiv : (F.order d : ℝ) / 2 ^ (encNat (F.order d)).length ≤ 1 := + (div_le_one (by positivity)).mpr hord_le + have hbound : + (F.order d : ℝ) / 2 ^ (encNat (F.order d)).length / 2 ^ n ≤ 1 / 2 ^ n := + div_le_div_of_nonneg_right hdiv (by positivity) + simpa using hbound + +/-- Probabilistic polynomial-time ElGamal key generation for a group description family +`d : ℕ → F.Desc` ([BonehShoup2023], Section 11.5, p. 445, and Exercise 11.5, p. 459): sample +`a ← sampleElGamalExp n (d n)` and output +`(encPair F.encDesc encBits (d n, encode (a • g)), encNat a)`. -/ +noncomputable def elGamalKeyGenProb (d : ℕ → F.Desc) (n : ℕ) : + ProbComp (List Bool × List Bool) := + F.sampleElGamalExp n (d n) >>= fun a => + pure (encPair F.encDesc encBits (d n, F.encodeElGamalPublicKey (d n, a)), encNat a) + +/-- `elGamalKeyGenProb` is uniformly strict PPT whenever `d` is computable in polynomial time. -/ +theorem isPPTOn_elGamalKeyGenProb {d : ℕ → F.Desc} + (hd : ComputableInPolyTime d encUnary F.encDesc) : + IsPPTOn encUnary (encPair encBits encBits) (F.elGamalKeyGenProb d) := by + have := hd.tidy + have := F.computableInPolyTime_encodeElGamalPublicKey.tidy + have htail : ComputableTidilyInPolyTime + (fun p : ℕ × ℕ => + (encPair F.encDesc encBits (d p.1, F.encodeElGamalPublicKey (d p.1, p.2)), encNat p.2)) + (encPair encUnary encNat) (encPair encBits encBits) := by fun_prop + unfold elGamalKeyGenProb + exact (F.isPPTOn_sampleElGamalExp (by fun_prop) hd.tidy).bind_with htail.isPPTOn + +/-- Probabilistic polynomial-time Hashed ElGamal KEM encapsulation for a group description family +`d : ℕ → F.Desc` ([BonehShoup2023], Section 11.5, p. 445, Remark 11.1, p. 446, and Exercise 11.9, +pp. 460–461): sample `b ← sampleElGamalExp n (d n)`, unpack `u = dropFrame pk`, and output +`(H (d n, encode (b • u)), encode (b • g))`. -/ +noncomputable def hashedElGamalEncapsProb (H : F.Desc × List Bool → List Bool) + (d : ℕ → F.Desc) (n : ℕ) (pk : List Bool) : ProbComp (List Bool × List Bool) := + F.sampleElGamalExp n (d n) >>= fun b => + let u := dropFrame pk + pure (H (d n, F.smul (d n, b, u)), + F.smul (d n, b, F.encode (d n) (F.generator (d n)))) + +/-- `hashedElGamalEncapsProb` is uniformly strict PPT whenever `H` and `d` are computable in +polynomial time. -/ +theorem isPPTOn_hashedElGamalEncapsProb {H : F.Desc × List Bool → List Bool} {d : ℕ → F.Desc} + (hH : ComputableInPolyTime H (encPair F.encDesc encBits) encBits) + (hd : ComputableInPolyTime d encUnary F.encDesc) : + IsPPTOn (encPair encUnary encBits) (encPair encBits encBits) + (fun p => F.hashedElGamalEncapsProb H d p.1 p.2) := by + let E := encPair (encPair encUnary encBits) encNat + have hd1 : ComputableTidilyInPolyTime (fun p : (ℕ × List Bool) × ℕ => d p.1.1) E F.encDesc := + hd.tidy.comp (by fun_prop) + have hgen : ComputableTidilyInPolyTime + (fun p : (ℕ × List Bool) × ℕ => F.encode (d p.1.1) (F.generator (d p.1.1))) E encBits := + F.computableInPolyTime_generator.tidy.comp hd1 + have hw : ComputableTidilyInPolyTime + (fun p : (ℕ × List Bool) × ℕ => F.smul (d p.1.1, p.2, dropFrame p.1.2)) E encBits := + F.computableInPolyTime_smul.tidy.comp (hd1.prod (by fun_prop)) + have hk : ComputableTidilyInPolyTime + (fun p : (ℕ × List Bool) × ℕ => H (d p.1.1, F.smul (d p.1.1, p.2, dropFrame p.1.2))) + E encBits := + hH.tidy.comp (hd1.prod hw) + have hv : ComputableTidilyInPolyTime + (fun p : (ℕ × List Bool) × ℕ => + F.smul (d p.1.1, p.2, F.encode (d p.1.1) (F.generator (d p.1.1)))) E encBits := + F.computableInPolyTime_smul.tidy.comp (hd1.prod ((by fun_prop : + ComputableTidilyInPolyTime (fun p : (ℕ × List Bool) × ℕ => p.2) E encNat).prod hgen)) + unfold hashedElGamalEncapsProb + exact (F.isPPTOn_sampleElGamalExp (by fun_prop) (hd.tidy.comp (by fun_prop))).bind_with + (hk.prod hv).isPPTOn + +/-- Deterministic polynomial-time Hashed ElGamal KEM decapsulation ([BonehShoup2023], Section 11.5, +p. 445, Remark 11.1, p. 446): given secret key `sk = encNat a` and KEM ciphertext +`ctKem = encode (b • g)`, recover `H (d n, encode (a • v))`. -/ +def hashedElGamalDecaps (H : F.Desc × List Bool → List Bool) (d : ℕ → F.Desc) + (n : ℕ) (sk ctKem : List Bool) : List Bool := + H (d n, F.smul (d n, ofBits sk, ctKem)) + +/-- `hashedElGamalDecaps` is computable in polynomial time whenever `H` and `d` are. -/ +theorem computableInPolyTime_hashedElGamalDecaps {H : F.Desc × List Bool → List Bool} + {d : ℕ → F.Desc} + (hH : ComputableInPolyTime H (encPair F.encDesc encBits) encBits) + (hd : ComputableInPolyTime d encUnary F.encDesc) : + ComputableInPolyTime + (fun p : ℕ × List Bool × List Bool => F.hashedElGamalDecaps H d p.1 p.2.1 p.2.2) + (encPair encUnary (encPair encBits encBits)) encBits := by + have := hd.tidy + have := hH.tidy + have := F.computableInPolyTime_smul.tidy + unfold hashedElGamalDecaps + exact .of_tidy (by fun_prop) + +/-- **Hashed ElGamal KEM decapsulation correctness**: for any `n : ℕ`, any `(pk, sk)` in the +support of `elGamalKeyGenProb d n`, and any `(k, ctKem)` in the support of +`hashedElGamalEncapsProb H d n pk`, `hashedElGamalDecaps H d n sk ctKem = k`. -/ +theorem hashedElGamalDecaps_hashedElGamalEncapsProb (H : F.Desc × List Bool → List Bool) + (d : ℕ → F.Desc) (n : ℕ) {keys : List Bool × List Bool} + (hkeys : keys ∈ (ProbComp.eval (F.elGamalKeyGenProb d n)).support) + {encapsulated : List Bool × List Bool} + (hencaps : encapsulated ∈ (ProbComp.eval (F.hashedElGamalEncapsProb H d n keys.1)).support) : + F.hashedElGamalDecaps H d n keys.2 encapsulated.2 = encapsulated.1 := by + simp only [elGamalKeyGenProb, ProbComp.eval_bind, ProbComp.eval_pure, PMF.mem_support_bind_iff, + PMF.support_pure, Set.mem_singleton_iff] at hkeys + rcases hkeys with ⟨a, _, rfl⟩ + simp only [hashedElGamalEncapsProb, ProbComp.eval_bind, ProbComp.eval_pure, + PMF.mem_support_bind_iff, PMF.support_pure, Set.mem_singleton_iff] at hencaps + rcases hencaps with ⟨b, _, rfl⟩ + have hbits : ofBits (encNat a) = a := Nat.foldr_bit_bits a + simp only [hashedElGamalDecaps, hbits, dropFrame_encPair_encBits, + encodeElGamalPublicKey_eq_encode, F.smul_encode, smul_smul, mul_comm (a : ZMod (F.order (d n)))] + +/-- DDH distinguisher constructed from a `KEMAdversary` (`Distinguisher`) for +`(elGamalKeyGenProb d, hashedElGamalEncapsProb H d)`. -/ +def kemToDDHDistinguisher (H : F.Desc × List Bool → List Bool) + (distinguisher : Distinguisher) (n : ℕ) + (input : F.Desc × List Bool × List Bool × List Bool) : ProbComp Bool := + let pk := encPair F.encDesc encBits (input.1, input.2.1) + distinguisher n + (encPair encBits (encPair encBits encBits) (pk, (H (input.1, input.2.2.2), input.2.2.1))) + +/-- KDF distinguisher constructed from a `KEMAdversary` (`Distinguisher`) for +`(elGamalKeyGenProb d, hashedElGamalEncapsProb H d)`. -/ +def kemToKDFDistinguisher (distinguisher : Distinguisher) (n : ℕ) + (input : F.Desc × List Bool × List Bool × List Bool) : ProbComp Bool := + let pk := encPair F.encDesc encBits (input.1, input.2.1) + distinguisher n + (encPair encBits (encPair encBits encBits) (pk, (input.2.2.2, input.2.2.1))) + +/-- `ddhIdealGame` for `kemToDDHDistinguisher` is identical to `kdfRealGame` for +`kemToKDFDistinguisher`. -/ +theorem ddhIdealGame_kemToDDHDistinguisher_eq_kdfRealGame (setup : ℕ → PMF F.Desc) + (H : F.Desc × List Bool → List Bool) (distinguisher : Distinguisher) (n : ℕ) : + F.ddhIdealGame setup (F.kemToDDHDistinguisher H distinguisher) n = + F.kdfRealGame setup H (F.kemToKDFDistinguisher distinguisher) n := + rfl + +/-- `kemToDDHDistinguisher` is uniform strict PPT whenever `H` is polynomial time and +`distinguisher` is uniform strict PPT. -/ +theorem isPPTOn_kemToDDHDistinguisher {H : F.Desc × List Bool → List Bool} + (hH : ComputableInPolyTime H (encPair F.encDesc encBits) encBits) + {distinguisher : Distinguisher} (hD : IsPPT encBool distinguisher) : + IsPPTOn (encPair encUnary (encPair F.encDesc (encPair encBits (encPair encBits encBits)))) + encBool (fun input => F.kemToDDHDistinguisher H distinguisher input.1 input.2) := by + let E0 := encPair encUnary (encPair F.encDesc (encPair encBits (encPair encBits encBits))) + have hk : ComputableInPolyTime + (fun input : ℕ × F.Desc × List Bool × List Bool × List Bool => + H (input.2.1, input.2.2.2.2)) E0 encBits := + hH.comp (by fun_prop) + exact hD.on.preprocess + (prepare := fun input : ℕ × F.Desc × List Bool × List Bool × List Bool => + (input.1, + encPair encBits (encPair encBits encBits) + (encPair F.encDesc encBits (input.2.1, input.2.2.1), + (H (input.2.1, input.2.2.2.2), input.2.2.2.1)))) + (by fun_prop) + +/-- `kemToKDFDistinguisher` is uniform strict PPT whenever `distinguisher` is. -/ +theorem isPPTOn_kemToKDFDistinguisher {distinguisher : Distinguisher} + (hD : IsPPT encBool distinguisher) : + IsPPTOn (encPair encUnary (encPair F.encDesc (encPair encBits (encPair encBits encBits)))) + encBool (fun input => F.kemToKDFDistinguisher distinguisher input.1 input.2) := + hD.on.preprocess + (prepare := fun input : ℕ × F.Desc × List Bool × List Bool × List Bool => + (input.1, + encPair encBits (encPair encBits encBits) + (encPair F.encDesc encBits (input.2.1, input.2.2.1), + (input.2.2.2.2, input.2.2.2.1)))) + (by fun_prop) + +private theorem advantage_eval_kemRealGame_ddhRealGame_le + (H : F.Desc × List Bool → List Bool) (d : ℕ → F.Desc) + (distinguisher : Distinguisher) (n : ℕ) : + Game.advantage + (ProbComp.eval + (kemRealGame (F.elGamalKeyGenProb d) (F.hashedElGamalEncapsProb H d) distinguisher n)) + (F.ddhRealGame (fun m => PMF.pure (d m)) (F.kemToDDHDistinguisher H distinguisher) n) ≤ + 2 / 2 ^ n := by + let k (α β : ZMod (F.order (d n))) : Game := + ProbComp.eval (distinguisher n + (encPair encBits (encPair encBits encBits) + (encPair F.encDesc encBits (d n, F.encode (d n) (α • F.generator (d n))), + (H (d n, F.encode (d n) ((α * β) • F.generator (d n))), + F.encode (d n) (β • F.generator (d n)))))) + have hreal : + ProbComp.eval + (kemRealGame (F.elGamalKeyGenProb d) (F.hashedElGamalEncapsProb H d) distinguisher n) = + (ProbComp.eval (F.sampleElGamalExp n (d n))).bind fun a => + (ProbComp.eval (F.sampleElGamalExp n (d n))).bind fun b => + k (a : ZMod (F.order (d n))) (b : ZMod (F.order (d n))) := by + simp only [kemRealGame, elGamalKeyGenProb, hashedElGamalEncapsProb, ProbComp.eval_bind, + ProbComp.eval_pure, PMF.bind_bind, PMF.pure_bind, dropFrame_encPair_encBits, + encodeElGamalPublicKey_eq_encode, F.smul_encode, smul_smul, + mul_comm _ (_ : ZMod (F.order (d n))), k] + have hddh : + F.ddhRealGame (fun m => PMF.pure (d m)) (F.kemToDDHDistinguisher H distinguisher) n = + (PMF.uniformOfFintype (ZMod (F.order (d n)))).bind fun α => + (PMF.uniformOfFintype (ZMod (F.order (d n)))).bind fun β => k α β := by + simp only [ddhRealGame, kemToDDHDistinguisher, PMF.monad_bind_eq_bind, PMF.pure_bind, k] + rw [hreal, hddh] + refine (Game.advantage_triangle _ + ((PMF.uniformOfFintype (ZMod (F.order (d n)))).bind fun α => + (ProbComp.eval (F.sampleElGamalExp n (d n))).bind fun b => + k α (b : ZMod (F.order (d n)))) _).trans ?_ + have h1 := F.advantage_bind_sampleElGamalExp_le n (d n) (fun α => + (ProbComp.eval (F.sampleElGamalExp n (d n))).bind fun b => k α (b : ZMod (F.order (d n)))) + have h2 := advantage_bind_le_nnreal (PMF.uniformOfFintype (ZMod (F.order (d n)))) _ _ + (fun α => F.advantage_bind_sampleElGamalExp_le n (d n) (k α)) + calc _ ≤ (1 : ℝ≥0) / 2 ^ n + 1 / 2 ^ n := add_le_add h1 h2 + _ = 2 / 2 ^ n := by ring + +private theorem advantage_kdfIdealGame_eval_kemIdealGame_le + (H : F.Desc × List Bool → List Bool) (d : ℕ → F.Desc) + (distinguisher : Distinguisher) (n : ℕ) : + Game.advantage + (F.kdfIdealGame (fun m => PMF.pure (d m)) (fun m => m) + (F.kemToKDFDistinguisher distinguisher) n) + (ProbComp.eval + (kemIdealGame (F.elGamalKeyGenProb d) (F.hashedElGamalEncapsProb H d) distinguisher n)) ≤ + 2 / 2 ^ n := by + let k (α β : ZMod (F.order (d n))) : Game := + (Cslib.BitString.uniformList n).bind fun pad => + ProbComp.eval (distinguisher n + (encPair encBits (encPair encBits encBits) + (encPair F.encDesc encBits (d n, F.encode (d n) (α • F.generator (d n))), + (pad, F.encode (d n) (β • F.generator (d n)))))) + have hideal : + ProbComp.eval + (kemIdealGame (F.elGamalKeyGenProb d) (F.hashedElGamalEncapsProb H d) distinguisher n) = + (ProbComp.eval (F.sampleElGamalExp n (d n))).bind fun a => + (ProbComp.eval (F.sampleElGamalExp n (d n))).bind fun b => + k (a : ZMod (F.order (d n))) (b : ZMod (F.order (d n))) := by + simp only [kemIdealGame, elGamalKeyGenProb, hashedElGamalEncapsProb, ProbComp.eval_bind, + ProbComp.eval_pure, Cslib.BitString.eval_sampleList, PMF.bind_bind, PMF.pure_bind, + encodeElGamalPublicKey_eq_encode, F.smul_encode, k] + have hkdf : + F.kdfIdealGame (fun m => PMF.pure (d m)) (fun m => m) + (F.kemToKDFDistinguisher distinguisher) n = + (PMF.uniformOfFintype (ZMod (F.order (d n)))).bind fun α => + (PMF.uniformOfFintype (ZMod (F.order (d n)))).bind fun β => k α β := by + simp only [kdfIdealGame, kemToKDFDistinguisher, PMF.monad_bind_eq_bind, PMF.pure_bind, k] + rw [Game.advantage_comm, hideal, hkdf] + refine (Game.advantage_triangle _ + ((PMF.uniformOfFintype (ZMod (F.order (d n)))).bind fun α => + (ProbComp.eval (F.sampleElGamalExp n (d n))).bind fun b => + k α (b : ZMod (F.order (d n)))) _).trans ?_ + have h1 := F.advantage_bind_sampleElGamalExp_le n (d n) (fun α => + (ProbComp.eval (F.sampleElGamalExp n (d n))).bind fun b => k α (b : ZMod (F.order (d n)))) + have h2 := advantage_bind_le_nnreal (PMF.uniformOfFintype (ZMod (F.order (d n)))) _ _ + (fun α => F.advantage_bind_sampleElGamalExp_le n (d n) (k α)) + calc _ ≤ (1 : ℝ≥0) / 2 ^ n + 1 / 2 ^ n := add_le_add h1 h2 + _ = 2 / 2 ^ n := by ring + +/-- **Quantitative KEM IND-CPA bound for Hashed ElGamal**: the KEM distinguishing advantage of +`distinguisher` against `(elGamalKeyGenProb d, hashedElGamalEncapsProb H d)` is bounded by the DDH +advantage of `kemToDDHDistinguisher H distinguisher` plus the KDF advantage of +`kemToKDFDistinguisher distinguisher` plus `4 / 2 ^ n`. -/ +theorem advantage_kemGame_hashedElGamalEncapsProb_le + (H : F.Desc × List Bool → List Bool) (d : ℕ → F.Desc) + (distinguisher : Distinguisher) (n : ℕ) : + Game.advantage + (ProbComp.eval + (kemRealGame (F.elGamalKeyGenProb d) (F.hashedElGamalEncapsProb H d) distinguisher n)) + (ProbComp.eval + (kemIdealGame (F.elGamalKeyGenProb d) (F.hashedElGamalEncapsProb H d) distinguisher n)) ≤ + Game.advantage + (F.ddhRealGame (fun m => PMF.pure (d m)) (F.kemToDDHDistinguisher H distinguisher) n) + (F.ddhIdealGame (fun m => PMF.pure (d m)) (F.kemToDDHDistinguisher H distinguisher) n) + + Game.advantage + (F.kdfRealGame (fun m => PMF.pure (d m)) H (F.kemToKDFDistinguisher distinguisher) n) + (F.kdfIdealGame (fun m => PMF.pure (d m)) (fun m => m) + (F.kemToKDFDistinguisher distinguisher) n) + + 4 / 2 ^ n := by + have h0 := F.advantage_eval_kemRealGame_ddhRealGame_le H d distinguisher n + have h3 := F.advantage_kdfIdealGame_eval_kemIdealGame_le H d distinguisher n + have htri1 := Game.advantage_triangle + (ProbComp.eval + (kemRealGame (F.elGamalKeyGenProb d) (F.hashedElGamalEncapsProb H d) distinguisher n)) + (F.ddhRealGame (fun m => PMF.pure (d m)) (F.kemToDDHDistinguisher H distinguisher) n) + (ProbComp.eval + (kemIdealGame (F.elGamalKeyGenProb d) (F.hashedElGamalEncapsProb H d) distinguisher n)) + have htri2 := Game.advantage_triangle + (F.ddhRealGame (fun m => PMF.pure (d m)) (F.kemToDDHDistinguisher H distinguisher) n) + (F.ddhIdealGame (fun m => PMF.pure (d m)) (F.kemToDDHDistinguisher H distinguisher) n) + (ProbComp.eval + (kemIdealGame (F.elGamalKeyGenProb d) (F.hashedElGamalEncapsProb H d) distinguisher n)) + have htri3 := Game.advantage_triangle + (F.kdfRealGame (fun m => PMF.pure (d m)) H (F.kemToKDFDistinguisher distinguisher) n) + (F.kdfIdealGame (fun m => PMF.pure (d m)) (fun m => m) + (F.kemToKDFDistinguisher distinguisher) n) + (ProbComp.eval + (kemIdealGame (F.elGamalKeyGenProb d) (F.hashedElGamalEncapsProb H d) distinguisher n)) + have htri2' : + Game.advantage + (F.ddhRealGame (fun m => PMF.pure (d m)) (F.kemToDDHDistinguisher H distinguisher) n) + (ProbComp.eval + (kemIdealGame (F.elGamalKeyGenProb d) (F.hashedElGamalEncapsProb H d) distinguisher n)) ≤ + Game.advantage + (F.ddhRealGame (fun m => PMF.pure (d m)) (F.kemToDDHDistinguisher H distinguisher) n) + (F.ddhIdealGame (fun m => PMF.pure (d m)) (F.kemToDDHDistinguisher H distinguisher) n) + + Game.advantage + (F.kdfRealGame (fun m => PMF.pure (d m)) H (F.kemToKDFDistinguisher distinguisher) n) + (ProbComp.eval + (kemIdealGame (F.elGamalKeyGenProb d) (F.hashedElGamalEncapsProb H d) + distinguisher n)) := by + simpa only [← F.ddhIdealGame_kemToDDHDistinguisher_eq_kdfRealGame] using htri2 + exact (htri1.trans (add_le_add h0 (htri2'.trans (add_le_add le_rfl + (htri3.trans (add_le_add le_rfl h3)))))).trans_eq (by ring) + +/-- **Hashed ElGamal KEM is `Encryption.KEMINDCPA`-secure under DDH and `SecureKDF`** +([BonehShoup2023], Section 11.5.2, Theorem 11.5, pp. 449–451, and Exercise 11.9, pp. 460–461): for +any group description family `d : ℕ → F.Desc`, if `F.DDH (fun n => PMF.pure (d n))` and +`F.SecureKDF (fun n => PMF.pure (d n)) H (fun n => n)` hold and `H` is computable in polynomial +time, then `(elGamalKeyGenProb d, hashedElGamalEncapsProb H d)` satisfies `Encryption.KEMINDCPA`. -/ +theorem DDH.kemINDCPA_hashedElGamalEncapsProb {F : PrimeOrderGroupFamily} + {H : F.Desc × List Bool → List Bool} {d : ℕ → F.Desc} + (hDDH : F.DDH (fun n => PMF.pure (d n))) + (hKDF : F.SecureKDF (fun n => PMF.pure (d n)) H (fun n => n)) + (hH : ComputableInPolyTime H (encPair F.encDesc encBits) encBits) : + KEMINDCPA (F.elGamalKeyGenProb d) (F.hashedElGamalEncapsProb H d) := by + intro distinguisher hD + have hddh := hDDH _ (F.isPPTOn_kemToDDHDistinguisher hH hD) + have hkdf := hKDF _ (F.isPPTOn_kemToKDFDistinguisher hD) + have h4 : Negligible fun n => (4 : ℝ≥0) / 2 ^ n := negligible_const_div_two_pow 4 + exact negligible_of_le ((hddh.add hkdf).add h4) + (F.advantage_kemGame_hashedElGamalEncapsProb_le H d distinguisher) + +/-- **Theorem 11.5 via `Encryption.INDCPAOf`** ([BonehShoup2023], Section 11.5.2, Theorem 11.5, +pp. 449–451): combining `DDH.kemINDCPA_hashedElGamalEncapsProb` with `KEMINDCPA.hybrid_indcpa`, +Hashed ElGamal coupled with any uniform strict-PPT one-time semantically secure symmetric cipher +`encryptSym` (`DEMOneTimeINDCPAOf encMsg encryptSym`) satisfies `Encryption.INDCPAOf`. -/ +theorem DDH.indcpaOf_hybrid_hashedElGamal {F : PrimeOrderGroupFamily} + {Msg : Type} {encMsg : Msg ↪ List Bool} + {H : F.Desc × List Bool → List Bool} {d : ℕ → F.Desc} + {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)} + (hDDH : F.DDH (fun n => PMF.pure (d n))) + (hKDF : F.SecureKDF (fun n => PMF.pure (d n)) H (fun n => n)) + (hdem : DEMOneTimeINDCPAOf encMsg encryptSym) + (hH : ComputableInPolyTime H (encPair F.encDesc encBits) encBits) + (hd : ComputableInPolyTime d encUnary F.encDesc) + (hencryptSym : IsPPTOn (encPair encUnary (encPair encBits encMsg)) encBits + (fun p => encryptSym p.1 p.2.1 p.2.2)) : + INDCPAOf encMsg (F.elGamalKeyGenProb d) + (hybridEncrypt (F.hashedElGamalEncapsProb H d) encryptSym) := + (hDDH.kemINDCPA_hashedElGamalEncapsProb hKDF hH).hybrid_indcpa hdem + (F.isPPTOn_elGamalKeyGenProb hd) (F.isPPTOn_hashedElGamalEncapsProb hH hd) hencryptSym + +/-- **Theorem 11.5 via `Encryption.INDCPAOn`** ([BonehShoup2023], Section 11.5.2, Theorem 11.5, +pp. 449–451): combining `DDH.kemINDCPA_hashedElGamalEncapsProb` with `KEMINDCPA.hybrid_indcpaOn`, +for any polynomial-time admissibility predicate `valid` that ignores the public key (such as +the equal-length predicate `fun _ _ m₀ m₁ => m₀.length == m₁.length`), Hashed ElGamal coupled with +any one-time semantically secure symmetric cipher `encryptSym` +(`DEMOneTimeINDCPAOn valid encMsg encryptSym`) satisfies `Encryption.INDCPAOn`. -/ +theorem DDH.indcpaOn_hybrid_hashedElGamal {F : PrimeOrderGroupFamily} + {Msg : Type} {encMsg : Msg ↪ List Bool} + {valid : ℕ → List Bool → Msg → Msg → Bool} + {H : F.Desc × List Bool → List Bool} {d : ℕ → F.Desc} + {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)} + (hDDH : F.DDH (fun n => PMF.pure (d n))) + (hKDF : F.SecureKDF (fun n => PMF.pure (d n)) H (fun n => n)) + (hdem : DEMOneTimeINDCPAOn valid encMsg encryptSym) + (hvalid : ComputableInPolyTime + (fun p : ℕ × List Bool × Msg × Msg => valid p.1 p.2.1 p.2.2.1 p.2.2.2) + (encPair encUnary (encPair encBits (encPair encMsg encMsg))) encBool) + (hpk : ∀ n pk m₀ m₁, valid n pk m₀ m₁ = valid n [] m₀ m₁) + (hH : ComputableInPolyTime H (encPair F.encDesc encBits) encBits) + (hd : ComputableInPolyTime d encUnary F.encDesc) + (hencryptSym : IsPPTOn (encPair encUnary (encPair encBits encMsg)) encBits + (fun p => encryptSym p.1 p.2.1 p.2.2)) : + INDCPAOn valid encMsg (F.elGamalKeyGenProb d) + (hybridEncrypt (F.hashedElGamalEncapsProb H d) encryptSym) := + (hDDH.kemINDCPA_hashedElGamalEncapsProb hKDF hH).hybrid_indcpaOn hdem hvalid hpk + (F.isPPTOn_elGamalKeyGenProb hd) (F.isPPTOn_hashedElGamalEncapsProb hH hd) hencryptSym + +/-- **Theorem 11.5 via `Encryption.WordINDCPA`** ([BonehShoup2023], Section 11.5.2, Theorem 11.5, +pp. 449–451): combining `DDH.indcpaOn_hybrid_hashedElGamal` with Attack Game 11.1's equal-length +rule (`fun _ _ m₀ m₁ => m₀.length == m₁.length`), Hashed ElGamal coupled with any equal-length +one-time semantically secure word cipher `encryptSym` (`DEMOneTimeWordINDCPA encryptSym`) satisfies +`Encryption.WordINDCPA`. -/ +theorem DDH.wordINDCPA_hybrid_hashedElGamal {F : PrimeOrderGroupFamily} + {H : F.Desc × List Bool → List Bool} {d : ℕ → F.Desc} + {encryptSym : ℕ → List Bool → List Bool → ProbComp (List Bool)} + (hDDH : F.DDH (fun n => PMF.pure (d n))) + (hKDF : F.SecureKDF (fun n => PMF.pure (d n)) H (fun n => n)) + (hdem : DEMOneTimeWordINDCPA encryptSym) + (hH : ComputableInPolyTime H (encPair F.encDesc encBits) encBits) + (hd : ComputableInPolyTime d encUnary F.encDesc) + (hencryptSym : IsPPTOn (encPair encUnary (encPair encBits encBits)) encBits + (fun p => encryptSym p.1 p.2.1 p.2.2)) : + WordINDCPA (F.elGamalKeyGenProb d) + (hybridEncrypt (F.hashedElGamalEncapsProb H d) encryptSym) := + hDDH.indcpaOn_hybrid_hashedElGamal hKDF hdem + (ComputableInPolyTime.of_tidy (by polytime)) (fun _ _ _ _ => rfl) hH hd hencryptSym + +/-- Probabilistic polynomial-time multiplicative ElGamal encryption for a group description family +`d : ℕ → F.Desc` and message encoder `encodeMsg : F.Desc → Msg → List Bool` +([BonehShoup2023], Exercise 11.5, p. 459): sample `b ← sampleElGamalExp n (d n)`, unpack +`u = dropFrame pk`, and output +`encPair encBits encBits (encodeElGamalEncrypt (d n, u, encodeMsg (d n) m, b))`. -/ +noncomputable def elGamalEncryptProb {Msg : Type} (encodeMsg : F.Desc → Msg → List Bool) + (d : ℕ → F.Desc) (n : ℕ) (pk : List Bool) (m : Msg) : ProbComp (List Bool) := + F.sampleElGamalExp n (d n) >>= fun b => + let u := dropFrame pk + pure (encPair encBits encBits (F.encodeElGamalEncrypt (d n, u, encodeMsg (d n) m, b))) + +/-- `elGamalEncryptProb` is uniformly strict PPT whenever `encodeMsg` and `d` are computable in +polynomial time. -/ +theorem isPPTOn_elGamalEncryptProb {Msg : Type} {encMsg : Msg ↪ List Bool} + {encodeMsg : F.Desc → Msg → List Bool} {d : ℕ → F.Desc} + (hencMsg : ComputableInPolyTime (fun p : F.Desc × Msg => encodeMsg p.1 p.2) + (encPair F.encDesc encMsg) encBits) + (hd : ComputableInPolyTime d encUnary F.encDesc) : + IsPPTOn (encPair encUnary (encPair encBits encMsg)) encBits + (fun p => F.elGamalEncryptProb encodeMsg d p.1 p.2.1 p.2.2) := by + have := hd.tidy + have := hencMsg.tidy + have := F.computableInPolyTime_encodeElGamalEncrypt.tidy + have henc : ComputableTidilyInPolyTime + (fun p : (ℕ × List Bool × Msg) × ℕ => + encPair encBits encBits + (F.encodeElGamalEncrypt (d p.1.1, dropFrame p.1.2.1, encodeMsg (d p.1.1) p.1.2.2, p.2))) + (encPair (encPair encUnary (encPair encBits encMsg)) encNat) encBits := by fun_prop + unfold elGamalEncryptProb + exact (F.isPPTOn_sampleElGamalExp (by fun_prop) (hd.tidy.comp (by fun_prop))).bind_with + henc.isPPTOn + +/-- Deterministic polynomial-time multiplicative ElGamal decryption on words: given secret key +`sk = encNat a` and ciphertext `ct = encPair encBits encBits (v, e)`, compute +`decodeElGamal (d n, ofBits sk, unframe ct, dropFrame ct)`. -/ +def elGamalDecryptDet (d : ℕ → F.Desc) (n : ℕ) (sk ct : List Bool) : List Bool := + F.decodeElGamal (d n, ofBits sk, unframe ct, dropFrame ct) + +/-- `elGamalDecryptDet` is computable in polynomial time whenever `d` is. -/ +theorem computableInPolyTime_elGamalDecryptDet {d : ℕ → F.Desc} + (hd : ComputableInPolyTime d encUnary F.encDesc) : + ComputableInPolyTime + (fun p : ℕ × List Bool × List Bool => F.elGamalDecryptDet d p.1 p.2.1 p.2.2) + (encPair encUnary (encPair encBits encBits)) encBits := by + have := hd.tidy + have := F.computableInPolyTime_decodeElGamal.tidy + unfold elGamalDecryptDet + exact .of_tidy (by fun_prop) + +/-- **Multiplicative ElGamal decryption correctness on `ProbComp` outputs**: for any `(pk, sk)` in +the support of `elGamalKeyGenProb d n`, any `m : F.Carrier (d n)`, and any `ct` in the support of +`elGamalEncryptProb (fun d x => x) d n pk (F.encode (d n) m)`, +`elGamalDecryptDet d n sk ct = F.encode (d n) m`. -/ +theorem elGamalDecryptDet_elGamalEncryptProb (d : ℕ → F.Desc) (n : ℕ) + {keys : List Bool × List Bool} + (hkeys : keys ∈ (ProbComp.eval (F.elGamalKeyGenProb d n)).support) + (m : F.Carrier (d n)) {ct : List Bool} + (hct : ct ∈ (ProbComp.eval + (F.elGamalEncryptProb (fun _ x => x) d n keys.1 (F.encode (d n) m))).support) : + F.elGamalDecryptDet d n keys.2 ct = F.encode (d n) m := by + simp only [elGamalKeyGenProb, ProbComp.eval_bind, ProbComp.eval_pure, PMF.mem_support_bind_iff, + PMF.support_pure, Set.mem_singleton_iff] at hkeys + rcases hkeys with ⟨a, _, rfl⟩ + simp only [elGamalEncryptProb, ProbComp.eval_bind, ProbComp.eval_pure, PMF.mem_support_bind_iff, + PMF.support_pure, Set.mem_singleton_iff] at hct + rcases hct with ⟨b, _, rfl⟩ + have hbits : ofBits (encNat a) = a := Nat.foldr_bit_bits a + simp only [elGamalDecryptDet, hbits, unframe_encPair_encBits, dropFrame_encPair_encBits_pair, + dropFrame_encPair_encBits, F.decodeElGamal_encodeElGamalEncrypt] + +/-- The native `Encryption.gameOn` experiment for +`(elGamalKeyGenProb d, elGamalEncryptProb encodeMsg d)` is within statistical distance `2 / 2 ^ n` +of the ideal exact-uniform PMF game +`elGamalMsgCPAGameOn valid encodeMsg (fun n => PMF.pure (d n))`. -/ +theorem advantage_gameOn_elGamalMsgCPAGameOn_le {Msg : Type} + (valid : ℕ → List Bool → Msg → Msg → Bool) + (encodeMsg : F.Desc → Msg → List Bool) (d : ℕ → F.Desc) + (adversary : Encryption.AdversaryOf Msg) (bit : Bool) (n : ℕ) : + Game.advantage + (ProbComp.eval + (gameOn valid (F.elGamalKeyGenProb d) (F.elGamalEncryptProb encodeMsg d) adversary bit n)) + (F.elGamalMsgCPAGameOn valid encodeMsg (fun m => PMF.pure (d m)) adversary bit n) ≤ + 2 / 2 ^ n := by + let innerB (α : ZMod (F.order (d n))) (choice : (Msg × Msg) × List Bool) + (β : ZMod (F.order (d n))) : Game := + let m := if bit then choice.1.2 else choice.1.1 + let ct := encPair encBits encBits + (F.encode (d n) (β • F.generator (d n)), + F.add (d n, F.encode (d n) ((α * β) • F.generator (d n)), encodeMsg (d n) m)) + ProbComp.eval (adversary.guess n choice.2 ct) + let innerA (useExactB : Bool) (α : ZMod (F.order (d n))) : Game := + let pk := encPair F.encDesc encBits (d n, F.encode (d n) (α • F.generator (d n))) + (ProbComp.eval (adversary.choose n pk)).bind fun choice => + if valid n pk choice.1.1 choice.1.2 then + if useExactB then + (PMF.uniformOfFintype (ZMod (F.order (d n)))).bind (innerB α choice) + else + (ProbComp.eval (F.sampleElGamalExp n (d n))).bind fun b => + innerB α choice (b : ZMod (F.order (d n))) + else + PMF.pure false + have hgame0 : + ProbComp.eval + (gameOn valid (F.elGamalKeyGenProb d) (F.elGamalEncryptProb encodeMsg d) adversary bit n) = + (ProbComp.eval (F.sampleElGamalExp n (d n))).bind fun a => + innerA false (a : ZMod (F.order (d n))) := by + simp only [gameOn, elGamalKeyGenProb, elGamalEncryptProb, ProbComp.eval_bind, + ProbComp.eval_pure, PMF.bind_bind, PMF.pure_bind, apply_ite ProbComp.eval, + encodeElGamalPublicKey_eq_encode, innerA, innerB] + refine congrArg _ (funext fun a => congrArg _ (funext fun choice => ?_)) + by_cases hv : valid n + (encPair F.encDesc encBits + (d n, F.encode (d n) ((a : ZMod (F.order (d n))) • F.generator (d n)))) + choice.1.1 choice.1.2 = true + · simp only [hv, ↓reduceIte, Bool.false_eq_true, dropFrame_encPair_encBits, + encodeElGamalEncrypt, F.smul_encode, smul_smul, mul_comm _ (a : ZMod (F.order (d n)))] + · simp only [hv, Bool.false_eq_true, ↓reduceIte] + have hgame1 : + F.elGamalMsgCPAGameOn valid encodeMsg (fun m => PMF.pure (d m)) adversary bit n = + (PMF.uniformOfFintype (ZMod (F.order (d n)))).bind (innerA true) := by + simp only [elGamalMsgCPAGameOn, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.pure_bind, + innerA, innerB, ↓reduceIte] + rw [hgame0, hgame1] + refine (Game.advantage_triangle _ + ((PMF.uniformOfFintype (ZMod (F.order (d n)))).bind (innerA false)) _).trans ?_ + have h1 := F.advantage_bind_sampleElGamalExp_le n (d n) (innerA false) + have h2 : Game.advantage + ((PMF.uniformOfFintype (ZMod (F.order (d n)))).bind (innerA false)) + ((PMF.uniformOfFintype (ZMod (F.order (d n)))).bind (innerA true)) ≤ 1 / 2 ^ n := by + refine advantage_bind_le_nnreal _ _ _ fun α => ?_ + dsimp only [innerA] + refine advantage_bind_le_nnreal _ _ _ fun choice => ?_ + by_cases hv : valid n (encPair F.encDesc encBits (d n, F.encode (d n) (α • F.generator (d n)))) + choice.1.1 choice.1.2 = true + · simp only [hv, ↓reduceIte, Bool.false_eq_true] + exact F.advantage_bind_sampleElGamalExp_le n (d n) (innerB α choice) + · simp only [hv, Bool.false_eq_true, ↓reduceIte, Game.advantage_self, zero_le] + calc _ ≤ (1 : ℝ≥0) / 2 ^ n + 1 / 2 ^ n := add_le_add h1 h2 + _ = 2 / 2 ^ n := by ring + +/-- **Multiplicative ElGamal satisfies `Encryption.INDCPAOn` under DDH** ([BonehShoup2023], +Exercise 11.5(a), p. 459): for any polynomial-time group description family `d : ℕ → F.Desc`, +polynomial-time message encoder `encodeMsg`, and polynomial-time admissibility predicate `valid` +admitting only group elements (`AdmitsGroupElements encodeMsg valid`), +`(elGamalKeyGenProb d, elGamalEncryptProb encodeMsg d)` satisfies `Encryption.INDCPAOn valid encMsg` +whenever `F.DDH (fun n => PMF.pure (d n))` holds. -/ +theorem DDH.indcpaOn_elGamalEncryptProb {F : PrimeOrderGroupFamily} + {Msg : Type} {encMsg : Msg ↪ List Bool} + {valid : ℕ → List Bool → Msg → Msg → Bool} + {encodeMsg : F.Desc → Msg → List Bool} {d : ℕ → F.Desc} + (hDDH : F.DDH (fun n => PMF.pure (d n))) + (hvalid : ComputableInPolyTime + (fun p : ℕ × List Bool × Msg × Msg => valid p.1 p.2.1 p.2.2.1 p.2.2.2) + (encPair encUnary (encPair encBits (encPair encMsg encMsg))) encBool) + (hsound : F.AdmitsGroupElements encodeMsg valid) + (hencMsg : ComputableInPolyTime (fun p : F.Desc × Msg => encodeMsg p.1 p.2) + (encPair F.encDesc encMsg) encBits) : + INDCPAOn valid encMsg (F.elGamalKeyGenProb d) (F.elGamalEncryptProb encodeMsg d) := by + intro adversary hA + have hmid := hDDH.negligible_elGamalMsgCPAGameOn hvalid hsound hencMsg hA + have h2 : Negligible fun n => (2 : ℝ≥0) / 2 ^ n := negligible_const_div_two_pow 2 + refine negligible_of_le ((h2.add hmid).add h2) fun n => ?_ + have h0 := F.advantage_gameOn_elGamalMsgCPAGameOn_le valid encodeMsg d adversary false n + have h1 := F.advantage_gameOn_elGamalMsgCPAGameOn_le valid encodeMsg d adversary true n + rw [Game.advantage_comm] at h1 + have htri1 := Game.advantage_triangle + (ProbComp.eval + (gameOn valid (F.elGamalKeyGenProb d) (F.elGamalEncryptProb encodeMsg d) adversary false n)) + (F.elGamalMsgCPAGameOn valid encodeMsg (fun m => PMF.pure (d m)) adversary false n) + (ProbComp.eval + (gameOn valid (F.elGamalKeyGenProb d) (F.elGamalEncryptProb encodeMsg d) adversary true n)) + have htri2 := Game.advantage_triangle + (F.elGamalMsgCPAGameOn valid encodeMsg (fun m => PMF.pure (d m)) adversary false n) + (F.elGamalMsgCPAGameOn valid encodeMsg (fun m => PMF.pure (d m)) adversary true n) + (ProbComp.eval + (gameOn valid (F.elGamalKeyGenProb d) (F.elGamalEncryptProb encodeMsg d) adversary true n)) + exact (htri1.trans (add_le_add le_rfl htri2)).trans + (by rw [add_assoc]; exact add_le_add h0 (add_le_add le_rfl h1)) + +/-- **Bit ElGamal satisfies `Encryption.INDCPA` under DDH** ([BonehShoup2023], Exercise 11.5(a), +p. 459): specialization of `DDH.indcpaOn_elGamalEncryptProb` to `encodeBit`. -/ +theorem DDH.indcpa_elGamalBitEncryptProb {F : PrimeOrderGroupFamily} {d : ℕ → F.Desc} + (hDDH : F.DDH (fun n => PMF.pure (d n))) : + INDCPA (F.elGamalKeyGenProb d) (F.elGamalEncryptProb F.encodeBit d) := + hDDH.indcpaOn_elGamalEncryptProb + (ComputableTidilyInPolyTime.const true).computableInPolyTime + F.admitsGroupElements_encodeBit F.computableInPolyTime_encodeBit + +end Cslib.Crypto.PrimeOrderGroupFamily diff --git a/ComplexityTests/Crypto/DiffieHellman.lean b/ComplexityTests/Crypto/DiffieHellman.lean index 84728b0d4..9eee87885 100644 --- a/ComplexityTests/Crypto/DiffieHellman.lean +++ b/ComplexityTests/Crypto/DiffieHellman.lean @@ -8,7 +8,10 @@ import Complexity.Crypto.Computational.DiscreteLog.SchnorrGroup import Complexity.Crypto.Computational.DiffieHellman import Complexity.Crypto.Computational.DiffieHellman.EncodingBounds import Complexity.Crypto.Computational.ElGamal +import Complexity.Crypto.Computational.ElGamal.KDF +import Complexity.Crypto.Computational.ElGamal.ProbComp import Complexity.Crypto.Negligible.Basic +import Complexity.Tactic.PolyTime import Complexity.Tactic.PPT import Mathlib.Tactic.NormNum.Prime @@ -451,4 +454,145 @@ example (α β γ : ℕ → ZMod (schnorrGroups.order d23)) : (Filter.Eventually.of_forall fun _ => by decide) (Filter.Eventually.of_forall one_half_le_advantage_exactDDHDistinguisher) +/-! ### Non-degenerate `SecureKDF` (`linearHashKDF`) and strict-PPT ElGamal tests -/ + +/-- Concrete evaluation of `linearHashSeedLen` and `linearHashKDF` on `d23` with non-degenerate +output length `k = 4 > 0` and encoding bound `B = 6`: at `n = 3`, the block-matrix seed length is +`4 * (2 * 6 + 1) = 52`, and `linearHashKDF` produces a 4-bit key. -/ +example : schnorrGroups.linearHashSeedLen (fun _ => 4) (fun _ => 6) 3 d23 = 52 := by decide +example : + (schnorrGroups.linearHashKDF (fun _ => 4) (fun _ => 6) + ((d23, List.replicate 52 true), Nat.bits 16)).length = 4 := by decide + +/-- Positive-side non-degenerate `SecureKDF` instantiation (`k = 4 > 0`): for any setup law whose +supported descriptions have group order at least `2 ^ n` and encoded group elements of length at +most `6`, `linearHashKDF (fun _ => 4) (fun _ => 6)` is a `SecureKDF` for `schnorrGroups.withSeed` +with output key length `4 > 0`. -/ +example (setup : ℕ → PMF schnorrGroups.Desc) + (hsize : ∀ n, ∀ d ∈ (setup n).support, 2 ^ n ≤ schnorrGroups.order d) + (hbound : ∀ n, ∀ d ∈ (setup n).support, ∀ x : schnorrGroups.Carrier d, + (schnorrGroups.encode d x).length ≤ 6) : + schnorrGroups.withSeed.SecureKDF + (schnorrGroups.seededSetup setup + (schnorrGroups.linearHashSeedLen (fun _ => 4) (fun _ => 6))) + (schnorrGroups.linearHashKDF (fun _ => 4) (fun _ => 6)) + (fun _ => 4) := + schnorrGroups.secureKDF_linearHashKDF_const setup (fun _ => 6) 4 + Nat.two_pow_pos hbound hsize negligible_inv_two_pow + +/-- Negative-side KDF counterexample: a constant 1-bit KDF `constZeroKDF := fun _ => [false]` +always outputs `[false]` instead of a uniform 1-bit key. -/ +def constZeroKDF : schnorrGroups.Desc × List Bool → List Bool := + fun _ => [false] + +/-- A uniform strict-PPT KDF distinguisher that inspects the first bit of the candidate key +`input.2.2.2`. -/ +noncomputable def firstBitKDFDistinguisher (_ : ℕ) + (input : schnorrGroups.Desc × List Bool × List Bool × List Bool) : ProbComp Bool := + pure (input.2.2.2.headD false) + +/-- `firstBitKDFDistinguisher` is uniform strict PPT. -/ +theorem isPPTOn_firstBitKDFDistinguisher : + IsPPTOn + (encPair encUnary + (encPair schnorrGroups.encDesc (encPair encBits (encPair encBits encBits)))) + encBool (fun input => firstBitKDFDistinguisher input.1 input.2) := by + have hhead : ComputableTidilyInPolyTime (fun s : List Bool => s.headD false) encBits encBool := by + fun_prop + have hproj : ComputableTidilyInPolyTime + (fun input : ℕ × schnorrGroups.Desc × List Bool × List Bool × List Bool => input.2.2.2.2) + (encPair encUnary + (encPair schnorrGroups.encDesc (encPair encBits (encPair encBits encBits)))) + encBits := by fun_prop + exact (hhead.comp hproj).isPPTOn + +/-- `firstBitKDFDistinguisher` achieves KDF advantage `1 / 2` against `constZeroKDF` for +1-bit keys (`msgLen = fun _ => 1`) at every security parameter `n`. -/ +theorem advantage_firstBitKDFDistinguisher_constZeroKDF (n : ℕ) : + Game.advantage + (schnorrGroups.kdfRealGame (fun _ => PMF.pure d23) constZeroKDF firstBitKDFDistinguisher n) + (schnorrGroups.kdfIdealGame (fun _ => PMF.pure d23) (fun _ => 1) firstBitKDFDistinguisher n) = + 1 / 2 := by + have hreal : + schnorrGroups.kdfRealGame (fun _ => PMF.pure d23) constZeroKDF firstBitKDFDistinguisher n = + PMF.pure false := by + simp [PrimeOrderGroupFamily.kdfRealGame, constZeroKDF, firstBitKDFDistinguisher] + have hideal : + schnorrGroups.kdfIdealGame (fun _ => PMF.pure d23) (fun _ => 1) firstBitKDFDistinguisher n = + (BitString.uniformList 1).bind (fun k => PMF.pure (k.headD false)) := by + simp [PrimeOrderGroupFamily.kdfIdealGame, firstBitKDFDistinguisher] + have hunif : + ((BitString.uniformList 1).bind (fun k => PMF.pure (k.headD false))) true = 1 / 2 := by + rw [BitString.uniformList_succ] + simp [BitString.uniformList_zero] + rw [hreal, hideal, Game.advantage, Game.succProbability, Game.succProbability] + have hreal_true : (PMF.pure false : Game) true = 0 := by simp + rw [hreal_true, hunif] + simp [one_div, ENNReal.toNNReal_ofNat] + +/-- Refutation test: `constZeroKDF` is not a `SecureKDF` for 1-bit keys (`msgLen = fun _ => 1`), +confirming that `SecureKDF` is non-vacuous and refutable on bad KDF candidates. -/ +theorem not_secureKDF_constZeroKDF : + ¬ schnorrGroups.SecureKDF (fun _ => PMF.pure d23) constZeroKDF (fun _ => 1) := by + intro hsec + have hneg := hsec firstBitKDFDistinguisher isPPTOn_firstBitKDFDistinguisher + simp only [advantage_firstBitKDFDistinguisher_constZeroKDF] at hneg + have h0 := hneg 0 + simp only [pow_zero, one_mul] at h0 + exact absurd (tendsto_nhds_unique h0 tendsto_const_nhds) (by norm_num) + +/-- The constant group description family `fun _ : ℕ => d23` is computable in polynomial time. -/ +theorem computableInPolyTime_const_d23 : + ComputableInPolyTime (fun _ : ℕ => d23) encUnary schnorrGroups.encDesc := + ComputableInPolyTime.of_tidy (ComputableTidilyInPolyTime.const d23) + +/-- Support-level round-trip correctness of `elGamalKeyGenProb`, `hashedElGamalEncapsProb`, and +`hashedElGamalDecaps` on `d23`. -/ +example (n : ℕ) {keys : List Bool × List Bool} + (hkeys : keys ∈ (ProbComp.eval (schnorrGroups.elGamalKeyGenProb (fun _ => d23) n)).support) + {encapsulated : List Bool × List Bool} + (hencaps : encapsulated ∈ + (ProbComp.eval + (schnorrGroups.hashedElGamalEncapsProb Prod.snd (fun _ => d23) n keys.1)).support) : + schnorrGroups.hashedElGamalDecaps Prod.snd (fun _ => d23) n keys.2 encapsulated.2 = + encapsulated.1 := + schnorrGroups.hashedElGamalDecaps_hashedElGamalEncapsProb Prod.snd (fun _ => d23) n hkeys hencaps + +/-- Support-level round-trip correctness of `elGamalKeyGenProb`, `elGamalEncryptProb`, and +`elGamalDecryptDet` on `d23`. -/ +example (n : ℕ) {keys : List Bool × List Bool} + (hkeys : keys ∈ (ProbComp.eval (schnorrGroups.elGamalKeyGenProb (fun _ => d23) n)).support) + (m : schnorrGroups.Carrier d23) {ct : List Bool} + (hct : ct ∈ + (ProbComp.eval + (schnorrGroups.elGamalEncryptProb (fun _ x => x) (fun _ => d23) n keys.1 + (schnorrGroups.encode d23 m))).support) : + schnorrGroups.elGamalDecryptDet (fun _ => d23) n keys.2 ct = schnorrGroups.encode d23 m := + schnorrGroups.elGamalDecryptDet_elGamalEncryptProb (fun _ => d23) n hkeys m hct + +/-- Concrete instantiation of `DDH.kemINDCPA_hashedElGamalEncapsProb`, +`DDH.wordINDCPA_hybrid_hashedElGamal` (with `otpWordEncrypt`), +`DDH.indcpaOn_elGamalEncryptProb`, and `DDH.indcpa_elGamalBitEncryptProb`. -/ +example (d : ℕ → schnorrGroups.Desc) + (hd : ComputableInPolyTime d encUnary schnorrGroups.encDesc) + (hDDH : schnorrGroups.DDH (fun n => PMF.pure (d n))) + (H : schnorrGroups.Desc × List Bool → List Bool) + (hKDF : schnorrGroups.SecureKDF (fun n => PMF.pure (d n)) H (fun n => n)) + (hH : ComputableInPolyTime H (encPair schnorrGroups.encDesc encBits) encBits) : + Encryption.KEMINDCPA (schnorrGroups.elGamalKeyGenProb d) + (schnorrGroups.hashedElGamalEncapsProb H d) ∧ + Encryption.WordINDCPA (schnorrGroups.elGamalKeyGenProb d) + (Encryption.hybridEncrypt (schnorrGroups.hashedElGamalEncapsProb H d) + Encryption.otpWordEncrypt) ∧ + Encryption.INDCPAOn twoElements encBits (schnorrGroups.elGamalKeyGenProb d) + (schnorrGroups.elGamalEncryptProb (fun _ x => x) d) ∧ + Encryption.INDCPA (schnorrGroups.elGamalKeyGenProb d) + (schnorrGroups.elGamalEncryptProb schnorrGroups.encodeBit d) := + ⟨hDDH.kemINDCPA_hashedElGamalEncapsProb hKDF hH, + hDDH.wordINDCPA_hybrid_hashedElGamal hKDF Encryption.demOneTimeWordINDCPA_otpWordEncrypt + hH hd Encryption.isPPTOn_otpWordEncrypt, + hDDH.indcpaOn_elGamalEncryptProb computableInPolyTime_twoElements + admitsGroupElements_twoElements (by fun_prop), + hDDH.indcpa_elGamalBitEncryptProb⟩ + end ComplexityTests.Crypto.DiffieHellman diff --git a/ROADMAP.md b/ROADMAP.md index fe13ded3d..04debc880 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -120,9 +120,8 @@ families and full-input native runtime. - **Sigma protocols and Fiat–Shamir** ([#581]): computational Schnorr signatures under discrete log against strict PPT forgers; eavesdropping security in the strict-PPT model, with the statistical-distance term from sampling `ZMod q`. -- **Diffie–Hellman and ElGamal:** efficient key generation and encryption, Hashed ElGamal with a - general semantically secure symmetric cipher `E_s` (Boneh–Shoup Theorem 11.5) and a - nondegenerate `SecureKDF` instantiation ([#1047]), and Cramer–Shoup CCA security ([#1000]). +- **Diffie–Hellman and ElGamal:** Hashed ElGamal with a general semantically secure symmetric + cipher `E_s` (Boneh–Shoup Theorem 11.5) ([#1047]). - **Chosen-ciphertext security** ([#1000]): authenticated encryption by encrypt-then-MAC and Cramer–Shoup from DDH, with KEM–DEM hybrid encryption ([#881]) as the chosen-plaintext starting point (Boneh–Shoup Exercise 11.9). From ed6219a2f522467c9e5268b3abbc2d6e5b1eea9a Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Mon, 26 Oct 2026 18:00:35 -0400 Subject: [PATCH 2/2] fix(crypto): address review feedback on #1222 (non-vacuous KDF tests, plain polytime, conditional seed docs) --- .../Crypto/Computational/ElGamal/KDF.lean | 16 +- .../Computational/ElGamal/ProbComp.lean | 163 ++++++++++++------ ComplexityTests/Crypto/DiffieHellman.lean | 72 ++++++-- 3 files changed, 177 insertions(+), 74 deletions(-) diff --git a/Complexity/Crypto/Computational/ElGamal/KDF.lean b/Complexity/Crypto/Computational/ElGamal/KDF.lean index 7bbe41ab9..d22221ff7 100644 --- a/Complexity/Crypto/Computational/ElGamal/KDF.lean +++ b/Complexity/Crypto/Computational/ElGamal/KDF.lean @@ -47,10 +47,10 @@ via the Leftover Hash Lemma, without any computational assumptions on the hash f To formalize this over an arbitrary `PrimeOrderGroupFamily`: 1. `PrimeOrderGroupFamily.withSeed` augments the public group description `d : F.Desc` with a public bit-string seed `s : List Bool`, giving `F.withSeed.Desc = F.Desc × List Bool`. Under - `PrimeOrderGroupFamily.seededSetup`, `s` is sampled uniformly from `{0, 1}^{seedLen n d}` - independently of the group description `d ← setup n`. When `seedLen` is polynomial-time - computable in unary, `DDH.withSeed` transfers the `DDH` assumption from `(F, setup)` to - `(F.withSeed, F.seededSetup setup seedLen)`. + `PrimeOrderGroupFamily.seededSetup`, given the sampled group description `d ← setup n`, `s` is + sampled uniformly from `{0, 1}^{seedLen n d}` conditional on `d` (and independently of the group + exponents). When `seedLen` is polynomial-time computable in unary, `DDH.withSeed` transfers the + `DDH` assumption from `(F, setup)` to `(F.withSeed, F.seededSetup setup seedLen)`. 2. `PrimeOrderGroupFamily.linearHashKDF` pads the encoded group element `w : List Bool` to the fixed self-delimiting width `2 * bound d + 1` via `Cslib.BitString.padWord (bound d) w` and hashes it with the public Boolean matrix seed `s` via `Cslib.BitString.LinearHash.wordHash (keyLen d) s`. @@ -72,8 +72,8 @@ To formalize this over an arbitrary `PrimeOrderGroupFamily`: * `Cslib.Crypto.PrimeOrderGroupFamily.withSeed`: prime-order group family with a public hash seed in the description. -* `Cslib.Crypto.PrimeOrderGroupFamily.seededSetup`: setup distribution augmenting `setup n` with an - independent uniform bit-string seed. +* `Cslib.Crypto.PrimeOrderGroupFamily.seededSetup`: setup distribution augmenting `setup n` with a + bit-string seed sampled uniformly conditional on the sampled group description. * `Cslib.Crypto.PrimeOrderGroupFamily.seededDDHDistinguisher`: DDH reduction that samples the public seed internally. * `Cslib.Crypto.PrimeOrderGroupFamily.linearHashKDF`: polynomial-time key-derivation function built @@ -152,8 +152,8 @@ abbrev withSeed : PrimeOrderGroupFamily where (encPair (encPair F.encDesc encBits) (encPair encNat encBits)) F.encDesc).prod (by fun_prop)) -/-- Setup distribution for `F.withSeed`: draw `d ← setup n` and an independent uniform seed -`s ← Cslib.BitString.uniformList (seedLen n d)`, and return `(d, s)`. -/ +/-- Setup distribution for `F.withSeed`: draw `d ← setup n`, then sample a uniform seed +`s ← Cslib.BitString.uniformList (seedLen n d)` conditional on `d`, and return `(d, s)`. -/ noncomputable def seededSetup (setup : ℕ → PMF F.Desc) (seedLen : ℕ → F.Desc → ℕ) (n : ℕ) : PMF F.withSeed.Desc := do let d ← setup n diff --git a/Complexity/Crypto/Computational/ElGamal/ProbComp.lean b/Complexity/Crypto/Computational/ElGamal/ProbComp.lean index 236dd315e..74558b0ce 100644 --- a/Complexity/Crypto/Computational/ElGamal/ProbComp.lean +++ b/Complexity/Crypto/Computational/ElGamal/ProbComp.lean @@ -21,7 +21,6 @@ import Complexity.Crypto.Negligible.Basic import Complexity.Probability.PMF import Complexity.Probability.PMF.Event import Complexity.Probability.StatisticalDistance -import Complexity.Tactic.PolyTime import Complexity.Tactic.PPT /-! @@ -127,20 +126,20 @@ noncomputable def sampleElGamalExp (n : ℕ) (d : F.Desc) : ProbComp ℕ := private theorem isPPTOn_sampleElGamalExp {γ : Type} {encIn : γ ↪ List Bool} {n : γ → ℕ} {d : γ → F.Desc} - (hn : ComputableTidilyInPolyTime n encIn encUnary) - (hd : ComputableTidilyInPolyTime d encIn F.encDesc) : + (hn : ComputableInPolyTime n encIn encUnary) + (hd : ComputableInPolyTime d encIn F.encDesc) : IsPPTOn encIn encNat (fun a => F.sampleElGamalExp (n a) (d a)) := by - have hord : ComputableTidilyInPolyTime (fun a => F.order (d a)) encIn encNat := - F.computableInPolyTime_order.tidy.comp hd - have hlen : ComputableTidilyInPolyTime + have hord : ComputableInPolyTime (fun a => F.order (d a)) encIn encNat := + F.computableInPolyTime_order.comp hd + have hlen : ComputableInPolyTime (fun a => (encNat (F.order (d a))).length) encIn encUnary := - (ComputableTidilyInPolyTime.encoding_length encNat).comp hord - have hadd : ComputableTidilyInPolyTime (fun p : ℕ × ℕ => p.1 + p.2) + (ComputableInPolyTime.encoding_length encNat).comp hord + have hadd : ComputableInPolyTime (fun p : ℕ × ℕ => p.1 + p.2) (encPair encUnary encUnary) encUnary := by fun_prop - have hwidth : ComputableTidilyInPolyTime + have hwidth : ComputableInPolyTime (fun a => n a + (encNat (F.order (d a))).length) encIn encUnary := hadd.comp (hn.prod hlen) - exact isPPTOn_sampleModNat (.of_tidy hwidth) (.of_tidy hord) + exact isPPTOn_sampleModNat hwidth hord /-- Replacing one `sampleElGamalExp n d` draw by an exact uniform draw on `ZMod (F.order d)` changes `Game.advantage` by at most `1 / 2 ^ n`. -/ @@ -185,14 +184,23 @@ noncomputable def elGamalKeyGenProb (d : ℕ → F.Desc) (n : ℕ) : theorem isPPTOn_elGamalKeyGenProb {d : ℕ → F.Desc} (hd : ComputableInPolyTime d encUnary F.encDesc) : IsPPTOn encUnary (encPair encBits encBits) (F.elGamalKeyGenProb d) := by - have := hd.tidy - have := F.computableInPolyTime_encodeElGamalPublicKey.tidy - have htail : ComputableTidilyInPolyTime - (fun p : ℕ × ℕ => - (encPair F.encDesc encBits (d p.1, F.encodeElGamalPublicKey (d p.1, p.2)), encNat p.2)) - (encPair encUnary encNat) (encPair encBits encBits) := by fun_prop + let E := encPair encUnary encNat + have hd1 : ComputableInPolyTime (fun p : ℕ × ℕ => d p.1) E F.encDesc := + hd.comp (ComputableInPolyTime.fst _ _) + have ha : ComputableInPolyTime (fun p : ℕ × ℕ => p.2) E encNat := + ComputableInPolyTime.snd _ _ + have hu : ComputableInPolyTime + (fun p : ℕ × ℕ => F.encodeElGamalPublicKey (d p.1, p.2)) E encBits := + F.computableInPolyTime_encodeElGamalPublicKey.comp (hd1.prod ha) + have hpk : ComputableInPolyTime + (fun p : ℕ × ℕ => encPair F.encDesc encBits (d p.1, F.encodeElGamalPublicKey (d p.1, p.2))) + E encBits := + (ComputableInPolyTime.of_eq fun _ => rfl).comp (hd1.prod hu) + have hsk : ComputableInPolyTime (fun p : ℕ × ℕ => encNat p.2) E encBits := + (ComputableInPolyTime.of_eq fun _ => rfl).comp ha unfold elGamalKeyGenProb - exact (F.isPPTOn_sampleElGamalExp (by fun_prop) hd.tidy).bind_with htail.isPPTOn + exact (F.isPPTOn_sampleElGamalExp ComputableInPolyTime.id' hd).bind_with + (hpk.prod hsk).isPPTOn /-- Probabilistic polynomial-time Hashed ElGamal KEM encapsulation for a group description family `d : ℕ → F.Desc` ([BonehShoup2023], Section 11.5, p. 445, Remark 11.1, p. 446, and Exercise 11.9, @@ -213,26 +221,30 @@ theorem isPPTOn_hashedElGamalEncapsProb {H : F.Desc × List Bool → List Bool} IsPPTOn (encPair encUnary encBits) (encPair encBits encBits) (fun p => F.hashedElGamalEncapsProb H d p.1 p.2) := by let E := encPair (encPair encUnary encBits) encNat - have hd1 : ComputableTidilyInPolyTime (fun p : (ℕ × List Bool) × ℕ => d p.1.1) E F.encDesc := - hd.tidy.comp (by fun_prop) - have hgen : ComputableTidilyInPolyTime + have hd1 : ComputableInPolyTime (fun p : (ℕ × List Bool) × ℕ => d p.1.1) E F.encDesc := + hd.comp ((ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.fst _ _)) + have hb : ComputableInPolyTime (fun p : (ℕ × List Bool) × ℕ => p.2) E encNat := + ComputableInPolyTime.snd _ _ + have hu : ComputableInPolyTime (fun p : (ℕ × List Bool) × ℕ => dropFrame p.1.2) E encBits := + ComputableInPolyTime.dropFrame.comp + ((ComputableInPolyTime.snd _ _).comp (ComputableInPolyTime.fst _ _)) + have hgen : ComputableInPolyTime (fun p : (ℕ × List Bool) × ℕ => F.encode (d p.1.1) (F.generator (d p.1.1))) E encBits := - F.computableInPolyTime_generator.tidy.comp hd1 - have hw : ComputableTidilyInPolyTime + F.computableInPolyTime_generator.comp hd1 + have hw : ComputableInPolyTime (fun p : (ℕ × List Bool) × ℕ => F.smul (d p.1.1, p.2, dropFrame p.1.2)) E encBits := - F.computableInPolyTime_smul.tidy.comp (hd1.prod (by fun_prop)) - have hk : ComputableTidilyInPolyTime + F.computableInPolyTime_smul.comp (hd1.prod (hb.prod hu)) + have hk : ComputableInPolyTime (fun p : (ℕ × List Bool) × ℕ => H (d p.1.1, F.smul (d p.1.1, p.2, dropFrame p.1.2))) E encBits := - hH.tidy.comp (hd1.prod hw) - have hv : ComputableTidilyInPolyTime + hH.comp (hd1.prod hw) + have hv : ComputableInPolyTime (fun p : (ℕ × List Bool) × ℕ => F.smul (d p.1.1, p.2, F.encode (d p.1.1) (F.generator (d p.1.1)))) E encBits := - F.computableInPolyTime_smul.tidy.comp (hd1.prod ((by fun_prop : - ComputableTidilyInPolyTime (fun p : (ℕ × List Bool) × ℕ => p.2) E encNat).prod hgen)) + F.computableInPolyTime_smul.comp (hd1.prod (hb.prod hgen)) unfold hashedElGamalEncapsProb - exact (F.isPPTOn_sampleElGamalExp (by fun_prop) (hd.tidy.comp (by fun_prop))).bind_with - (hk.prod hv).isPPTOn + exact (F.isPPTOn_sampleElGamalExp (ComputableInPolyTime.fst _ _) + (hd.comp (ComputableInPolyTime.fst _ _))).bind_with (hk.prod hv).isPPTOn /-- Deterministic polynomial-time Hashed ElGamal KEM decapsulation ([BonehShoup2023], Section 11.5, p. 445, Remark 11.1, p. 446): given secret key `sk = encNat a` and KEM ciphertext @@ -249,11 +261,21 @@ theorem computableInPolyTime_hashedElGamalDecaps {H : F.Desc × List Bool → Li ComputableInPolyTime (fun p : ℕ × List Bool × List Bool => F.hashedElGamalDecaps H d p.1 p.2.1 p.2.2) (encPair encUnary (encPair encBits encBits)) encBits := by - have := hd.tidy - have := hH.tidy - have := F.computableInPolyTime_smul.tidy + let E := encPair encUnary (encPair encBits encBits) + have hd1 : ComputableInPolyTime (fun p : ℕ × List Bool × List Bool => d p.1) E F.encDesc := + hd.comp (ComputableInPolyTime.fst _ _) + have ha : ComputableInPolyTime + (fun p : ℕ × List Bool × List Bool => ofBits p.2.1) E encNat := + ComputableInPolyTime.bitsToNat.comp + ((ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.snd _ _)) + have hct : ComputableInPolyTime + (fun p : ℕ × List Bool × List Bool => p.2.2) E encBits := + (ComputableInPolyTime.snd _ _).comp (ComputableInPolyTime.snd _ _) + have hw : ComputableInPolyTime + (fun p : ℕ × List Bool × List Bool => F.smul (d p.1, ofBits p.2.1, p.2.2)) E encBits := + F.computableInPolyTime_smul.comp (hd1.prod (ha.prod hct)) unfold hashedElGamalDecaps - exact .of_tidy (by fun_prop) + exact hH.comp (hd1.prod hw) /-- **Hashed ElGamal KEM decapsulation correctness**: for any `n : ℕ`, any `(pk, sk)` in the support of `elGamalKeyGenProb d n`, and any `(k, ctKem)` in the support of @@ -552,9 +574,22 @@ theorem DDH.wordINDCPA_hybrid_hashedElGamal {F : PrimeOrderGroupFamily} (hencryptSym : IsPPTOn (encPair encUnary (encPair encBits encBits)) encBits (fun p => encryptSym p.1 p.2.1 p.2.2)) : WordINDCPA (F.elGamalKeyGenProb d) - (hybridEncrypt (F.hashedElGamalEncapsProb H d) encryptSym) := - hDDH.indcpaOn_hybrid_hashedElGamal hKDF hdem - (ComputableInPolyTime.of_tidy (by polytime)) (fun _ _ _ _ => rfl) hH hd hencryptSym + (hybridEncrypt (F.hashedElGamalEncapsProb H d) encryptSym) := by + let E := encPair encUnary (encPair encBits (encPair encBits encBits)) + have hl0 : ComputableInPolyTime + (fun p : ℕ × List Bool × List Bool × List Bool => p.2.2.1.length) E encUnary := + (ComputableInPolyTime.encoding_length encBits).comp + ((ComputableInPolyTime.fst _ _).comp + ((ComputableInPolyTime.snd _ _).comp (ComputableInPolyTime.snd _ _))) + have hl1 : ComputableInPolyTime + (fun p : ℕ × List Bool × List Bool × List Bool => p.2.2.2.length) E encUnary := + (ComputableInPolyTime.encoding_length encBits).comp + ((ComputableInPolyTime.snd _ _).comp + ((ComputableInPolyTime.snd _ _).comp (ComputableInPolyTime.snd _ _))) + have hbeq : ComputableInPolyTime (fun p : ℕ × ℕ => p.1 == p.2) + (encPair encUnary encUnary) encBool := by fun_prop + exact hDDH.indcpaOn_hybrid_hashedElGamal hKDF hdem + (hbeq.comp (hl0.prod hl1)) (fun _ _ _ _ => rfl) hH hd hencryptSym /-- Probabilistic polynomial-time multiplicative ElGamal encryption for a group description family `d : ℕ → F.Desc` and message encoder `encodeMsg : F.Desc → Msg → List Bool` @@ -576,17 +611,39 @@ theorem isPPTOn_elGamalEncryptProb {Msg : Type} {encMsg : Msg ↪ List Bool} (hd : ComputableInPolyTime d encUnary F.encDesc) : IsPPTOn (encPair encUnary (encPair encBits encMsg)) encBits (fun p => F.elGamalEncryptProb encodeMsg d p.1 p.2.1 p.2.2) := by - have := hd.tidy - have := hencMsg.tidy - have := F.computableInPolyTime_encodeElGamalEncrypt.tidy - have henc : ComputableTidilyInPolyTime + let E := encPair (encPair encUnary (encPair encBits encMsg)) encNat + have hp1 : ComputableInPolyTime (fun p : (ℕ × List Bool × Msg) × ℕ => p.1) + E (encPair encUnary (encPair encBits encMsg)) := + ComputableInPolyTime.fst _ _ + have hd1 : ComputableInPolyTime (fun p : (ℕ × List Bool × Msg) × ℕ => d p.1.1) E F.encDesc := + hd.comp ((ComputableInPolyTime.fst _ _).comp hp1) + have hp12 : ComputableInPolyTime (fun p : (ℕ × List Bool × Msg) × ℕ => p.1.2) + E (encPair encBits encMsg) := + (ComputableInPolyTime.snd _ _).comp hp1 + have hu : ComputableInPolyTime + (fun p : (ℕ × List Bool × Msg) × ℕ => dropFrame p.1.2.1) E encBits := + ComputableInPolyTime.dropFrame.comp ((ComputableInPolyTime.fst _ _).comp hp12) + have hm : ComputableInPolyTime (fun p : (ℕ × List Bool × Msg) × ℕ => p.1.2.2) E encMsg := + (ComputableInPolyTime.snd _ _).comp hp12 + have hem : ComputableInPolyTime + (fun p : (ℕ × List Bool × Msg) × ℕ => encodeMsg (d p.1.1) p.1.2.2) E encBits := + hencMsg.comp (hd1.prod hm) + have hb : ComputableInPolyTime (fun p : (ℕ × List Bool × Msg) × ℕ => p.2) E encNat := + ComputableInPolyTime.snd _ _ + have hraw : ComputableInPolyTime + (fun p : (ℕ × List Bool × Msg) × ℕ => + F.encodeElGamalEncrypt (d p.1.1, dropFrame p.1.2.1, encodeMsg (d p.1.1) p.1.2.2, p.2)) + E (encPair encBits encBits) := + F.computableInPolyTime_encodeElGamalEncrypt.comp (hd1.prod (hu.prod (hem.prod hb))) + have henc : ComputableInPolyTime (fun p : (ℕ × List Bool × Msg) × ℕ => encPair encBits encBits (F.encodeElGamalEncrypt (d p.1.1, dropFrame p.1.2.1, encodeMsg (d p.1.1) p.1.2.2, p.2))) - (encPair (encPair encUnary (encPair encBits encMsg)) encNat) encBits := by fun_prop + E encBits := + (ComputableInPolyTime.of_eq fun _ => rfl).comp hraw unfold elGamalEncryptProb - exact (F.isPPTOn_sampleElGamalExp (by fun_prop) (hd.tidy.comp (by fun_prop))).bind_with - henc.isPPTOn + exact (F.isPPTOn_sampleElGamalExp (ComputableInPolyTime.fst _ _) + (hd.comp (ComputableInPolyTime.fst _ _))).bind_with henc.isPPTOn /-- Deterministic polynomial-time multiplicative ElGamal decryption on words: given secret key `sk = encNat a` and ciphertext `ct = encPair encBits encBits (v, e)`, compute @@ -600,10 +657,20 @@ theorem computableInPolyTime_elGamalDecryptDet {d : ℕ → F.Desc} ComputableInPolyTime (fun p : ℕ × List Bool × List Bool => F.elGamalDecryptDet d p.1 p.2.1 p.2.2) (encPair encUnary (encPair encBits encBits)) encBits := by - have := hd.tidy - have := F.computableInPolyTime_decodeElGamal.tidy + let E := encPair encUnary (encPair encBits encBits) + have hd1 : ComputableInPolyTime (fun p : ℕ × List Bool × List Bool => d p.1) E F.encDesc := + hd.comp (ComputableInPolyTime.fst _ _) + have ha : ComputableInPolyTime (fun p : ℕ × List Bool × List Bool => ofBits p.2.1) E encNat := + ComputableInPolyTime.bitsToNat.comp + ((ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.snd _ _)) + have hct : ComputableInPolyTime (fun p : ℕ × List Bool × List Bool => p.2.2) E encBits := + (ComputableInPolyTime.snd _ _).comp (ComputableInPolyTime.snd _ _) + have hv : ComputableInPolyTime (fun p : ℕ × List Bool × List Bool => unframe p.2.2) E encBits := + ComputableInPolyTime.unframe.comp hct + have he : ComputableInPolyTime (fun p : ℕ × List Bool × List Bool => dropFrame p.2.2) E encBits := + ComputableInPolyTime.dropFrame.comp hct unfold elGamalDecryptDet - exact .of_tidy (by fun_prop) + exact F.computableInPolyTime_decodeElGamal.comp (hd1.prod (ha.prod (hv.prod he))) /-- **Multiplicative ElGamal decryption correctness on `ProbComp` outputs**: for any `(pk, sk)` in the support of `elGamalKeyGenProb d n`, any `m : F.Carrier (d n)`, and any `ct` in the support of @@ -741,7 +808,7 @@ theorem DDH.indcpa_elGamalBitEncryptProb {F : PrimeOrderGroupFamily} {d : ℕ (hDDH : F.DDH (fun n => PMF.pure (d n))) : INDCPA (F.elGamalKeyGenProb d) (F.elGamalEncryptProb F.encodeBit d) := hDDH.indcpaOn_elGamalEncryptProb - (ComputableTidilyInPolyTime.const true).computableInPolyTime + (ComputableInPolyTime.const true) F.admitsGroupElements_encodeBit F.computableInPolyTime_encodeBit end Cslib.Crypto.PrimeOrderGroupFamily diff --git a/ComplexityTests/Crypto/DiffieHellman.lean b/ComplexityTests/Crypto/DiffieHellman.lean index 9eee87885..2031655b9 100644 --- a/ComplexityTests/Crypto/DiffieHellman.lean +++ b/ComplexityTests/Crypto/DiffieHellman.lean @@ -11,7 +11,6 @@ import Complexity.Crypto.Computational.ElGamal import Complexity.Crypto.Computational.ElGamal.KDF import Complexity.Crypto.Computational.ElGamal.ProbComp import Complexity.Crypto.Negligible.Basic -import Complexity.Tactic.PolyTime import Complexity.Tactic.PPT import Mathlib.Tactic.NormNum.Prime @@ -464,21 +463,58 @@ example : (schnorrGroups.linearHashKDF (fun _ => 4) (fun _ => 6) ((d23, List.replicate 52 true), Nat.bits 16)).length = 4 := by decide -/-- Positive-side non-degenerate `SecureKDF` instantiation (`k = 4 > 0`): for any setup law whose -supported descriptions have group order at least `2 ^ n` and encoded group elements of length at -most `6`, `linearHashKDF (fun _ => 4) (fun _ => 6)` is a `SecureKDF` for `schnorrGroups.withSeed` -with output key length `4 > 0`. -/ +/-- Every element of `schnorrGroups.Carrier d23` (order `11`, modulus `23`) has binary encoding +length at most `6`. -/ +theorem schnorrGroups_encode_d23_length_le (x : schnorrGroups.Carrier d23) : + (schnorrGroups.encode d23 x).length ≤ 6 := by + have : NeZero d23.1.1 := ⟨by decide⟩ + have hfin : ∀ i : Fin 23, i.val.bits.length ≤ 6 := by decide + exact hfin ⟨((Additive.toMul x).1 : ZMod d23.1.1).val, ZMod.val_lt _⟩ + +/-- Unconditional concrete finite quantitative bound on `d23` (`order d23 = 11`, `B = 6`, `k = 4`): +for any KDF distinguisher, the advantage of distinguishing `linearHashKDF (fun _ => 4) (fun _ => 6)` +from a truly uniform 4-bit key on `d23` is bounded by `NNReal.sqrt (2 ^ 4 / 11) / 2`. -/ +example (distinguisher : ℕ → schnorrGroups.withSeed.Desc × List Bool × List Bool × List Bool → + ProbComp Bool) (n : ℕ) : + Game.advantage + (schnorrGroups.withSeed.kdfRealGame + (schnorrGroups.seededSetup (fun _ => PMF.pure d23) + (schnorrGroups.linearHashSeedLen (fun _ => 4) (fun _ => 6))) + (schnorrGroups.linearHashKDF (fun _ => 4) (fun _ => 6)) + distinguisher n) + (schnorrGroups.withSeed.kdfIdealGame + (schnorrGroups.seededSetup (fun _ => PMF.pure d23) + (schnorrGroups.linearHashSeedLen (fun _ => 4) (fun _ => 6))) + (fun _ => 4) distinguisher n) ≤ + NNReal.sqrt (2 ^ 4 / (11 : ℝ≥0)) / 2 := + schnorrGroups.advantage_kdfGame_linearHashKDF_le + (fun _ => PMF.pure d23) (fun _ => 4) (fun _ => 6) (fun _ => 4) distinguisher n 11 + (by decide) (fun _ _ => rfl) + (fun d hd x => by + rw [PMF.support_pure, Set.mem_singleton_iff] at hd + subst hd + exact schnorrGroups_encode_d23_length_le x) + (fun d hd => by + rw [PMF.support_pure, Set.mem_singleton_iff] at hd + subst hd + decide) + +/-- Positive-side non-degenerate asymptotic `SecureKDF` instantiation (`k = 4 > 0`): for any setup +law whose supported descriptions have group order at least `2 ^ n`, `schnorrGroups.withSeed` admits +a `SecureKDF` with output key length `4 > 0` (constructed via `linearHashKDF` using the canonical +polynomial encoding-length bound of `schnorrGroups`). -/ example (setup : ℕ → PMF schnorrGroups.Desc) - (hsize : ∀ n, ∀ d ∈ (setup n).support, 2 ^ n ≤ schnorrGroups.order d) - (hbound : ∀ n, ∀ d ∈ (setup n).support, ∀ x : schnorrGroups.Carrier d, - (schnorrGroups.encode d x).length ≤ 6) : - schnorrGroups.withSeed.SecureKDF - (schnorrGroups.seededSetup setup - (schnorrGroups.linearHashSeedLen (fun _ => 4) (fun _ => 6))) - (schnorrGroups.linearHashKDF (fun _ => 4) (fun _ => 6)) - (fun _ => 4) := - schnorrGroups.secureKDF_linearHashKDF_const setup (fun _ => 6) 4 - Nat.two_pow_pos hbound hsize negligible_inv_two_pow + (hsize : ∀ n, ∀ d ∈ (setup n).support, 2 ^ n ≤ schnorrGroups.order d) : + ∃ (seedLen : ℕ → schnorrGroups.Desc → ℕ) + (H : schnorrGroups.withSeed.Desc × List Bool → List Bool), + ComputableInPolyTime (fun p => seedLen p.1 p.2) + (encPair encUnary schnorrGroups.encDesc) encUnary ∧ + ComputableInPolyTime H + (encPair schnorrGroups.withSeed.encDesc encBits) encBits ∧ + (∀ ds : schnorrGroups.withSeed.Desc, ∀ w : List Bool, (H (ds, w)).length = 4) ∧ + schnorrGroups.withSeed.SecureKDF + (schnorrGroups.seededSetup setup seedLen) H (fun _ => 4) := + schnorrGroups.exists_secureKDF_withSeed setup 4 Nat.two_pow_pos hsize negligible_inv_two_pow /-- Negative-side KDF counterexample: a constant 1-bit KDF `constZeroKDF := fun _ => [false]` always outputs `[false]` instead of a uniform 1-bit key. -/ @@ -497,9 +533,9 @@ theorem isPPTOn_firstBitKDFDistinguisher : (encPair encUnary (encPair schnorrGroups.encDesc (encPair encBits (encPair encBits encBits)))) encBool (fun input => firstBitKDFDistinguisher input.1 input.2) := by - have hhead : ComputableTidilyInPolyTime (fun s : List Bool => s.headD false) encBits encBool := by + have hhead : ComputableInPolyTime (fun s : List Bool => s.headD false) encBits encBool := by fun_prop - have hproj : ComputableTidilyInPolyTime + have hproj : ComputableInPolyTime (fun input : ℕ × schnorrGroups.Desc × List Bool × List Bool × List Bool => input.2.2.2.2) (encPair encUnary (encPair schnorrGroups.encDesc (encPair encBits (encPair encBits encBits)))) @@ -544,7 +580,7 @@ theorem not_secureKDF_constZeroKDF : /-- The constant group description family `fun _ : ℕ => d23` is computable in polynomial time. -/ theorem computableInPolyTime_const_d23 : ComputableInPolyTime (fun _ : ℕ => d23) encUnary schnorrGroups.encDesc := - ComputableInPolyTime.of_tidy (ComputableTidilyInPolyTime.const d23) + ComputableInPolyTime.const d23 /-- Support-level round-trip correctness of `elGamalKeyGenProb`, `hashedElGamalEncapsProb`, and `hashedElGamalDecaps` on `d23`. -/