feat(crypto): Schnorr identification under the discrete-logarithm assumption

Complexity.lean

@@ -903,6 +903,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Poly
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Fin
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Gcd
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Log
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.PowMod
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Prime
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Search
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Option
@@ -1287,6 +1288,8 @@ public import Complexity.Computability.WordRAM.Time
 public import Complexity.Computability.WordRAM.Trace
 public import Complexity.Crypto.Computational.Basic
 public import Complexity.Crypto.Computational.Commitment
+public import Complexity.Crypto.Computational.DiscreteLog
+public import Complexity.Crypto.Computational.DiscreteLog.SchnorrGroup
 public import Complexity.Crypto.Computational.Encryption.Basic
 public import Complexity.Crypto.Computational.Encryption.Circular
 public import Complexity.Crypto.Computational.Encryption.PolyTime
@@ -1425,6 +1428,7 @@ public import Complexity.Crypto.Computational.PseudorandomFunction
 public import Complexity.Crypto.Computational.PseudorandomFunction.RandomOracle
 public import Complexity.Crypto.Computational.PseudorandomFunction.TruthTable
 public import Complexity.Crypto.Computational.PseudorandomGenerator
+public import Complexity.Crypto.Computational.SchnorrIdentification
 public import Complexity.Crypto.Computational.Signature
 public import Complexity.Crypto.Computational.Stretch
 public import Complexity.Crypto.Computational.Stretch.Quantitative

Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/PowMod.lean

