feat(crypto): exact security of Schnorr signatures with δ = 1/q (#581 3b-ii, part 1)

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

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

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]

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.