From 8662848dedebee15ee6bec88519d029d8594cac8 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 23 Oct 2026 14:21:28 -0400 Subject: [PATCH 1/2] feat(crypto): prove generated-key GSW security from exact decision LWE Identify the actual serialized public-key law, construct one uniform hidden-bit reduction with loss two, and instantiate IND-CPA with a positive-noise parameter family. Include native-efficiency clients, regressions, and a self-contained checked security abstract. AI-assisted by OpenAI Codex. Core/reduction integration: worker-codex-gsw-lwe-security-20261023. Parameter subtask: worker-codex-gsw-parameters-20261023. Abstract subtask: /root/library_map. Independent source/API/correctness review: /root/maintenance_audit. Independent abstract review: /root/refactor_plan_review. No remaining findings. All six repository checks passed on the final source. Mathematical sources are credited in module docstrings; hardness, circular security and FHE are not claimed. --- Complexity.lean | 6 + .../Encryption/PublicKeyReplacement.lean | 147 ++++++++ .../Computational/Homomorphic/GSW/LWE.lean | 84 +++++ .../Homomorphic/GSW/Parameters.lean | 210 ++++++++++++ .../Homomorphic/GSW/Security.lean | 169 +++++++++ .../Crypto/Computational/LWE/Basic.lean | 100 ++++++ Complexity/Crypto/Negligible/Dyadic.lean | 60 ++++ .../Languages/Probabilistic/Vector.lean | 10 + ComplexityTests.lean | 4 + .../Abstracts/GSWSecurityAbstract.lean | 263 ++++++++++++++ .../Abstracts/GSWSecurityBridge.lean | 321 ++++++++++++++++++ ComplexityTests/Crypto/GSWParameters.lean | 165 +++++++++ ComplexityTests/Crypto/GSWSecurity.lean | 156 +++++++++ 13 files changed, 1695 insertions(+) create mode 100644 Complexity/Crypto/Computational/Encryption/PublicKeyReplacement.lean create mode 100644 Complexity/Crypto/Computational/Homomorphic/GSW/LWE.lean create mode 100644 Complexity/Crypto/Computational/Homomorphic/GSW/Parameters.lean create mode 100644 Complexity/Crypto/Computational/Homomorphic/GSW/Security.lean create mode 100644 Complexity/Crypto/Computational/LWE/Basic.lean create mode 100644 Complexity/Crypto/Negligible/Dyadic.lean create mode 100644 ComplexityTests/Abstracts/GSWSecurityAbstract.lean create mode 100644 ComplexityTests/Abstracts/GSWSecurityBridge.lean create mode 100644 ComplexityTests/Crypto/GSWParameters.lean create mode 100644 ComplexityTests/Crypto/GSWSecurity.lean diff --git a/Complexity.lean b/Complexity.lean index 374cc26b97..0c484af1da 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1276,6 +1276,7 @@ public import Complexity.Crypto.Computational.Commitment public import Complexity.Crypto.Computational.Encryption.Basic public import Complexity.Crypto.Computational.Encryption.Circular public import Complexity.Crypto.Computational.Encryption.PolyTime +public import Complexity.Crypto.Computational.Encryption.PublicKeyReplacement public import Complexity.Crypto.Computational.GGM.Circuit public import Complexity.Crypto.Computational.GGM.Evaluation public import Complexity.Crypto.Computational.GGM.Expansion @@ -1316,10 +1317,13 @@ public import Complexity.Crypto.Computational.Homomorphic.GSW.Basic public import Complexity.Crypto.Computational.Homomorphic.GSW.Decoding public import Complexity.Crypto.Computational.Homomorphic.GSW.Gadget public import Complexity.Crypto.Computational.Homomorphic.GSW.Hiding +public import Complexity.Crypto.Computational.Homomorphic.GSW.LWE public import Complexity.Crypto.Computational.Homomorphic.GSW.Noise +public import Complexity.Crypto.Computational.Homomorphic.GSW.Parameters public import Complexity.Crypto.Computational.Homomorphic.GSW.Sampling public import Complexity.Crypto.Computational.Homomorphic.GSW.Sampling.Randomness public import Complexity.Crypto.Computational.Homomorphic.GSW.Sampling.Serialized +public import Complexity.Crypto.Computational.Homomorphic.GSW.Security public import Complexity.Crypto.Computational.Homomorphic.GSW.Serialized public import Complexity.Crypto.Computational.Homomorphic.GSW.Serialized.Correctness public import Complexity.Crypto.Computational.Homomorphic.GSW.Serialized.PolyTime @@ -1348,6 +1352,7 @@ public import Complexity.Crypto.Computational.Homomorphic.Leveled.Security public import Complexity.Crypto.Computational.Homomorphic.Refresh public import Complexity.Crypto.Computational.Hybrid.SavedPrediction public import Complexity.Crypto.Computational.Hybrid.Sequence +public import Complexity.Crypto.Computational.LWE.Basic public import Complexity.Crypto.Computational.OneWay public import Complexity.Crypto.Computational.OneWay.BPP public import Complexity.Crypto.Computational.OneWay.Collision @@ -1411,6 +1416,7 @@ public import Complexity.Crypto.Game.Hybrid public import Complexity.Crypto.Game.Statistical public import Complexity.Crypto.Negligible public import Complexity.Crypto.Negligible.Basic +public import Complexity.Crypto.Negligible.Dyadic public import Complexity.Crypto.Primitives.PRG.Circuit public import Complexity.Crypto.Primitives.PRG.Game public import Complexity.Crypto.Primitives.PRG.NextBit diff --git a/Complexity/Crypto/Computational/Encryption/PublicKeyReplacement.lean b/Complexity/Crypto/Computational/Encryption/PublicKeyReplacement.lean new file mode 100644 index 0000000000..9c3bbc437c --- /dev/null +++ b/Complexity/Crypto/Computational/Encryption/PublicKeyReplacement.lean @@ -0,0 +1,147 @@ +/- +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.Basic +public import Complexity.Crypto.Computational.Encryption.Basic +import Complexity.Probability.PMF +import Complexity.Tactic.PPT + +/-! +# Replacing the public-key distribution in chosen-message security + +One uniform distinguisher samples a hidden fair challenge bit after the adversary has chosen its +messages and saved state. It runs the actual encryption and guessing stages, then returns the +guess XOR the hidden bit. Comparing this same distinguisher on two public-key distributions +controls the change in their chosen-message gaps, with an exact factor of two. + +## Main definitions + +* `publicKeyGame`: the chosen-message experiment for a specified public-key law. +* `keyDistinguisher`: the single reduction, preserving the adversary's saved state. + +## Main results + +* `eval_game_eq_publicKeyGame`: the actual encryption game uses its public-key marginal. +* `isPPT_keyDistinguisher`: native strict PPT composition of the actual reduction. +* `probability_keyDistinguisher`: the exact affine identity for the signed chosen-message gap. +* `advantage_publicKeyGame_le`: quantitative public-key replacement with loss two. + +## References + +* [D. Boneh, V. Shoup, *A Graduate Course in Applied Cryptography*][BonehShoup2023], + Section 11.2, for the chosen-message experiment and game-reduction method. +-/ + +@[expose] public section + +namespace Cslib.Crypto.Encryption + +open Probability Turing.MultiTapeTM + +/-- Run the chosen-message experiment with a specified public-key distribution. The complete +state returned by message selection is passed unchanged to guessing. -/ +noncomputable def publicKeyGame (keys : PMF (List Bool)) + (encrypt : ℕ → List Bool → Bool → ProbComp (List Bool)) + (adversary : Adversary) (bit : Bool) (security : ℕ) : Game := do + let pk ← keys + let choice ← ProbComp.eval (adversary.choose security pk) + let ciphertext ← ProbComp.eval + (encrypt security pk (if bit then choice.1.2 else choice.1.1)) + ProbComp.eval (adversary.guess security choice.2 ciphertext) + +/-- An honest key generator contributes precisely its public-key marginal. -/ +theorem eval_game_eq_publicKeyGame (keyGen : ℕ → ProbComp (List Bool × List Bool)) + (encrypt : ℕ → List Bool → Bool → ProbComp (List Bool)) + (adversary : Adversary) (bit : Bool) (security : ℕ) : + ProbComp.eval (game keyGen encrypt adversary bit security) = + publicKeyGame ((ProbComp.eval (keyGen security)).map Prod.fst) + encrypt adversary bit security := eval_game keyGen encrypt adversary bit security + +/-- A single uniform distinguisher with its own hidden fair challenge bit. The adversary sees +only the supplied public key and the actual challenge ciphertext, with its saved state retained. -/ +noncomputable def keyDistinguisher + (encrypt : ℕ → List Bool → Bool → ProbComp (List Bool)) + (adversary : Adversary) : Distinguisher := fun security pk => do + let choice ← adversary.choose security pk + let bit ← ProbComp.uniform Bool + let ciphertext ← encrypt security pk (if bit then choice.1.2 else choice.1.1) + let guess ← adversary.guess security choice.2 ciphertext + return guess ^^ bit + +/-- The reduction is one uniform strict PPT program when encryption and both adversary stages +are certified on their complete inputs. -/ +theorem isPPT_keyDistinguisher + {encrypt : ℕ → List Bool → Bool → ProbComp (List Bool)} {adversary : Adversary} + (hencrypt : IsPPTOn (encPair encUnary (encPair encBits encBool)) encBits + (fun input => encrypt input.1 input.2.1 input.2.2)) + (hadversary : adversary.IsPPT) : IsPPT encBool (keyDistinguisher encrypt adversary) := by + have hchoose := hadversary.choose + have hguess := hadversary.guess + unfold keyDistinguisher + ppt + +/-- The hidden-bit experiment averages the two chosen-message games, complementing the second. +No finiteness or independence assumption is imposed on the saved state. -/ +theorem distinguishingGame_keyDistinguisher (keys : PMF (List Bool)) + (encrypt : ℕ → List Bool → Bool → ProbComp (List Bool)) + (adversary : Adversary) (security : ℕ) : + distinguishingGame keys (keyDistinguisher encrypt adversary security) = (do + let bit ← PMF.uniformOfFintype Bool + (publicKeyGame keys encrypt adversary bit security).map (fun guess => guess ^^ bit)) := by + simp only [distinguishingGame, keyDistinguisher, publicKeyGame, ProbComp.eval_bind, + ProbComp.eval_uniform, ProbComp.eval_pure, PMF.monad_bind_eq_bind, PMF.map_bind] + rw [PMF.bind_comm] + congr 1 + funext pk + rw [PMF.bind_comm] + rfl + +/-- Acceptance is one half plus half the signed chosen-message gap. -/ +theorem probability_keyDistinguisher (keys : PMF (List Bool)) + (encrypt : ℕ → List Bool → Bool → ProbComp (List Bool)) + (adversary : Adversary) (security : ℕ) : + (Game.succProbability + (distinguishingGame keys (keyDistinguisher encrypt adversary security)) : ℝ) = + (1 + (Game.succProbability (publicKeyGame keys encrypt adversary false security) : ℝ) - + Game.succProbability (publicKeyGame keys encrypt adversary true security)) / 2 := by + rw [distinguishingGame_keyDistinguisher] + simp only [Game.succProbability, ENNReal.coe_toNNReal_eq_toReal, + PMF.monad_bind_eq_bind, PMF.bind_apply_toReal, Fintype.sum_bool, + PMF.uniformOfFintype_apply, Fintype.card_bool] + norm_num [PMF.toReal_false_eq_one_sub] + ring + +/-- Replacing the public-key law costs at most twice the advantage of one uniform hidden-bit +distinguisher, plus the chosen-message advantage under the replacement law. -/ +theorem advantage_publicKeyGame_le (real ideal : PMF (List Bool)) + (encrypt : ℕ → List Bool → Bool → ProbComp (List Bool)) + (adversary : Adversary) (security : ℕ) : + Game.advantage (publicKeyGame real encrypt adversary false security) + (publicKeyGame real encrypt adversary true security) ≤ + 2 * Game.advantage + (distinguishingGame real (keyDistinguisher encrypt adversary security)) + (distinguishingGame ideal (keyDistinguisher encrypt adversary security)) + + Game.advantage (publicKeyGame ideal encrypt adversary false security) + (publicKeyGame ideal encrypt adversary true security) := by + apply NNReal.coe_le_coe.mp + simp only [NNReal.coe_add, NNReal.coe_mul, NNReal.coe_ofNat, Game.coe_advantage, + probability_keyDistinguisher] + have h := abs_sub_le + ((Game.succProbability (publicKeyGame real encrypt adversary false security) : ℝ) - + Game.succProbability (publicKeyGame real encrypt adversary true security)) + ((Game.succProbability (publicKeyGame ideal encrypt adversary false security) : ℝ) - + Game.succProbability (publicKeyGame ideal encrypt adversary true security)) 0 + have hscale (a b c d : ℝ) : + 2 * |(1 + a - b) / 2 - (1 + c - d) / 2| = |(a - b) - (c - d)| := by + calc + _ = |2 * ((1 + a - b) / 2 - (1 + c - d) / 2)| := by rw [abs_mul]; norm_num + _ = _ := by congr 1; ring + simpa only [hscale, sub_zero] using h + +end Cslib.Crypto.Encryption diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/LWE.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/LWE.lean new file mode 100644 index 0000000000..d084353fe5 --- /dev/null +++ b/Complexity/Crypto/Computational/Homomorphic/GSW/LWE.lean @@ -0,0 +1,84 @@ +/- +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.LWE.Basic +public import Complexity.Crypto.Computational.Homomorphic.GSW.Serialized.Correctness + +/-! +# The decision-LWE distribution of generated GSW public keys + +The public marginal of the actual key generator is exactly the decision-LWE law with independent +centered-binomial errors reduced modulo `2 ^ w`. The joint key generator still retains its secret; +the equality below exposes only the public marginal, as required by the security experiment. + +## Main definitions + +* `noiseLaw`: the precise modular error law supplied to the decision-LWE hypothesis. + +## Main results + +* `eval_errorVector_mod`: independently sampled integer errors give the independent modular law. +* `eval_keyGen_publicMatrix`: the actual generated public matrix has the stated decision-LWE law. +* `eval_keyGenSerialized_publicWord`: the serialized key generator exposes that exact word ensemble. + +## References + +* [C. Gentry, A. Sahai and B. Waters, *Homomorphic Encryption from Learning with Errors: + Conceptually-Simpler, Asymptotically-Faster, Attribute-Based*, Section 3.1][GentrySahaiWaters2013] +-/ + +@[expose] public section + +namespace Cslib.Crypto.Homomorphic.GSW + +open Probability + +/-- Reduce the difference of two independent `η`-bit counts modulo the actual modulus. -/ +noncomputable def noiseLaw (w η : ℕ) : PMF (ZMod (2 ^ w)) := + (ProbComp.eval (sampleCenteredBinomial η)).map (fun error : ℤ => (error : ZMod (2 ^ w))) + +/-- Reducing independent integer errors preserves the complete independent modular error law. -/ +theorem eval_errorVector_mod (m w η : ℕ) : + (ProbComp.eval (OracleComp.replicateFin m (sampleCenteredBinomial η))).map + (fun error i => (error i : ZMod (2 ^ w))) = + PMF.pi (fun _ : Fin m => noiseLaw w η) := by + rw [← ProbComp.eval_replicateFin_map_coords, ProbComp.eval_replicateFin] + simp only [noiseLaw, ProbComp.eval_map] + +/-- The generated public matrix is an exact decision-LWE sample. This equality neither reveals +the generated secret nor asserts that any parameter or error family is computationally hard. -/ +theorem eval_keyGen_publicMatrix (n m w η : ℕ) : + (ProbComp.eval (keyGen n m w η)).map Prod.fst = + LWE.publicMatrixLaw n m w (noiseLaw w η) := by + simp only [keyGen, ProbComp.eval_bind, ProbComp.eval_pure, eval_sampleKeyInputs, + PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.bind_bind, PMF.pure_bind, + PMF.map_bind, PMF.pure_map, LWE.publicMatrixLaw] + rw [← eval_errorVector_mod m w η] + simp only [PMF.bind_map, Function.comp_def] + rfl + +/-- Encoding the actual public marginal gives the exact word ensemble in the hardness +hypothesis, with no secret or error coordinates appended to the adversary's input. -/ +theorem eval_keyGen_publicWord (n m w η : ℕ → ℕ) (security : ℕ) : + (ProbComp.eval (keyGen (n security) (m security) (w security) (η security))).map + (fun keys => Matrix.toBinary keys.1) = + LWE.realEnsemble n m w (fun k => noiseLaw (w k) (η k)) security := by + rw [LWE.realEnsemble, ← eval_keyGen_publicMatrix, PMF.map_comp] + rfl + +/-- The actual serialized key generator has precisely the public marginal used by decision LWE. +The encoded secret is discarded before the distinguisher is called. -/ +theorem eval_keyGenSerialized_publicWord (n m w η : ℕ → ℕ) (security : ℕ) : + (ProbComp.eval + (keyGenSerialized (n security) (m security) (w security) (η security))).map Prod.fst = + LWE.realEnsemble n m w (fun k => noiseLaw (w k) (η k)) security := by + rw [eval_keyGenSerialized, PMF.map_comp] + exact eval_keyGen_publicWord n m w η security + +end Cslib.Crypto.Homomorphic.GSW diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/Parameters.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/Parameters.lean new file mode 100644 index 0000000000..652171a405 --- /dev/null +++ b/Complexity/Crypto/Computational/Homomorphic/GSW/Parameters.lean @@ -0,0 +1,210 @@ +/- +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.Negligible.Dyadic +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Log +import Complexity.Foundations.Data.Nat.Log + +/-! +# Compatible positive-noise GSW parameters + +For `k = λ + 1`, choose `n = η = k`, `w = 16 + 8 * clog 2 k`, ciphertext dimension +`N = (n + 1) * w`, and `m = N + 2 * λ` samples. This explicit family satisfies the statistical +entropy margin and the strict fresh-encryption and one-NAND noise margins simultaneously. + +These are arithmetic and native-runtime facts about the parameter functions. They neither assert +decision-LWE hardness for the finite centered-binomial error nor prove bootstrappability. + +## Main definitions + +* `dimension`, `noise`, `width`, `rows`, `samples`, `modulus`: the numerical parameter family. + +## Main results + +* `entropy_margin`: twice the security parameter in surplus source bits. +* `fresh_margin`, `nand_margin`: strict decoding margins with positive noise. +* `negligible_statistical_error`: the shared-public-matrix error is negligible. +* `computableTidilyInPolyTime_*`: uniform unary native computation of each parameter. + +## References + +* [C. Gentry, A. Sahai and B. Waters, *Homomorphic Encryption from Learning with Errors: + Conceptually-Simpler, Asymptotically-Faster, Attribute-Based*, Sections 3.1–3.2] + [GentrySahaiWaters2013] + +The family here supplies explicit compatible inequalities for the power-of-two specialization; +it is not a claim about the paper's hardness parameters. +-/ + +@[expose] public section + +namespace Cslib.Crypto.Homomorphic.GSW.Parameters + +open Turing.MultiTapeTM Turing.MultiTapeTM.ComputableTidilyInPolyTime +open scoped NNReal + +/-- Number of secret coordinates. -/ +def dimension (security : ℕ) : ℕ := security + 1 + +/-- Positive centered-binomial width. -/ +def noise (security : ℕ) : ℕ := security + 1 + +/-- Number of binary digits in one modular coordinate. -/ +def width (security : ℕ) : ℕ := 16 + 8 * Nat.clog 2 (security + 1) + +/-- Number of ciphertext rows. -/ +def rows (security : ℕ) : ℕ := (dimension security + 1) * width security + +/-- Number of public samples and source bits in each encryption row. -/ +def samples (security : ℕ) : ℕ := rows security + 2 * security + +/-- Power-of-two modulus. -/ +def modulus (security : ℕ) : ℕ := 2 ^ width security + +/-- The noise is positive even at security parameter zero. -/ +theorem noise_pos (security : ℕ) : 0 < noise security := by simp [noise] + +/-- Every parameter uses a nonempty modular bit representation. -/ +theorem width_pos (security : ℕ) : 0 < width security := by unfold width; omega + +/-- Each encryption row has the surplus required by the shared-public-matrix bound. -/ +theorem entropy_margin (security : ℕ) : rows security + 2 * security ≤ samples security := le_rfl + +private theorem clog_le (security : ℕ) : Nat.clog 2 (security + 1) ≤ security := + Nat.clog_le_of_le_pow (Nat.lt_two_pow_self (n := security)) + +/-- The digit width has a simple linear majorant. -/ +theorem width_le (security : ℕ) : width security ≤ 16 * (security + 1) := by + have := clog_le security + unfold width + omega + +/-- The ciphertext dimension has a uniform quadratic majorant. -/ +theorem rows_le (security : ℕ) : rows security ≤ 32 * (security + 1) ^ 2 := by + calc + rows security ≤ (security + 2) * (16 * (security + 1)) := by + exact Nat.mul_le_mul_left _ (width_le security) + _ ≤ 32 * (security + 1) ^ 2 := by nlinarith + +/-- The number of public samples has a uniform quadratic majorant. -/ +theorem samples_le (security : ℕ) : samples security ≤ 34 * (security + 1) ^ 2 := by + have := rows_le security + unfold samples + nlinarith + +/-- The modulus dominates the eighth power of the positive parameter. -/ +theorem modulus_ge (security : ℕ) : 65536 * (security + 1) ^ 8 ≤ modulus security := by + have h := Nat.pow_le_pow_left (Nat.le_pow_clog (by decide : 1 < 2) (security + 1)) 8 + calc + _ ≤ 65536 * (2 ^ Nat.clog 2 (security + 1)) ^ 8 := Nat.mul_le_mul_left _ h + _ = modulus security := by simp [modulus, width, pow_add, pow_mul, Nat.mul_comm] + +/-- The modulus also has an explicit polynomial upper bound. -/ +theorem modulus_le (security : ℕ) : modulus security ≤ 16777216 * (security + 1) ^ 8 := by + have h := Nat.pow_le_pow_left + (Nat.pow_clog_le_mul (by decide : 1 < 2) (by omega : security + 1 ≠ 0)) 8 + calc + modulus security = 65536 * (2 ^ Nat.clog 2 (security + 1)) ^ 8 := by + simp [modulus, width, pow_add, pow_mul, Nat.mul_comm] + _ ≤ 65536 * (2 * (security + 1)) ^ 8 := Nat.mul_le_mul_left _ h + _ = _ := by ring + +/-- NAND of two fresh ciphertexts lies strictly inside the decoder's noise margin. -/ +theorem nand_margin (security : ℕ) : + 4 * (1 + rows security) * samples security * noise security < modulus security := by + have hk : 1 ≤ (security + 1) ^ 2 := by + have : 0 < (security + 1) ^ 2 := by positivity + omega + have hrows : 1 + rows security ≤ 33 * (security + 1) ^ 2 := by + have := rows_le security + omega + have hbound : 4 * (1 + rows security) * samples security * noise security ≤ + 4488 * (security + 1) ^ 5 := by + calc + _ ≤ 4 * (33 * (security + 1) ^ 2) * (34 * (security + 1) ^ 2) * (security + 1) := + Nat.mul_le_mul_right _ (Nat.mul_le_mul (Nat.mul_le_mul_left _ hrows) (samples_le security)) + _ = _ := by ring + have hpow : (security + 1) ^ 5 ≤ (security + 1) ^ 8 := Nat.pow_le_pow_right (by omega) (by decide) + have hpos : 0 < (security + 1) ^ 5 := by positivity + exact hbound.trans_lt ((by nlinarith : 4488 * (security + 1) ^ 5 < + 65536 * (security + 1) ^ 8).trans_le (modulus_ge security)) + +/-- Fresh encryption lies strictly inside the decoder's noise margin. -/ +theorem fresh_margin (security : ℕ) : 4 * samples security * noise security < modulus security := by + exact (Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ + (by omega : 4 ≤ 4 * (1 + rows security)))).trans_lt (nand_margin security) + +/-- The secret dimension is uniformly computable on unary parameters. -/ +@[fun_prop] +theorem computableTidilyInPolyTime_dimension : + ComputableTidilyInPolyTime dimension encUnary encUnary := by + unfold dimension + fun_prop + +/-- The positive noise width is uniformly computable on unary parameters. -/ +@[fun_prop] +theorem computableTidilyInPolyTime_noise : + ComputableTidilyInPolyTime noise encUnary encUnary := by + unfold noise + fun_prop + +/-- The logarithmic digit width is uniformly computable on unary parameters. -/ +@[fun_prop] +theorem computableTidilyInPolyTime_width : + ComputableTidilyInPolyTime width encUnary encUnary := by + have := unary_clog_const 2 + unfold width + fun_prop + +/-- The ciphertext dimension is uniformly computable on unary parameters. -/ +@[fun_prop] +theorem computableTidilyInPolyTime_rows : + ComputableTidilyInPolyTime rows encUnary encUnary := by + unfold rows + fun_prop + +/-- The public sample count is uniformly computable on unary parameters. -/ +@[fun_prop] +theorem computableTidilyInPolyTime_samples : + ComputableTidilyInPolyTime samples encUnary encUnary := by + unfold samples + fun_prop + +/-- Even the modulus itself has a uniform unary native certificate. This uses bounded powers +of a ceiling logarithm, rather than treating arbitrary unary exponentiation as efficient. -/ +@[fun_prop] +theorem computableTidilyInPolyTime_modulus : + ComputableTidilyInPolyTime modulus encUnary encUnary := by + have := unary_pow_clog_const (input := encUnary) (size := fun security => security + 1) + (by fun_prop) 256 2 + have hmodulus : modulus = fun security => 65536 * 256 ^ Nat.clog 2 (security + 1) := by + funext security + norm_num [modulus, width, pow_add, pow_mul] + rw [hmodulus] + fun_prop + +/-- Every numerical parameter, including the modulus, is polynomially bounded. -/ +theorem polynomiallyBounded_parameters : + PolynomiallyBounded dimension ∧ PolynomiallyBounded noise ∧ PolynomiallyBounded width ∧ + PolynomiallyBounded rows ∧ PolynomiallyBounded samples ∧ PolynomiallyBounded modulus := + ⟨computableTidilyInPolyTime_dimension.polynomiallyBounded, + computableTidilyInPolyTime_noise.polynomiallyBounded, + computableTidilyInPolyTime_width.polynomiallyBounded, + computableTidilyInPolyTime_rows.polynomiallyBounded, + computableTidilyInPolyTime_samples.polynomiallyBounded, + computableTidilyInPolyTime_modulus.polynomiallyBounded⟩ + +/-- The exact shared-public-matrix error bound is negligible for this positive-noise family. -/ +theorem negligible_statistical_error : + Negligible (fun security => (rows security : ℝ≥0) * + NNReal.sqrt ((2 : ℝ≥0) ^ rows security / 2 ^ samples security)) := + negligible_mul_sqrt_pow_two_div_pow_two computableTidilyInPolyTime_rows.polynomiallyBounded + (Filter.Eventually.of_forall entropy_margin) + +end Cslib.Crypto.Homomorphic.GSW.Parameters diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/Security.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/Security.lean new file mode 100644 index 0000000000..2cd367f0af --- /dev/null +++ b/Complexity/Crypto/Computational/Homomorphic/GSW/Security.lean @@ -0,0 +1,169 @@ +/- +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.Encryption.PublicKeyReplacement +public import Complexity.Crypto.Computational.Homomorphic.GSW.Hiding +public import Complexity.Crypto.Computational.Homomorphic.GSW.LWE +public import Complexity.Crypto.Computational.Homomorphic.GSW.Parameters +public import Complexity.Crypto.Computational.Homomorphic.GSW.Serialized.PolyTime + +/-! +# Generated-key GSW security from the exact decision-LWE assumption + +The actual serialized key generator and encryption program satisfy chosen-message security +under decision LWE for their precise centered-binomial error law. A single uniform adversary +reduction has loss two; the remaining statistical error comes from the shared uniform public +matrix. Every runtime premise concerns the actual serialized program on its complete input. + +## Main definitions + +* `hidingError`: the explicit statistical term in the chosen-message advantage bound. +* `lweDistinguisher`: the uniform hidden-bit reduction using actual serialized encryption. + +## Main results + +* `advantage_game_le`: twice the decision-LWE advantage plus the explicit statistical term. +* `indCPA_of_decisionLWE`: negligible chosen-message advantage under an eventual entropy margin. +* `Parameters.indCPA`: the concrete positive-noise family instantiates all runtime and entropy + requirements, leaving only its specified decision-LWE assumption. + +This is ordinary single-challenge public-key security against uniform classical strict PPT +adversaries. It does not provide circular security, a quantum worst-case lattice reduction, +or a bootstrappability theorem. + +## References + +* [C. Gentry, A. Sahai and B. Waters, *Homomorphic Encryption from Learning with Errors: + Conceptually-Simpler, Asymptotically-Faster, Attribute-Based*][GentrySahaiWaters2013], + Sections 3.1–3.2. +-/ + +@[expose] public section + +namespace Cslib.Crypto.Homomorphic.GSW + +open Probability Turing.MultiTapeTM +open scoped NNReal + +/-- The shared-public-matrix statistical term, with `N = (n + 1) * w` ciphertext rows. -/ +noncomputable def hidingError (n m w : ℕ) : ℝ≥0 := + ((n + 1) * w : ℕ) * NNReal.sqrt ((2 : ℝ≥0) ^ ((n + 1) * w) / 2 ^ m) + +/-- The reduction uses the actual serialized encryption algorithm, including total decoding of +arbitrary challenge words. Its hidden fair bit is not supplied to either adversary stage. -/ +noncomputable def lweDistinguisher (n m w : ℕ → ℕ) + (adversary : Encryption.Adversary) : Distinguisher := + Encryption.keyDistinguisher + (fun security => encryptSerialized (n security) (m security) (w security)) adversary + +/-- Efficient parameter functions instantiate the actual reduction's uniform native certificate. -/ +theorem isPPT_lweDistinguisher {n m w : ℕ → ℕ} {adversary : Encryption.Adversary} + (hn : ComputableTidilyInPolyTime n encUnary encUnary) + (hm : ComputableTidilyInPolyTime m encUnary encUnary) + (hw : ComputableTidilyInPolyTime w encUnary encUnary) + (hadversary : adversary.IsPPT) : IsPPT encBool (lweDistinguisher n m w adversary) := by + apply Encryption.isPPT_keyDistinguisher ?_ hadversary + exact isPPTOn_encryptSerialized (hn.comp (by fun_prop)) (hm.comp (by fun_prop)) + (hw.comp (by fun_prop)) (by fun_prop) (by fun_prop) + +/-- In the uniform-matrix experiment, serialized message selection, encryption and guessing +agree with the typed adaptive hiding game, including the full saved word. -/ +theorem publicKeyGame_uniformEnsemble (n m w : ℕ → ℕ) + (adversary : Encryption.Adversary) (bit : Bool) (security : ℕ) : + Encryption.publicKeyGame (LWE.uniformEnsemble n m w security) + (fun k => encryptSerialized (n k) (m k) (w k)) adversary bit security = + uniformPublicGame (n := n security) (m := m security) (w := w security) + (fun A => ProbComp.eval (adversary.choose security (serializePublicMatrix A))) + (fun state ciphertext => + ProbComp.eval (adversary.guess security state (serializeCiphertext ciphertext))) + bit := by + simp only [Encryption.publicKeyGame, LWE.uniformEnsemble, uniformPublicGame, + PMF.monad_bind_eq_bind, PMF.bind_map, Function.comp_def, eval_encryptSerialized, + Matrix.ofBinary_toBinary, encrypt, ProbComp.eval_bind, ProbComp.eval_pure, + eval_sampleCoins, PMF.bind_bind, PMF.pure_bind, serializePublicMatrix] + +/-- The uniform public-key word gives the typed hiding theorem's full adaptive bound. -/ +theorem advantage_uniformEnsemble_le (n m w : ℕ → ℕ) + (adversary : Encryption.Adversary) (security : ℕ) : + Game.advantage + (Encryption.publicKeyGame (LWE.uniformEnsemble n m w security) + (fun k => encryptSerialized (n k) (m k) (w k)) adversary false security) + (Encryption.publicKeyGame (LWE.uniformEnsemble n m w security) + (fun k => encryptSerialized (n k) (m k) (w k)) adversary true security) ≤ + hidingError (n security) (m security) (w security) := by + apply NNReal.coe_le_coe.mp + rw [Game.coe_advantage, publicKeyGame_uniformEnsemble, publicKeyGame_uniformEnsemble] + simpa only [Game.succProbability, ENNReal.coe_toNNReal_eq_toReal, hidingError, + NNReal.coe_mul, NNReal.coe_natCast, Real.coe_sqrt, NNReal.coe_div, NNReal.coe_pow, + NNReal.coe_ofNat, Nat.mul_comm] using + uniformPublicGame_advantage_le (n := n security) (m := m security) (w := w security) + (fun A => ProbComp.eval (adversary.choose security (serializePublicMatrix A))) + (fun state ciphertext => + ProbComp.eval (adversary.guess security state (serializeCiphertext ciphertext))) + +/-- One uniform reduction bounds actual chosen-message advantage by twice its exact decision-LWE +advantage plus the shared-public-matrix statistical error. No efficiency is needed for this law. -/ +theorem advantage_game_le (n m w η : ℕ → ℕ) + (adversary : Encryption.Adversary) (security : ℕ) : + Game.advantage + (ProbComp.eval (Encryption.game + (fun k => keyGenSerialized (n k) (m k) (w k) (η k)) + (fun k => encryptSerialized (n k) (m k) (w k)) adversary false security)) + (ProbComp.eval (Encryption.game + (fun k => keyGenSerialized (n k) (m k) (w k) (η k)) + (fun k => encryptSerialized (n k) (m k) (w k)) adversary true security)) ≤ + 2 * Game.advantage + (distinguishingGame (LWE.realEnsemble n m w (fun k => noiseLaw (w k) (η k)) security) + (lweDistinguisher n m w adversary security)) + (distinguishingGame (LWE.uniformEnsemble n m w security) + (lweDistinguisher n m w adversary security)) + + hidingError (n security) (m security) (w security) := by + simp only [Encryption.eval_game_eq_publicKeyGame, eval_keyGenSerialized_publicWord] + exact (Encryption.advantage_publicKeyGame_le _ (LWE.uniformEnsemble n m w security) + _ adversary security).trans + (add_le_add le_rfl (advantage_uniformEnsemble_le n m w adversary security)) + +open Filter in +/-- The actual encryption scheme is IND-CPA secure under its exact decision-LWE assumption, +provided efficient dimensions have an eventual entropy surplus of twice the security parameter. -/ +theorem indCPA_of_decisionLWE {n m w η : ℕ → ℕ} + (hn : ComputableTidilyInPolyTime n encUnary encUnary) + (hm : ComputableTidilyInPolyTime m encUnary encUnary) + (hw : ComputableTidilyInPolyTime w encUnary encUnary) + (hmargin : ∀ᶠ security in atTop, (n security + 1) * w security + 2 * security ≤ m security) + (hLWE : DecisionLWE n m w (fun k => noiseLaw (w k) (η k))) : + Encryption.INDCPA (fun k => keyGenSerialized (n k) (m k) (w k) (η k)) + (fun k => encryptSerialized (n k) (m k) (w k)) := by + intro adversary hadversary + have hsource := hLWE (lweDistinguisher n m w adversary) + (isPPT_lweDistinguisher hn hm hw hadversary) + have hrows : PolynomiallyBounded (fun k => (n k + 1) * w k) := by + have := hn.polynomiallyBounded + have := hw.polynomiallyBounded + fun_prop + have herror := negligible_mul_sqrt_pow_two_div_pow_two hrows hmargin + apply negligible_of_le + ((hsource.polynomiallyBounded_mul (p := fun _ => 2) (by fun_prop)).add herror) + exact advantage_game_le n m w η adversary + +/-- The positive-noise parameter family supplies every dimension/runtime/entropy premise. +Only decision LWE for its precise centered-binomial law remains a security assumption. -/ +theorem Parameters.indCPA + (hLWE : DecisionLWE Parameters.dimension Parameters.samples Parameters.width + (fun k => noiseLaw (Parameters.width k) (Parameters.noise k))) : + Encryption.INDCPA + (fun k => keyGenSerialized (Parameters.dimension k) (Parameters.samples k) + (Parameters.width k) (Parameters.noise k)) + (fun k => encryptSerialized (Parameters.dimension k) (Parameters.samples k) + (Parameters.width k)) := + indCPA_of_decisionLWE Parameters.computableTidilyInPolyTime_dimension + Parameters.computableTidilyInPolyTime_samples Parameters.computableTidilyInPolyTime_width + (Filter.Eventually.of_forall Parameters.entropy_margin) hLWE + +end Cslib.Crypto.Homomorphic.GSW diff --git a/Complexity/Crypto/Computational/LWE/Basic.lean b/Complexity/Crypto/Computational/LWE/Basic.lean new file mode 100644 index 0000000000..78e543d641 --- /dev/null +++ b/Complexity/Crypto/Computational/LWE/Basic.lean @@ -0,0 +1,100 @@ +/- +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.Basic +public import Complexity.Foundations.Data.Matrix.Binary +public import Complexity.Probability.Product +public import Mathlib.Data.Matrix.Mul +public import Mathlib.LinearAlgebra.Matrix.Notation + +/-! +# Decision LWE with power-of-two moduli + +The real experiment draws a uniform secret `t`, a uniform matrix `B`, and independent errors +with a specified residue distribution. Its public sample is the row-major binary encoding of +`[B * t + e | B]`. The comparison experiment draws an entirely uniform matrix of the same shape. +Only the public matrix is exposed; the secret and the sampled errors are not part of the word +given to a distinguisher. + +`DecisionLWE` is an explicit computational hardness hypothesis for these two ensembles, against +uniform classical strict polynomial-time programs. It makes no assertion of hardness for any +particular parameter or error family. In particular, using a bounded noise distribution does +not identify it with a discrete Gaussian or establish a worst-case lattice reduction. + +## Main definitions + +* `Cslib.Crypto.LWE.publicMatrixLaw`: independent decision-LWE samples with a shared uniform secret. +* `Cslib.Crypto.LWE.realEnsemble`, `Cslib.Crypto.LWE.uniformEnsemble`: the binary experiments. +* `Cslib.Crypto.DecisionLWE`: indistinguishability of those experiments for the specified families. + +## Main results + +* `Cslib.Crypto.LWE.length_of_mem_support_realEnsemble`: every real sample has the declared length. +* `Cslib.Crypto.LWE.length_of_mem_support_uniformEnsemble`: the comparison uses the same length. + +## References + +* [C. Gentry, A. Sahai and B. Waters, *Homomorphic Encryption from Learning with Errors: + Conceptually-Simpler, Asymptotically-Faster, Attribute-Based*, Section 2][GentrySahaiWaters2013] +-/ + +@[expose] public section + +namespace Cslib.Crypto + +open Probability +open scoped _root_.Matrix + +namespace LWE + +/-- Draw the public matrix `[B * t + e | B]`. The errors are independent of one another, of +the uniform matrix, and of the uniform secret shared by all rows. -/ +noncomputable def publicMatrixLaw (n m w : ℕ) (noise : PMF (ZMod (2 ^ w))) : + PMF (Matrix (Fin m) (Fin (n + 1)) (ZMod (2 ^ w))) := do + let secret ← PMF.uniformOfFintype (Fin n → ZMod (2 ^ w)) + let publicPart ← PMF.uniformOfFintype (Matrix (Fin m) (Fin n) (ZMod (2 ^ w))) + let error ← PMF.pi (fun _ : Fin m => noise) + return fun i => Fin.cons ((publicPart *ᵥ secret) i + error i) (publicPart i) + +/-- Binary decision-LWE samples, using `w` bits per residue and a uniform secret. -/ +noncomputable def realEnsemble (n m w : ℕ → ℕ) + (noise : (security : ℕ) → PMF (ZMod (2 ^ w security))) (security : ℕ) : PMF (List Bool) := + (publicMatrixLaw (n security) (m security) (w security) (noise security)).map Matrix.toBinary + +/-- Encode a uniform matrix with exactly the real experiment's dimensions and modulus. -/ +noncomputable def uniformEnsemble (n m w : ℕ → ℕ) (security : ℕ) : PMF (List Bool) := + (PMF.uniformOfFintype + (Matrix (Fin (m security)) (Fin (n security + 1)) (ZMod (2 ^ w security)))).map Matrix.toBinary + +/-- The real public word contains exactly one fixed-width residue for each matrix entry. -/ +theorem length_of_mem_support_realEnsemble {n m w : ℕ → ℕ} + {noise : (security : ℕ) → PMF (ZMod (2 ^ w security))} {security : ℕ} {word : List Bool} + (h : word ∈ (realEnsemble n m w noise security).support) : + word.length = m security * (n security + 1) * w security := by + obtain ⟨A, _, rfl⟩ := (PMF.mem_support_map_iff _ _ _).mp h + exact Matrix.length_toBinary A + +/-- Uniform public words have the same complete serialized length as real public words. -/ +theorem length_of_mem_support_uniformEnsemble {n m w : ℕ → ℕ} {security : ℕ} {word : List Bool} + (h : word ∈ (uniformEnsemble n m w security).support) : + word.length = m security * (n security + 1) * w security := by + obtain ⟨A, _, rfl⟩ := (PMF.mem_support_map_iff _ _ _).mp h + exact Matrix.length_toBinary A + +end LWE + +/-- Decision-LWE hardness for the exact dimension, sample count, binary modulus width and error +families. The adversary receives the unary security parameter and only the encoded public matrix. +This is a hypothesis against uniform classical strict PPT distinguishers, not a theorem of +hardness or a claim about quantum adversaries. -/ +def DecisionLWE (n m w : ℕ → ℕ) + (noise : (security : ℕ) → PMF (ZMod (2 ^ w security))) : Prop := + ComputationallyIndistinguishable (LWE.realEnsemble n m w noise) (LWE.uniformEnsemble n m w) + +end Cslib.Crypto diff --git a/Complexity/Crypto/Negligible/Dyadic.lean b/Complexity/Crypto/Negligible/Dyadic.lean new file mode 100644 index 0000000000..a601b5207c --- /dev/null +++ b/Complexity/Crypto/Negligible/Dyadic.lean @@ -0,0 +1,60 @@ +/- +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.Negligible.Basic + +/-! +# Negligibility of dyadic square-root bounds + +An entropy surplus of twice the security parameter gives geometric decay after taking a square +root. Polynomially many output rows preserve negligibility. The output and source bit counts need +not themselves be polynomially bounded or computable. + +## Main results + +* `sqrt_pow_two_div_pow_two_le`: the pointwise geometric estimate. +* `negligible_mul_sqrt_pow_two_div_pow_two`: polynomial losses preserve the estimate, including + when the entropy margin holds only eventually. +-/ + +@[expose] public section + +namespace Cslib.Crypto + +open scoped NNReal + +/-- Twice the security parameter in surplus bits bounds the square-root ratio by `2⁻ⁿ`. -/ +theorem sqrt_pow_two_div_pow_two_le {outputBits sourceBits n : ℕ} + (hmargin : outputBits + 2 * n ≤ sourceBits) : + NNReal.sqrt ((2 : ℝ≥0) ^ outputBits / 2 ^ sourceBits) ≤ (1 / 2 : ℝ≥0) ^ n := by + rw [NNReal.sqrt_le_iff_le_sq] + calc + _ ≤ (2 : ℝ≥0) ^ outputBits / 2 ^ (outputBits + 2 * n) := + div_le_div_of_nonneg_left (by positivity) (by positivity) + (pow_le_pow_right₀ (by norm_num) hmargin) + _ = _ := by + rw [pow_add, mul_comm 2 n, pow_mul] + simp only [one_div, inv_pow] + field_simp + +open Filter in +/-- A polynomial number of square-root dyadic errors is negligible under an eventual entropy +surplus of twice the security parameter. -/ +theorem negligible_mul_sqrt_pow_two_div_pow_two + {count outputBits sourceBits : ℕ → ℕ} (hcount : PolynomiallyBounded count) + (hmargin : ∀ᶠ n in atTop, outputBits n + 2 * n ≤ sourceBits n) : + Negligible (fun n => (count n : ℝ≥0) * + NNReal.sqrt ((2 : ℝ≥0) ^ outputBits n / 2 ^ sourceBits n)) := by + apply negligible_of_eventually_le + ((negligible_geometric (ratio := (1 / 2 : ℝ≥0)) (by norm_num)).polynomiallyBounded_mul + hcount) + filter_upwards [hmargin] with n hn + exact mul_le_mul' le_rfl (sqrt_pow_two_div_pow_two_le hn) + +end Cslib.Crypto diff --git a/Complexity/Languages/Probabilistic/Vector.lean b/Complexity/Languages/Probabilistic/Vector.lean index 4ac2dab119..6ee99fa159 100644 --- a/Complexity/Languages/Probabilistic/Vector.lean +++ b/Complexity/Languages/Probabilistic/Vector.lean @@ -96,6 +96,16 @@ theorem eval_replicateFin_map {β : Type} {source : ProbComp α} {encoded : Prob rw [eval_replicate_map h, ← OracleComp.map_ofFn_replicateFin, eval_map, PMF.map_comp] simp only [Function.comp_def, List.map_ofFn] +/-- Mapping each coordinate after independent runs agrees with mapping each run's outcome. +Neither outcome type needs to be finite. -/ +theorem eval_replicateFin_map_coords {β : Type} (count : ℕ) (program : ProbComp α) + (f : α → β) : + eval (OracleComp.replicateFin count (f <$> program)) = + (eval (OracleComp.replicateFin count program)).map (fun values i => f (values i)) := by + apply PMF.map_injective List.ofFn_injective + rw [← eval_map, OracleComp.map_ofFn_replicateFin, PMF.map_comp] + exact eval_replicateFin_map (eval_map f program) count + /-- Disjoint blocks of one uniform tape realize a vector of independently sampled values. The output type may be infinite, and either the count or the block width may be zero. -/ theorem eval_replicateFin_of_uniformList (count width : ℕ) (program : ProbComp α) diff --git a/ComplexityTests.lean b/ComplexityTests.lean index f834417ece..f8d5291ecc 100644 --- a/ComplexityTests.lean +++ b/ComplexityTests.lean @@ -14,6 +14,8 @@ import ComplexityTests.Abstracts.FaginAbstract import ComplexityTests.Abstracts.FaginBridge import ComplexityTests.Abstracts.FormulaBoundsAbstract import ComplexityTests.Abstracts.FormulaBoundsBridge +import ComplexityTests.Abstracts.GSWSecurityAbstract +import ComplexityTests.Abstracts.GSWSecurityBridge import ComplexityTests.Abstracts.PCPAbstract import ComplexityTests.Abstracts.PCPBridge import ComplexityTests.Abstracts.ResolutionAbstract @@ -116,7 +118,9 @@ import ComplexityTests.Crypto.GMWPointwise import ComplexityTests.Crypto.GSW import ComplexityTests.Crypto.GSWHiding import ComplexityTests.Crypto.GSWNative +import ComplexityTests.Crypto.GSWParameters import ComplexityTests.Crypto.GSWSampling +import ComplexityTests.Crypto.GSWSecurity import ComplexityTests.Crypto.HomomorphicEvaluation import ComplexityTests.Crypto.HomomorphicExample import ComplexityTests.Crypto.HomomorphicFixedKey diff --git a/ComplexityTests/Abstracts/GSWSecurityAbstract.lean b/ComplexityTests/Abstracts/GSWSecurityAbstract.lean new file mode 100644 index 0000000000..f3368952a7 --- /dev/null +++ b/ComplexityTests/Abstracts/GSWSecurityAbstract.lean @@ -0,0 +1,263 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +-- upstream: local-only (formal abstract tests) + +import ComplexityTests.Abstracts.Check +import ComplexityTests.Abstracts.GSWSecurityBridge + +/-! # Generated-key GSW security from decision LWE + +The explicit positive-noise GSW algorithms below are uniform strict polynomial time and satisfy +single-challenge IND-CPA under decision LWE for their exact centered-binomial error family. +The assumption concerns public matrices; the conclusion concerns adaptive message selection and +ciphertexts. The reduction uses one uniform distinguisher with loss two and a negligible +shared-public-matrix statistical error. + +The definitions and theorem statements are self-contained over upstream mathematics and plain +machines. Lean checks their connection to the implementation through `GSWSecurityBridge`; +`#check_abstract` permits no internal implementation dependencies in these public statements. +This is classical public-key security, not circular security, a worst-case lattice reduction, +or an FHE or bootstrappability theorem. Decryption and homomorphic correctness are separate results. + +## References + +* [C. Gentry, A. Sahai and B. Waters, *Homomorphic Encryption from Learning with Errors: + Conceptually-Simpler, Asymptotically-Faster, Attribute-Based*][GentrySahaiWaters2013], + Sections 2.1, 3.1–3.2. +* [D. Boneh, V. Shoup, *A Graduate Course in Applied Cryptography*][BonehShoup2023], Section 11.2. +* [NIST, *Module-Lattice-Based Key-Encapsulation Mechanism Standard*][NISTFIPS203], Algorithm 8, + for the count-difference noise construction, without identifying this scheme with ML-KEM. +-/ + +namespace ComplexityTests.Abstracts.GSWSecurityAbstract + +/-- Self-delimiting framing: double each bit `b` to `[true,b]` and terminate with `[false]`. -/ +def frame (w : List Bool) : List Bool := w.flatMap (fun b => [true, b]) ++ [false] + +/-- Encode a pair by framing its first component and appending its second. -/ +def encodePair {α β : Type} (a : α ↪ List Bool) (b : β ↪ List Bool) (p : α × β) : + List Bool := frame (a p.1) ++ b p.2 + +theorem encodePair_injective {α β : Type} (a : α ↪ List Bool) (b : β ↪ List Bool) : + Function.Injective (encodePair a b) := GSWSecurityBridge.encodePair_injective a b + +/-- The injective pair encoding. The arrow `↪` means an injective function. -/ +def pairEncoding {α β : Type} (a : α ↪ List Bool) (b : β ↪ List Bool) : α × β ↪ List Bool := + ⟨encodePair a b, encodePair_injective a b⟩ + +/-- Bitstrings encode as themselves. -/ +def bitsEncoding : List Bool ↪ List Bool := Function.Embedding.refl _ + +/-- The security parameter is supplied in unary: `n` consecutive true bits. -/ +def unaryEncoding : ℕ ↪ List Bool := ⟨fun n => List.replicate n true, + fun _ _ h => by simpa only [List.length_replicate] using congrArg List.length h⟩ + +/-- A Boolean output encodes as one bit. -/ +def boolEncoding : Bool ↪ List Bool := ⟨fun b => [b], fun _ _ h => by injection h⟩ + +/-- One deterministic finite-state binary multitape Turing machine halts with the encoded +answer on every encoded input, within polynomially bounded time and space in its bit length. +`ComputableInTimeAndSpaceOfLength` is the upstream machine contract; both bounds are uniform. -/ +def PolyTime {α β : Type} (f : α → β) (a : α ↪ List Bool) (b : β ↪ List Bool) : Prop := + ∃ t s : ℕ → ℕ, Cslib.PolynomiallyBounded t ∧ Cslib.PolynomiallyBounded s ∧ + Turing.MultiTapeTM.ComputableInTimeAndSpaceOfLength f a b t s + +/-- Exactly `n` independent fair bits, as a word of length `n`. -/ +noncomputable def uniformBits (n : ℕ) : PMF (List Bool) := + (Cslib.Probability.PMF.uniformOfFintype (Fin n → Bool)).map List.ofFn + +/-- A uniformly strict polynomial-time probability law: one deterministic evaluator, supplied +with polynomially many independent fair bits, realizes every input's law exactly. Its time +includes reading the coin tape and writing the encoded output. Both evaluator and polynomial +are fixed before the input. This also bounds every execution, rather than its expectation. -/ +def StrictPPT {α β : Type} (a : α ↪ List Bool) (b : β ↪ List Bool) + (law : α → PMF β) : Prop := + ∃ (c d : ℕ) (evaluate : α → List Bool → β), + PolyTime (fun p : α × List Bool => evaluate p.1 p.2) (pairEncoding a bitsEncoding) b ∧ + ∀ x, law x = (uniformBits (c * ((a x).length + 1) ^ d)).map (evaluate x) + +/-- A nonnegative error is negligible if multiplication by every fixed power of the security +parameter still tends to zero. The threshold and decay bound may depend on the whole adversary. -/ +def Negligible (ε : ℕ → NNReal) : Prop := + ∀ k : ℕ, Filter.Tendsto (fun n : ℕ => (n : NNReal) ^ k * ε n) + Filter.atTop (nhds 0) + +/-- Probability that a Boolean experiment returns true. -/ +noncomputable def probability (p : PMF Bool) : NNReal := (p true).toNNReal + +/-- Every uniform strict PPT test has negligible distinguishing advantage. +The test receives the unary security parameter and a sample. `bind` samples the word and then runs +the test with independent coins; `nndist` is the absolute difference of success probabilities. -/ +def Indistinguishable (X Y : ℕ → PMF (List Bool)) : Prop := + ∀ test : ℕ → List Bool → PMF Bool, + StrictPPT (pairEncoding unaryEncoding bitsEncoding) boolEncoding + (fun p => test p.1 p.2) → + Negligible (fun n => nndist (probability ((X n).bind (test n))) + (probability ((Y n).bind (test n)))) + +/-- The secret dimension and centered-binomial width are positive at every parameter. -/ +def dimension (security : ℕ) : ℕ := security + 1 + +/-- Each residue uses `16 + 8 * ceil(log₂(security+1))` binary digits; the modulus is +`2 ^ digitWidth security`. The ceiling logarithm is `Nat.clog`. -/ +def digitWidth (security : ℕ) : ℕ := 16 + 8 * Nat.clog 2 (security + 1) + +/-- The public matrix has this many rows, giving `2 * security` surplus entropy bits. -/ +def sampleCount (security : ℕ) : ℕ := (dimension security + 1) * digitWidth security + 2 * security + +/-- Collect independent draws in their original order; the empty list requires no draw. -/ +noncomputable def independentList {α : Type} (count : ℕ) (law : PMF α) : PMF (List α) := + (List.replicate count ()).mapM (fun _ => law) + +/-- A canonical residue representative chosen uniformly from `0,...,2^w-1`. -/ +noncomputable def residueLaw (w : ℕ) : PMF ℕ := + (Cslib.Probability.PMF.uniformOfFintype (Fin (2 ^ w))).map Fin.val + +/-- The exact signed noise is the difference of the counts in two independent words of length +`noiseWidth`. Its support is `[-noiseWidth,noiseWidth]`; this is not a discrete Gaussian. -/ +noncomputable def errorLaw (noiseWidth : ℕ) : PMF ℤ := do + let positive ← uniformBits noiseWidth + let negative ← uniformBits noiseWidth + return (positive.count true : ℤ) - negative.count true + +/-- Write exactly `w` digits, least significant first, including leading zeros. -/ +def lowBits (w value : ℕ) : List Bool := (List.range w).map value.testBit + +/-- The leading entry of `[B*t+e | B]`, reduced by signed Euclidean remainder. -/ +def rowHead (n w : ℕ) (inputs : List ℕ × (List (List ℕ) × List ℤ)) (i : ℕ) : ℕ := + (((((List.range n).map fun j => + (inputs.2.1.getD i []).getD j 0 * inputs.1.getD j 0).sum : ℕ) + + inputs.2.2.getD i 0 : ℤ) % (2 ^ w : ℤ)).toNat + +/-- Row-major serialization of the public matrix, with its noisy column first. -/ +def publicWord (n m w : ℕ) (inputs : List ℕ × (List (List ℕ) × List ℤ)) : List Bool := + (List.range m).flatMap fun i => + lowBits w (rowHead n w inputs i) ++ + (List.range n).flatMap fun j => lowBits w ((inputs.2.1.getD i []).getD j 0 % 2 ^ w) + +/-- Serialize the secret residues; these bits are not given to the adversary. -/ +def secretWord (n w : ℕ) (secret : List ℕ) : List Bool := + (List.range n).flatMap fun j => lowBits w (secret.getD j 0 % 2 ^ w) + +/-- Generate the actual public/secret pair. The secret, matrix rows, and signed errors are all +sampled independently, with `n = noiseWidth = security+1`. -/ +noncomputable def keyGeneration (security : ℕ) : PMF (List Bool × List Bool) := do + let secret ← independentList (dimension security) (residueLaw (digitWidth security)) + let matrix ← independentList (sampleCount security) + (independentList (dimension security) (residueLaw (digitWidth security))) + let errors ← independentList (sampleCount security) (errorLaw (dimension security)) + return (publicWord (dimension security) (sampleCount security) (digitWidth security) + (secret, (matrix, errors)), secretWord (dimension security) (digitWidth security) secret) + +/-- Read a fixed-width matrix entry. Missing bits are zero, and excess bits are ignored. -/ +def matrixEntry (cols w : ℕ) (word : List Bool) (i j : ℕ) : ℕ := + ((word.drop ((i * cols + j) * w) ++ List.replicate w false).take w).foldr Nat.bit 0 + +/-- An entry of `message*G + R*A`, before binary decomposition. -/ +def ciphertextEntry (n m w : ℕ) (publicKey : List Bool) (message : Bool) + (coins : List (List (List Bool))) (i k j : ℕ) : ℕ := + ((if i = j then message.toNat * 2 ^ k else 0) + + ((List.range m).map fun r => + if ((coins.getD i []).getD k []).getD r false then + matrixEntry (n + 1) w publicKey r j else 0).sum) % 2 ^ w + +/-- Write every bit of the square ciphertext. Its row order is `(i,k)` and column order `(j,l)`; +this is the bit decomposition of `message*G + R*A`, equivalent to the GSW flattening formula. -/ +def ciphertextWord (n m w : ℕ) (publicKey : List Bool) (message : Bool) + (coins : List (List (List Bool))) : List Bool := + (List.range (n + 1)).flatMap fun i => + (List.range w).flatMap fun k => + (List.range (n + 1)).flatMap fun j => + lowBits w (ciphertextEntry n m w publicKey message coins i k j) + +/-- Encrypt using only the public word and independent fair matrix coins. This law is total +on every public word, including malformed lengths. -/ +noncomputable def encryption (security : ℕ) (publicKey : List Bool) (message : Bool) : + PMF (List Bool) := do + let coins ← independentList (dimension security + 1) + (independentList (digitWidth security) (independentList (sampleCount security) + (Cslib.Probability.PMF.uniformOfFintype Bool))) + return ciphertextWord (dimension security) (sampleCount security) (digitWidth security) + publicKey message coins + +/-- The decision-LWE comparison is an entirely uniform matrix of the same shape and modulus, +encoded in the same row-major, least-significant-first order. -/ +noncomputable def uniformPublic (security : ℕ) : PMF (List Bool) := + (Cslib.Probability.PMF.uniformOfFintype + (Fin (sampleCount security) → Fin (dimension security + 1) → + ZMod (2 ^ digitWidth security))).map + (fun A => (List.ofFn fun i => + (List.ofFn fun j => lowBits (digitWidth security) (A i j).val).flatten).flatten) + +/-- **Exact decision-LWE assumption.** The public sample `[B*t+e | B]`, with uniform secret, +uniform matrix and the independent signed noise above, is indistinguishable from the uniform +matrix. Neither the secret nor errors are exposed. This is an assumption against uniform +classical strict PPT tests; no lattice reduction or hardness theorem is asserted. -/ +def DecisionLWE : Prop := + Indistinguishable (fun security => (keyGeneration security).map Prod.fst) uniformPublic + +/-- Generate keys, let the adversary choose two messages after seeing the public key, encrypt +the selected message, and pass its entire saved word unchanged to the guessing stage. -/ +noncomputable def chosenMessageGame + (choose : ℕ → List Bool → PMF ((Bool × Bool) × List Bool)) + (guess : ℕ → List Bool → List Bool → PMF Bool) (bit : Bool) (security : ℕ) : PMF Bool := do + let keys ← keyGeneration security + let choice ← choose security keys.1 + let ciphertext ← encryption security keys.1 (if bit then choice.1.2 else choice.1.1) + guess security choice.2 ciphertext + +/-- Single-challenge IND-CPA: every two-stage uniform strict PPT adversary has negligible +advantage. Both clocks charge the unary parameter and complete inputs; saved state can include +the public key. The adversary is fixed before the parameter, without nonuniform advice. -/ +def ChosenMessageSecure : Prop := + ∀ (choose : ℕ → List Bool → PMF ((Bool × Bool) × List Bool)) + (guess : ℕ → List Bool → List Bool → PMF Bool), + StrictPPT (pairEncoding unaryEncoding bitsEncoding) + (pairEncoding (pairEncoding boolEncoding boolEncoding) bitsEncoding) + (fun p => choose p.1 p.2) → + StrictPPT (pairEncoding unaryEncoding (pairEncoding bitsEncoding bitsEncoding)) boolEncoding + (fun p => guess p.1 p.2.1 p.2.2) → + Negligible (fun security => + nndist (probability (chosenMessageGame choose guess false security)) + (probability (chosenMessageGame choose guess true security))) + +/-- **Native efficiency.** Both actual honest algorithms have one uniform strict polynomial +clock. This includes the complete public/secret output and every ciphertext bit, for arbitrary +public input words; no fixed-dimensional finite encoding supplies efficiency for free. -/ +theorem native_algorithms : + StrictPPT unaryEncoding (pairEncoding bitsEncoding bitsEncoding) keyGeneration ∧ + StrictPPT (pairEncoding unaryEncoding (pairEncoding bitsEncoding boolEncoding)) bitsEncoding + (fun p => encryption p.1 p.2.1 p.2.2) := + GSWSecurityBridge.native_algorithms + +/-- **GSW generated-key IND-CPA from exact decision LWE.** For this explicit positive-noise +family, only the preceding LWE hypothesis is assumed. Security holds for every uniform classical +strict PPT message-selection and guessing pair, retaining arbitrary saved words. -/ +theorem indCPA (hLWE : DecisionLWE) : ChosenMessageSecure := + GSWSecurityBridge.indCPA hLWE + +/-- +info: abstract audit passed for `ComplexityTests.Abstracts.GSWSecurityAbstract`: 40 root +declarations, 164 dependencies checked +-/ +#guard_msgs (whitespace := lax) in +#check_abstract ComplexityTests.Abstracts.GSWSecurityAbstract + +/-- +info: 'ComplexityTests.Abstracts.GSWSecurityAbstract.native_algorithms' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms ComplexityTests.Abstracts.GSWSecurityAbstract.native_algorithms +/-- +info: 'ComplexityTests.Abstracts.GSWSecurityAbstract.indCPA' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms ComplexityTests.Abstracts.GSWSecurityAbstract.indCPA + +end ComplexityTests.Abstracts.GSWSecurityAbstract diff --git a/ComplexityTests/Abstracts/GSWSecurityBridge.lean b/ComplexityTests/Abstracts/GSWSecurityBridge.lean new file mode 100644 index 0000000000..94c7f0cf5b --- /dev/null +++ b/ComplexityTests/Abstracts/GSWSecurityBridge.lean @@ -0,0 +1,321 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +-- upstream: local-only (formal abstract tests) + +import ComplexityTests.Abstracts.CryptographyBridge +import Complexity.Crypto.Computational.Homomorphic.GSW.Security + +/-! # Bridge for generated-key GSW security + +The public abstract uses explicit PMF laws and the plain finite-coin-tape presentation of strict +PPT. This bridge identifies those laws with the complete serialized programs and reuses the +native generated-key security theorem. The bridge introduces no notation or elaboration rules. +-/ + +namespace ComplexityTests.Abstracts.GSWSecurityBridge + +/-- Self-delimiting framing: double each bit `b` to `[true,b]` and terminate with `[false]`. -/ +def frame (w : List Bool) : List Bool := w.flatMap (fun b => [true, b]) ++ [false] + +/-- Encode a pair by framing its first component and appending its second. -/ +def encodePair {α β : Type} (a : α ↪ List Bool) (b : β ↪ List Bool) (p : α × β) : + List Bool := frame (a p.1) ++ b p.2 + +theorem encodePair_injective {α β : Type} (a : α ↪ List Bool) (b : β ↪ List Bool) : + Function.Injective (encodePair a b) := CryptographyBridge.encodePair_injective a b + +/-- The injective pair encoding. The arrow `↪` means an injective function. -/ +def pairEncoding {α β : Type} (a : α ↪ List Bool) (b : β ↪ List Bool) : α × β ↪ List Bool := + ⟨encodePair a b, encodePair_injective a b⟩ + +/-- Bitstrings encode as themselves. -/ +def bitsEncoding : List Bool ↪ List Bool := Function.Embedding.refl _ + +/-- The security parameter is supplied in unary: `n` consecutive true bits. -/ +def unaryEncoding : ℕ ↪ List Bool := ⟨fun n => List.replicate n true, + fun _ _ h => by simpa only [List.length_replicate] using congrArg List.length h⟩ + +/-- A Boolean output encodes as one bit. -/ +def boolEncoding : Bool ↪ List Bool := ⟨fun b => [b], fun _ _ h => by injection h⟩ + +/-- One deterministic finite-state binary multitape Turing machine halts with the encoded +answer on every encoded input, within polynomially bounded time and space in its bit length. +`ComputableInTimeAndSpaceOfLength` is the upstream machine contract; both bounds are uniform. -/ +def PolyTime {α β : Type} (f : α → β) (a : α ↪ List Bool) (b : β ↪ List Bool) : Prop := + ∃ t s : ℕ → ℕ, Cslib.PolynomiallyBounded t ∧ Cslib.PolynomiallyBounded s ∧ + Turing.MultiTapeTM.ComputableInTimeAndSpaceOfLength f a b t s + +/-- Exactly `n` independent fair bits, as a word of length `n`. -/ +noncomputable def uniformBits (n : ℕ) : PMF (List Bool) := + (Cslib.Probability.PMF.uniformOfFintype (Fin n → Bool)).map List.ofFn + +/-- A uniformly strict polynomial-time probability law: one deterministic evaluator, supplied +with polynomially many independent fair bits, realizes every input's law exactly. Its time +includes reading the coin tape and writing the encoded output. Both evaluator and polynomial +are fixed before the input. This also bounds every execution, rather than its expectation. -/ +def StrictPPT {α β : Type} (a : α ↪ List Bool) (b : β ↪ List Bool) + (law : α → PMF β) : Prop := + ∃ (c d : ℕ) (evaluate : α → List Bool → β), + PolyTime (fun p : α × List Bool => evaluate p.1 p.2) (pairEncoding a bitsEncoding) b ∧ + ∀ x, law x = (uniformBits (c * ((a x).length + 1) ^ d)).map (evaluate x) + +/-- A nonnegative error is negligible if multiplication by every fixed power of the security +parameter still tends to zero. The threshold and decay bound may depend on the whole adversary. -/ +def Negligible (ε : ℕ → NNReal) : Prop := + ∀ k : ℕ, Filter.Tendsto (fun n : ℕ => (n : NNReal) ^ k * ε n) + Filter.atTop (nhds 0) + +/-- Probability that a Boolean experiment returns true. -/ +noncomputable def probability (p : PMF Bool) : NNReal := (p true).toNNReal + +/-- Every uniform strict PPT test has negligible distinguishing advantage. +The test receives the unary security parameter and a sample. `bind` samples the word and then runs +the test with independent coins; `nndist` is the absolute difference of success probabilities. -/ +def Indistinguishable (X Y : ℕ → PMF (List Bool)) : Prop := + ∀ test : ℕ → List Bool → PMF Bool, + StrictPPT (pairEncoding unaryEncoding bitsEncoding) boolEncoding + (fun p => test p.1 p.2) → + Negligible (fun n => nndist (probability ((X n).bind (test n))) + (probability ((Y n).bind (test n)))) + +/-- The secret dimension and centered-binomial width are positive at every parameter. -/ +def dimension (security : ℕ) : ℕ := security + 1 + +/-- Each residue uses `16 + 8 * ceil(log₂(security+1))` binary digits; the modulus is +`2 ^ digitWidth security`. The ceiling logarithm is `Nat.clog`. -/ +def digitWidth (security : ℕ) : ℕ := 16 + 8 * Nat.clog 2 (security + 1) + +/-- The public matrix has this many rows, giving `2 * security` surplus entropy bits. -/ +def sampleCount (security : ℕ) : ℕ := (dimension security + 1) * digitWidth security + 2 * security + +/-- Collect independent draws in their original order; the empty list requires no draw. -/ +noncomputable def independentList {α : Type} (count : ℕ) (law : PMF α) : PMF (List α) := + (List.replicate count ()).mapM (fun _ => law) + +/-- A canonical residue representative chosen uniformly from `0,...,2^w-1`. -/ +noncomputable def residueLaw (w : ℕ) : PMF ℕ := + (Cslib.Probability.PMF.uniformOfFintype (Fin (2 ^ w))).map Fin.val + +/-- The exact signed noise is the difference of the counts in two independent words of length +`noiseWidth`. Its support is `[-noiseWidth,noiseWidth]`; this is not a discrete Gaussian. -/ +noncomputable def errorLaw (noiseWidth : ℕ) : PMF ℤ := do + let positive ← uniformBits noiseWidth + let negative ← uniformBits noiseWidth + return (positive.count true : ℤ) - negative.count true + +/-- Write exactly `w` digits, least significant first, including leading zeros. -/ +def lowBits (w value : ℕ) : List Bool := (List.range w).map value.testBit + +/-- The leading entry of `[B*t+e | B]`, reduced by signed Euclidean remainder. -/ +def rowHead (n w : ℕ) (inputs : List ℕ × (List (List ℕ) × List ℤ)) (i : ℕ) : ℕ := + (((((List.range n).map fun j => + (inputs.2.1.getD i []).getD j 0 * inputs.1.getD j 0).sum : ℕ) + + inputs.2.2.getD i 0 : ℤ) % (2 ^ w : ℤ)).toNat + +/-- Row-major serialization of the public matrix, with its noisy column first. -/ +def publicWord (n m w : ℕ) (inputs : List ℕ × (List (List ℕ) × List ℤ)) : List Bool := + (List.range m).flatMap fun i => + lowBits w (rowHead n w inputs i) ++ + (List.range n).flatMap fun j => lowBits w ((inputs.2.1.getD i []).getD j 0 % 2 ^ w) + +/-- Serialize the secret residues; these bits are not given to the adversary. -/ +def secretWord (n w : ℕ) (secret : List ℕ) : List Bool := + (List.range n).flatMap fun j => lowBits w (secret.getD j 0 % 2 ^ w) + +/-- Generate the actual public/secret pair. The secret, matrix rows, and signed errors are all +sampled independently, with `n = noiseWidth = security+1`. -/ +noncomputable def keyGeneration (security : ℕ) : PMF (List Bool × List Bool) := do + let secret ← independentList (dimension security) (residueLaw (digitWidth security)) + let matrix ← independentList (sampleCount security) + (independentList (dimension security) (residueLaw (digitWidth security))) + let errors ← independentList (sampleCount security) (errorLaw (dimension security)) + return (publicWord (dimension security) (sampleCount security) (digitWidth security) + (secret, (matrix, errors)), secretWord (dimension security) (digitWidth security) secret) + +/-- Read a fixed-width matrix entry. Missing bits are zero, and excess bits are ignored. -/ +def matrixEntry (cols w : ℕ) (word : List Bool) (i j : ℕ) : ℕ := + ((word.drop ((i * cols + j) * w) ++ List.replicate w false).take w).foldr Nat.bit 0 + +/-- An entry of `message*G + R*A`, before binary decomposition. -/ +def ciphertextEntry (n m w : ℕ) (publicKey : List Bool) (message : Bool) + (coins : List (List (List Bool))) (i k j : ℕ) : ℕ := + ((if i = j then message.toNat * 2 ^ k else 0) + + ((List.range m).map fun r => + if ((coins.getD i []).getD k []).getD r false then + matrixEntry (n + 1) w publicKey r j else 0).sum) % 2 ^ w + +/-- Write every bit of the square ciphertext. Its row order is `(i,k)` and column order `(j,l)`; +this is the bit decomposition of `message*G + R*A`, equivalent to the GSW flattening formula. -/ +def ciphertextWord (n m w : ℕ) (publicKey : List Bool) (message : Bool) + (coins : List (List (List Bool))) : List Bool := + (List.range (n + 1)).flatMap fun i => + (List.range w).flatMap fun k => + (List.range (n + 1)).flatMap fun j => + lowBits w (ciphertextEntry n m w publicKey message coins i k j) + +/-- Encrypt using only the public word and independent fair matrix coins. This law is total +on every public word, including malformed lengths. -/ +noncomputable def encryption (security : ℕ) (publicKey : List Bool) (message : Bool) : + PMF (List Bool) := do + let coins ← independentList (dimension security + 1) + (independentList (digitWidth security) (independentList (sampleCount security) + (Cslib.Probability.PMF.uniformOfFintype Bool))) + return ciphertextWord (dimension security) (sampleCount security) (digitWidth security) + publicKey message coins + +/-- The decision-LWE comparison is an entirely uniform matrix of the same shape and modulus, +encoded in the same row-major, least-significant-first order. -/ +noncomputable def uniformPublic (security : ℕ) : PMF (List Bool) := + (Cslib.Probability.PMF.uniformOfFintype + (Fin (sampleCount security) → Fin (dimension security + 1) → + ZMod (2 ^ digitWidth security))).map + (fun A => (List.ofFn fun i => + (List.ofFn fun j => lowBits (digitWidth security) (A i j).val).flatten).flatten) + +/-- **Exact decision-LWE assumption.** The public sample `[B*t+e | B]`, with uniform secret, +uniform matrix and the independent signed noise above, is indistinguishable from the uniform +matrix. Neither the secret nor errors are exposed. This is an assumption against uniform +classical strict PPT tests; no lattice reduction or hardness theorem is asserted. -/ +def DecisionLWE : Prop := + Indistinguishable (fun security => (keyGeneration security).map Prod.fst) uniformPublic + +/-- Generate keys, let the adversary choose two messages after seeing the public key, encrypt +the selected message, and pass its entire saved word unchanged to the guessing stage. -/ +noncomputable def chosenMessageGame + (choose : ℕ → List Bool → PMF ((Bool × Bool) × List Bool)) + (guess : ℕ → List Bool → List Bool → PMF Bool) (bit : Bool) (security : ℕ) : PMF Bool := do + let keys ← keyGeneration security + let choice ← choose security keys.1 + let ciphertext ← encryption security keys.1 (if bit then choice.1.2 else choice.1.1) + guess security choice.2 ciphertext + +/-- Single-challenge IND-CPA: every two-stage uniform strict PPT adversary has negligible +advantage. Both clocks charge the unary parameter and complete inputs; saved state can include +the public key. The adversary is fixed before the parameter, without nonuniform advice. -/ +def ChosenMessageSecure : Prop := + ∀ (choose : ℕ → List Bool → PMF ((Bool × Bool) × List Bool)) + (guess : ℕ → List Bool → List Bool → PMF Bool), + StrictPPT (pairEncoding unaryEncoding bitsEncoding) + (pairEncoding (pairEncoding boolEncoding boolEncoding) bitsEncoding) + (fun p => choose p.1 p.2) → + StrictPPT (pairEncoding unaryEncoding (pairEncoding bitsEncoding bitsEncoding)) boolEncoding + (fun p => guess p.1 p.2.1 p.2.2) → + Negligible (fun security => + nndist (probability (chosenMessageGame choose guess false security)) + (probability (chosenMessageGame choose guess true security))) + +open Cslib Cslib.Probability Turing.MultiTapeTM + +private theorem independentList_eval {α : Type} (count : ℕ) (program : ProbComp α) : + independentList count (ProbComp.eval program) = + ProbComp.eval (OracleComp.replicate count program) := by + induction count with + | zero => rfl + | succ count ih => + simp only [independentList] at ih + simp only [independentList, List.replicate_succ, List.mapM_cons, + OracleComp.replicate_succ, ProbComp.eval_bind, + ProbComp.eval_map, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.map, + Function.comp_def, ih] + +private theorem keyGeneration_eq (security : ℕ) : + keyGeneration security = ProbComp.eval + (Crypto.Homomorphic.GSW.keyGenSerialized (dimension security) (sampleCount security) + (digitWidth security) (dimension security)) := by + simp only [keyGeneration, Crypto.Homomorphic.GSW.keyGenSerialized, + Crypto.Homomorphic.GSW.sampleKeyInputsSerialized, ProbComp.eval_bind, ProbComp.eval_pure, + ← independentList_eval, eval_sampleBinaryNat, eval_sampleCenteredBinomial, + PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.bind_bind, PMF.pure_bind] + rfl + +private theorem encryption_eq (security : ℕ) (publicKey : List Bool) (message : Bool) : + encryption security publicKey message = ProbComp.eval + (Crypto.Homomorphic.GSW.encryptSerialized (dimension security) (sampleCount security) + (digitWidth security) publicKey message) := by + simp only [encryption, Crypto.Homomorphic.GSW.encryptSerialized, + Crypto.Homomorphic.GSW.sampleCoinsSerialized, ProbComp.eval_bind, ProbComp.eval_pure, + ← independentList_eval, ProbComp.eval_uniform, PMF.monad_bind_eq_bind, + PMF.monad_pure_eq_pure] + rfl + +private theorem uniformPublic_eq (security : ℕ) : + uniformPublic security = + Crypto.LWE.uniformEnsemble dimension sampleCount digitWidth security := by + unfold uniformPublic Crypto.LWE.uniformEnsemble + congr 1 + funext A + simpa only [← BitString.lowBits_eq_ofFn, BitString.lowBits, lowBits] using + (Matrix.toBinary_eq A).symm + +private theorem decisionLWE_iff : DecisionLWE ↔ + Crypto.DecisionLWE Crypto.Homomorphic.GSW.Parameters.dimension + Crypto.Homomorphic.GSW.Parameters.samples Crypto.Homomorphic.GSW.Parameters.width + (fun security => Crypto.Homomorphic.GSW.noiseLaw + (Crypto.Homomorphic.GSW.Parameters.width security) + (Crypto.Homomorphic.GSW.Parameters.noise security)) := by + change CryptographyBridge.Indistinguishable _ _ ↔ _ + rw [CryptographyBridge.indistinguishable_iff] + change Crypto.ComputationallyIndistinguishable _ _ ↔ + Crypto.ComputationallyIndistinguishable _ _ + have hreal : (fun security => (keyGeneration security).map Prod.fst) = + Crypto.LWE.realEnsemble dimension sampleCount digitWidth + (fun security => Crypto.Homomorphic.GSW.noiseLaw + (digitWidth security) (dimension security)) := by + funext security + rw [keyGeneration_eq, Crypto.Homomorphic.GSW.eval_keyGenSerialized_publicWord] + rw [hreal, show uniformPublic = Crypto.LWE.uniformEnsemble dimension sampleCount digitWidth + from funext uniformPublic_eq] + rfl + +/-- The complete honest algorithms have strict native polynomial clocks. -/ +theorem native_algorithms : + StrictPPT unaryEncoding (pairEncoding bitsEncoding bitsEncoding) keyGeneration ∧ + StrictPPT (pairEncoding unaryEncoding (pairEncoding bitsEncoding boolEncoding)) bitsEncoding + (fun p => encryption p.1 p.2.1 p.2.2) := by + constructor + · change CryptographyBridge.StrictPPT _ _ _ + apply CryptographyBridge.strictPPT_iff.mpr + refine ⟨fun security => Crypto.Homomorphic.GSW.keyGenSerialized (dimension security) + (sampleCount security) (digitWidth security) (dimension security), ?_, ?_⟩ + · exact Crypto.Homomorphic.GSW.isPPTOn_keyGenSerialized + Crypto.Homomorphic.GSW.Parameters.computableTidilyInPolyTime_dimension + Crypto.Homomorphic.GSW.Parameters.computableTidilyInPolyTime_samples + Crypto.Homomorphic.GSW.Parameters.computableTidilyInPolyTime_width + Crypto.Homomorphic.GSW.Parameters.computableTidilyInPolyTime_noise + · exact fun security => (keyGeneration_eq security).symm + · change CryptographyBridge.StrictPPT _ _ _ + apply CryptographyBridge.strictPPT_iff.mpr + refine ⟨fun p => Crypto.Homomorphic.GSW.encryptSerialized (dimension p.1) + (sampleCount p.1) (digitWidth p.1) p.2.1 p.2.2, ?_, ?_⟩ + · exact Crypto.Homomorphic.GSW.isPPTOn_encryptSerialized + (Crypto.Homomorphic.GSW.Parameters.computableTidilyInPolyTime_dimension.comp (by fun_prop)) + (Crypto.Homomorphic.GSW.Parameters.computableTidilyInPolyTime_samples.comp (by fun_prop)) + (Crypto.Homomorphic.GSW.Parameters.computableTidilyInPolyTime_width.comp (by fun_prop)) + (by fun_prop) (by fun_prop) + · exact fun p => (encryption_eq p.1 p.2.1 p.2.2).symm + +/-- Transfer the actual generated-key theorem to the inspectable probability-law presentation. -/ +theorem indCPA (hLWE : DecisionLWE) : ChosenMessageSecure := by + intro choose guess hchoose hguess + obtain ⟨chooseProgram, hchooseProgram, hchooseLaw⟩ := + CryptographyBridge.strictPPT_iff.mp hchoose + obtain ⟨guessProgram, hguessProgram, hguessLaw⟩ := + CryptographyBridge.strictPPT_iff.mp hguess + let adversary : Crypto.Encryption.Adversary := + ⟨fun security pk => chooseProgram (security, pk), + fun security state ciphertext => guessProgram (security, state, ciphertext)⟩ + have h := Crypto.Homomorphic.GSW.Parameters.indCPA (decisionLWE_iff.mp hLWE) + adversary ⟨hchooseProgram, hguessProgram⟩ + simpa only [Crypto.Encryption.game, adversary, ProbComp.eval_bind, keyGeneration_eq, + encryption_eq, hchooseLaw, hguessLaw, chosenMessageGame, PMF.monad_bind_eq_bind, + Negligible, Crypto.Negligible, Asymptotics.SuperpolynomialDecay, + Crypto.Game.advantage, Crypto.Game.succProbability, probability, + dimension, sampleCount, digitWidth, Crypto.Homomorphic.GSW.Parameters.dimension, + Crypto.Homomorphic.GSW.Parameters.samples, Crypto.Homomorphic.GSW.Parameters.width, + Crypto.Homomorphic.GSW.Parameters.noise, Crypto.Homomorphic.GSW.Parameters.rows] using h + +end ComplexityTests.Abstracts.GSWSecurityBridge diff --git a/ComplexityTests/Crypto/GSWParameters.lean b/ComplexityTests/Crypto/GSWParameters.lean new file mode 100644 index 0000000000..775158c426 --- /dev/null +++ b/ComplexityTests/Crypto/GSWParameters.lean @@ -0,0 +1,165 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Crypto.Computational.Homomorphic.GSW.Parameters +import Complexity.Crypto.Computational.Homomorphic.GSW.Sampling +import Complexity.Crypto.Computational.Homomorphic.GSW.Hiding + +/-! +GSW parameter regressions connect the growing family to actual sampled keys, encryption and NAND, +and to the real-valued statistical bound. Positive signed errors occur at every parameter. These +checks supply no decision-LWE hardness or bootstrappability claim. +-/ + +namespace ComplexityTests.GSWParameters + +open Cslib Cslib.Crypto Cslib.Probability Cslib.Crypto.Homomorphic.GSW +open Turing.MultiTapeTM +open scoped NNReal + +-- Parameter zero remains nontrivial, and a ceiling-logarithm jump changes the actual dimensions. +example : Parameters.dimension 0 = 1 ∧ Parameters.noise 0 = 1 ∧ Parameters.width 0 = 16 ∧ + Parameters.rows 0 = 32 ∧ Parameters.samples 0 = 32 ∧ Parameters.modulus 0 = 65536 := by + decide +kernel + +example : Parameters.width 1 = 24 ∧ Parameters.samples 1 = 74 ∧ + Parameters.width 2 = 32 ∧ Parameters.samples 2 = 132 := by + decide +kernel + +-- Every unary-output native premise is instantiated by the same family, including the modulus. +example : ComputableTidilyInPolyTime + (fun security => (Parameters.dimension security, Parameters.noise security, + Parameters.width security, Parameters.rows security, Parameters.samples security, + Parameters.modulus security)) encUnary + (encPair encUnary (encPair encUnary (encPair encUnary + (encPair encUnary (encPair encUnary encUnary))))) := by + fun_prop + +-- A finite exceptional parameter does not defeat the eventual-margin theorem. The output bit +-- count here is exponential; the theorem does not require a polynomial bound on that count. +example : Negligible (fun n => (((n + 1) ^ 2 : ℕ) : ℝ≥0) * NNReal.sqrt + ((2 : ℝ≥0) ^ (2 ^ n) / 2 ^ (if n = 0 then 0 else 2 ^ n + 2 * n))) := by + apply negligible_mul_sqrt_pow_two_div_pow_two (count := fun n => (n + 1) ^ 2) (by fun_prop) + filter_upwards [Filter.eventually_gt_atTop 0] with n hn + simp only [ite_eq_right (by omega : n ≠ 0)] + exact le_rfl + +-- Without surplus entropy the error can be constantly one and hence non-negligible. +example : ¬ Negligible (fun n => NNReal.sqrt ((2 : ℝ≥0) ^ n / 2 ^ n)) := by + simpa using not_negligible_const (by norm_num : (1 : ℝ≥0) ≠ 0) + +private def keyInputs (security : ℕ) : + KeyInputs (Parameters.dimension security) (Parameters.samples security) + (Parameters.width security) := + ⟨fun _ => 5, fun _ _ => 3, fun _ => (Parameters.noise security : ℤ)⟩ + +private def keys (security : ℕ) := + (publicMatrix (keyInputs security).publicPart (keyInputs security).secret + (keyInputs security).error, (keyInputs security).secret) + +private def coins (security : ℕ) : + Matrix (Fin (Parameters.dimension security + 1) × Fin (Parameters.width security)) + (Fin (Parameters.samples security)) Bool := fun _ _ => true + +private def ciphertext (security : ℕ) (message : Bool) := + encryptWithCoins (keys security).1 message (coins security) + +private theorem keyInputs_supported (security : ℕ) : + keyInputs security ∈ (ProbComp.eval (sampleKeyInputs (Parameters.dimension security) + (Parameters.samples security) (Parameters.width security) + (Parameters.noise security))).support := by + rw [mem_support_sampleKeyInputs_iff] + simp [keyInputs] + +-- Both nonzero signed endpoints occur in the actual error law at every security parameter. +example (security : ℕ) : + (Parameters.noise security : ℤ) ∈ + (ProbComp.eval (sampleCenteredBinomial (Parameters.noise security))).support ∧ + -(Parameters.noise security : ℤ) ∈ + (ProbComp.eval (sampleCenteredBinomial (Parameters.noise security))).support ∧ + (Parameters.noise security : ℤ) ≠ 0 := by + simp only [mem_support_sampleCenteredBinomial_iff, Int.natAbs_neg, Int.natAbs_natCast, + le_refl, true_and] + exact_mod_cast (Parameters.noise_pos security).ne' + +private theorem keys_supported (security : ℕ) : + keys security ∈ (ProbComp.eval (keyGen (Parameters.dimension security) + (Parameters.samples security) (Parameters.width security) + (Parameters.noise security))).support := by + simp only [keyGen, ProbComp.eval_bind, ProbComp.eval_pure, + PMF.mem_support_bind_iff, PMF.mem_support_pure_iff] + exact ⟨keyInputs security, keyInputs_supported security, rfl⟩ + +private theorem ciphertext_supported (security : ℕ) (message : Bool) : + ciphertext security message ∈ (ProbComp.eval (encrypt (keys security).1 message)).support := + (mem_support_encrypt_iff _ _ _).mpr ⟨coins security, rfl⟩ + +-- There are no uninstantiated width or noise-margin hypotheses in these growing-family clients. +example (security : ℕ) (message : Bool) : + decrypt (keys security).2 (ciphertext security message) = message := by + apply keyGen_encrypt_correct (η := Parameters.noise security) (Parameters.width_pos security) + ?_ (keys_supported security) message (ciphertext_supported security message) + simpa only [Parameters.modulus, Nat.mul_assoc] using Parameters.fresh_margin security + +example (security : ℕ) (left right : Bool) : + decrypt (keys security).2 (nand (ciphertext security left) (ciphertext security right)) = + !(left && right) := by + apply keyGen_nand_correct (η := Parameters.noise security) (Parameters.width_pos security) + ?_ (keys_supported security) left right + (ciphertext_supported security left) (ciphertext_supported security right) + simpa only [Parameters.modulus, Parameters.rows, Nat.mul_assoc] using + Parameters.nand_margin security + +-- Match the real-valued bound used by the actual adaptive uniform-public-matrix game. +example : Asymptotics.SuperpolynomialDecay Filter.atTop (fun n : ℕ => (n : ℝ)) + (fun n => ((Parameters.dimension n + 1) * Parameters.width n : ℕ) * + Real.sqrt ((2 : ℝ) ^ (Parameters.width n * (Parameters.dimension n + 1)) / + 2 ^ Parameters.samples n)) := by + simpa only [Parameters.rows, NNReal.coe_mul, NNReal.coe_natCast, Real.coe_sqrt, + NNReal.coe_div, NNReal.coe_pow, NNReal.coe_ofNat, Nat.mul_comm] using + negligible_iff_coe.mp Parameters.negligible_statistical_error + +-- The actual uniform-public-matrix chosen-message games have negligible advantage, including +-- adversaries with arbitrary parameter-dependent saved state and no efficiency restriction. +example {State : ℕ → Type} + (choose : ∀ n, Matrix (Fin (Parameters.samples n)) (Fin (Parameters.dimension n + 1)) + (ZMod (2 ^ Parameters.width n)) → PMF ((Bool × Bool) × State n)) + (guess : ∀ n, State n → Ciphertext (Parameters.dimension n) (Parameters.width n) → PMF Bool) : + Negligible (fun n => Game.advantage (uniformPublicGame (choose n) (guess n) false) + (uniformPublicGame (choose n) (guess n) true)) := by + apply negligible_of_le Parameters.negligible_statistical_error + intro n + apply NNReal.coe_le_coe.mp + simpa only [Game.coe_advantage, Game.succProbability, ENNReal.coe_toNNReal_eq_toReal, + NNReal.coe_mul, NNReal.coe_natCast, Real.coe_sqrt, NNReal.coe_div, NNReal.coe_pow, + NNReal.coe_ofNat, Parameters.rows, Nat.mul_comm] using + uniformPublicGame_advantage_le (choose n) (guess n) + +/-- info: 'Cslib.Crypto.negligible_mul_sqrt_pow_two_div_pow_two' depends on axioms: [propext, Classical.choice, Quot.sound] -/ +#guard_msgs in +#print axioms Cslib.Crypto.negligible_mul_sqrt_pow_two_div_pow_two + +/-- info: 'Cslib.Crypto.Homomorphic.GSW.Parameters.nand_margin' depends on axioms: [propext, Classical.choice, Quot.sound] -/ +#guard_msgs in +#print axioms Cslib.Crypto.Homomorphic.GSW.Parameters.nand_margin + +/-- +info: 'Cslib.Crypto.Homomorphic.GSW.Parameters.computableTidilyInPolyTime_modulus' depends on axioms: [propext, + Classical.choice, + Quot.sound] +-/ +#guard_msgs in +#print axioms Cslib.Crypto.Homomorphic.GSW.Parameters.computableTidilyInPolyTime_modulus + +/-- +info: 'Cslib.Crypto.Homomorphic.GSW.Parameters.negligible_statistical_error' depends on axioms: [propext, + Classical.choice, + Quot.sound] +-/ +#guard_msgs in +#print axioms Cslib.Crypto.Homomorphic.GSW.Parameters.negligible_statistical_error + +end ComplexityTests.GSWParameters diff --git a/ComplexityTests/Crypto/GSWSecurity.lean b/ComplexityTests/Crypto/GSWSecurity.lean new file mode 100644 index 0000000000..9809325347 --- /dev/null +++ b/ComplexityTests/Crypto/GSWSecurity.lean @@ -0,0 +1,156 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Crypto.Computational.Homomorphic.GSW.Security +import Mathlib.Logic.Equiv.Bool + +/-! +Regression clients for the actual GSW security reduction. A deliberately revealing test +encryption checks the hidden-bit orientation, preservation of saved public-key state and the +factor-two loss. The GSW clients use the actual growing parameter family and native algorithms; +their security theorem retains its precise decision-LWE hypothesis. +-/ + +namespace ComplexityTests.GSWSecurity + +open Cslib Cslib.Probability Cslib.Crypto Cslib.Crypto.Homomorphic.GSW +open Turing.MultiTapeTM +open scoped NNReal + +private def revealingEncrypt (_ : ℕ) (_ : List Bool) (message : Bool) : ProbComp (List Bool) := + pure [message] + +private def savedKeyAdversary : Encryption.Adversary where + choose _ pk := pure ((false, true), pk) + guess _ state ciphertext := pure (state.headD false ^^ ciphertext.headD false) + +-- Losing the saved word or reversing the hidden-bit orientation changes this exact law. +private theorem saved_key_reduction (security : ℕ) (pk : List Bool) : + ProbComp.eval (Encryption.keyDistinguisher revealingEncrypt savedKeyAdversary security pk) = + PMF.pure (pk.headD false) := by + simp [Encryption.keyDistinguisher, revealingEncrypt, savedKeyAdversary, + PMF.map, Function.comp_def] + +example : + ProbComp.eval (Encryption.keyDistinguisher revealingEncrypt savedKeyAdversary 0 [true]) = + PMF.pure true := saved_key_reduction 0 [true] + +private noncomputable def idealTestKeys : PMF (List Bool) := + (PMF.uniformOfFintype Bool).map (fun bit => [bit]) + +private theorem test_distinguisher_real : + distinguishingGame (PMF.pure [false]) + (Encryption.keyDistinguisher revealingEncrypt savedKeyAdversary 0) = PMF.pure false := by + simp [distinguishingGame, saved_key_reduction] + +private theorem test_distinguisher_ideal : + distinguishingGame idealTestKeys + (Encryption.keyDistinguisher revealingEncrypt savedKeyAdversary 0) = + PMF.uniformOfFintype Bool := by + simp [distinguishingGame, idealTestKeys, PMF.bind_map, saved_key_reduction, Function.comp_def] + +private theorem test_public_game (bit : Bool) : + Encryption.publicKeyGame (PMF.pure [false]) revealingEncrypt savedKeyAdversary bit 0 = + PMF.pure bit := by + cases bit <;> simp [Encryption.publicKeyGame, revealingEncrypt, savedKeyAdversary, + ProbComp.eval_pure] + +private theorem test_ideal_game (bit : Bool) : + Encryption.publicKeyGame idealTestKeys revealingEncrypt savedKeyAdversary bit 0 = + PMF.uniformOfFintype Bool := by + cases bit + · simp [Encryption.publicKeyGame, revealingEncrypt, savedKeyAdversary, + idealTestKeys, ProbComp.eval_pure, PMF.map] + · simpa [Encryption.publicKeyGame, revealingEncrypt, savedKeyAdversary, + idealTestKeys, ProbComp.eval_pure, PMF.map, Equiv.boolNot, Function.comp_def] using + PMF.uniformOfFintype_map_equiv Equiv.boolNot + +-- The factor two is attained: a chosen-message gap of one corresponds to a key gap of one half, +-- while the replacement world's chosen-message gap is zero. +example : + Game.advantage + (Encryption.publicKeyGame (PMF.pure [false]) revealingEncrypt savedKeyAdversary false 0) + (Encryption.publicKeyGame (PMF.pure [false]) revealingEncrypt savedKeyAdversary true 0) = 1 ∧ + Game.advantage + (distinguishingGame (PMF.pure [false]) + (Encryption.keyDistinguisher revealingEncrypt savedKeyAdversary 0)) + (distinguishingGame idealTestKeys + (Encryption.keyDistinguisher revealingEncrypt savedKeyAdversary 0)) = 1 / 2 ∧ + Game.advantage + (Encryption.publicKeyGame idealTestKeys revealingEncrypt savedKeyAdversary false 0) + (Encryption.publicKeyGame idealTestKeys revealingEncrypt savedKeyAdversary true 0) = 0 := by + rw [test_public_game, test_public_game, test_distinguisher_real, test_distinguisher_ideal, + test_ideal_game, test_ideal_game] + norm_num [Game.advantage, Game.succProbability, NNReal.nndist_eq, ENNReal.toNNReal_ofNat] + +-- This real client chooses messages as a function of the public key and retains its full word. +private def adaptiveAdversary : Encryption.Adversary where + choose _ pk := pure ((pk.headD false, !pk.headD false), pk) + guess _ state ciphertext := pure (state.headD false ^^ ciphertext.headD false) + +private theorem adaptiveAdversary_isPPT : adaptiveAdversary.IsPPT := by + constructor <;> simp only [adaptiveAdversary] <;> ppt + +-- The reduction covers all input words, including malformed or oversized matrix encodings. +example : IsPPT encBool + (lweDistinguisher Parameters.dimension Parameters.samples Parameters.width adaptiveAdversary) := + isPPT_lweDistinguisher Parameters.computableTidilyInPolyTime_dimension + Parameters.computableTidilyInPolyTime_samples Parameters.computableTidilyInPolyTime_width + adaptiveAdversary_isPPT + +-- Both honest algorithms are strict PPT for the same growing, positive-noise parameter family. +example : IsPPTOn encUnary (encPair encBits encBits) + (fun security => keyGenSerialized (Parameters.dimension security) (Parameters.samples security) + (Parameters.width security) (Parameters.noise security)) := + isPPTOn_keyGenSerialized Parameters.computableTidilyInPolyTime_dimension + Parameters.computableTidilyInPolyTime_samples Parameters.computableTidilyInPolyTime_width + Parameters.computableTidilyInPolyTime_noise + +example : IsPPTOn (encPair encUnary (encPair encBits encBool)) encBits + (fun p => encryptSerialized (Parameters.dimension p.1) (Parameters.samples p.1) + (Parameters.width p.1) p.2.1 p.2.2) := + isPPTOn_encryptSerialized (by fun_prop) (by fun_prop) (by fun_prop) + (by fun_prop) (by fun_prop) + +-- No separate encryption-efficiency, security-of-encryption, or zero-noise premise is supplied. +example + (hLWE : DecisionLWE Parameters.dimension Parameters.samples Parameters.width + (fun k => noiseLaw (Parameters.width k) (Parameters.noise k))) : + Encryption.INDCPA + (fun k => keyGenSerialized (Parameters.dimension k) (Parameters.samples k) + (Parameters.width k) (Parameters.noise k)) + (fun k => encryptSerialized (Parameters.dimension k) (Parameters.samples k) + (Parameters.width k)) := Parameters.indCPA hLWE + +/-- +info: 'Cslib.Crypto.Encryption.advantage_publicKeyGame_le' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms Encryption.advantage_publicKeyGame_le + +/-- +info: 'Cslib.Crypto.Homomorphic.GSW.eval_keyGenSerialized_publicWord' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms eval_keyGenSerialized_publicWord + +/-- +info: 'Cslib.Crypto.Homomorphic.GSW.advantage_game_le' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms advantage_game_le + +/-- +info: 'Cslib.Crypto.Homomorphic.GSW.Parameters.indCPA' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms Parameters.indCPA + +end ComplexityTests.GSWSecurity From a406f81f19d5cb9c7383cacc1ca37e3d82e60eae Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 23 Oct 2026 14:21:35 -0400 Subject: [PATCH 2/2] doc(crypto): record the generated-key GSW security milestone Document the actual algorithms, exact centered-binomial decision-LWE hypothesis, explicit parameter family and quantitative reduction. Link the checked security abstract without promoting full FHE to the catalogue. Keep native evaluation, shallow decryption and bootstrappability open. AI-assisted by OpenAI Codex; independently source-reviewed by /root/maintenance_audit. --- ROADMAP.md | 26 ++++++++++++++++++++++++-- 1 file changed, 24 insertions(+), 2 deletions(-) diff --git a/ROADMAP.md b/ROADMAP.md index 6d67d276f4..eff306b011 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -233,8 +233,30 @@ existing developments, source credit and saved branches remain available for a f it neither assumes whole-matrix two-universality nor gives a bound for every fixed matrix. [Regressions](ComplexityTests/Crypto/GSWHiding.lean) include a composite-modulus counterexample to whole-matrix universality and an adaptive game with exact nonzero advantage. - Computational security, native decryption and NAND certificates, admissible parameter families - and bootstrappability remain open in #486. + The [generated-key security theorem](Complexity/Crypto/Computational/Homomorphic/GSW/Security.lean) + proves single-challenge IND-CPA for the actual serialized key generator and encryption program + against uniform classical strict PPT adversaries. Its + [decision-LWE assumption](Complexity/Crypto/Computational/LWE/Basic.lean) compares the public + word `[B*t+e | B]` with a uniform matrix of the same shape; the + [distribution bridge](Complexity/Crypto/Computational/Homomorphic/GSW/LWE.lean) supplies exactly + the sampled centered-binomial error law, without exposing the secret or errors. + One uniform hidden-bit reduction preserves the adversary's full saved state and bounds its + chosen-message advantage by twice its decision-LWE advantage plus the statistical term above. + The [positive-noise parameter family](Complexity/Crypto/Computational/Homomorphic/GSW/Parameters.lean) + takes `n = η = λ+1`, `w = 16+8*ceil(log₂(λ+1))` and `m = (n+1)*w+2λ`. + It proves the entropy surplus, uniform native parameter routines and strict fresh/one-NAND + correctness margins simultaneously; the security theorem leaves only the specified LWE + hypothesis. [Regression clients](ComplexityTests/Crypto/GSWSecurity.lean) check saved-state + preservation, the attained factor-two loss, adaptive message choice and actual algorithm + certificates. A [checked formal abstract](ComplexityTests/Abstracts/GSWSecurityAbstract.lean) + spells out both algorithms, their native efficiency and this precise conditional security + result. It remains outside the curated headline catalogue while the full FHE recovery is open. + Hardness for the specified noise family is assumed; no worst-case lattice reduction is supplied. + Native decryption/NAND/evaluation certificates, bootstrappability with compatible parameters + and the concrete FHE instantiation remain open in #486. This parameter family proves fresh + and one-NAND correctness; it does not yet supply the augmented-decryption circuit or the + separate joint circular-security assumption needed + for the fixed-key endpoint. 4. **Completeness of oblivious transfer.** In the ideal oblivious-transfer hybrid model, every polynomial-time multiparty functionality admits a protocol secure against static malicious corruptions, with security defined by real/ideal simulation and allowing abort, under the