@@ -0,0 +1,120 @@
+/-
+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.Computability.Machines.Turing.MultiTape.Encodings.Nat
+public import Complexity.Computability.Machines.Turing.MultiTape.PolyTime
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.BinaryDiv
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
+import Complexity.Foundations.Data.BitString.List.Binary
+import Complexity.Tactic.PolyTime.Init
+import Mathlib.Data.ZMod.Basic
+
+/-!
+# Polynomial-time modular exponentiation
+
+Square-and-multiply computes `a ^ e % m` on binary naturals with a positive modulus. It folds over
+the exponent's binary digits from the most significant one, squaring the accumulator and
+multiplying by `a` at each `1` digit, reducing modulo `m` after every product. Every intermediate
+value is below `m`, so the work is polynomial in the lengths of `a`, `e` and `m`.
+
+Without a modulus, `a ^ e` has about `e` times as many digits as `a`, exponentially many in the
+length of `e`; the statement therefore requires a positive modulus.
+
+## Main results
+
+* `Turing.MultiTapeTM.ComputableInPolyTime.binary_powMod`: modular exponentiation of computed
+  binary values with a positive modulus.
+
+## References
+
+* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09]
+-/
+
+public section
+
+namespace Turing.MultiTapeTM
+
+namespace BinaryPowMod
+
+/-- One square-and-multiply step modulo `m` for the base `a`: square the accumulator, and
+multiply by `a` when the next exponent digit, most significant first, is `1`. -/
+private def step (par : ℕ × ℕ) (acc : ℕ) (bit : Bool) : ℕ :=
+  acc * acc % par.2 * (if bit then par.1 else 1) % par.2
+
+/-- Folding `step` over a most-significant-first word computes the power of its value. -/
+private theorem foldl_step (a m : ℕ) (word : List Bool) :
+    word.foldl (step (a, m)) (1 % m) = a ^ Cslib.BitString.binaryValue word % m := by
+  induction word using List.reverseRecOn with
+  | nil => simp [Cslib.BitString.binaryValue]
+  | append_singleton word bit ih =>
+    rw [List.foldl_append, List.foldl_cons, List.foldl_nil, ih,
+      Cslib.BitString.binaryValue_snoc, step, ← ZMod.natCast_eq_natCast_iff']
+    cases bit <;> simp only [Nat.cast_mul, ZMod.natCast_mod, Nat.cast_pow, Bool.toNat_false,
+      Bool.toNat_true, Bool.false_eq_true, ite_false, ite_true, pow_add, pow_mul, add_zero, pow_one,
+      mul_one] <;> ring
+
+/-- The exponent's digits, most significant first, give `a ^ e % m`. -/
+private theorem powMod_eq (a e m : ℕ) :
+    e.bits.reverse.foldl (step (a, m)) (1 % m) = a ^ e % m := by
+  rw [foldl_step, Cslib.BitString.binaryValue_reverse_bits]
+
+/-- Modular exponentiation with the modulus `m + 1`, which is positive. -/
+private theorem computableTidilyInPolyTime_powMod_succ :
+    ComputableTidilyInPolyTime (fun p : ℕ × ℕ × ℕ => p.1 ^ p.2.1 % (p.2.2 + 1))
+      (encPair encNat (encPair encNat encNat)) encNat := by
+  have hpar : ComputableTidilyInPolyTime (fun p : ℕ × ℕ × ℕ => (p.1, p.2.2 + 1))
+      (encPair encNat (encPair encNat encNat)) (encPair encNat encNat) := by
+    fun_prop
+  have hlist : ComputableTidilyInPolyTime (fun p : ℕ × ℕ × ℕ => p.2.1.bits.reverse)
+      (encPair encNat (encPair encNat encNat)) encBits := by
+    fun_prop
+  have hinit : ComputableTidilyInPolyTime (fun p : ℕ × ℕ × ℕ => 1 % (p.2.2 + 1))
+      (encPair encNat (encPair encNat encNat)) encNat := by
+    fun_prop
+  have hstep : ComputableTidilyInPolyTime
+      (fun q : ((ℕ × ℕ) × ℕ) × Bool => step q.1.1 q.1.2 q.2)
+      (encPair (encPair (encPair encNat encNat) encNat) encBool) encNat := by
+    unfold step
+    fun_prop
+  have hfold := ComputableTidilyInPolyTime.foldlWith (encP := encPair encNat encNat)
+    (encA := encBool) (encL := encBits) (encB := encNat) hpar hlist hinit hstep
+    (B := fun p => (encPair encNat (encPair encNat encNat) p).length)
+    (PolyBounded.self)
+    (fun p i _ => by
+      rw [foldl_step]
+      have hle : p.1 ^ Cslib.BitString.binaryValue (p.2.1.bits.reverse.take i) % (p.2.2 + 1) ≤
+          p.2.2 := Nat.lt_succ_iff.mp (Nat.mod_lt _ (Nat.succ_pos _))
+      calc (encNat _).length ≤ (encNat p.2.2).length := by
+            simp only [encNat_apply]
+            rw [Nat.size_eq_bits_len, Nat.size_eq_bits_len]
+            exact Nat.size_le_size hle
+        _ ≤ (encPair encNat encNat p.2).length := length_le_encPair_right encNat encNat p.2
+        _ ≤ (encPair encNat (encPair encNat encNat) p).length :=
+          length_le_encPair_right encNat (encPair encNat encNat) p)
+  simpa only [powMod_eq] using hfold
+
+end BinaryPowMod
+
+/-- **Modular exponentiation** of computed binary values with a positive modulus, by
+square-and-multiply. -/
+theorem ComputableInPolyTime.binary_powMod {α : Type} {input : α ↪ List Bool}
+    {base exponent modulus : α → ℕ} (hbase : ComputableInPolyTime base input encNat)
+    (hexponent : ComputableInPolyTime exponent input encNat)
+    (hmodulus : ComputableInPolyTime modulus input encNat) (hpos : ∀ a, 0 < modulus a) :
+    ComputableInPolyTime (fun a => base a ^ exponent a % modulus a) input encNat := by
+  have hpred : ComputableTidilyInPolyTime (fun a => modulus a - 1) input encNat :=
+    ComputableTidilyInPolyTime.binary_sub' hmodulus.tidy (ComputableTidilyInPolyTime.const 1)
+  have hcomp := BinaryPowMod.computableTidilyInPolyTime_powMod_succ.comp
+    (hbase.tidy.prod (hexponent.tidy.prod hpred))
+  refine ComputableInPolyTime.of_tidy ?_
+  simpa only [Function.comp_def, Nat.sub_add_cancel (hpos _)] using hcomp
+
+end Turing.MultiTapeTM
+
+end

Complexity/Crypto/Computational/DiscreteLog.lean

@@ -0,0 +1,146 @@
+/-
+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.Computability.Machines.Turing.MultiTape.Encodings.Decoder
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Pair
+public import Complexity.Computability.Machines.Turing.MultiTape.PolyTime
+public import Complexity.Computability.Probabilistic.PPT
+public import Complexity.Crypto.Game
+public import Mathlib.Algebra.Field.ZMod
+public import Mathlib.Algebra.Module.Defs
+import Complexity.Probability.PMF
+
+/-!
+# The discrete-logarithm assumption
+
+A `PrimeOrderGroupFamily` is a family of cyclic groups of prime order, indexed by public
+descriptions such as `(p, q, g)` for the subgroup of order `q` of `(ZMod p)ˣ` generated by `g`.
+Groups are written additively, as `ZMod q`-modules, so the book's `g ^ α` is `α • g`. Algorithms
+see a group through its description and the words encoding its elements. The family supplies
+exactly the operations that algorithms using it need, as plain polynomial-time functions of the
+description and the encoded operands: the order, the encoded generator, addition, and
+multiplication by a natural number.
+
+The discrete-logarithm experiment ([BonehShoup2023], Attack Game 10.4) draws a description from a
+setup law, a uniform `α : ZMod q` and gives the adversary the description and the encoding of
+`α • g`; the adversary wins when the binary number it outputs is `α` modulo `q`. `DiscreteLog`
+asserts that every uniform strict PPT adversary wins with negligible probability.
+
+As for `DecisionLWE`, this is a hypothesis, not a theorem. The setup law is arbitrary and is not
+claimed to be efficiently sampleable: generating primes with certainty is not a strict PPT task,
+since a fair-coin machine with a fixed clock fails with positive probability. Descriptions are
+public, and an adversary's running time may depend on their length.
+
+## Main definitions
+
+* `Cslib.Crypto.PrimeOrderGroupFamily`: cyclic groups of prime order with efficient operations.
+* `Cslib.Crypto.PrimeOrderGroupFamily.discreteLogGame`: the discrete-logarithm experiment.
+* `Cslib.Crypto.PrimeOrderGroupFamily.DiscreteLog`: the discrete-logarithm assumption.
+
+## Main results
+
+* `Cslib.Crypto.PrimeOrderGroupFamily.smul_generator_injective`: a discrete logarithm modulo `q`
+  is unique.
+
+## References
+
+* [D. Boneh, V. Shoup, *A Graduate Course in Applied Cryptography*,
+  Version 0.6][BonehShoup2023], Section 10.5.
+-/
+
+@[expose] public section
+
+namespace Cslib.Crypto
+
+open Probability Turing.MultiTapeTM
+
+/-- A family of cyclic groups of prime order, indexed by public descriptions, with
+polynomial-time operations on encoded elements. -/
+structure PrimeOrderGroupFamily where
+  /-- Public descriptions of the groups. -/
+  Desc : Type
+  /-- The encoding of descriptions given to algorithms. -/
+  encDesc : Desc ↪ List Bool
+  /-- The order of each group. -/
+  order : Desc → ℕ
+  /-- Every order is prime. -/
+  prime_order : ∀ d, (order d).Prime
+  /-- The groups, written additively. -/
+  Carrier : Desc → Type
+  /-- Each group is commutative. -/
+  [addCommGroup : ∀ d, AddCommGroup (Carrier d)]
+  /-- Each group is a `ZMod q`-module, where `q` is its order. -/
+  [module : ∀ d, Module (ZMod (order d)) (Carrier d)]
+  /-- The generator of each group. -/
+  generator : ∀ d, Carrier d
+  /-- Each group has `q` elements. -/
+  card_carrier : ∀ d, Nat.card (Carrier d) = order d
+  /-- The generator is not the identity, so it generates the group of prime order. -/
+  generator_ne_zero : ∀ d, generator d ≠ 0
+  /-- Group elements as words. -/
+  encode : ∀ d, Carrier d → List Bool
+  /-- Distinct elements have distinct encodings. -/
+  encode_injective : ∀ d, Function.Injective (encode d)
+  /-- Addition of encoded elements. -/
+  add : Desc × List Bool × List Bool → List Bool
+  /-- `add` adds encoded elements. -/
+  add_encode : ∀ d x y, add (d, encode d x, encode d y) = encode d (x + y)
+  /-- Multiplication of an encoded element by a natural number. -/
+  smul : Desc × ℕ × List Bool → List Bool
+  /-- `smul` multiplies encoded elements by natural numbers. -/
+  smul_encode : ∀ d (a : ℕ) x, smul (d, a, encode d x) = encode d ((a : ZMod (order d)) • x)
+  /-- The order is computable in polynomial time from the description. -/
+  computableInPolyTime_order : ComputableInPolyTime order encDesc encNat
+  /-- The encoded generator is computable in polynomial time from the description. -/
+  computableInPolyTime_generator :
+    ComputableInPolyTime (fun d => encode d (generator d)) encDesc encBits
+  /-- Addition is computable in polynomial time. -/
+  computableInPolyTime_add :
+    ComputableInPolyTime add (encPair encDesc (encPair encBits encBits)) encBits
+  /-- Multiplication by a binary natural number is computable in polynomial time. -/
+  computableInPolyTime_smul :
+    ComputableInPolyTime smul (encPair encDesc (encPair encNat encBits)) encBits
+
+namespace PrimeOrderGroupFamily
+
+variable (F : PrimeOrderGroupFamily)
+
+attribute [instance] addCommGroup module
+
+instance (d : F.Desc) : Fact (F.order d).Prime := ⟨F.prime_order d⟩
+
+instance (d : F.Desc) : NeZero (F.order d) := ⟨(F.prime_order d).ne_zero⟩
+
+/-- A discrete logarithm modulo `q` is unique: `α ↦ α • g` is injective. -/
+theorem smul_generator_injective (d : F.Desc) :
+    Function.Injective fun α : ZMod (F.order d) => α • F.generator d :=
+  smul_left_injective (ZMod (F.order d)) (F.generator_ne_zero d)
+
+/-- The discrete-logarithm experiment ([BonehShoup2023], Attack Game 10.4): draw a description
+and a uniform `α`, give the adversary the description and the encoding of `α • g`, and accept
+when the binary number it outputs is `α` modulo `q`. -/
+noncomputable def discreteLogGame (setup : ℕ → PMF F.Desc)
+    (adversary : ℕ → F.Desc × List Bool → ProbComp (List Bool)) (n : ℕ) : Game := do
+  let d ← setup n
+  let α ← PMF.uniformOfFintype (ZMod (F.order d))
+  let guess ← ProbComp.eval (adversary n (d, F.encode d (α • F.generator d)))
+  return decide ((ofBits guess : ZMod (F.order d)) = α)
+
+/-- The discrete-logarithm assumption for a family and a setup law: every uniform strict PPT
+adversary, given the unary security parameter, the description and the encoded instance, finds
+the discrete logarithm with negligible probability. This is a hypothesis, not a theorem. -/
+def DiscreteLog (setup : ℕ → PMF F.Desc) : Prop :=
+  ∀ adversary : ℕ → F.Desc × List Bool → ProbComp (List Bool),
+    IsPPTOn (encPair encUnary (encPair F.encDesc encBits)) encBits
+      (fun input => adversary input.1 input.2) →
+    Negligible fun n => Game.succProbability (F.discreteLogGame setup adversary n)
+
+end PrimeOrderGroupFamily
+
+end Cslib.Crypto