From d7ad836808794c94a38950473a907cfe3c469230 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sun, 25 Oct 2026 09:18:14 -0400 Subject: [PATCH 1/2] feat(crypto): concrete leveled and fully homomorphic encryption from GSW (#486) Instantiate Gentry's generic bootstrapping constructions with GSW at the logarithmic-depth parameter family. `exists_leveled_of_decisionLWE` covers every polynomially bounded depth family by one correct, compact, native and IND-CPA leveled scheme, assuming only decision LWE for exactly this family. `fullyHomomorphic_of_decisionLWE` gives the fixed-key self-loop scheme for all circuits, assuming in addition the explicit one-key circular-security hypothesis for the base GSW scheme. All public conclusions use plain computability. Update the ROADMAP landmark to record what remains open. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- Complexity.lean | 1 + .../Homomorphic/GSW/FullyHomomorphic.lean | 129 ++++++++++++++++++ .../Crypto/GSWFullyHomomorphic.lean | 67 +++++++++ ROADMAP.md | 9 +- 4 files changed, 201 insertions(+), 5 deletions(-) create mode 100644 Complexity/Crypto/Computational/Homomorphic/GSW/FullyHomomorphic.lean create mode 100644 ComplexityTests/Crypto/GSWFullyHomomorphic.lean diff --git a/Complexity.lean b/Complexity.lean index 79d3065071..459dcfccef 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1439,6 +1439,7 @@ public import Complexity.Crypto.Computational.Homomorphic.GSW.DecryptionCircuit. public import Complexity.Crypto.Computational.Homomorphic.GSW.DepthParameters public import Complexity.Crypto.Computational.Homomorphic.GSW.DepthParameters.Scheme public import Complexity.Crypto.Computational.Homomorphic.GSW.DepthParameters.Security +public import Complexity.Crypto.Computational.Homomorphic.GSW.FullyHomomorphic public import Complexity.Crypto.Computational.Homomorphic.GSW.Gadget public import Complexity.Crypto.Computational.Homomorphic.GSW.Hiding public import Complexity.Crypto.Computational.Homomorphic.GSW.LWE diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/FullyHomomorphic.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/FullyHomomorphic.lean new file mode 100644 index 0000000000..98fa967043 --- /dev/null +++ b/Complexity/Crypto/Computational/Homomorphic/GSW/FullyHomomorphic.lean @@ -0,0 +1,129 @@ +/- +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.Homomorphic.GSW.DepthParameters.Scheme +public import Complexity.Crypto.Computational.Homomorphic.Leveled.Bootstrapping +public import Complexity.Crypto.Computational.Homomorphic.FixedKey.Bootstrapping +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain + +/-! +# Fully homomorphic encryption from GSW and decision LWE + +Gentry's generic bootstrapping constructions are instantiated with GSW at the logarithmic-depth +parameter family. The base scheme is `DepthParameters.scheme`, its decryption circuits are the +actual raw-input decryptors, and its bootstrappability, correctness, widths and native runtime +are proved without computational assumptions. + +* **Leveled FHE.** For every polynomially bounded depth family, the acyclic key-chain + construction evaluates all circuits of that depth, with polynomial widths independent of the + depth, native algorithms, and IND-CPA security assuming only decision LWE for this exact + family [Gentry2009, Theorems 3 and 4]. +* **Fully homomorphic encryption.** The one-key self-loop construction evaluates every circuit, + assuming decision LWE for this family *and* the separate one-key circular-security assumption + `Encryption.CircularSecure` for the base scheme [Gentry2009, Section 2, the self-loop + construction]. This is a one-key specialization of the KDM security Gentry assumes there. + Circular security is not derived from LWE. + +Neither theorem asserts lattice hardness, a worst-case reduction, circuit privacy, or an exact +concrete-security loss. + +## Main results + +* `Cslib.Crypto.Homomorphic.GSW.DepthParameters.exists_leveled_of_decisionLWE`: leveled FHE. +* `Cslib.Crypto.Homomorphic.GSW.DepthParameters.fullyHomomorphic_of_decisionLWE`: FHE under the + additional circular-security assumption. + +## References + +* [C. Gentry, *Fully homomorphic encryption using ideal lattices*, Section 2, Theorems 3 and 4 + and the self-loop construction][Gentry2009] +* [C. Gentry, A. Sahai and B. Waters, Sections 3.2–3.4][GentrySahaiWaters2013] +-/ + +@[expose] public section + +namespace Cslib.Crypto.Homomorphic.GSW.DepthParameters + +open Circuits Probability Turing.MultiTapeTM +open Parameters (dimension noise) + +/-- Leveled FHE from GSW: under decision LWE for this family, every polynomially bounded depth +family is covered by one actual scheme with an efficiently computable budget. Its secret and +ciphertext widths are polynomial and do not depend on the requested depth, its four algorithms +are native, and it is IND-CPA. No circular-security assumption is used. -/ +theorem exists_leveled_of_decisionLWE + (hLWE : DecisionLWE dimension samples width (fun k => noiseLaw (width k) (noise k))) + {depth : ℕ → ℕ} (hdepth : PolynomiallyBounded depth) : + ∃ budget : ℕ → ℕ, + ComputableInPolyTime budget encUnary encUnary ∧ + (∀ k, depth k ≤ budget k) ∧ + (Leveled.scheme decryptionCircuits budget).Correct ∧ + (∀ k c, c.2.depth ≤ depth k → (Leveled.scheme decryptionCircuits budget).permitted k c) ∧ + (Leveled.scheme decryptionCircuits budget).FixedWidth (fun k => 3 * secretWidth k + 1) + (fun k => ciphertextWidth k + 1) ∧ + PolynomiallyBounded (fun k => 3 * secretWidth k + 1) ∧ + PolynomiallyBounded (fun k => ciphertextWidth k + 1) ∧ + IsPPTOn encUnary (encPair encBits encBits) (Leveled.scheme decryptionCircuits budget).keyGen ∧ + IsPPTOn (encPair encUnary (encPair encBits encBool)) encBits + (fun p => (Leveled.scheme decryptionCircuits budget).encrypt p.1 p.2.1 p.2.2) ∧ + ComputableInPolyTime + (fun p : ℕ × List Bool × List Bool => + (Leveled.scheme decryptionCircuits budget).decrypt p.1 p.2.1 p.2.2) + (encPair encUnary (encPair encBits encBits)) encBool ∧ + IsPPTOn + (encPair encUnary (encPair encBits + (encPair (Boolean.encCircuit 1) (encList encBits)))) + encBits + (fun p => (Leveled.scheme decryptionCircuits budget).evaluate p.1 p.2.1 p.2.2.1 p.2.2.2) ∧ + Encryption.INDCPA (Leveled.scheme decryptionCircuits budget).keyGen + (Leveled.scheme decryptionCircuits budget).encrypt := by + obtain ⟨budget, hbudget, hle, hcorrect, hpermitted, hwidth, hsecret, hciphertext, hkeyGen, + hencrypt, hdecrypt, hevaluate, hsecure⟩ := + Leveled.exists_scheme_of_polynomiallyBounded decryptionCircuits correct fixedWidth + bootstrappable (indCPA_scheme hLWE) isPPTOn_keyGen isPPTOn_encrypt isPPTOn_evaluate + computableInPolyTime_decryptionCircuits.tidy hdepth + exact ⟨budget, hbudget.computableInPolyTime, hle, hcorrect, hpermitted, hwidth, hsecret, + hciphertext, hkeyGen, hencrypt, hdecrypt.computableInPolyTime, hevaluate, hsecure⟩ + +/-- Fully homomorphic encryption from GSW: under decision LWE for this family and the explicit +one-key circular-security assumption for the base scheme, the self-loop construction correctly +evaluates every finite circuit. Its widths are those of GSW, its decryption circuits have +polynomial size, its four algorithms are native, and it is IND-CPA. -/ +theorem fullyHomomorphic_of_decisionLWE + (hLWE : DecisionLWE dimension samples width (fun k => noiseLaw (width k) (noise k))) + (hcircular : Encryption.CircularSecure scheme.keyGen scheme.encrypt) : + (FixedKey.scheme decryptionCircuits).Correct ∧ + (∀ k c, (FixedKey.scheme decryptionCircuits).permitted k c) ∧ + (FixedKey.scheme decryptionCircuits).FixedWidth secretWidth ciphertextWidth ∧ + PolynomiallyBounded secretWidth ∧ PolynomiallyBounded ciphertextWidth ∧ + PolynomiallyBounded + (fun k => ((FixedKey.decryptionCircuits decryptionCircuits).circuit k).size) ∧ + IsPPTOn encUnary (encPair encBits encBits) (FixedKey.scheme decryptionCircuits).keyGen ∧ + IsPPTOn (encPair encUnary (encPair encBits encBool)) encBits + (fun p => (FixedKey.scheme decryptionCircuits).encrypt p.1 p.2.1 p.2.2) ∧ + ComputableInPolyTime + (fun p : ℕ × List Bool × List Bool => + (FixedKey.scheme decryptionCircuits).decrypt p.1 p.2.1 p.2.2) + (encPair encUnary (encPair encBits encBits)) encBool ∧ + IsPPTOn + (encPair encUnary (encPair encBits + (encPair (Boolean.encCircuit 1) (encList encBits)))) + encBits + (fun p => (FixedKey.scheme decryptionCircuits).evaluate p.1 p.2.1 p.2.2.1 p.2.2.2) ∧ + Encryption.INDCPA (FixedKey.scheme decryptionCircuits).keyGen + (FixedKey.scheme decryptionCircuits).encrypt := by + obtain ⟨hcorrect, hpermitted, hwidth, hsecret, hciphertext, hsize, hkeyGen, hencrypt, + hdecrypt, hevaluate, hsecure⟩ := + FixedKey.fullyHomomorphic decryptionCircuits correct fixedWidth bootstrappable + (indCPA_scheme hLWE) hcircular isPPTOn_keyGen isPPTOn_encrypt isPPTOn_evaluate + computableInPolyTime_decryptionCircuits.tidy + exact ⟨hcorrect, hpermitted, hwidth, hsecret, hciphertext, hsize, hkeyGen, hencrypt, + hdecrypt.computableInPolyTime, hevaluate, hsecure⟩ + +end Cslib.Crypto.Homomorphic.GSW.DepthParameters diff --git a/ComplexityTests/Crypto/GSWFullyHomomorphic.lean b/ComplexityTests/Crypto/GSWFullyHomomorphic.lean new file mode 100644 index 0000000000..055548c92b --- /dev/null +++ b/ComplexityTests/Crypto/GSWFullyHomomorphic.lean @@ -0,0 +1,67 @@ +/- +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.FullyHomomorphic + +/-! +Clients of the concrete GSW endpoints. The base widths are computed at security parameter zero. +Under the stated assumptions, the leveled scheme for a constant depth family and the fixed-key +scheme both evaluate the actual compiled NAND circuit correctly on fresh encryptions. The +decision-LWE and circular-security premises remain hypotheses; nothing here instantiates them. +-/ + +namespace ComplexityTests.Crypto.GSWFullyHomomorphic + +open Cslib Cslib.Crypto Cslib.Circuits Cslib.Circuits.Boolean Cslib.Crypto.Homomorphic +open Cslib.Crypto.Homomorphic.GSW Cslib.Crypto.Homomorphic.GSW.DepthParameters +open Cslib.Probability +open Parameters (dimension noise) + +-- At security parameter zero the base secret holds one 65536-bit residue, and a ciphertext is a +-- square bit matrix with `2 * 65536` rows. The leveled widths add only an endpoint secret pair +-- and a tag, whatever the depth budget. +example : secretWidth 0 = 65536 ∧ ciphertextWidth 0 = 131072 ^ 2 ∧ + 3 * secretWidth 0 + 1 = 196609 := by + decide +kernel + +/-- Under decision LWE alone, one leveled scheme evaluates the compiled NAND circuit, whose +depth is two, on all supported fresh encryptions. -/ +example (hLWE : DecisionLWE dimension samples width (fun k => noiseLaw (width k) (noise k))) : + ∃ budget : ℕ → ℕ, ∀ k keys, + keys ∈ (ProbComp.eval ((Leveled.scheme decryptionCircuits budget).keyGen k)).support → + ∀ a b inputs, (Leveled.scheme decryptionCircuits budget).FreshInputs k keys.1 [a, b] inputs → + ∀ c ∈ (ProbComp.eval + ((Leveled.scheme decryptionCircuits budget).evaluate k keys.1 ⟨2, nandCircuit⟩ + inputs)).support, + (Leveled.scheme decryptionCircuits budget).decrypt k keys.2 c = !(a && b) := by + obtain ⟨budget, -, -, hcorrect, hpermitted, -⟩ := + exists_leveled_of_decisionLWE hLWE (PolynomiallyBounded.const 2) + refine ⟨budget, fun k keys hkeys a b inputs hinputs c hc => ?_⟩ + have h := hcorrect.decrypt_evaluate k keys hkeys ⟨2, nandCircuit⟩ + (hpermitted k _ (by decide +kernel)) [a, b] inputs rfl hinputs c hc + rw [h, eval_nandCircuit] + rfl + +/-- With the additional circular-security premise, the fixed-key scheme permits the NAND circuit +at every security parameter and evaluates it correctly, with no depth budget in key generation. -/ +example (hLWE : DecisionLWE dimension samples width (fun k => noiseLaw (width k) (noise k))) + (hcircular : Encryption.CircularSecure scheme.keyGen scheme.encrypt) (k : ℕ) + (keys : List Bool × List Bool) + (hkeys : keys ∈ (ProbComp.eval ((FixedKey.scheme decryptionCircuits).keyGen k)).support) + (a b : Bool) (inputs : List (List Bool)) + (hinputs : (FixedKey.scheme decryptionCircuits).FreshInputs k keys.1 [a, b] inputs) + (c : List Bool) (hc : c ∈ (ProbComp.eval + ((FixedKey.scheme decryptionCircuits).evaluate k keys.1 ⟨2, nandCircuit⟩ inputs)).support) : + (FixedKey.scheme decryptionCircuits).decrypt k keys.2 c = !(a && b) ∧ + c.length = ciphertextWidth k := by + obtain ⟨hcorrect, hpermitted, hwidth, -⟩ := fullyHomomorphic_of_decisionLWE hLWE hcircular + refine ⟨?_, hwidth.evaluate_length k keys hkeys _ (hpermitted k _) [a, b] inputs rfl hinputs c + hc⟩ + rw [hcorrect.decrypt_evaluate k keys hkeys _ (hpermitted k _) [a, b] inputs rfl hinputs c hc, + eval_nandCircuit] + rfl + +end ComplexityTests.Crypto.GSWFullyHomomorphic diff --git a/ROADMAP.md b/ROADMAP.md index 7062df1633..1fef3e71a2 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -60,11 +60,10 @@ Priorities live in this list and in the tiers of [#897]. polynomial-length messages. Authentication trees from one-time signatures and collision-resistant hashing are an intermediate development step; for the theorem itself, universal one-way hash functions replace the collision-resistance assumption. -- **Gentry's bootstrapping, instantiated** ([#486]). A concrete LWE-based scheme satisfying the - correctness, security, bootstrappability and native-efficiency hypotheses of the generic - theorem: full native evaluation of the augmented GSW decryption circuit, bootstrappability - with compatible parameters, and the joint circular-security assumption needed for the - fixed-key endpoint. Further targets: a uniform generator for the leveled scheme's wrapper +- **Gentry's bootstrapping, instantiated** ([#486]). GSW at its logarithmic-depth parameter + family instantiates the generic theorem: leveled FHE under decision LWE for exactly that + family, and FHE under the additional one-key circular-security assumption. Open: the checked + formal abstract of these endpoints, a uniform generator for the leveled scheme's wrapper decryption circuits (uniform compactness), reuse of evaluated ciphertexts as fresh inputs (multi-hop evaluation), and Gentry's exact concrete-security loss. - **Completeness of oblivious transfer.** In the ideal OT-hybrid model, every polynomial-time From 655377a3bba5a3fc68faec7e0c9eac498bdb473d Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sun, 25 Oct 2026 09:48:32 -0400 Subject: [PATCH 2/2] fix(crypto): hoist the common decryption circuit in the GSW leveled endpoint Address the #1025 pre-check. `exists_leveled_of_decisionLWE` now chooses one polynomial-size decryption circuit family, the native certificate of the common decryption algorithm and the fixed width bounds before the depth family, and states that every per-depth scheme uses exactly that decryption algorithm, as in Gentry's Definitions 1 and 3. Rename the fixed-key endpoint to `fullyHomomorphic_of_decisionLWE_of_circularSecure`, and state the gate set, the per-family runtime convention and the quasi-polynomial LWE modulus in the documentation and ROADMAP. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- .../Homomorphic/GSW/FullyHomomorphic.lean | 130 +++++++++++------- .../Crypto/GSWFullyHomomorphic.lean | 28 +++- ROADMAP.md | 10 +- 3 files changed, 111 insertions(+), 57 deletions(-) diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/FullyHomomorphic.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/FullyHomomorphic.lean index 98fa967043..fdba4c2dda 100644 --- a/Complexity/Crypto/Computational/Homomorphic/GSW/FullyHomomorphic.lean +++ b/Complexity/Crypto/Computational/Homomorphic/GSW/FullyHomomorphic.lean @@ -18,12 +18,20 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Pl Gentry's generic bootstrapping constructions are instantiated with GSW at the logarithmic-depth parameter family. The base scheme is `DepthParameters.scheme`, its decryption circuits are the actual raw-input decryptors, and its bootstrappability, correctness, widths and native runtime -are proved without computational assumptions. - -* **Leveled FHE.** For every polynomially bounded depth family, the acyclic key-chain - construction evaluates all circuits of that depth, with polynomial widths independent of the - depth, native algorithms, and IND-CPA security assuming only decision LWE for this exact - family [Gentry2009, Theorems 3 and 4]. +are proved without computational assumptions. Bootstrappability is for Gentry's gate set +Γ = {identity, NAND}: the schemes evaluate De Morgan circuits by compiling each De Morgan level +into two NAND levels. + +The security premise is decision LWE for exactly this family: secret dimension `λ + 1`, +centered-binomial noise of width `λ + 1`, and the quasi-polynomial modulus `2 ^ (16384 * t ^ 2)` +with `t = 1 + ⌈log₂ (λ + 2)⌉`. + +* **Leveled FHE.** One polynomial-size decryption circuit family, one natively computable + decryption algorithm and fixed polynomial widths are chosen first. Then every polynomially + bounded depth family is covered by an actual scheme with that decryption algorithm, assuming + only decision LWE [Gentry2009, Definition 3 and Theorem 3]. Security is asymptotic IND-CPA, a + consequence of [Gentry2009, Theorem 4] without its exact loss. Native certificates are uniform + for each depth family; key generation reads only the unary security parameter. * **Fully homomorphic encryption.** The one-key self-loop construction evaluates every circuit, assuming decision LWE for this family *and* the separate one-key circular-security assumption `Encryption.CircularSecure` for the base scheme [Gentry2009, Section 2, the self-loop @@ -36,13 +44,13 @@ concrete-security loss. ## Main results * `Cslib.Crypto.Homomorphic.GSW.DepthParameters.exists_leveled_of_decisionLWE`: leveled FHE. -* `Cslib.Crypto.Homomorphic.GSW.DepthParameters.fullyHomomorphic_of_decisionLWE`: FHE under the - additional circular-security assumption. +* `Cslib.Crypto.Homomorphic.GSW.DepthParameters.fullyHomomorphic_of_decisionLWE_of_circularSecure`: + FHE under the additional circular-security assumption. ## References -* [C. Gentry, *Fully homomorphic encryption using ideal lattices*, Section 2, Theorems 3 and 4 - and the self-loop construction][Gentry2009] +* [C. Gentry, *Fully homomorphic encryption using ideal lattices*, Section 2, Definitions 1–5, + Theorems 3 and 4 and the self-loop construction][Gentry2009] * [C. Gentry, A. Sahai and B. Waters, Sections 3.2–3.4][GentrySahaiWaters2013] -/ @@ -53,49 +61,73 @@ namespace Cslib.Crypto.Homomorphic.GSW.DepthParameters open Circuits Probability Turing.MultiTapeTM open Parameters (dimension noise) -/-- Leveled FHE from GSW: under decision LWE for this family, every polynomially bounded depth -family is covered by one actual scheme with an efficiently computable budget. Its secret and -ciphertext widths are polynomial and do not depend on the requested depth, its four algorithms -are native, and it is IND-CPA. No circular-security assumption is used. -/ +/-- Leveled FHE from GSW under decision LWE for this family, with quasi-polynomial modulus. +One polynomial-size circuit family computes the common decryption algorithm +`Leveled.decrypt decryptionCircuits`, which is natively computable, and the key and ciphertext +widths are fixed polynomials; all of these are chosen before the depth. Every polynomially +bounded depth family is then covered by an actual scheme with an efficiently computable budget +and exactly that decryption algorithm: it is correct for every circuit of the requested depth, +has the fixed widths, native algorithms and IND-CPA security. No circular-security assumption is +used. -/ theorem exists_leveled_of_decisionLWE - (hLWE : DecisionLWE dimension samples width (fun k => noiseLaw (width k) (noise k))) - {depth : ℕ → ℕ} (hdepth : PolynomiallyBounded depth) : - ∃ budget : ℕ → ℕ, - ComputableInPolyTime budget encUnary encUnary ∧ - (∀ k, depth k ≤ budget k) ∧ - (Leveled.scheme decryptionCircuits budget).Correct ∧ - (∀ k c, c.2.depth ≤ depth k → (Leveled.scheme decryptionCircuits budget).permitted k c) ∧ - (Leveled.scheme decryptionCircuits budget).FixedWidth (fun k => 3 * secretWidth k + 1) - (fun k => ciphertextWidth k + 1) ∧ - PolynomiallyBounded (fun k => 3 * secretWidth k + 1) ∧ - PolynomiallyBounded (fun k => ciphertextWidth k + 1) ∧ - IsPPTOn encUnary (encPair encBits encBits) (Leveled.scheme decryptionCircuits budget).keyGen ∧ - IsPPTOn (encPair encUnary (encPair encBits encBool)) encBits - (fun p => (Leveled.scheme decryptionCircuits budget).encrypt p.1 p.2.1 p.2.2) ∧ + (hLWE : DecisionLWE dimension samples width (fun k => noiseLaw (width k) (noise k))) : + ∃ circuits : ∀ k, Circuit Boolean.signature + ((3 * secretWidth k + 1) + (ciphertextWidth k + 1)) 1, + PolynomiallyBounded (fun k => (circuits k).size) ∧ + (∀ k (sk ciphertext : List Bool), sk.length = 3 * secretWidth k + 1 → + ciphertext.length = ciphertextWidth k + 1 → + (circuits k).eval Boolean.interpretation + (BitString.ofList ((3 * secretWidth k + 1) + (ciphertextWidth k + 1)) + (sk ++ ciphertext)) 0 = + Leveled.decrypt decryptionCircuits k sk ciphertext) ∧ ComputableInPolyTime - (fun p : ℕ × List Bool × List Bool => - (Leveled.scheme decryptionCircuits budget).decrypt p.1 p.2.1 p.2.2) + (fun p : ℕ × List Bool × List Bool => Leveled.decrypt decryptionCircuits p.1 p.2.1 p.2.2) (encPair encUnary (encPair encBits encBits)) encBool ∧ - IsPPTOn - (encPair encUnary (encPair encBits - (encPair (Boolean.encCircuit 1) (encList encBits)))) - encBits - (fun p => (Leveled.scheme decryptionCircuits budget).evaluate p.1 p.2.1 p.2.2.1 p.2.2.2) ∧ - Encryption.INDCPA (Leveled.scheme decryptionCircuits budget).keyGen - (Leveled.scheme decryptionCircuits budget).encrypt := by - obtain ⟨budget, hbudget, hle, hcorrect, hpermitted, hwidth, hsecret, hciphertext, hkeyGen, - hencrypt, hdecrypt, hevaluate, hsecure⟩ := + PolynomiallyBounded (fun k => 3 * secretWidth k + 1) ∧ + PolynomiallyBounded (fun k => ciphertextWidth k + 1) ∧ + ∀ depth : ℕ → ℕ, PolynomiallyBounded depth → + ∃ budget : ℕ → ℕ, + ComputableInPolyTime budget encUnary encUnary ∧ + (∀ k, depth k ≤ budget k) ∧ + (Leveled.scheme decryptionCircuits budget).decrypt = + Leveled.decrypt decryptionCircuits ∧ + (Leveled.scheme decryptionCircuits budget).Correct ∧ + (∀ k c, c.2.depth ≤ depth k → (Leveled.scheme decryptionCircuits budget).permitted k c) ∧ + (Leveled.scheme decryptionCircuits budget).FixedWidth (fun k => 3 * secretWidth k + 1) + (fun k => ciphertextWidth k + 1) ∧ + IsPPTOn encUnary (encPair encBits encBits) + (Leveled.scheme decryptionCircuits budget).keyGen ∧ + IsPPTOn (encPair encUnary (encPair encBits encBool)) encBits + (fun p => (Leveled.scheme decryptionCircuits budget).encrypt p.1 p.2.1 p.2.2) ∧ + IsPPTOn + (encPair encUnary (encPair encBits + (encPair (Boolean.encCircuit 1) (encList encBits)))) + encBits + (fun p => + (Leveled.scheme decryptionCircuits budget).evaluate p.1 p.2.1 p.2.2.1 p.2.2.2) ∧ + Encryption.INDCPA (Leveled.scheme decryptionCircuits budget).keyGen + (Leveled.scheme decryptionCircuits budget).encrypt := by + have hD := computableInPolyTime_decryptionCircuits.tidy + obtain ⟨circuits, hsize, hcircuits⟩ := Leveled.exists_decrypt_circuits decryptionCircuits hD + have hdecrypt := (Leveled.computableTidilyInPolyTime_scheme_decrypt decryptionCircuits hD + (fun _ => 0)).computableInPolyTime + obtain ⟨hsecret, hciphertext⟩ := Leveled.polynomiallyBounded_widths decryptionCircuits hD + refine ⟨circuits, hsize, fun k sk c hsk hc => hcircuits (fun _ => 0) k sk c hsk hc, hdecrypt, + hsecret, hciphertext, fun depth hdepth => ?_⟩ + obtain ⟨budget, hbudget, hle, hcorrect, hpermitted, hwidth, -, -, hkeyGen, hencrypt, -, + hevaluate, hsecure⟩ := Leveled.exists_scheme_of_polynomiallyBounded decryptionCircuits correct fixedWidth - bootstrappable (indCPA_scheme hLWE) isPPTOn_keyGen isPPTOn_encrypt isPPTOn_evaluate - computableInPolyTime_decryptionCircuits.tidy hdepth - exact ⟨budget, hbudget.computableInPolyTime, hle, hcorrect, hpermitted, hwidth, hsecret, - hciphertext, hkeyGen, hencrypt, hdecrypt.computableInPolyTime, hevaluate, hsecure⟩ - -/-- Fully homomorphic encryption from GSW: under decision LWE for this family and the explicit -one-key circular-security assumption for the base scheme, the self-loop construction correctly -evaluates every finite circuit. Its widths are those of GSW, its decryption circuits have -polynomial size, its four algorithms are native, and it is IND-CPA. -/ -theorem fullyHomomorphic_of_decisionLWE + bootstrappable (indCPA_scheme hLWE) isPPTOn_keyGen isPPTOn_encrypt isPPTOn_evaluate hD + hdepth + exact ⟨budget, hbudget.computableInPolyTime, hle, rfl, hcorrect, hpermitted, hwidth, hkeyGen, + hencrypt, hevaluate, hsecure⟩ + +/-- Fully homomorphic encryption from GSW: under decision LWE for this family, with +quasi-polynomial modulus, and the explicit one-key circular-security assumption for the base +scheme, the self-loop construction correctly evaluates every finite circuit. Its widths are those +of GSW, its decryption circuits have polynomial size, its four algorithms are native, and it is +IND-CPA. -/ +theorem fullyHomomorphic_of_decisionLWE_of_circularSecure (hLWE : DecisionLWE dimension samples width (fun k => noiseLaw (width k) (noise k))) (hcircular : Encryption.CircularSecure scheme.keyGen scheme.encrypt) : (FixedKey.scheme decryptionCircuits).Correct ∧ diff --git a/ComplexityTests/Crypto/GSWFullyHomomorphic.lean b/ComplexityTests/Crypto/GSWFullyHomomorphic.lean index 055548c92b..af4a9ed19b 100644 --- a/ComplexityTests/Crypto/GSWFullyHomomorphic.lean +++ b/ComplexityTests/Crypto/GSWFullyHomomorphic.lean @@ -37,14 +37,35 @@ example (hLWE : DecisionLWE dimension samples width (fun k => noiseLaw (width k) ((Leveled.scheme decryptionCircuits budget).evaluate k keys.1 ⟨2, nandCircuit⟩ inputs)).support, (Leveled.scheme decryptionCircuits budget).decrypt k keys.2 c = !(a && b) := by - obtain ⟨budget, -, -, hcorrect, hpermitted, -⟩ := - exists_leveled_of_decisionLWE hLWE (PolynomiallyBounded.const 2) + obtain ⟨-, -, -, -, -, -, hleveled⟩ := exists_leveled_of_decisionLWE hLWE + obtain ⟨budget, -, -, -, hcorrect, hpermitted, -⟩ := hleveled _ (PolynomiallyBounded.const 2) refine ⟨budget, fun k keys hkeys a b inputs hinputs c hc => ?_⟩ have h := hcorrect.decrypt_evaluate k keys hkeys ⟨2, nandCircuit⟩ (hpermitted k _ (by decide +kernel)) [a, b] inputs rfl hinputs c hc rw [h, eval_nandCircuit] rfl +/-- The schemes for two different depth families share one decryption algorithm, computed by one +polynomial-size circuit family chosen before either depth, as in Gentry's Definition 3. -/ +example (hLWE : DecisionLWE dimension samples width (fun k => noiseLaw (width k) (noise k))) : + ∃ circuits : ∀ k, Circuit Boolean.signature + ((3 * secretWidth k + 1) + (ciphertextWidth k + 1)) 1, + PolynomiallyBounded (fun k => (circuits k).size) ∧ + ∃ shallow deep : ℕ → ℕ, (∀ k, 2 ≤ shallow k ∧ k ≤ deep k) ∧ + (Leveled.scheme decryptionCircuits shallow).decrypt = + (Leveled.scheme decryptionCircuits deep).decrypt ∧ + ∀ k sk c, sk.length = 3 * secretWidth k + 1 → c.length = ciphertextWidth k + 1 → + (circuits k).eval Boolean.interpretation + (BitString.ofList ((3 * secretWidth k + 1) + (ciphertextWidth k + 1)) (sk ++ c)) 0 = + (Leveled.scheme decryptionCircuits deep).decrypt k sk c := by + obtain ⟨circuits, hsize, hcircuits, -, -, -, hleveled⟩ := exists_leveled_of_decisionLWE hLWE + obtain ⟨shallow, -, hshallow, hdecShallow, -⟩ := hleveled _ (PolynomiallyBounded.const 2) + obtain ⟨deep, -, hdeep, hdecDeep, -⟩ := hleveled _ PolynomiallyBounded.id + refine ⟨circuits, hsize, shallow, deep, fun k => ⟨hshallow k, hdeep k⟩, + hdecShallow.trans hdecDeep.symm, fun k sk c hsk hc => ?_⟩ + rw [hdecDeep] + exact hcircuits k sk c hsk hc + /-- With the additional circular-security premise, the fixed-key scheme permits the NAND circuit at every security parameter and evaluates it correctly, with no depth budget in key generation. -/ example (hLWE : DecisionLWE dimension samples width (fun k => noiseLaw (width k) (noise k))) @@ -57,7 +78,8 @@ example (hLWE : DecisionLWE dimension samples width (fun k => noiseLaw (width k) ((FixedKey.scheme decryptionCircuits).evaluate k keys.1 ⟨2, nandCircuit⟩ inputs)).support) : (FixedKey.scheme decryptionCircuits).decrypt k keys.2 c = !(a && b) ∧ c.length = ciphertextWidth k := by - obtain ⟨hcorrect, hpermitted, hwidth, -⟩ := fullyHomomorphic_of_decisionLWE hLWE hcircular + obtain ⟨hcorrect, hpermitted, hwidth, -⟩ := + fullyHomomorphic_of_decisionLWE_of_circularSecure hLWE hcircular refine ⟨?_, hwidth.evaluate_length k keys hkeys _ (hpermitted k _) [a, b] inputs rfl hinputs c hc⟩ rw [hcorrect.decrypt_evaluate k keys hkeys _ (hpermitted k _) [a, b] inputs rfl hinputs c hc, diff --git a/ROADMAP.md b/ROADMAP.md index 1fef3e71a2..c55e3f271a 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -61,11 +61,11 @@ Priorities live in this list and in the tiers of [#897]. collision-resistant hashing are an intermediate development step; for the theorem itself, universal one-way hash functions replace the collision-resistance assumption. - **Gentry's bootstrapping, instantiated** ([#486]). GSW at its logarithmic-depth parameter - family instantiates the generic theorem: leveled FHE under decision LWE for exactly that - family, and FHE under the additional one-key circular-security assumption. Open: the checked - formal abstract of these endpoints, a uniform generator for the leveled scheme's wrapper - decryption circuits (uniform compactness), reuse of evaluated ciphertexts as fresh inputs - (multi-hop evaluation), and Gentry's exact concrete-security loss. + family instantiates the generic theorem: leveled FHE under decision LWE with quasi-polynomial + modulus for exactly that family, and FHE under the additional one-key circular-security + assumption. Open: the checked formal abstract of these endpoints, a uniform generator for the + leveled scheme's wrapper decryption circuits (uniform compactness), reuse of evaluated + ciphertexts as fresh inputs (multi-hop evaluation), and Gentry's exact concrete-security loss. - **Completeness of oblivious transfer.** In the ideal OT-hybrid model, every polynomial-time multiparty functionality admits a protocol secure against static malicious corruptions, with real/ideal simulation and abort, under the standard communication assumptions.