From 03b3dd2cc9cc083b22e96052bedf60de4385cb76 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 24 Oct 2026 02:58:02 -0400 Subject: [PATCH 1/3] refactor(crypto): accept plain certificates in security constructors --- Complexity/Crypto/Computational/Basic.lean | 3 +- Complexity/Crypto/Computational/OneWay.lean | 4 +-- .../Computational/OneWay/Normalize.lean | 3 +- .../Computational/OneWayToSignature.lean | 2 +- .../Crypto/Computational/PRGToOneWay.lean | 2 +- ComplexityTests.lean | 1 + ComplexityTests/Crypto/PlainConstructors.lean | 32 +++++++++++++++++++ 7 files changed, 41 insertions(+), 6 deletions(-) create mode 100644 ComplexityTests/Crypto/PlainConstructors.lean diff --git a/Complexity/Crypto/Computational/Basic.lean b/Complexity/Crypto/Computational/Basic.lean index 634273996..f02e6f24e 100644 --- a/Complexity/Crypto/Computational/Basic.lean +++ b/Complexity/Crypto/Computational/Basic.lean @@ -7,6 +7,7 @@ Authors: Samuel Schlesinger module -- upstream: candidate +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain public import Complexity.Computability.Probabilistic.Parameter public import Complexity.Crypto.Game import Complexity.Crypto.Negligible.Basic @@ -137,7 +138,7 @@ theorem ComputationallyIndistinguishable.bind {X Y : ℕ → PMF (List Bool)} /-- Efficient parameter-dependent deterministic postprocessing preserves indistinguishability. -/ theorem ComputationallyIndistinguishable.map {X Y : ℕ → PMF (List Bool)} (h : ComputationallyIndistinguishable X Y) {f : ℕ → List Bool → List Bool} - (hf : ComputableTidilyInPolyTime (fun p : ℕ × List Bool => f p.1 p.2) + (hf : ComputableInPolyTime (fun p : ℕ × List Bool => f p.1 p.2) (encPair encUnary encBits) encBits) : ComputationallyIndistinguishable (fun n => (X n).map (f n)) (fun n => (Y n).map (f n)) := by have hp : IsPPT encBits (fun n word => pure (f n word)) := by ppt diff --git a/Complexity/Crypto/Computational/OneWay.lean b/Complexity/Crypto/Computational/OneWay.lean index e9b0f13b5..88853a7ce 100644 --- a/Complexity/Crypto/Computational/OneWay.lean +++ b/Complexity/Crypto/Computational/OneWay.lean @@ -108,11 +108,11 @@ theorem OneWay.inversion_negligible {f : List Bool → List Bool} (h : OneWay f) /-- Establish one-wayness by bounding every efficient inverter's success probability. -/ theorem OneWay.of_inversion_negligible {f : List Bool → List Bool} - (hf : ComputableTidilyInPolyTime f encBits encBits) + (hf : ComputableInPolyTime f encBits encBits) (h : ∀ adversary : Inverter, IsPPT encBits adversary → Negligible (fun n => Game.succProbability (ProbComp.eval (inversionGame f adversary n)))) : OneWay f := by - refine ⟨.of_tidy hf, fun adversary hPPT => ?_⟩ + refine ⟨hf, fun adversary hPPT => ?_⟩ simpa only [Game.advantage_pure_false] using h adversary hPPT /-- A length-preserving permutation that is one-way against every uniform PPT inverter. -/ diff --git a/Complexity/Crypto/Computational/OneWay/Normalize.lean b/Complexity/Crypto/Computational/OneWay/Normalize.lean index b8f2819a4..9bc3d1ab3 100644 --- a/Complexity/Crypto/Computational/OneWay/Normalize.lean +++ b/Complexity/Crypto/Computational/OneWay/Normalize.lean @@ -91,7 +91,8 @@ theorem OneWay.normalize {f : List Bool → List Bool} (hf : OneWay f) (bound : (hbound : ComputableTidilyInPolyTime bound encUnary encUnary) : OneWay (OneWayNormalization.normalize f bound) := by apply OneWay.of_inversion_negligible - (OneWayNormalization.computableTidilyInPolyTime_normalize hf.polyTime.tidy hbound) + (.of_tidy <| + OneWayNormalization.computableTidilyInPolyTime_normalize hf.polyTime.tidy hbound) intro adversary hPPT have hreduce : IsPPT encBits (fun n image => adversary n (BitString.padWord (bound n) image)) := by ppt diff --git a/Complexity/Crypto/Computational/OneWayToSignature.lean b/Complexity/Crypto/Computational/OneWayToSignature.lean index a1c491b1e..077f84cdf 100644 --- a/Complexity/Crypto/Computational/OneWayToSignature.lean +++ b/Complexity/Crypto/Computational/OneWayToSignature.lean @@ -148,7 +148,7 @@ theorem SignatureScheme.OneTimeEUFCMA.exists_oneWay {S : SignatureScheme} have hf : ComputableTidilyInPolyTime f encBits encBits := (ComputableTidilyInPolyTime.of_eq (encIn := encPair encUnary encBits) (encMid := encBits) fun _ => rfl).comp (hparam.prod hpk) - refine ⟨f, OneWay.of_inversion_negligible hf ?_⟩ + refine ⟨f, OneWay.of_inversion_negligible (.of_tidy hf) ?_⟩ intro adversary hadversary let forgerBody (n : ℕ) (pk : List Bool) : ProbComp (List Bool × List Bool) := do let size ← sampleDyadicIndex (schedule (n + 1)) diff --git a/Complexity/Crypto/Computational/PRGToOneWay.lean b/Complexity/Crypto/Computational/PRGToOneWay.lean index 9c9589725..fe347b472 100644 --- a/Complexity/Crypto/Computational/PRGToOneWay.lean +++ b/Complexity/Crypto/Computational/PRGToOneWay.lean @@ -148,7 +148,7 @@ theorem PseudorandomGenerator.oneWay_of_card_le {generator : List Bool → List (hgenerator : PseudorandomGenerator generator ℓ) {ε : ℕ → ℝ≥0} (hε : Negligible ε) (P : ℕ → Finset (List Bool)) (hP : ∀ n (x : List Bool), ℓ x.length = ℓ n → x ∈ P n) (hcard : ∀ n, (#(P n) : ℝ≥0) ≤ ε n * 2 ^ ℓ n) : OneWay generator := by - refine OneWay.of_inversion_negligible hgenerator.polyTime.tidy fun adversary hadversary => ?_ + refine OneWay.of_inversion_negligible hgenerator.polyTime fun adversary hadversary => ?_ have hind := hgenerator.indistinguishable (test generator adversary) (isPPT_test hgenerator.polyTime.tidy hadversary) refine negligible_of_le (hind.add_fun hε) fun n => ?_ diff --git a/ComplexityTests.lean b/ComplexityTests.lean index fbb107e50..3d5202fa5 100644 --- a/ComplexityTests.lean +++ b/ComplexityTests.lean @@ -118,6 +118,7 @@ import ComplexityTests.Crypto.KeyChainSecurity import ComplexityTests.Crypto.LeveledSecurity import ComplexityTests.Crypto.MAC import ComplexityTests.Crypto.MerkleDamgard +import ComplexityTests.Crypto.PlainConstructors import ComplexityTests.Crypto.SchnorrDiscreteLog import ComplexityTests.Crypto.SigmaIdentification import ComplexityTests.Crypto.SigmaProtocol diff --git a/ComplexityTests/Crypto/PlainConstructors.lean b/ComplexityTests/Crypto/PlainConstructors.lean new file mode 100644 index 000000000..da31e0633 --- /dev/null +++ b/ComplexityTests/Crypto/PlainConstructors.lean @@ -0,0 +1,32 @@ +/- +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.PRGToOneWay + +/-! Public cryptographic constructors accept ordinary deterministic certificates. -/ + +open Cslib Cslib.Crypto Cslib.Probability Turing.MultiTapeTM + +example {f : List Bool → List Bool} (hf : ComputableInPolyTime f encBits encBits) + (hnegligible : ∀ adversary : Inverter, IsPPT encBits adversary → + Negligible (fun n => Game.succProbability (ProbComp.eval (inversionGame f adversary n)))) : + OneWay f := OneWay.of_inversion_negligible hf hnegligible + +-- The real reduction uses the PRG's existing plain field, without a public tidy conversion. +example {generator : List Bool → List Bool} {length : ℕ → ℕ} + (hgenerator : PseudorandomGenerator generator length) (hdouble : ∀ n, 2 * n ≤ length n) : + OneWay generator := hgenerator.oneWay hdouble + +-- Both the unary parameter and arbitrary sample word are part of the certified input. +example {X Y : ℕ → PMF (List Bool)} (h : ComputationallyIndistinguishable X Y) : + ComputationallyIndistinguishable (fun n => (X n).map (fun word => word.take n)) + (fun n => (Y n).map (fun word => word.take n)) := + h.map (by polytime) + +/-- info: 'Cslib.Crypto.OneWay.of_inversion_negligible' depends on axioms: +[propext, Classical.choice, Quot.sound] -/ +#guard_msgs (whitespace := lax) in +#print axioms OneWay.of_inversion_negligible From 7b2231d4bbb15a227411aedf7c7ef9be86e801ce Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 24 Oct 2026 03:11:46 -0400 Subject: [PATCH 2/3] Adapt commitment and abstract bridge proof clients --- Complexity/Crypto/Computational/Commitment.lean | 3 ++- abstracts/ComplexityAbstracts/CryptographyBridge.lean | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/Complexity/Crypto/Computational/Commitment.lean b/Complexity/Crypto/Computational/Commitment.lean index 600602773..4057c1dcc 100644 --- a/Complexity/Crypto/Computational/Commitment.lean +++ b/Complexity/Crypto/Computational/Commitment.lean @@ -182,7 +182,8 @@ theorem PseudorandomGenerator.naorCommit_indistinguishable_uniform (fun p : ℕ × List Bool => naorCommit id (r p.1) (b p.1) p.2) (encPair encUnary encBits) encBits := by apply computableTidilyInPolyTime_naorCommit <;> fun_prop - have hind := hG.indistinguishable.map (f := fun n y => naorCommit id (r n) (b n) y) hmap + have hind := hG.indistinguishable.map (f := fun n y => naorCommit id (r n) (b n) y) + (.of_tidy hmap) simpa only [← naorCommitEnsemble_eq_map, uniformList_map_naorCommit_id] using hind /-- **Computational hiding of Naor bit commitment (deterministic-family formulation).** diff --git a/abstracts/ComplexityAbstracts/CryptographyBridge.lean b/abstracts/ComplexityAbstracts/CryptographyBridge.lean index d881262fa..bca0b76ed 100644 --- a/abstracts/ComplexityAbstracts/CryptographyBridge.lean +++ b/abstracts/ComplexityAbstracts/CryptographyBridge.lean @@ -125,7 +125,7 @@ def OneWay (f : List Bool → List Bool) : Prop := theorem oneWay_iff {f : List Bool → List Bool} : OneWay f ↔ Crypto.OneWay f := by constructor · rintro ⟨hf, hsecure⟩ - apply Crypto.OneWay.of_inversion_negligible (polyTime_iff.mp hf) + apply Crypto.OneWay.of_inversion_negligible (.of_tidy (polyTime_iff.mp hf)) intro adversary ha have h := hsecure (fun n word => ProbComp.eval (adversary n word)) (strictPPT_iff.mpr ⟨fun p => adversary p.1 p.2, ha, fun _ => rfl⟩) From f56fac6db89f255fd35ef7499f601699a6ac610a Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 24 Oct 2026 04:43:33 -0400 Subject: [PATCH 3/3] chore(crypto): regenerate lowered constructor tidy baseline --- scripts/tidy_surface_baseline.json | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/scripts/tidy_surface_baseline.json b/scripts/tidy_surface_baseline.json index adec39e90..335542ed6 100644 --- a/scripts/tidy_surface_baseline.json +++ b/scripts/tidy_surface_baseline.json @@ -335,7 +335,6 @@ "Complexity/Computability/TreeEval/Space.lean": 2, "Complexity/Computability/USTCON/Reader/Cert.lean": 3, "Complexity/Computability/USTCON/Space.lean": 1, - "Complexity/Crypto/Computational/Basic.lean": 1, "Complexity/Crypto/Computational/Commitment.lean": 13, "Complexity/Crypto/Computational/Encryption/PolyTime.lean": 2, "Complexity/Crypto/Computational/GGM/Evaluation.lean": 3, @@ -376,7 +375,7 @@ "Complexity/Crypto/Computational/Homomorphic/Leveled/Security.lean": 3, "Complexity/Crypto/Computational/Hybrid/SavedPrediction.lean": 6, "Complexity/Crypto/Computational/Hybrid/Sequence.lean": 4, - "Complexity/Crypto/Computational/OneWay.lean": 4, + "Complexity/Crypto/Computational/OneWay.lean": 3, "Complexity/Crypto/Computational/OneWay/BPP.lean": 1, "Complexity/Crypto/Computational/OneWay/MCSP.lean": 6, "Complexity/Crypto/Computational/OneWay/NP.lean": 6,