From f212a83c6fe3964d517892e645d995ee3fabece0 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sat, 24 Oct 2026 02:53:44 +0000 Subject: [PATCH] feat(crypto): separate restricted and general auxiliary-input zero knowledge (#698) --- .../Crypto/Computational/GMW/Simulator.lean | 56 +++ .../Crypto/Computational/ZeroKnowledge.lean | 386 ++++++++++++++---- ComplexityTests/Crypto/ZeroKnowledge.lean | 62 +++ ROADMAP.md | 21 +- 4 files changed, 449 insertions(+), 76 deletions(-) diff --git a/Complexity/Crypto/Computational/GMW/Simulator.lean b/Complexity/Crypto/Computational/GMW/Simulator.lean index e15c5725ed..3b65dff084 100644 --- a/Complexity/Crypto/Computational/GMW/Simulator.lean +++ b/Complexity/Crypto/Computational/GMW/Simulator.lean @@ -53,6 +53,8 @@ The proof uses four distribution transformations: * `Cslib.Crypto.GMW.gmwRealWithPads`: a guessed-challenge attempt with supplied unopened pads. * `Cslib.Crypto.GMW.gmwRealPRGPads`, `Cslib.Crypto.GMW.gmwRealUniformPads`: its two pad sources. * `Cslib.Crypto.GMW.gmwViewReduction`: the single-challenge pointwise reduction. +* `Cslib.Crypto.GMW.AdvicePRG`: explicit advice-supplied PRG premise at seed size `n + 7` for + arbitrary polynomially bounded instance, witness, and auxiliary-input families. ## Main results @@ -1019,6 +1021,60 @@ theorem gmwView_negligible_of_advice_prg {α : Type} {enc : α ↪ List Bool} simpa only [Nat.cast_mul] using gmwView_advantage_le generator length f Vstar adversary n (a n) (w n) (z n) (hw_sat n) +/-- Explicit advice-PRG premise at GMW seed size `n + 7` for an instance encoding `enc`: +`generator` has output length `length`, is computable in polynomial time, and its output at seed +length `n + 7` is indistinguishable from uniform strings of length `length (n + 7)` against every +full-input uniform strict PPT test supplied with arbitrary polynomially bounded instance, witness, +and auxiliary-input families `(a, w, z)`. + +This stronger advice-supplied premise is **not** derived here from uniform `PseudorandomGenerator` +security or uniform `OneWay` security. -/ +def AdvicePRG {α : Type} (enc : α ↪ List Bool) (generator : List Bool → List Bool) + (length : ℕ → ℕ) : Prop := + ComputableInPolyTime generator encBits encBits ∧ + (∀ s, (generator s).length = length s.length) ∧ + ∀ test : (ℕ × (α × (List Bool × List Bool))) × List Bool → ProbComp Bool, + IsPPTOn + (encPair (encPair encUnary (encPair enc (encPair encBits encBits))) encBits) + encBool test → + ∀ (a : ℕ → α) (w z : ℕ → List Bool), + PolynomiallyBounded (fun n => (enc (a n)).length) → + PolynomiallyBounded (fun n => (w n).length) → + PolynomiallyBounded (fun n => (z n).length) → + Negligible (fun n => Game.advantage + (ProbComp.eval ((generator <$> BitString.sampleList (n + 7)) >>= + fun challenge => test ((n, a n, w n, z n), challenge))) + (ProbComp.eval (BitString.sampleList (length (n + 7)) >>= + fun challenge => test ((n, a n, w n, z n), challenge)))) + +/-- Under `AdvicePRG enc generator length`, the real GMW interaction view and `gmwSimulator` +have negligible distinguishing advantage against every full-input uniform strict PPT distinguisher +across all polynomially bounded valid instance, witness, and auxiliary-input families. -/ +theorem AdvicePRG.gmwView_negligible {α : Type} {enc : α ↪ List Bool} + {generator : List Bool → List Bool} {length : ℕ → ℕ} {f : α → CNF ℕ} + {Vstar : ℕ → α → List Bool → WordOracleComp Unit (List Bool)} + {adversary : ℕ → α → List Bool → List Bool → ProbComp Bool} + (hAdv : AdvicePRG enc generator length) + (hf : ComputableInPolyTime f enc encCNF) + (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits + (fun p => Vstar p.1 p.2.1 p.2.2)) + (hadv : IsPPTOn (encPair (encPair encUnary (encPair enc encBits)) encBits) encBool + (fun p => adversary p.1.1 p.1.2.1 p.1.2.2 p.2)) + {a : ℕ → α} {w z : ℕ → List Bool} + (ha : PolynomiallyBounded (fun n => (enc (a n)).length)) + (hw : PolynomiallyBounded (fun n => (w n).length)) + (hz : PolynomiallyBounded (fun n => (z n).length)) + (hw_sat : ∀ n, ThreeSAT.verifier (f (a n), w n) = true) : + Negligible (fun n => Game.advantage + (distinguishingGame + (((gmwProver generator (n + 7) (length (n + 7)) (f (a n)) (w n)).run + (Vstar n (a n) (z n)) + (gmwProver generator (n + 7) (length (n + 7)) (f (a n)) (w n)).init).map Prod.fst) + (adversary n (a n) (z n))) + (distinguishingGame (ProbComp.eval (gmwSimulator generator length f Vstar n (a n) (z n))) + (adversary n (a n) (z n)))) := + gmwView_negligible_of_advice_prg hAdv.1.tidy hAdv.2.1 hf.tidy hV hadv hAdv.2.2 ha hw hz hw_sat + /-- **Zero-knowledge simulation of the 3-copy GMW protocol.** For any uniform strict oracle PPT malicious verifier `Vstar` and any deterministic polynomial-time families of instances `a`, valid `ThreeSAT` witnesses `w`, and auxiliary inputs `z`, the real interaction view of `Vstar` with diff --git a/Complexity/Crypto/Computational/ZeroKnowledge.lean b/Complexity/Crypto/Computational/ZeroKnowledge.lean index 608d160352..401b2c6183 100644 --- a/Complexity/Crypto/Computational/ZeroKnowledge.lean +++ b/Complexity/Crypto/Computational/ZeroKnowledge.lean @@ -20,10 +20,12 @@ import Complexity.Logics.Propositional.CNF.PolyTime Goldreich, Micali, and Wigderson [GoldreichMicaliWigderson1991] proved that if one-way functions exist, then every language in `NP` has a computational zero-knowledge interactive proof system. -This module defines computational zero-knowledge interactive proofs (`ZeroKnowledgeProof`) and -constructs such a proof system for `ThreeSAT` and hence for every language in `NP` via -`ThreeSAT_npHard` and Naor's bit commitment scheme [Naor1991] -(`Complexity.Crypto.Computational.Commitment`). +This module defines computational zero-knowledge interactive proofs (`ZeroKnowledgeProof`) together +with explicit public API predicates distinguishing restricted polynomial-time-generable +zero-knowledge (`GenerableZeroKnowledge`) from general auxiliary-input zero-knowledge over +arbitrary polynomially bounded valid families (`AuxiliaryInputZeroKnowledge`), and constructs a +proof system for `ThreeSAT` and hence for every language in `NP` via `ThreeSAT_npHard` and Naor's +bit commitment scheme [Naor1991] (`Complexity.Crypto.Computational.Commitment`). ### Protocol design and source credit @@ -37,21 +39,33 @@ each of 3 parallel copies commits to a random variable mask, the XOR-masked assi whether to open the mask and full truth tables or the masked assignment and the active truth-table entries. -### Uniform zero-knowledge and witness-relation conventions - -* **Uniform zero-knowledge (`ZeroKnowledgeProof.zero_knowledge`).** Matching the library's uniform - strict-PPT cryptographic conventions (`ComputationallyIndistinguishable`), `zero_knowledge` - quantifies over uniform strict oracle PPT malicious verifiers `Vstar` and deterministic - polynomial-time-generable families of instances `a : ℕ → α`, valid witnesses - `w : ℕ → List Bool` (`∀ n, isWitness (a n) (w n) = true`), and auxiliary inputs - `z : ℕ → List Bool` (`ComputableInPolyTime · encUnary _`), rather than non-uniformly over - arbitrary sequences `(x, w) ∈ R_L` and `z ∈ {0, 1}^*`. Fixed-instance zero-knowledge - (`ZeroKnowledgeProof.zero_knowledge_const`) is an immediate corollary for constant families - `fun _ => a` and `fun _ => w`. - The separate finite theorem `GMW.gmwView_advantage_le` applies pointwise without generation - assumptions. Its full-input clock and `GMW.gmwView_negligible_of_advice_prg` expose the stronger - advice-PRG premise needed for arbitrary polynomially bounded families; they do not strengthen - this bundled uniform-family field or derive that premise from uniform one-wayness. +### Restricted versus general auxiliary-input zero-knowledge and witness conventions + +* **Restricted polynomial-time-generable zero-knowledge (`GenerableZeroKnowledge`, + `ZeroKnowledgeProof.zero_knowledge`, `ZeroKnowledgeProof.generableZeroKnowledge`).** + Matching the library's uniform strict-PPT cryptographic conventions + (`ComputationallyIndistinguishable`), `GenerableZeroKnowledge` quantifies over uniform strict + oracle PPT malicious verifiers `Vstar` (producing one efficient witness-free simulator `S` per + `Vstar` before the choice of families) and deterministic polynomial-time-generable families of + instances `a : ℕ → α`, valid witnesses `w : ℕ → List Bool` (`∀ n, isWitness (a n) (w n) = true`), + and auxiliary inputs `z : ℕ → List Bool` (`ComputableInPolyTime · encUnary _`). Fixed-instance + zero-knowledge (`ZeroKnowledgeProof.zero_knowledge_const`) is an immediate corollary for constant + families `fun _ => a` and `fun _ => w`. +* **General auxiliary-input zero-knowledge (`AuxiliaryInputZeroKnowledge`, + `ZeroKnowledgeProof.AuxiliaryInputZeroKnowledge`).** + Quantifies over the same uniform strict oracle PPT malicious verifiers `Vstar` and chooses one + efficient witness-free simulator `S` per `Vstar` before the choice of families, then ranges over + arbitrary polynomially bounded families of instances `a : ℕ → α`, valid witnesses + `w : ℕ → List Bool`, and auxiliary inputs `z : ℕ → List Bool` (`PolynomiallyBounded`), against + all full-input uniform strict PPT distinguishers `adversary` charged for the complete encoded + input `((1^n, (a n, z n)), view)`. Every system satisfying `AuxiliaryInputZeroKnowledge` + satisfies `GenerableZeroKnowledge` (`AuxiliaryInputZeroKnowledge.generableZeroKnowledge`). + Under the explicit advice-PRG premise `GMW.AdvicePRG` + (from `GMW.gmwView_negligible_of_advice_prg`), the GMW proof systems satisfy + `ZeroKnowledgeProof.AuxiliaryInputZeroKnowledge` + (`PseudorandomGenerator.auxiliaryInputZeroKnowledge_zeroKnowledgeProofOfReduction`, + `PseudorandomGenerator.auxiliaryInputZeroKnowledge_zeroKnowledgeProofThreeSAT`); this module does + not derive `GMW.AdvicePRG` from uniform PRG or one-way function assumptions. * **Bundled witness relation (`ZeroKnowledgeProof.isWitness`).** `ZeroKnowledgeProof` bundles its own polynomial-time witness predicate `isWitness : α → List Bool → Bool` characterizing `A` (`mem_iff_exists_witness`). No witness-length bound is imposed, so `isWitness` by itself need not @@ -64,25 +78,39 @@ entries. ## Main definitions +* `Cslib.Crypto.GenerableZeroKnowledge`: uniform computational zero-knowledge over deterministic + polynomial-time-generable instance, valid-witness, and auxiliary-input families. +* `Cslib.Crypto.AuxiliaryInputZeroKnowledge`, + `Cslib.Crypto.ZeroKnowledgeProof.AuxiliaryInputZeroKnowledge`: general auxiliary-input + computational zero-knowledge over arbitrary polynomially bounded valid families against + full-input uniform strict PPT distinguishers. * `Cslib.Crypto.ZeroKnowledgeProof`: a computational zero-knowledge interactive proof system for a language `A`, bundling a uniform strict oracle PPT verifier, an honest prover with a uniform strict PPT interaction realization, perfect completeness, soundness `1 / 3` against unbounded - provers, and uniform zero-knowledge with poly-time-generable auxiliary input. + provers, and `GenerableZeroKnowledge`. * `Cslib.Crypto.PseudorandomGenerator.zeroKnowledgeProofOfReduction`, `Cslib.Crypto.PseudorandomGenerator.zeroKnowledgeProofThreeSAT`: GMW zero-knowledge proof systems for any language Karp-reducible to `ThreeSAT` and for `ThreeSAT` itself. ## Main results +* `Cslib.Crypto.AuxiliaryInputZeroKnowledge.generableZeroKnowledge`, + `Cslib.Crypto.ZeroKnowledgeProof.AuxiliaryInputZeroKnowledge.generableZeroKnowledge`: + general auxiliary-input zero-knowledge implies poly-time-generable zero-knowledge. * `Cslib.Crypto.ZeroKnowledgeProof.isInteractiveProof`, `Cslib.Crypto.ZeroKnowledgeProof.mem_IP`: every language with a `ZeroKnowledgeProof` belongs to `IP`. -* `Cslib.Crypto.ZeroKnowledgeProof.zero_knowledge_const`: fixed-instance computational - zero-knowledge for any fixed instance and valid witness. -* `Cslib.Crypto.PseudorandomGenerator.exists_zeroKnowledgeProof_of_mem_NP`: any pseudorandom - generator with stretch at least `3 * k + 1` yields a computational zero-knowledge proof system - for every language in `NP`. -* `Cslib.Crypto.OneWay.exists_zeroKnowledgeProof_of_mem_NP`: if a one-way function exists, every - language in `NP` has a computational zero-knowledge proof system. +* `Cslib.Crypto.ZeroKnowledgeProof.zero_knowledge_const`, + `Cslib.Crypto.ZeroKnowledgeProof.AuxiliaryInputZeroKnowledge.zero_knowledge_const`: + fixed-instance computational zero-knowledge. +* `Cslib.Crypto.PseudorandomGenerator.exists_zeroKnowledgeProof_of_mem_NP`, + `Cslib.Crypto.OneWay.exists_zeroKnowledgeProof_of_mem_NP`: GMW zero-knowledge proof systems for + every language in `NP` from any pseudorandom generator (with stretch `3 * k + 1`) or one-way + function, establishing `GenerableZeroKnowledge`. +* `Cslib.Crypto.PseudorandomGenerator.auxiliaryInputZeroKnowledge_zeroKnowledgeProofOfReduction`, + `Cslib.Crypto.PseudorandomGenerator.auxiliaryInputZeroKnowledge_zeroKnowledgeProofThreeSAT`, + `Cslib.Crypto.PseudorandomGenerator.exists_auxiliaryInputZeroKnowledge_of_mem_NP`: + general `AuxiliaryInputZeroKnowledge` for the GMW proof systems under the explicit advice-PRG + premise `GMW.AdvicePRG`. ## References @@ -100,6 +128,134 @@ namespace Cslib.Crypto open Probability Complexity Logic.PL Turing.MultiTapeTM ComputableTidilyInPolyTime open scoped NNReal ENNReal +/-! ### Restricted versus general auxiliary-input zero-knowledge predicates -/ + +/-- **Uniform computational zero-knowledge with polynomial-time-generable families.** +For every uniform strict oracle PPT malicious verifier `Vstar` (taking security parameter `n`, +instance `a`, and auxiliary input `z`, charged for the complete encoded input `(1^n, (a, z))`), +there exists a single uniform strict PPT witness-free simulator `S` (chosen before the families and +charged for `(1^n, (a, z))`) whose output ensemble is computationally indistinguishable from the +real interaction output across all deterministic polynomial-time-generable families of instances +`a : ℕ → α`, valid witnesses `w : ℕ → List Bool` (`∀ n, isWitness (a n) (w n) = true`), and +auxiliary inputs `z : ℕ → List Bool` (`ComputableInPolyTime · encUnary _`). -/ +def GenerableZeroKnowledge {α : Type} (enc : α ↪ List Bool) + (prover : ℕ → α → List Bool → Prover Unit) + (isWitness : α → List Bool → Bool) : Prop := + ∀ Vstar : ℕ → α → List Bool → WordOracleComp Unit (List Bool), + IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits + (fun p : ℕ × α × List Bool => Vstar p.1 p.2.1 p.2.2) → + ∃ S : ℕ → α → List Bool → ProbComp (List Bool), + IsPPTOn (encPair encUnary (encPair enc encBits)) encBits + (fun p : ℕ × α × List Bool => S p.1 p.2.1 p.2.2) ∧ + ∀ (a : ℕ → α) (w z : ℕ → List Bool), + ComputableInPolyTime a encUnary enc → + ComputableInPolyTime w encUnary encBits → + ComputableInPolyTime z encUnary encBits → + (∀ n, isWitness (a n) (w n) = true) → + ComputationallyIndistinguishable + (fun n => ((prover n (a n) (w n)).run (Vstar n (a n) (z n)) + (prover n (a n) (w n)).init).map Prod.fst) + (fun n => ProbComp.eval (S n (a n) (z n))) + +/-- **General auxiliary-input computational zero-knowledge for arbitrary polynomially bounded +valid families.** +For every uniform strict oracle PPT malicious verifier `Vstar` (charged for its complete encoded +input `(1^n, (a, z))`), there exists a single uniform strict PPT witness-free simulator `S` +(chosen before the families and distinguisher, and charged for `(1^n, (a, z))`) such that for all +arbitrary polynomially bounded families of instances `a : ℕ → α`, valid witnesses +`w : ℕ → List Bool` (`∀ n, isWitness (a n) (w n) = true`), and auxiliary inputs +`z : ℕ → List Bool`, and for every uniform strict PPT distinguisher `adversary` (charged for its +complete encoded input `((1^n, (a, z)), view)`), the distinguishing advantage between the real +interaction view and the simulated view is negligible. -/ +def AuxiliaryInputZeroKnowledge {α : Type} (enc : α ↪ List Bool) + (prover : ℕ → α → List Bool → Prover Unit) + (isWitness : α → List Bool → Bool) : Prop := + ∀ Vstar : ℕ → α → List Bool → WordOracleComp Unit (List Bool), + IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits + (fun p : ℕ × α × List Bool => Vstar p.1 p.2.1 p.2.2) → + ∃ S : ℕ → α → List Bool → ProbComp (List Bool), + IsPPTOn (encPair encUnary (encPair enc encBits)) encBits + (fun p : ℕ × α × List Bool => S p.1 p.2.1 p.2.2) ∧ + ∀ (a : ℕ → α) (w z : ℕ → List Bool), + PolynomiallyBounded (fun n => (enc (a n)).length) → + PolynomiallyBounded (fun n => (w n).length) → + PolynomiallyBounded (fun n => (z n).length) → + (∀ n, isWitness (a n) (w n) = true) → + ∀ adversary : ℕ → α → List Bool → List Bool → ProbComp Bool, + IsPPTOn (encPair (encPair encUnary (encPair enc encBits)) encBits) encBool + (fun p => adversary p.1.1 p.1.2.1 p.1.2.2 p.2) → + Negligible (fun n => Game.advantage + (distinguishingGame + (((prover n (a n) (w n)).run (Vstar n (a n) (z n)) + (prover n (a n) (w n)).init).map Prod.fst) + (adversary n (a n) (z n))) + (distinguishingGame + (ProbComp.eval (S n (a n) (z n))) + (adversary n (a n) (z n)))) + +/-- **General auxiliary-input zero-knowledge implies poly-time-generable zero-knowledge.** +Every deterministic polynomial-time-generable family has polynomially bounded encoded output length, +and every unary-indexed `ComputationallyIndistinguishable` distinguisher lifts to a full-input +distinguisher by ignoring the extra `(a, z)` component. -/ +theorem AuxiliaryInputZeroKnowledge.generableZeroKnowledge {α : Type} {enc : α ↪ List Bool} + {prover : ℕ → α → List Bool → Prover Unit} {isWitness : α → List Bool → Bool} + (h : AuxiliaryInputZeroKnowledge enc prover isWitness) : + GenerableZeroKnowledge enc prover isWitness := by + intro Vstar hV + obtain ⟨S, hS_ppt, hS_zk⟩ := h Vstar hV + refine ⟨S, hS_ppt, fun a w z ha hw hz hw_sat adversary hadversary => ?_⟩ + have ha_poly : PolynomiallyBounded (fun n => (enc (a n)).length) := + ((encoding_length enc).comp ha.tidy).polynomiallyBounded + have hw_poly : PolynomiallyBounded (fun n => (w n).length) := + ((encoding_length encBits).comp hw.tidy).polynomiallyBounded + have hz_poly : PolynomiallyBounded (fun n => (z n).length) := + ((encoding_length encBits).comp hz.tidy).polynomiallyBounded + have htest : IsPPTOn (encPair (encPair encUnary (encPair enc encBits)) encBits) encBool + (fun p => adversary p.1.1 p.2) := + hadversary.preprocess (by fun_prop) (by fun_prop) + exact hS_zk a w z ha_poly hw_poly hz_poly hw_sat (fun n _ _ view => adversary n view) htest + +/-- Under `GenerableZeroKnowledge`, any full-input uniform strict PPT distinguisher +`adversary n (a n) (z n)` also has negligible distinguishing advantage on deterministic +polynomial-time-generable families `a, w, z`, since `(a n, z n)` can be recomputed from `1^n`. -/ +theorem GenerableZeroKnowledge.advantage_negligible {α : Type} {enc : α ↪ List Bool} + {prover : ℕ → α → List Bool → Prover Unit} {isWitness : α → List Bool → Bool} + (h : GenerableZeroKnowledge enc prover isWitness) + {Vstar : ℕ → α → List Bool → WordOracleComp Unit (List Bool)} + (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits + (fun p : ℕ × α × List Bool => Vstar p.1 p.2.1 p.2.2)) : + ∃ S : ℕ → α → List Bool → ProbComp (List Bool), + IsPPTOn (encPair encUnary (encPair enc encBits)) encBits + (fun p : ℕ × α × List Bool => S p.1 p.2.1 p.2.2) ∧ + ∀ (a : ℕ → α) (w z : ℕ → List Bool), + ComputableInPolyTime a encUnary enc → + ComputableInPolyTime w encUnary encBits → + ComputableInPolyTime z encUnary encBits → + (∀ n, isWitness (a n) (w n) = true) → + ∀ adversary : ℕ → α → List Bool → List Bool → ProbComp Bool, + IsPPTOn (encPair (encPair encUnary (encPair enc encBits)) encBits) encBool + (fun p => adversary p.1.1 p.1.2.1 p.1.2.2 p.2) → + Negligible (fun n => Game.advantage + (distinguishingGame + (((prover n (a n) (w n)).run (Vstar n (a n) (z n)) + (prover n (a n) (w n)).init).map Prod.fst) + (adversary n (a n) (z n))) + (distinguishingGame + (ProbComp.eval (S n (a n) (z n))) + (adversary n (a n) (z n)))) := by + obtain ⟨S, hS_ppt, hS_zk⟩ := h Vstar hV + refine ⟨S, hS_ppt, fun a w z ha hw hz hw_sat adversary hadversary => ?_⟩ + have ha_tidy := ha.tidy + have hz_tidy := hz.tidy + have hD : IsPPT encBool (fun n view => adversary n (a n) (z n) view) := + hadversary.preprocess + (input := encPair encUnary encBits) + (prepare := fun p => ((p.1, a p.1, z p.1), p.2)) + (by fun_prop) + exact hS_zk a w z ha hw hz hw_sat (fun n view => adversary n (a n) (z n) view) hD + +/-! ### Bundled computational zero-knowledge proof systems -/ + /-- A computational zero-knowledge interactive proof system for a language `A : Set α` (with instance encoding `enc : α ↪ List Bool`), indexed by a security parameter `n : ℕ` [Goldreich, Micali, and Wigderson][GoldreichMicaliWigderson1991]. @@ -116,13 +272,16 @@ Micali, and Wigderson][GoldreichMicaliWigderson1991]. `isWitness a w` is `ThreeSAT.verifier (f a, w)`, checking a `ThreeSAT` witness for `f a`. * `complete` and `sound`: completeness `1` for valid witnesses and soundness error at most `1 / 3` against all computationally unbounded stateful provers `P : Prover Unit`. -* `zero_knowledge`: **uniform zero-knowledge with poly-time-generable auxiliary input**. For every - uniform strict oracle PPT malicious verifier `Vstar` (taking security parameter `n`, instance `a`, - and auxiliary input `z`), there is a uniform strict PPT simulator `S` (taking `(1^n, a, z)` - without any witness) whose output ensemble is computationally indistinguishable from the real - interaction output across all deterministic polynomial-time-generable families of instances - `a : ℕ → α`, valid witnesses `w : ℕ → List Bool`, and auxiliary inputs `z : ℕ → List Bool` - (`ComputableInPolyTime · encUnary _`). -/ +* `zero_knowledge`: **uniform zero-knowledge with poly-time-generable families** + (`GenerableZeroKnowledge enc prover isWitness`). For every uniform strict oracle PPT malicious + verifier `Vstar` (taking security parameter `n`, instance `a`, and auxiliary input `z`), there is + a uniform strict PPT simulator `S` (taking `(1^n, a, z)` without any witness) whose output + ensemble is computationally indistinguishable from the real interaction output across all + deterministic polynomial-time-generable families of instances `a : ℕ → α`, valid witnesses + `w : ℕ → List Bool`, and auxiliary inputs `z : ℕ → List Bool` + (`ComputableInPolyTime · encUnary _`). The stronger general auxiliary-input property over + arbitrary polynomially bounded valid families is stated separately as + `ZeroKnowledgeProof.AuxiliaryInputZeroKnowledge`. -/ structure ZeroKnowledgeProof {α : Type} (enc : α ↪ List Bool) (A : Set α) where /-- The honest verifier, indexed by security parameter `n` and instance `a`. -/ verifier : ℕ → α → WordOracleComp Unit Bool @@ -163,33 +322,16 @@ structure ZeroKnowledgeProof {α : Type} (enc : α ↪ List Bool) (A : Set α) w /-- Uniform computational zero-knowledge with poly-time-generable auxiliary input against all uniform strict oracle PPT malicious verifiers, quantified over polynomial-time-generable families of instances `a`, valid witnesses `w`, and auxiliary inputs `z`. -/ - zero_knowledge : - ∀ Vstar : ℕ → α → List Bool → WordOracleComp Unit (List Bool), - IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits - (fun p : ℕ × α × List Bool => Vstar p.1 p.2.1 p.2.2) → - ∃ S : ℕ → α → List Bool → ProbComp (List Bool), - IsPPTOn (encPair encUnary (encPair enc encBits)) encBits - (fun p : ℕ × α × List Bool => S p.1 p.2.1 p.2.2) ∧ - ∀ (a : ℕ → α) (w z : ℕ → List Bool), - ComputableInPolyTime a encUnary enc → - ComputableInPolyTime w encUnary encBits → - ComputableInPolyTime z encUnary encBits → - (∀ n, isWitness (a n) (w n) = true) → - ComputationallyIndistinguishable - (fun n => ((prover n (a n) (w n)).run (Vstar n (a n) (z n)) - (prover n (a n) (w n)).init).map Prod.fst) - (fun n => ProbComp.eval (S n (a n) (z n))) + zero_knowledge : GenerableZeroKnowledge enc prover isWitness -/-- The equivalent tidy contract used internally by compositional proofs. -/ -theorem ZeroKnowledgeProof.polyTime_isWitness_tidy {α : Type} {enc : α ↪ List Bool} {A : Set α} - (h : ZeroKnowledgeProof enc A) : +private theorem ZeroKnowledgeProof.polyTime_isWitness_tidy {α : Type} {enc : α ↪ List Bool} + {A : Set α} (h : ZeroKnowledgeProof enc A) : ComputableTidilyInPolyTime (fun p : α × List Bool => h.isWitness p.1 p.2) (encPair enc encBits) encBool := by simpa only [← computableInPolyTime_iff_computableTidilyInPolyTime] using h.polyTime_isWitness -/-- The equivalent tidy contract used internally by compositional proofs. -/ -theorem ZeroKnowledgeProof.zero_knowledge_tidy {α : Type} {enc : α ↪ List Bool} {A : Set α} - (h : ZeroKnowledgeProof enc A) : +private theorem ZeroKnowledgeProof.zero_knowledge_tidy {α : Type} {enc : α ↪ List Bool} + {A : Set α} (h : ZeroKnowledgeProof enc A) : ∀ Vstar : ℕ → α → List Bool → WordOracleComp Unit (List Bool), IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits (fun p : ℕ × α × List Bool => Vstar p.1 p.2.1 p.2.2) → @@ -205,12 +347,62 @@ theorem ZeroKnowledgeProof.zero_knowledge_tidy {α : Type} {enc : α ↪ List Bo (fun n => ((h.prover n (a n) (w n)).run (Vstar n (a n) (z n)) (h.prover n (a n) (w n)).init).map Prod.fst) (fun n => ProbComp.eval (S n (a n) (z n))) := by - simpa only [← computableInPolyTime_iff_computableTidilyInPolyTime] using h.zero_knowledge + simpa only [GenerableZeroKnowledge, ← computableInPolyTime_iff_computableTidilyInPolyTime] + using h.zero_knowledge namespace ZeroKnowledgeProof variable {α : Type} {enc : α ↪ List Bool} {A : Set α} +/-- Named projection for the restricted polynomial-time-generable zero-knowledge property bundled by +`ZeroKnowledgeProof`. -/ +theorem generableZeroKnowledge (zk : ZeroKnowledgeProof enc A) : + GenerableZeroKnowledge enc zk.prover zk.isWitness := + zk.zero_knowledge + +/-- General auxiliary-input computational zero-knowledge for a bundled `ZeroKnowledgeProof` system, +ranging over arbitrary polynomially bounded instance, valid-witness, and auxiliary-input +families. -/ +def AuxiliaryInputZeroKnowledge (zk : ZeroKnowledgeProof enc A) : Prop := + Cslib.Crypto.AuxiliaryInputZeroKnowledge enc zk.prover zk.isWitness + +/-- General auxiliary-input zero-knowledge for `zk` implies the bundled restricted +`GenerableZeroKnowledge` guarantee. -/ +theorem AuxiliaryInputZeroKnowledge.generableZeroKnowledge {zk : ZeroKnowledgeProof enc A} + (h : zk.AuxiliaryInputZeroKnowledge) : + GenerableZeroKnowledge enc zk.prover zk.isWitness := + Cslib.Crypto.AuxiliaryInputZeroKnowledge.generableZeroKnowledge h + +/-- Fixed-instance auxiliary-input zero-knowledge under `zk.AuxiliaryInputZeroKnowledge`: for any +fixed instance `a`, valid witness `w`, and arbitrary polynomially bounded auxiliary-input family +`z : ℕ → List Bool`, the real and simulated views have negligible distinguishing advantage against +every full-input uniform strict PPT distinguisher. -/ +theorem AuxiliaryInputZeroKnowledge.zero_knowledge_const {zk : ZeroKnowledgeProof enc A} + (h : zk.AuxiliaryInputZeroKnowledge) + {Vstar : ℕ → α → List Bool → WordOracleComp Unit (List Bool)} + (hV : IsOraclePPTOn (encPair encUnary (encPair enc encBits)) encBits + (fun p : ℕ × α × List Bool => Vstar p.1 p.2.1 p.2.2)) : + ∃ S : ℕ → α → List Bool → ProbComp (List Bool), + IsPPTOn (encPair encUnary (encPair enc encBits)) encBits + (fun p : ℕ × α × List Bool => S p.1 p.2.1 p.2.2) ∧ + ∀ a w (z : ℕ → List Bool), + zk.isWitness a w = true → + PolynomiallyBounded (fun n => (z n).length) → + ∀ adversary : ℕ → α → List Bool → List Bool → ProbComp Bool, + IsPPTOn (encPair (encPair encUnary (encPair enc encBits)) encBits) encBool + (fun p => adversary p.1.1 p.1.2.1 p.1.2.2 p.2) → + Negligible (fun n => Game.advantage + (distinguishingGame + (((zk.prover n a w).run (Vstar n a (z n)) + (zk.prover n a w).init).map Prod.fst) + (adversary n a (z n))) + (distinguishingGame + (ProbComp.eval (S n a (z n))) + (adversary n a (z n)))) := by + obtain ⟨S, hS_ppt, hS_zk⟩ := h Vstar hV + exact ⟨S, hS_ppt, fun a w z hw hz adversary hadv => + hS_zk (fun _ => a) (fun _ => w) z (.const _) (.const _) hz (fun _ => hw) adversary hadv⟩ + /-- At every security parameter `n`, the honest verifier of a zero-knowledge proof system is an interactive proof for `A` with completeness `2 / 3` and soundness `1 / 3`. -/ theorem isInteractiveProof (zk : ZeroKnowledgeProof enc A) (n : ℕ) : @@ -240,17 +432,19 @@ theorem zero_knowledge_const (zk : ZeroKnowledgeProof enc A) (fun p : ℕ × α × List Bool => S p.1 p.2.1 p.2.2) ∧ ∀ a w (z : ℕ → List Bool), zk.isWitness a w = true → - ComputableTidilyInPolyTime z encUnary encBits → + ComputableInPolyTime z encUnary encBits → ComputationallyIndistinguishable (fun n => ((zk.prover n a w).run (Vstar n a (z n)) (zk.prover n a w).init).map Prod.fst) (fun n => ProbComp.eval (S n a (z n))) := by obtain ⟨S, hS_ppt, hS_zk⟩ := zk.zero_knowledge_tidy Vstar hV exact ⟨S, hS_ppt, fun a w z hw hz => - hS_zk (fun _ => a) (fun _ => w) z (const a) (const w) hz (fun _ => hw)⟩ + hS_zk (fun _ => a) (fun _ => w) z (const a) (const w) hz.tidy (fun _ => hw)⟩ end ZeroKnowledgeProof +/-! ### GMW zero-knowledge proof systems -/ + /-- Construct the Goldreich–Micali–Wigderson zero-knowledge proof system for any language `A` with a polynomial-time many-one reduction `f : α → CNF ℕ` to `ThreeSAT`, using a pseudorandom generator with stretch at least `3 * k + 1` and the 3-copy masked-3SAT commitment protocol in @@ -261,13 +455,15 @@ noncomputable def PseudorandomGenerator.zeroKnowledgeProofOfReduction {generator : List Bool → List Bool} {length : ℕ → ℕ} (hG : PseudorandomGenerator generator length) (hstretch : ∀ k, 3 * k + 1 ≤ length k) - {f : α → CNF ℕ} (hf : ComputableTidilyInPolyTime f enc encCNF) + {f : α → CNF ℕ} (hf : ComputableInPolyTime f enc encCNF) (hred : ∀ a, a ∈ A ↔ f a ∈ ThreeSAT) : ZeroKnowledgeProof enc A where verifier := GMW.gmwVerifier generator length f prover n a w := GMW.gmwProver generator (n + 7) (length (n + 7)) (f a) w isWitness a w := ThreeSAT.verifier (f a, w) - polyTime_isWitness := by fun_prop + polyTime_isWitness := by + have := hf.tidy + fun_prop mem_iff_exists_witness a := by rw [hred a] refine ⟨fun ha => ?_, fun ⟨w, hw⟩ => ?_⟩ @@ -276,18 +472,38 @@ noncomputable def PseudorandomGenerator.zeroKnowledgeProofOfReduction · simp only [ThreeSAT.verifier, SAT.verifier, Bool.and_eq_true, List.all_eq_true, decide_eq_true_eq] at hw exact ⟨hw.1, SAT.assignment (f a) w, hw.2⟩ - isOraclePPT_verifier := GMW.isOraclePPTOn_gmwVerifier hG.polyTime.tidy hG.length_eq hf + isOraclePPT_verifier := GMW.isOraclePPTOn_gmwVerifier hG.polyTime.tidy hG.length_eq hf.tidy interact n a w prog := GMW.gmwInteract generator (n + 7) (length (n + 7)) (f a) w prog eval_interact n a w prog := GMW.eval_gmwInteract generator (n + 7) (length (n + 7)) (f a) w prog - isPPT_interact _ hV := GMW.isPPTOn_gmwInteract hG.polyTime.tidy hG.length_eq hf hV + isPPT_interact _ hV := GMW.isPPTOn_gmwInteract hG.polyTime.tidy hG.length_eq hf.tidy hV complete n a _ hw := GMW.acceptProb_gmwVerifier_gmwProver hG.length_eq f n a hw sound n a ha P := GMW.acceptProb_gmwVerifier_le hG.length_eq hstretch f n a (mt (hred a).mpr ha) P zero_knowledge Vstar hV := ⟨GMW.gmwSimulator generator length f Vstar, - GMW.isPPTOn_gmwSimulator hG.polyTime.tidy hG.length_eq hf hV, + GMW.isPPTOn_gmwSimulator hG.polyTime.tidy hG.length_eq hf.tidy hV, fun _ _ _ ha hw_comp hz hw_sat => - GMW.gmwView_indistinguishable_gmwSimulator hG hf hV ha.tidy hw_comp.tidy hz.tidy hw_sat⟩ + GMW.gmwView_indistinguishable_gmwSimulator hG hf.tidy hV ha.tidy hw_comp.tidy hz.tidy + hw_sat⟩ + +/-- Under the explicit advice-PRG premise `GMW.AdvicePRG enc generator length`, the GMW proof +system `hG.zeroKnowledgeProofOfReduction hstretch hf hred` satisfies general auxiliary-input +zero-knowledge (`ZeroKnowledgeProof.AuxiliaryInputZeroKnowledge`) across all arbitrary polynomially +bounded valid instance, witness, and auxiliary-input families. -/ +theorem PseudorandomGenerator.auxiliaryInputZeroKnowledge_zeroKnowledgeProofOfReduction + {α : Type} {enc : α ↪ List Bool} {A : Set α} + {generator : List Bool → List Bool} {length : ℕ → ℕ} + (hG : PseudorandomGenerator generator length) + (hstretch : ∀ k, 3 * k + 1 ≤ length k) + {f : α → CNF ℕ} (hf : ComputableInPolyTime f enc encCNF) + (hred : ∀ a, a ∈ A ↔ f a ∈ ThreeSAT) + (hAdv : GMW.AdvicePRG enc generator length) : + (hG.zeroKnowledgeProofOfReduction hstretch hf hred).AuxiliaryInputZeroKnowledge := by + intro Vstar hV + exact ⟨GMW.gmwSimulator generator length f Vstar, + GMW.isPPTOn_gmwSimulator hG.polyTime.tidy hG.length_eq hf.tidy hV, + fun _ _ _ ha hw hz hw_sat _ hadv => + hAdv.gmwView_negligible hf hV hadv ha hw hz hw_sat⟩ /-- The Goldreich–Micali–Wigderson computational zero-knowledge proof system for `ThreeSAT`, built from any pseudorandom generator with stretch at least `3 * k + 1` via the 3-copy masked-3SAT @@ -299,10 +515,23 @@ noncomputable def PseudorandomGenerator.zeroKnowledgeProofThreeSAT ZeroKnowledgeProof encCNF ThreeSAT := hG.zeroKnowledgeProofOfReduction hstretch (by fun_prop) (fun _ => Iff.rfl) +/-- Under the explicit advice-PRG premise `GMW.AdvicePRG encCNF generator length`, the GMW proof +system `hG.zeroKnowledgeProofThreeSAT hstretch` satisfies general auxiliary-input zero-knowledge +(`ZeroKnowledgeProof.AuxiliaryInputZeroKnowledge`). -/ +theorem PseudorandomGenerator.auxiliaryInputZeroKnowledge_zeroKnowledgeProofThreeSAT + {generator : List Bool → List Bool} {length : ℕ → ℕ} + (hG : PseudorandomGenerator generator length) + (hstretch : ∀ k, 3 * k + 1 ≤ length k) + (hAdv : GMW.AdvicePRG encCNF generator length) : + (hG.zeroKnowledgeProofThreeSAT hstretch).AuxiliaryInputZeroKnowledge := + hG.auxiliaryInputZeroKnowledge_zeroKnowledgeProofOfReduction hstretch (by fun_prop) + (fun _ => Iff.rfl) hAdv + /-- **Goldreich–Micali–Wigderson theorem (from a pseudorandom generator).** Given a pseudorandom generator with stretch at least `3 * k + 1` (such as `fun k => 3 * k + 1`), every language `A ∈ NP enc` has a computational zero-knowledge interactive proof system -[Goldreich, Micali, and Wigderson][GoldreichMicaliWigderson1991]. -/ +[Goldreich, Micali, and Wigderson][GoldreichMicaliWigderson1991] in the uniform +polynomial-time-generable sense (`GenerableZeroKnowledge`). -/ theorem PseudorandomGenerator.exists_zeroKnowledgeProof_of_mem_NP {α : Type} {enc : α ↪ List Bool} {A : Set α} {generator : List Bool → List Bool} {length : ℕ → ℕ} @@ -311,13 +540,32 @@ theorem PseudorandomGenerator.exists_zeroKnowledgeProof_of_mem_NP (hA : A ∈ NP enc) : Nonempty (ZeroKnowledgeProof enc A) := by obtain ⟨f, hf, hred⟩ := ThreeSAT_npHard enc A hA - exact ⟨hG.zeroKnowledgeProofOfReduction hstretch hf.tidy hred⟩ + exact ⟨hG.zeroKnowledgeProofOfReduction hstretch hf hred⟩ + +/-- **Goldreich–Micali–Wigderson theorem under an explicit advice-PRG premise.** Given a +pseudorandom generator with stretch at least `3 * k + 1` that also satisfies the advice-supplied +premise `GMW.AdvicePRG enc generator length`, every language `A ∈ NP enc` has a computational +zero-knowledge interactive proof system satisfying general auxiliary-input zero-knowledge +(`ZeroKnowledgeProof.AuxiliaryInputZeroKnowledge`) across all polynomially bounded valid families. +This theorem takes `GMW.AdvicePRG` as an explicit hypothesis rather than deriving it from uniform +`PseudorandomGenerator` or `OneWay` security. -/ +theorem PseudorandomGenerator.exists_auxiliaryInputZeroKnowledge_of_mem_NP + {α : Type} {enc : α ↪ List Bool} {A : Set α} + {generator : List Bool → List Bool} {length : ℕ → ℕ} + (hG : PseudorandomGenerator generator length) + (hstretch : ∀ k, 3 * k + 1 ≤ length k) + (hAdv : GMW.AdvicePRG enc generator length) + (hA : A ∈ NP enc) : + ∃ zk : ZeroKnowledgeProof enc A, zk.AuxiliaryInputZeroKnowledge := by + obtain ⟨f, hf, hred⟩ := ThreeSAT_npHard enc A hA + exact ⟨hG.zeroKnowledgeProofOfReduction hstretch hf hred, + hG.auxiliaryInputZeroKnowledge_zeroKnowledgeProofOfReduction hstretch hf hred hAdv⟩ /-- **Goldreich–Micali–Wigderson theorem (from a one-way function).** If a one-way function exists, then every language `A ∈ NP enc` has a computational zero-knowledge interactive proof system [Goldreich, Micali, and Wigderson][GoldreichMicaliWigderson1991], in the uniform-family sense of -`ZeroKnowledgeProof.zero_knowledge`: instances, witnesses and auxiliary inputs range over -polynomial-time-generable families rather than arbitrary ones. -/ +`GenerableZeroKnowledge` (`ZeroKnowledgeProof.zero_knowledge`): instances, witnesses and auxiliary +inputs range over polynomial-time-generable families rather than arbitrary ones. -/ theorem OneWay.exists_zeroKnowledgeProof_of_mem_NP {α : Type} {enc : α ↪ List Bool} {A : Set α} {f : List Bool → List Bool} (hf : OneWay f) (hA : A ∈ NP enc) : diff --git a/ComplexityTests/Crypto/ZeroKnowledge.lean b/ComplexityTests/Crypto/ZeroKnowledge.lean index 6b90a195eb..cf5acf2ca9 100644 --- a/ComplexityTests/Crypto/ZeroKnowledge.lean +++ b/ComplexityTests/Crypto/ZeroKnowledge.lean @@ -115,6 +115,38 @@ noncomputable def univZeroKnowledgeProof : (congrArg (PMF.map Prod.fst) (GMW.eval_runTwoRound (fun _ => []) (fun _ => []) _ (0, [false, false, false]))) +/-- Unconditional general auxiliary-input zero-knowledge for `univZeroKnowledgeProof` across all +arbitrary polynomially bounded valid instance, witness, and auxiliary-input families. -/ +theorem univZeroKnowledgeProof_auxiliaryInputZeroKnowledge : + univZeroKnowledgeProof.AuxiliaryInputZeroKnowledge := by + intro Vstar hV + refine ⟨fun n a z => Prod.fst <$> + GMW.runTwoRound (fun _ => []) (fun _ => []) (Vstar n a z) (0, [false, false, false]), + ?_, fun a w z _ _ _ _ _ _ => ?_⟩ + · have hrun := GMW.isPPTOn_runTwoRound hV + (input := encPair encUnary (encPair encBits encBits)) + (prepare := fun p : ℕ × List Bool × List Bool => p) + (reply1 := fun _ => []) (reply2 := fun _ => []) (bound := fun _ => 0) + (by fun_prop) (by fun_prop) (by fun_prop) (by fun_prop) + (fun _ _ => le_rfl) (fun _ _ => le_rfl) + exact hrun.map (by fun_prop) + · convert negligible_zero using 2 with n + have heq : + ProbComp.eval (Prod.fst <$> GMW.runTwoRound (fun _ => []) (fun _ => []) + (Vstar n (a n) (z n)) (0, [false, false, false])) = + ((univZeroKnowledgeProof.prover n (a n) (w n)).run (Vstar n (a n) (z n)) + (univZeroKnowledgeProof.prover n (a n) (w n)).init).map Prod.fst := + (ProbComp.eval_map _ _).trans + (congrArg (PMF.map Prod.fst) + (GMW.eval_runTwoRound (fun _ => []) (fun _ => []) _ (0, [false, false, false]))) + rw [heq, Game.advantage_self] + +-- The stronger-to-restricted bridge recovers `GenerableZeroKnowledge` from +-- `AuxiliaryInputZeroKnowledge`. +example : GenerableZeroKnowledge encBits univZeroKnowledgeProof.prover + univZeroKnowledgeProof.isWitness := + univZeroKnowledgeProof_auxiliaryInputZeroKnowledge.generableZeroKnowledge + -- Concrete satisfiable 3CNF formula and witness check. private def satFormula : CNF ℕ := [[(0, true), (1, false)]] @@ -150,6 +182,36 @@ example {f : List Bool → List Bool} (hf : OneWay f) : Nonempty (ZeroKnowledgeProof encCNF ThreeSAT) := hf.exists_zeroKnowledgeProof_of_mem_NP ThreeSAT.mem_NP +-- Under an explicit advice-PRG premise, every NP language has a GMW zero-knowledge proof system +-- satisfying general `AuxiliaryInputZeroKnowledge`. +example {generator : List Bool → List Bool} {length : ℕ → ℕ} + (hG : PseudorandomGenerator generator length) + (hstretch : ∀ k, 3 * k + 1 ≤ length k) + (hAdv : GMW.AdvicePRG encCNF generator length) : + ∃ zk : ZeroKnowledgeProof encCNF ThreeSAT, zk.AuxiliaryInputZeroKnowledge := + hG.exists_auxiliaryInputZeroKnowledge_of_mem_NP hstretch hAdv ThreeSAT.mem_NP + +/-- +info: 'Cslib.Crypto.AuxiliaryInputZeroKnowledge.generableZeroKnowledge' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms Cslib.Crypto.AuxiliaryInputZeroKnowledge.generableZeroKnowledge + +/-- +info: 'Cslib.Crypto.PseudorandomGenerator.auxiliaryInputZeroKnowledge_zeroKnowledgeProofThreeSAT' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms PseudorandomGenerator.auxiliaryInputZeroKnowledge_zeroKnowledgeProofThreeSAT + +/-- +info: 'Cslib.Crypto.PseudorandomGenerator.exists_auxiliaryInputZeroKnowledge_of_mem_NP' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms Cslib.Crypto.PseudorandomGenerator.exists_auxiliaryInputZeroKnowledge_of_mem_NP + /-- info: 'Cslib.Crypto.PseudorandomGenerator.naorBitCommitment' depends on axioms: [propext, Classical.choice, Quot.sound] diff --git a/ROADMAP.md b/ROADMAP.md index 5d208cc9a0..bd8a65a29d 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -39,20 +39,27 @@ existing developments, source credit and saved branches remain available for a f 3-copy masked-3SAT truth-table commitment zero-knowledge proof system for `ThreeSAT` and every `A ∈ NP` (`ZeroKnowledgeProof`, `zeroKnowledgeProofThreeSAT`, `OneWay.exists_zeroKnowledgeProof_of_mem_NP`) from any uniform one-way function via HILL and - Cook–Levin, with uniform zero knowledge over deterministic polynomial-time-generable + Cook–Levin, with uniform zero knowledge (`GenerableZeroKnowledge`, + `ZeroKnowledgeProof.generableZeroKnowledge`) over deterministic polynomial-time-generable instance/witness/auxiliary-input families `(x n, w n, z n)` (and fixed-instance security via `zero_knowledge_const`) at soundness error `1 / 3` (the proof bounds it by `1 / 8 + 2^{-(n+8)}`). Because the auxiliary input is a deterministic polynomial-time function of `1^n`, this does not reach the - auxiliary-input statement above. - - *Pointwise reduction milestone (#427):* + general auxiliary-input statement above. + - *Pointwise reduction and auxiliary-input interface milestones (#427, #698):* `GMW.gmwView_advantage_le` bounds every valid instance/witness/auxiliary tuple by `(7/8)^(n+1)` plus `dyadicSize(n+1) * dyadicSize(totalLen(f a))` times one concrete PRG-challenge advantage at seed size `n+7`. The final test receives `(n,a,z,view)`; `isPPTOn_gmwViewReduction` charges the complete encoded tuple and challenge, including - adaptive queries and retained verifier randomness/state. The old uniform-family security - theorem is a corollary. `gmwView_negligible_of_advice_prg` covers arbitrary families with - separate polynomial length bounds only under an explicit stronger advice-PRG premise. - No implication from current uniform one-wayness/HILL to that premise is proved. The direct + adaptive queries and retained verifier randomness/state. `AuxiliaryInputZeroKnowledge` + (`ZeroKnowledgeProof.AuxiliaryInputZeroKnowledge`) states the general auxiliary-input notion + for arbitrary polynomially bounded valid families against full-input uniform strict PPT + distinguishers, with the stronger-to-restricted bridge + `AuxiliaryInputZeroKnowledge.generableZeroKnowledge`. Under the explicit advice-PRG premise + `GMW.AdvicePRG` (`gmwView_negligible_of_advice_prg`), the GMW proof systems satisfy + `ZeroKnowledgeProof.AuxiliaryInputZeroKnowledge` + (`PseudorandomGenerator.auxiliaryInputZeroKnowledge_zeroKnowledgeProofOfReduction`, + `PseudorandomGenerator.exists_auxiliaryInputZeroKnowledge_of_mem_NP`). + No implication from current uniform one-wayness/HILL to `GMW.AdvicePRG` is proved. The direct pad-replacement proof does not require the separate Naor commitment-hiding theorem. - *Open (this priority):* zero knowledge in Goldreich's sense (Def. 4.3.10), for every `x ∈ L` with arbitrary auxiliary input `z` against probabilistic polynomial-time verifiers;