From 2e5d6edeb3c2dc1d9317b329092ec90a6aa86bc3 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 23:02:34 -0400 Subject: [PATCH] feat(crypto): exact security of Schnorr signatures MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit With a nonzero base in a vector space of prime order `q`, Schnorr commitments are `1 / q`-unpredictable (`schnorr_commit_map_fst_le`). The Fiat-Shamir theorem then bounds a forger making `Qs` signing and `Qro` hash calls by `Qs · (Qs + Qro) / q + (Qro + 1) / N + √((Qro + 1) · ε')` (`schnorr_succProbability_eufCmaGame_le`, Boneh-Shoup Theorem 19.7 with Equation 19.21). The `ZMod 11` test now uses this corollary. Refs #581 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- Complexity.lean | 1 + .../SigmaProtocol/SchnorrSignature.lean | 100 ++++++++++++++++++ ComplexityTests/Crypto/FiatShamir.lean | 36 +++---- ROADMAP.md | 4 +- 4 files changed, 119 insertions(+), 22 deletions(-) create mode 100644 Complexity/Crypto/Protocols/SigmaProtocol/SchnorrSignature.lean diff --git a/Complexity.lean b/Complexity.lean index e4af55a60..ab4317679 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1483,6 +1483,7 @@ public import Complexity.Crypto.Protocols.SigmaProtocol.FiatShamir public import Complexity.Crypto.Protocols.SigmaProtocol.Identification public import Complexity.Crypto.Protocols.SigmaProtocol.Linear public import Complexity.Crypto.Protocols.SigmaProtocol.SchnorrIdentification +public import Complexity.Crypto.Protocols.SigmaProtocol.SchnorrSignature public import Complexity.Crypto.Protocols.Signature.RandomOracle public import Complexity.Foundations.Analysis.HarmonicMean public import Complexity.Foundations.Analysis.MarkovInequality diff --git a/Complexity/Crypto/Protocols/SigmaProtocol/SchnorrSignature.lean b/Complexity/Crypto/Protocols/SigmaProtocol/SchnorrSignature.lean new file mode 100644 index 000000000..e01cdce80 --- /dev/null +++ b/Complexity/Crypto/Protocols/SigmaProtocol/SchnorrSignature.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.Protocols.SigmaProtocol.FiatShamir +public import Complexity.Crypto.Protocols.SigmaProtocol.SchnorrIdentification +import Complexity.Probability.PMF + +/-! +# Schnorr signatures + +Schnorr signatures ([BonehShoup2023], Section 19.2) are the Fiat–Shamir signatures of Schnorr's +Sigma protocol. Over a vector space of prime order `q` with a nonzero base `g`, the commitment +`r • g` of a uniform `r` takes each value with probability at most `1 / q` +(`schnorr_commit_map_fst_le`). The Fiat–Shamir theorem then bounds the success of a forger making +at most `Qs` signing calls and `Qro` hash calls by + +`Qs · (Qs + Qro) / q + (Qro + 1) / N + √((Qro + 1) · ε')`, + +where `N` is the number of challenges and `ε'` the probability that the forking reduction computes +a discrete logarithm of the public key (`schnorr_succProbability_eufCmaGame_le`, +[BonehShoup2023], Theorem 19.7 with Equation 19.21). These are exact laws for one group and one +forger; the computational statement under the discrete-logarithm assumption is separate. + +## Main results + +* `Cslib.Crypto.Protocols.SigmaProtocol.schnorr_commit_map_fst_le`: Schnorr commitments are + `1 / q`-unpredictable. +* `Cslib.Crypto.Protocols.SigmaProtocol.schnorr_succProbability_eufCmaGame_le`: the security + bound for Schnorr signatures in the random-oracle model. + +## References + +* [D. Boneh, V. Shoup, *A Graduate Course in Applied Cryptography*, + Version 0.6][BonehShoup2023], Section 19.2. +* [C.-P. Schnorr, *Efficient Signature Generation by Smart Cards*][Schnorr1991] +-/ + +@[expose] public section + +namespace Cslib.Crypto.Protocols.SigmaProtocol + +open Probability ROMSignature +open scoped ENNReal NNReal + +variable {q : ℕ} [Fact q.Prime] {G C : Type} [AddCommGroup G] [Module (ZMod q) G] [DecidableEq G] + {ι : C ↪ ZMod q} {g : G} + +/-- **Unpredictable Schnorr commitments** ([BonehShoup2023], Definition 19.7): with a nonzero base, +the commitment `r • g` of a uniform `r` takes each value with probability at most `1 / q`. -/ +theorem schnorr_commit_map_fst_le (hg : g ≠ 0) (x : ZMod q) (y t : G) : + ((schnorr ι g).commit x y).map Prod.fst t ≤ (q : ℝ≥0∞)⁻¹ := by + classical + have hinj : Function.Injective fun r : ZMod q => r • g := fun r r' h => by + have h' : (r - r') • g = 0 := by rw [sub_smul]; exact sub_eq_zero.mpr h + exact sub_eq_zero.mp ((smul_eq_zero.mp h').resolve_right hg) + have hmap : ((schnorr ι g).commit x y).map Prod.fst = + (PMF.uniformOfFintype (ZMod q)).map fun r => r • g := by + simp only [schnorr, linear, PMF.map_comp] + rfl + rw [hmap, ← PMF.toOuterMeasure_apply_singleton, PMF.toOuterMeasure_map_apply, + Probability.PMF.toOuterMeasure_uniformOfFintype, ZMod.card] + calc ((Finset.univ.filter (· ∈ (fun r : ZMod q => r • g) ⁻¹' {t})).card : ℝ≥0∞) * + (q : ℝ≥0∞)⁻¹ + ≤ 1 * (q : ℝ≥0∞)⁻¹ := by + gcongr + exact_mod_cast Finset.card_le_one.mpr fun a ha b hb => + hinj (by simp_all) + _ = (q : ℝ≥0∞)⁻¹ := one_mul _ + +variable [Fintype C] [Nonempty C] [DecidableEq C] {M : Type} [DecidableEq M] + +/-- **Security of Schnorr signatures** ([BonehShoup2023], Theorem 19.7 with Equation 19.21, exact +form): with a nonzero base, a forger making at most `Qs` signing calls and `Qro` hash calls +succeeds with probability at most `Qs · (Qs + Qro) / q + (Qro + 1) / N + √((Qro + 1) · ε')`, where +`N` is the number of challenges and `ε'` the probability that the forking reduction computes a +discrete logarithm of the public key. -/ +theorem schnorr_succProbability_eufCmaGame_le (hg : g ≠ 0) + (A : Forger G M (G × ZMod q) (M × G) C) {Qs Qro : ℕ} (hA : A.CallBounded Qs Qro) : + (Game.succProbability (eufCmaGame (fiatShamir (schnorr ι g) (schnorrKeyGen g)) A) : ℝ) ≤ + Qs * (Qs + Qro) / q + (Qro + 1) / Fintype.card C + + √((Qro + 1) * Game.succProbability (oneWayGame (schnorrKeyGen g) + (fun α u => α • g = u) (FiatShamir.reduction (schnorr ι g) + (linearSimulate (fun _ => LinearMap.toSpanSingleton (ZMod q) G g) id ι) + (linearExtract ι) A Qs Qro))) := by + have hq : (q : ℝ≥0) ≠ 0 := by exact_mod_cast (Fact.out : q.Prime).ne_zero + have h := succProbability_eufCmaGame_le (P := schnorr ι g) (δ := (q : ℝ≥0)⁻¹) + (fun _ h => mem_support_schnorrKeyGen h) + (schnorr_specialSoundness.specialSoundOn (schnorrKeyGen g)) schnorr_specialHVZK + (fun key _ t => by + rw [ENNReal.coe_inv hq, ENNReal.coe_natCast] + exact schnorr_commit_map_fst_le (ι := ι) hg key.1 key.2 t) A hA + rwa [NNReal.coe_inv, NNReal.coe_natCast, ← div_eq_mul_inv] at h + +end Cslib.Crypto.Protocols.SigmaProtocol diff --git a/ComplexityTests/Crypto/FiatShamir.lean b/ComplexityTests/Crypto/FiatShamir.lean index 9b2afad59..555bb273f 100644 --- a/ComplexityTests/Crypto/FiatShamir.lean +++ b/ComplexityTests/Crypto/FiatShamir.lean @@ -6,6 +6,7 @@ Authors: Samuel Schlesinger import Complexity.Crypto.Protocols.SigmaProtocol.FiatShamir import Complexity.Crypto.Protocols.SigmaProtocol.SchnorrIdentification +import Complexity.Crypto.Protocols.SigmaProtocol.SchnorrSignature import Complexity.Probability.PMF import Mathlib.Tactic.LinearCombination import Mathlib.Tactic.NormNum.Prime @@ -14,10 +15,10 @@ import Mathlib.Tactic.NormNum.Prime # Tests for Fiat–Shamir signatures Schnorr signatures in `ZMod 11`, with base `2`, are Fiat–Shamir signatures from Schnorr's -protocol: honest signatures verify, and the commitments are `1 / 11`-unpredictable. Discrete -logarithms are easy here: a forger that computes the witness and signs a message honestly, with -one hash call, always wins, so the security theorem makes the reduction compute discrete -logarithms with probability at least `81 / 242`. +protocol, and honest signatures verify. Discrete logarithms are easy here: a forger that computes +the witness and signs a message honestly, with one hash call, always wins, so the security +theorem for Schnorr signatures makes the reduction compute discrete logarithms with probability +at least `81 / 242`. -/ namespace ComplexityTests.Crypto.FiatShamir @@ -38,18 +39,6 @@ noncomputable abbrev scheme := example : scheme.Correct := fiatShamir_correct schnorr_complete fun _ h => mem_support_schnorrKeyGen h -/-- Schnorr commitments in `ZMod 11` with base `2` are `1 / 11`-unpredictable: the commitment -`r • 2` of a uniform `r` is uniform. -/ -theorem commit_unpredictable (key : ZMod 11 × ZMod 11) (t : ZMod 11) : - ((schnorr ι (2 : ZMod 11)).commit key.1 key.2).map Prod.fst t ≤ ((11 : ℝ≥0)⁻¹ : ℝ≥0) := by - have h2 : (2 : ZMod 11) ≠ 0 := by decide - have hmap : ((schnorr ι (2 : ZMod 11)).commit key.1 key.2).map Prod.fst = - (PMF.uniformOfFintype (ZMod 11)).map (Equiv.mulRight₀ (2 : ZMod 11) h2) := by - simp only [schnorr, linear, PMF.map_comp] - rfl - rw [hmap, PMF.uniformOfFintype_map_equiv, PMF.uniformOfFintype_apply, ZMod.card] - simp - /-- The forger that computes the witness `6 • u` of `u` and signs `true` honestly, with one hash call. -/ noncomputable def knower : Forger (ZMod 11) Bool (ZMod 11 × ZMod 11) (Bool × ZMod 11) (ZMod 11) @@ -112,10 +101,8 @@ example : (81 / 242 : ℝ) ≤ Game.succProbability (oneWayGame (schnorrKeyGen ( (FiatShamir.reduction (schnorr ι (2 : ZMod 11)) (linearSimulate (fun _ => LinearMap.toSpanSingleton (ZMod 11) (ZMod 11) 2) id ι) (linearExtract ι) knower 0 1)) := by - have h := succProbability_eufCmaGame_le (δ := 11⁻¹) - (fun _ h => mem_support_schnorrKeyGen h) - ((schnorr_specialSoundness (ι := ι) (g := (2 : ZMod 11))).specialSoundOn (schnorrKeyGen 2)) - schnorr_specialHVZK (fun key _ t => commit_unpredictable key t) knower knower_callBounded + have h := schnorr_succProbability_eufCmaGame_le (ι := ι) (g := (2 : ZMod 11)) (by decide) + knower knower_callBounded have hknower : Game.succProbability (eufCmaGame (fiatShamir (M := Bool) (schnorr ι (2 : ZMod 11)) (schnorrKeyGen 2)) knower) = 1 := succProbability_knower rw [hknower, ZMod.card] at h @@ -125,7 +112,7 @@ example : (81 / 242 : ℝ) ≤ Game.succProbability (oneWayGame (schnorrKeyGen ( (linearSimulate (fun _ => LinearMap.toSpanSingleton (ZMod 11) (ZMod 11) 2) id ι) (linearExtract ι) knower 0 1)) : ℝ) with hε have hε0 : 0 ≤ ε := NNReal.coe_nonneg _ - simp only [Nat.cast_zero, zero_mul, zero_add, Nat.cast_one, + simp only [Nat.cast_zero, zero_mul, zero_div, zero_add, Nat.cast_one, show (1 : ℝ) + 1 = 2 by norm_num] at h have hsqrt : (9 / 11 : ℝ) ≤ √(2 * ε) := by simp only [NNReal.coe_one, Nat.cast_ofNat] at h @@ -142,6 +129,13 @@ info: 'Cslib.Crypto.Protocols.SigmaProtocol.succProbability_eufCmaGame_le' depen #guard_msgs (whitespace := lax) in #print axioms succProbability_eufCmaGame_le +/-- +info: 'Cslib.Crypto.Protocols.SigmaProtocol.schnorr_succProbability_eufCmaGame_le' depends on +axioms: [propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms schnorr_succProbability_eufCmaGame_le + /-- info: 'Cslib.Crypto.Protocols.SigmaProtocol.fiatShamir_correct' depends on axioms: [propext, Classical.choice, Quot.sound] diff --git a/ROADMAP.md b/ROADMAP.md index 47a932bf8..55247d45e 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -1196,7 +1196,9 @@ Jukna coverage below is an additional target beyond the V1 port: correct and, exactly, EUF-CMA secure with the bound `Qs · (Qs + Qro) · δ + (Qro + 1)/N + √((Qro + 1) · ε')` of Theorem 19.16 and Equation 19.21, by the - [difference lemma](Complexity/Languages/Probabilistic/UntilBad.lean), presampling and forking. + [difference lemma](Complexity/Languages/Probabilistic/UntilBad.lean), presampling and forking; + [Schnorr signatures](Complexity/Crypto/Protocols/SigmaProtocol/SchnorrSignature.lean) have + `1/q`-unpredictable commitments and the exact bound with `δ = 1/q`. Open (see #640): computational Schnorr signatures under discrete log for strict PPT forgers, and security against eavesdropping in the strict-PPT model, where simulating transcripts needs approximately uniform `ZMod q` samples and hence an explicit statistical-distance term.