From 1b210ba975ad4da10429404e4c9ffa2702019f0e Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 19:38:26 -0400 Subject: [PATCH 1/2] feat(crypto): Schnorr identification under the discrete-logarithm assumption Add a bundle of prime-order cyclic group families with plain polynomial-time operations, the discrete-logarithm assumption as a Prop hypothesis over an arbitrary setup law, the Schnorr-group instance (subgroups of prime order of (ZMod p)^x), and a plain certificate for binary modular exponentiation. Prove that Schnorr identification with k-bit challenges satisfies eps <= 1/2^k + sqrt eps' against direct attacks, where eps' is the DL success of an explicit rewinding adversary that is uniform strict PPT, and hence is secure under DL. Generalize the extraction theorems to special soundness on the generated statements. Refs #581. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- Complexity.lean | 4 + .../Complexity/PolyTime/Nat/PowMod.lean | 120 +++++++ .../Crypto/Computational/DiscreteLog.lean | 146 ++++++++ .../DiscreteLog/SchnorrGroup.lean | 228 ++++++++++++ .../Computational/SchnorrIdentification.lean | 337 ++++++++++++++++++ .../SigmaProtocol/Identification.lean | 57 +-- .../SigmaProtocol/SchnorrIdentification.lean | 2 +- ComplexityTests.lean | 1 + .../Crypto/SchnorrDiscreteLog.lean | 97 +++++ .../Crypto/SigmaIdentification.lean | 5 +- ROADMAP.md | 13 +- 11 files changed, 982 insertions(+), 28 deletions(-) create mode 100644 Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/PowMod.lean create mode 100644 Complexity/Crypto/Computational/DiscreteLog.lean create mode 100644 Complexity/Crypto/Computational/DiscreteLog/SchnorrGroup.lean create mode 100644 Complexity/Crypto/Computational/SchnorrIdentification.lean create mode 100644 ComplexityTests/Crypto/SchnorrDiscreteLog.lean diff --git a/Complexity.lean b/Complexity.lean index d76bc905b..9aca3243b 100644 --- a/Complexity.lean +++ b/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 diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/PowMod.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/PowMod.lean new file mode 100644 index 000000000..47e3d6d90 --- /dev/null +++ b/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 diff --git a/Complexity/Crypto/Computational/DiscreteLog.lean b/Complexity/Crypto/Computational/DiscreteLog.lean new file mode 100644 index 000000000..2fe3e9bc4 --- /dev/null +++ b/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 diff --git a/Complexity/Crypto/Computational/DiscreteLog/SchnorrGroup.lean b/Complexity/Crypto/Computational/DiscreteLog/SchnorrGroup.lean new file mode 100644 index 000000000..b2abfcbe5 --- /dev/null +++ b/Complexity/Crypto/Computational/DiscreteLog/SchnorrGroup.lean @@ -0,0 +1,228 @@ +/- +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.Computational.DiscreteLog +public import Mathlib.Algebra.Module.ZMod +public import Mathlib.Data.ZMod.Units +public import Mathlib.GroupTheory.OrderOfElement +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.BinaryDiv +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.PowMod +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain +import Complexity.Foundations.Data.Nat.Bits + +/-! +# Schnorr groups + +A Schnorr group is the subgroup of prime order `q` of `(ZMod p)ˣ`, for a prime `p`, generated by +a residue `g` of multiplicative order `q`. It is described by the triple `(p, q, g)` of binary +numbers, and its elements are encoded by the binary digits of their residues. Multiplication and +exponentiation are computed modulo `p`, by schoolbook multiplication and square-and-multiply. +These groups form a `PrimeOrderGroupFamily`, so the discrete-logarithm assumption and the +security theorems stated for such families apply to them. + +A description is valid when `p` and `q` are prime, `1 < g < p` and `g ^ q % p = 1`; these facts +imply that `g` has order `q` and that `q` divides `p - 1`. Validity is part of the description +type: algorithms receive only valid descriptions, and nothing here claims that valid descriptions +can be generated efficiently. + +## Main definitions + +* `Cslib.Crypto.SchnorrGroup.Valid`: valid descriptions `(p, q, g)`. +* `Cslib.Crypto.schnorrGroups`: Schnorr groups as a `PrimeOrderGroupFamily`. + +## References + +* [D. Boneh, V. Shoup, *A Graduate Course in Applied Cryptography*, + Version 0.6][BonehShoup2023], Section 10.4. +* [C.-P. Schnorr, *Efficient Signature Generation by Smart Cards*][Schnorr1991] +-/ + +@[expose] public section + +namespace Cslib.Crypto + +open Turing.MultiTapeTM + +namespace SchnorrGroup + +/-- A valid description `(p, q, g)` of a Schnorr group: `p` and `q` are prime, and the residue +`g` satisfies `1 < g < p` and `g ^ q ≡ 1 (mod p)`. -/ +structure Valid (d : ℕ × ℕ × ℕ) : Prop where + /-- The modulus is prime. -/ + prime_modulus : d.1.Prime + /-- The group order is prime. -/ + prime_order : d.2.1.Prime + /-- The generator is not `0` or `1`. -/ + one_lt_generator : 1 < d.2.2 + /-- The generator is a reduced residue. -/ + generator_lt : d.2.2 < d.1 + /-- The generator has order dividing `q`. -/ + generator_pow : d.2.2 ^ d.2.1 % d.1 = 1 + +/-- Valid Schnorr-group descriptions. -/ +abbrev Desc : Type := {d : ℕ × ℕ × ℕ // Valid d} + +/-- The generator as a unit modulo `p`. -/ +def generatorUnit (d : Desc) : (ZMod d.1.1)ˣ := + ZMod.unitOfCoprime d.1.2.2 ((Nat.coprime_comm.mp ((d.2.prime_modulus.coprime_iff_not_dvd).mpr + (Nat.not_dvd_of_pos_of_lt (by have := d.2.one_lt_generator; lia) d.2.generator_lt)))) + +/-- The Schnorr group of a description, written additively. -/ +abbrev Carrier (d : Desc) : Type := Additive (Subgroup.zpowers (generatorUnit d)) + +instance (d : Desc) : Fact d.1.2.1.Prime := ⟨d.2.prime_order⟩ + +/-- The generator has order dividing `q`. -/ +theorem generatorUnit_pow_order (d : Desc) : generatorUnit d ^ d.1.2.1 = 1 := by + ext + rw [Units.val_pow_eq_pow_val, generatorUnit, ZMod.coe_unitOfCoprime, Units.val_one, + ← Nat.cast_pow, ← ZMod.natCast_mod, d.2.generator_pow, Nat.cast_one] + +/-- Every element of the Schnorr group has order dividing `q`. -/ +theorem pow_order (d : Desc) (x : Subgroup.zpowers (generatorUnit d)) : x ^ d.1.2.1 = 1 := by + obtain ⟨k, hk⟩ := Subgroup.mem_zpowers_iff.mp x.2 + ext + rw [Subgroup.coe_pow, ← hk, ← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul, zpow_natCast, + generatorUnit_pow_order, one_zpow, Subgroup.coe_one] + +instance (d : Desc) : Module (ZMod d.1.2.1) (Carrier d) := + AddCommMonoid.zmodModule fun x => Additive.toMul.injective (by + rw [toMul_nsmul, pow_order, toMul_zero]) + +instance (d : Desc) : NeZero d.1.1 := ⟨d.2.prime_modulus.ne_zero⟩ + +/-- The generator is not the identity. -/ +theorem generatorUnit_ne_one (d : Desc) : generatorUnit d ≠ 1 := fun h => by + have hval := congrArg (fun u : (ZMod d.1.1)ˣ => (u : ZMod d.1.1).val) h + simp only [generatorUnit, ZMod.coe_unitOfCoprime, ZMod.val_natCast, + Nat.mod_eq_of_lt d.2.generator_lt, Units.val_one, + ZMod.val_one_eq_one_mod, Nat.mod_eq_of_lt d.2.prime_modulus.one_lt] at hval + exact absurd hval (ne_of_gt d.2.one_lt_generator) + +/-- The generator of the Schnorr group. -/ +def generator (d : Desc) : Carrier d := + Additive.ofMul ⟨generatorUnit d, Subgroup.mem_zpowers _⟩ + +/-- The Schnorr group has `q` elements. -/ +theorem card_carrier (d : Desc) : Nat.card (Carrier d) = d.1.2.1 := by + change Nat.card (Subgroup.zpowers (generatorUnit d)) = d.1.2.1 + rw [Nat.card_zpowers, orderOf_eq_prime (generatorUnit_pow_order d) (generatorUnit_ne_one d)] + +/-- The generator is not the identity of the Schnorr group. -/ +theorem generator_ne_zero (d : Desc) : generator d ≠ 0 := fun h => + generatorUnit_ne_one d (congrArg (fun x : Carrier d => ((Additive.toMul x : + Subgroup.zpowers (generatorUnit d)) : (ZMod d.1.1)ˣ)) h) + +/-- Elements are encoded by the binary digits of their residues modulo `p`. -/ +def encode (d : Desc) (x : Carrier d) : List Bool := + ((((Additive.toMul x : Subgroup.zpowers (generatorUnit d)) : (ZMod d.1.1)ˣ) : + ZMod d.1.1).val).bits + +/-- Distinct elements have distinct encodings. -/ +theorem encode_injective (d : Desc) : Function.Injective (encode d) := fun _ _ h => + Additive.toMul.injective (Subtype.ext (Units.ext (ZMod.val_injective _ + (encNat.injective h)))) + +/-- Reading back binary digits. -/ +private theorem ofBits_bits (n : ℕ) : ofBits n.bits = n := Nat.foldr_bit_bits n + +/-- Multiplication modulo `p` of encoded residues. -/ +def add (input : Desc × List Bool × List Bool) : List Bool := + (ofBits input.2.1 * ofBits input.2.2 % input.1.1.1).bits + +/-- `add` multiplies encoded group elements. -/ +theorem add_encode (d : Desc) (x y : Carrier d) : + add (d, encode d x, encode d y) = encode d (x + y) := by + simp only [add, encode, ofBits_bits, toMul_add, Subgroup.coe_mul, Units.val_mul, ZMod.val_mul] + +/-- Exponentiation modulo `p` of an encoded residue. -/ +def smul (input : Desc × ℕ × List Bool) : List Bool := + (ofBits input.2.2 ^ input.2.1 % input.1.1.1).bits + +/-- `smul` raises encoded group elements to natural powers. -/ +theorem smul_encode (d : Desc) (a : ℕ) (x : Carrier d) : + smul (d, a, encode d x) = encode d ((a : ZMod d.1.2.1) • x) := by + rw [Nat.cast_smul_eq_nsmul] + simp only [smul, encode, ofBits_bits, toMul_nsmul, Subgroup.coe_pow, Units.val_pow_eq_pow_val] + rw [← ZMod.val_natCast, Nat.cast_pow, ZMod.natCast_zmod_val] + +/-- The encoded generator is the binary digits of `g`. -/ +theorem encode_generator (d : Desc) : encode d (generator d) = d.1.2.2.bits := by + change (((generatorUnit d : (ZMod d.1.1)ˣ) : ZMod d.1.1).val).bits = _ + rw [generatorUnit, ZMod.coe_unitOfCoprime, ZMod.val_natCast, + Nat.mod_eq_of_lt d.2.generator_lt] + +/-- Descriptions are encoded as the binary triple `(p, q, g)`. -/ +def encDesc : Desc ↪ List Bool := + (Function.Embedding.subtype _).trans (encPair encNat (encPair encNat encNat)) + +/-- Forgetting validity does not change the encoding. -/ +private theorem computableInPolyTime_val : + ComputableInPolyTime (Subtype.val : Desc → ℕ × ℕ × ℕ) encDesc + (encPair encNat (encPair encNat encNat)) := + ComputableInPolyTime.of_eq fun _ => rfl + +/-- The group order is computable in polynomial time from the description. -/ +theorem computableInPolyTime_order : + ComputableInPolyTime (fun d : Desc => d.1.2.1) encDesc encNat := by + have := computableInPolyTime_val + fun_prop + +/-- The encoded generator is computable in polynomial time from the description. -/ +theorem computableInPolyTime_generator : + ComputableInPolyTime (fun d => encode d (generator d)) encDesc encBits := by + have := computableInPolyTime_val + simp only [encode_generator] + fun_prop + +/-- Multiplication modulo `p` is computable in polynomial time. -/ +theorem computableInPolyTime_add : + ComputableInPolyTime add (encPair encDesc (encPair encBits encBits)) encBits := by + have := computableInPolyTime_val + unfold add + fun_prop + +/-- Exponentiation modulo `p` is computable in polynomial time, by square-and-multiply. -/ +theorem computableInPolyTime_smul : + ComputableInPolyTime smul (encPair encDesc (encPair encNat encBits)) encBits := by + have hval := computableInPolyTime_val + have hpow : ComputableInPolyTime + (fun input : Desc × ℕ × List Bool => ofBits input.2.2 ^ input.2.1 % input.1.1.1) + (encPair encDesc (encPair encNat encBits)) encNat := + ComputableInPolyTime.binary_powMod (by fun_prop) (by fun_prop) (by fun_prop) + fun input => input.1.2.prime_modulus.pos + unfold smul + fun_prop + +end SchnorrGroup + +open SchnorrGroup in +/-- Schnorr groups, the subgroups of prime order `q` of `(ZMod p)ˣ`, as a family of cyclic groups +of prime order with efficient operations. -/ +def schnorrGroups : PrimeOrderGroupFamily where + Desc := SchnorrGroup.Desc + encDesc := SchnorrGroup.encDesc + order d := d.1.2.1 + prime_order d := d.2.prime_order + Carrier := Carrier + generator := generator + card_carrier := card_carrier + generator_ne_zero := generator_ne_zero + encode := encode + encode_injective := encode_injective + add := add + add_encode := add_encode + smul := smul + smul_encode := smul_encode + computableInPolyTime_order := computableInPolyTime_order + computableInPolyTime_generator := computableInPolyTime_generator + computableInPolyTime_add := computableInPolyTime_add + computableInPolyTime_smul := computableInPolyTime_smul + +end Cslib.Crypto diff --git a/Complexity/Crypto/Computational/SchnorrIdentification.lean b/Complexity/Crypto/Computational/SchnorrIdentification.lean new file mode 100644 index 000000000..b89ca6dd9 --- /dev/null +++ b/Complexity/Crypto/Computational/SchnorrIdentification.lean @@ -0,0 +1,337 @@ +/- +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.Computational.DiscreteLog +public import Complexity.Probability.BitString +public import Complexity.Languages.Probabilistic.BitString +public import Cslib.Foundations.Data.BitString +import Complexity.Crypto.Negligible.Basic +import Complexity.Crypto.Protocols.SigmaProtocol.Identification +import Complexity.Foundations.Data.BitString.Counter +import Complexity.Foundations.Data.Nat.Bits +import Complexity.Probability.PMF +import Mathlib.FieldTheory.Finite.Basic +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.BinaryDiv +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.PowMod +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain +import Complexity.Tactic.PPT + +/-! +# Schnorr identification under the discrete-logarithm assumption + +Schnorr's identification scheme ([BonehShoup2023], Section 19.1) over a `PrimeOrderGroupFamily`: +the key is a description `d`, drawn from a setup law, a uniform secret `α` and the public key +`u = α • g`. An impersonator sees the description and the encoded public key and sends a +commitment word `t`; the verifier draws a uniform challenge word `c` of `k n` bits; the +impersonator answers with a word `z`. Challenges and responses are read as binary numbers modulo +the group order `q`, and the verifier accepts when `t` encodes `z • g - c • u`; on genuine group +elements this is Schnorr's check `z • g = t + c • u`. + +Rewinding an impersonator gives a discrete-logarithm adversary, `SchnorrImpersonator.rewind`. It +runs the impersonator to its commitment, answers two independent uniform challenges from the same +state, and computes `(c - c')⁻¹ (z - z')` modulo `q`, inverting by Fermat's little theorem. For each +security parameter, if `2 ^ k ≤ q` for every description the setup can produce, + + `ε ≤ 1 / 2 ^ k + √ε'`, + +where `ε` is the impersonator's success probability and `ε'` the discrete-logarithm success +probability of the rewinding adversary (`succProbability_schnorrDirectGame_le`, Theorem 19.1). +The rewinding adversary is uniform strict PPT whenever the impersonator is and `k` is computable +in polynomial time. Under the discrete-logarithm assumption, with negligible `1 / 2 ^ k`, every +uniform strict PPT impersonator therefore succeeds with negligible probability +(`negligible_schnorrDirectGame`). + +The impersonator may use fresh randomness in its second stage; its state is a word. Challenges +are bit strings because strict PPT machines sample them exactly; they cannot sample `ZMod q` +exactly, which matters for the honest prover and for simulation but not for this reduction. + +## Main definitions + +* `Cslib.Crypto.PrimeOrderGroupFamily.SchnorrImpersonator`: a two-stage word adversary. +* `Cslib.Crypto.PrimeOrderGroupFamily.schnorrDirectGame`: the direct impersonation attack. +* `Cslib.Crypto.PrimeOrderGroupFamily.SchnorrImpersonator.rewind`: the rewinding + discrete-logarithm adversary. + +## Main results + +* `Cslib.Crypto.PrimeOrderGroupFamily.succProbability_schnorrDirectGame_le`: `ε ≤ 1 / 2 ^ k + √ε'` + at each security parameter. +* `Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_rewind`: the rewinding adversary is uniform strict + PPT. +* `Cslib.Crypto.PrimeOrderGroupFamily.negligible_schnorrDirectGame`: Schnorr identification is + secure against direct attacks under the discrete-logarithm assumption. + +## References + +* [D. Boneh, V. Shoup, *A Graduate Course in Applied Cryptography*, + Version 0.6][BonehShoup2023], Section 19.1. +* [C.-P. Schnorr, *Efficient Signature Generation by Smart Cards*][Schnorr1991] +-/ + +@[expose] public section + +namespace Cslib.Crypto.PrimeOrderGroupFamily + +open Probability Turing.MultiTapeTM Protocols + +variable {F : PrimeOrderGroupFamily} + +variable (F) in +/-- A uniform impersonator against Schnorr identification. Its first stage sees the security +parameter, the group description and the encoded public key, and returns a commitment word and a +state word; its second stage sees the security parameter, the state and the challenge word. -/ +structure SchnorrImpersonator where + /-- Commit, keeping a state word. -/ + commit : ℕ → F.Desc × List Bool → ProbComp (List Bool × List Bool) + /-- Respond to a challenge word from the state word. -/ + respond : ℕ → List Bool × List Bool → ProbComp (List Bool) + +/-- Both stages of an impersonator are uniform strict PPT in their whole inputs. -/ +def SchnorrImpersonator.IsPPT (A : F.SchnorrImpersonator) : Prop := + IsPPTOn (encPair encUnary (encPair F.encDesc encBits)) (encPair encBits encBits) + (fun input => A.commit input.1 input.2) ∧ + IsPPTOn (encPair encUnary (encPair encBits encBits)) encBits + (fun input => A.respond input.1 input.2) + +variable (F) in +/-- The direct impersonation attack on Schnorr identification ([BonehShoup2023], Attack +Game 18.1), with challenges of `k n` bits. The verifier accepts when the commitment encodes +`z • g - c • u`. -/ +noncomputable def schnorrDirectGame (setup : ℕ → PMF F.Desc) (k : ℕ → ℕ) + (A : F.SchnorrImpersonator) (n : ℕ) : Game := do + let d ← setup n + let α ← PMF.uniformOfFintype (ZMod (F.order d)) + let ts ← ProbComp.eval (A.commit n (d, F.encode d (α • F.generator d))) + let c ← BitString.uniformList (k n) + let z ← ProbComp.eval (A.respond n (ts.2, c)) + return decide (ts.1 = F.encode d ((ofBits z : ZMod (F.order d)) • F.generator d - + (ofBits c : ZMod (F.order d)) • (α • F.generator d))) + +/-- The extracted witness `(c - c')⁻¹ (z - z')` modulo `q`, computed on natural numbers with the +inverse as a `(q - 2)`nd power. -/ +def extractNat (q c z c' z' : ℕ) : ℕ := + ((c % q + q - c' % q) % q) ^ (q - 2) % q * ((z % q + q - z' % q) % q) % q + +/-- The rewinding discrete-logarithm adversary (proof of [BonehShoup2023], Theorem 19.1): run the +impersonator to its commitment, answer two independent uniform `k n`-bit challenges from the same +state, and output the extracted witness in binary. -/ +noncomputable def SchnorrImpersonator.rewind (k : ℕ → ℕ) (A : F.SchnorrImpersonator) (n : ℕ) + (input : F.Desc × List Bool) : ProbComp (List Bool) := do + let ts ← A.commit n input + let c ← BitString.sampleList (k n) + let c' ← BitString.sampleList (k n) + let z ← A.respond n (ts.2, c) + let z' ← A.respond n (ts.2, c') + return (extractNat (F.order input.1) (ofBits c) (ofBits z) (ofBits c') (ofBits z')).bits + +/-! ### The exact bound -/ + +/-- Binary digits, least significant first, read as a number (a private copy of the bridge in +`Classes/Counting/Space.lean`). -/ +private theorem ofBits_eq_lsbValue (w : List Bool) : ofBits w = BitString.lsbValue w := by + induction w with + | nil => rfl + | cons b w ih => + change Nat.bit b (ofBits w) = b.toNat + 2 * BitString.lsbValue w + rw [ih] + cases b <;> simp [Nat.bit, Nat.add_comm] + +/-- Distinct `k`-bit challenges are distinct modulo `q` when `2 ^ k ≤ q`. -/ +private theorem challenge_ne {q k : ℕ} (hkq : 2 ^ k ≤ q) {c c' : BitString k} (hc : c ≠ c') : + (ofBits (List.ofFn c) : ZMod q) ≠ ofBits (List.ofFn c') := by + intro h + rw [ZMod.natCast_eq_natCast_iff', ofBits_eq_lsbValue, ofBits_eq_lsbValue, + Nat.mod_eq_of_lt ((BitString.lsbValue_lt _).trans_le (by simpa using hkq)), + Nat.mod_eq_of_lt ((BitString.lsbValue_lt _).trans_le (by simpa using hkq))] at h + exact hc (List.ofFn_injective (BitString.lsbValue_injective (by simp) h)) + +/-- Fermat's little theorem gives the inverse in `extractNat`. -/ +private theorem extractNat_cast {q : ℕ} [Fact q.Prime] {c z c' z' : ℕ} + (hc : (c : ZMod q) ≠ c') : + (extractNat q c z c' z' : ZMod q) = ((c : ZMod q) - c')⁻¹ * ((z : ZMod q) - z') := by + have hsub (a b : ℕ) : (((a % q + q - b % q) % q : ℕ) : ZMod q) = (a : ZMod q) - b := by + rw [ZMod.natCast_mod, Nat.cast_sub ((Nat.mod_lt _ (Fact.out : q.Prime).pos).le.trans + (Nat.le_add_left _ _)), Nat.cast_add, ZMod.natCast_mod, ZMod.natCast_mod, ZMod.natCast_self, + add_zero] + have hne : (c : ZMod q) - c' ≠ 0 := sub_ne_zero.mpr hc + have hinv : ((c : ZMod q) - c') ^ (q - 2) = ((c : ZMod q) - c')⁻¹ := by + refine eq_inv_of_mul_eq_one_left ?_ + rw [← pow_succ, show q - 2 + 1 = q - 1 by have := (Fact.out : q.Prime).two_le; lia, + ZMod.pow_card_sub_one_eq_one hne] + simp only [extractNat, Nat.cast_mul, ZMod.natCast_mod, Nat.cast_pow, hsub, hinv] + +/-- Schnorr's protocol on encoded commitments and binary responses, with statements carrying their +group description; only its verifier is used. -/ +private noncomputable def wordProtocol (F : PrimeOrderGroupFamily) (m : ℕ) : + SigmaProtocol ℕ ((d : F.Desc) × F.Carrier d) (List Bool) (BitString m) (List Bool) where + State := Unit + commit _ _ := PMF.pure ([], ()) + respond _ _ _ _ := [] + verify y t c z := decide (t = F.encode y.1 ((ofBits z : ZMod (F.order y.1)) • F.generator y.1 - + (ofBits (List.ofFn c) : ZMod (F.order y.1)) • y.2)) + +/-- Schnorr key generation at a security parameter, with the description in the statement. -/ +private noncomputable def wordKeyGen (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) + (n : ℕ) : PMF (ℕ × (d : F.Desc) × F.Carrier d) := do + let d ← setup n + let α ← PMF.uniformOfFintype (ZMod (F.order d)) + return (α.val, ⟨d, α • F.generator d⟩) + +/-- The relation: `x` is a discrete logarithm of the public key. -/ +private def wordRelation (F : PrimeOrderGroupFamily) (x : ℕ) (y : (d : F.Desc) × F.Carrier d) : + Prop := + (x : ZMod (F.order y.1)) • F.generator y.1 = y.2 + +private noncomputable instance (F : PrimeOrderGroupFamily) : + DecidableRel (wordRelation F) := fun _ _ => Classical.propDecidable _ + +/-- The extractor of `wordProtocol`. -/ +private def wordExtract (F : PrimeOrderGroupFamily) (m : ℕ) (y : (d : F.Desc) × F.Carrier d) + (_ : List Bool) (c : BitString m) (z : List Bool) (c' : BitString m) (z' : List Bool) : ℕ := + extractNat (F.order y.1) (ofBits (List.ofFn c)) (ofBits z) (ofBits (List.ofFn c')) (ofBits z') + +/-- An impersonator as a typed impersonator for `wordProtocol`. -/ +private noncomputable def SchnorrImpersonator.typed (A : F.SchnorrImpersonator) (n m : ℕ) : + SigmaProtocol.Impersonator ((d : F.Desc) × F.Carrier d) (List Bool) (BitString m) + (List Bool) where + State := List Bool + commit y := ProbComp.eval (A.commit n (y.1, F.encode y.1 y.2)) + respond s c := ProbComp.eval (A.respond n (s, List.ofFn c)) + +private theorem schnorrDirectGame_eq (setup : ℕ → PMF F.Desc) (k : ℕ → ℕ) + (A : F.SchnorrImpersonator) (n : ℕ) : + F.schnorrDirectGame setup k A n = + (wordProtocol F (k n)).directAttack (wordKeyGen F setup n) (A.typed n (k n)) := by + simp only [schnorrDirectGame, SigmaProtocol.directAttack, wordKeyGen, wordProtocol, + SchnorrImpersonator.typed, BitString.uniformList, Probability.PMF.monad_bind_eq_bind, + Probability.PMF.monad_pure_eq_pure, PMF.bind_bind, PMF.pure_bind, PMF.bind_map, + Function.comp_def] + +private theorem specialSoundOn (setup : ℕ → PMF F.Desc) {k : ℕ → ℕ} {n : ℕ} + (hkq : ∀ d ∈ (setup n).support, 2 ^ k n ≤ F.order d) : + (wordProtocol F (k n)).SpecialSoundOn (wordKeyGen F setup n) (wordRelation F) + (wordExtract F (k n)) := by + rintro ⟨x, d, u⟩ hkey t c z c' z' hc hz hz' + have hd : d ∈ (setup n).support := by + simp only [wordKeyGen, Probability.PMF.monad_bind_eq_bind, + Probability.PMF.monad_pure_eq_pure, PMF.mem_support_bind_iff, PMF.mem_support_pure_iff, + Prod.mk.injEq, Sigma.mk.injEq] at hkey + obtain ⟨d', hd', -, -, -, hdd, -⟩ := hkey + exact hdd ▸ hd' + simp only [SigmaProtocol.Accepts, wordProtocol, decide_eq_true_eq] at hz hz' + have heq := F.encode_injective d (hz.symm.trans hz') + have hcne := challenge_ne (hkq d hd) hc + simp only [wordRelation, wordExtract, extractNat_cast hcne, mul_smul] + rw [sub_smul, sub_eq_sub_iff_sub_eq_sub.mp heq, ← sub_smul, + inv_smul_smul₀ (sub_ne_zero.mpr hcne)] + +/-- Reading back the binary digits of a number recovers it. -/ +private theorem ofBits_bits (r : ℕ) : ofBits r.bits = r := Nat.foldr_bit_bits r + +/-- The rewinding adversary wins the discrete-logarithm game exactly when its output is a witness +for the generated statement. -/ +private theorem decide_wordRelation (d : F.Desc) (α : ZMod (F.order d)) (r : ℕ) : + decide (wordRelation F r ⟨d, α • F.generator d⟩) = + decide (((ofBits r.bits : ℕ) : ZMod (F.order d)) = α) := by + rw [ofBits_bits] + exact decide_eq_decide.mpr ⟨fun h => F.smul_generator_injective d h, fun h => by + simp only [wordRelation, h]⟩ + +private theorem oneWayGame_eq (setup : ℕ → PMF F.Desc) (k : ℕ → ℕ) (A : F.SchnorrImpersonator) + (n : ℕ) : + SigmaProtocol.oneWayGame (wordKeyGen F setup n) (wordRelation F) + ((A.typed n (k n)).rewind (wordExtract F (k n))) = + F.discreteLogGame setup (A.rewind k) n := by + simp only [SigmaProtocol.oneWayGame, wordKeyGen, discreteLogGame, + SigmaProtocol.Impersonator.rewind, SchnorrImpersonator.rewind, SchnorrImpersonator.typed, + ProbComp.eval_bind, ProbComp.eval_pure, BitString.eval_sampleList, BitString.uniformList, + Probability.PMF.monad_bind_eq_bind, Probability.PMF.monad_pure_eq_pure, PMF.bind_bind, + PMF.pure_bind, PMF.bind_map, Function.comp_def, wordExtract, decide_wordRelation] + +/-- **Schnorr identification against direct attacks, exact form** ([BonehShoup2023], +Theorem 19.1): at each security parameter where every possible group has at least `2 ^ k n` +elements, an impersonator's success probability is at most `1 / 2 ^ k n + √ε'`, where `ε'` is the +discrete-logarithm success probability of the rewinding adversary. -/ +theorem succProbability_schnorrDirectGame_le (setup : ℕ → PMF F.Desc) (k : ℕ → ℕ) + (A : F.SchnorrImpersonator) (n : ℕ) (hkq : ∀ d ∈ (setup n).support, 2 ^ k n ≤ F.order d) : + (Game.succProbability (F.schnorrDirectGame setup k A n) : ℝ) ≤ + 1 / 2 ^ k n + √(Game.succProbability (F.discreteLogGame setup (A.rewind k) n)) := by + have h := SigmaProtocol.succProbability_directAttack_le (specialSoundOn setup hkq) + (A.typed n (k n)) + rw [oneWayGame_eq] at h + rw [schnorrDirectGame_eq] + simpa only [Fintype.card_fun, Fintype.card_bool, Fintype.card_fin, Nat.cast_pow, + Nat.cast_ofNat] using h + +/-! ### Efficiency of the rewinding adversary -/ + +/-- The extracted witness is computable in polynomial time from the group description and the +four binary numbers. -/ +@[fun_prop] +private theorem computableTidilyInPolyTime_extractNat {α : Type} {input : α ↪ List Bool} + {d : α → F.Desc} {c z c' z' : α → ℕ} (hd : ComputableTidilyInPolyTime d input F.encDesc) + (hc : ComputableTidilyInPolyTime c input encNat) + (hz : ComputableTidilyInPolyTime z input encNat) + (hc' : ComputableTidilyInPolyTime c' input encNat) + (hz' : ComputableTidilyInPolyTime z' input encNat) : + ComputableTidilyInPolyTime (fun a => extractNat (F.order (d a)) (c a) (z a) (c' a) (z' a)) + input encNat := by + have hq : ComputableTidilyInPolyTime (fun a => F.order (d a)) input encNat := + F.computableInPolyTime_order.tidy.comp hd + have hdiff {x y : α → ℕ} (hx : ComputableTidilyInPolyTime x input encNat) + (hy : ComputableTidilyInPolyTime y input encNat) : + ComputableTidilyInPolyTime + (fun a => (x a % F.order (d a) + F.order (d a) - y a % F.order (d a)) % F.order (d a)) + input encNat := + .binary_mod' (.binary_sub' (.binary_add' (.binary_mod' hx hq) hq) (.binary_mod' hy hq)) hq + have hpow := (ComputableInPolyTime.binary_powMod (ComputableInPolyTime.of_tidy (hdiff hc hc')) + (ComputableInPolyTime.of_tidy (.binary_sub' hq (.const 2))) + (ComputableInPolyTime.of_tidy hq) fun a => (F.prime_order (d a)).pos).tidy + exact .binary_mod' (.binary_mul' hpow (hdiff hz hz')) hq + +/-- **The rewinding adversary is uniform strict PPT** when the impersonator is and the challenge +length is computable in polynomial time. -/ +theorem isPPTOn_rewind {k : ℕ → ℕ} (hk : ComputableInPolyTime k encUnary encUnary) + {A : F.SchnorrImpersonator} (hA : A.IsPPT) : + IsPPTOn (encPair encUnary (encPair F.encDesc encBits)) encBits + (fun input => A.rewind k input.1 input.2) := by + have hk' := hk.tidy + have hrespond := hA.2 + unfold SchnorrImpersonator.rewind + refine hA.1.bind_with ?_ + refine (ComputableTidilyInPolyTime.sampleList (by fun_prop)).bind_with ?_ + refine (ComputableTidilyInPolyTime.sampleList (by fun_prop)).bind_with ?_ + refine (hrespond.preprocess + (prepare := fun p : (((ℕ × F.Desc × List Bool) × List Bool × List Bool) × List Bool) × + List Bool => (p.1.1.1.1, (p.1.1.2.2, p.1.2))) (by fun_prop)).bind_with ?_ + refine (hrespond.preprocess + (prepare := fun p : ((((ℕ × F.Desc × List Bool) × List Bool × List Bool) × List Bool) × + List Bool) × List Bool => (p.1.1.1.1.1, (p.1.1.1.2.2, p.1.2))) (by fun_prop)).bind_with ?_ + exact ComputableTidilyInPolyTime.isPPTOn (by fun_prop) + +/-! ### Security under the discrete-logarithm assumption -/ + +open scoped NNReal in +/-- **Schnorr identification is secure against direct attacks under the discrete-logarithm +assumption** ([BonehShoup2023], Theorem 19.1). Suppose the challenge length `k` is computable in +polynomial time, every group the setup can produce at parameter `n` has at least `2 ^ k n` +elements, and `1 / 2 ^ k n` is negligible. Then every uniform strict PPT impersonator succeeds +with negligible probability. -/ +theorem negligible_schnorrDirectGame {setup : ℕ → PMF F.Desc} (hDL : F.DiscreteLog setup) + {k : ℕ → ℕ} (hk : ComputableInPolyTime k encUnary encUnary) + (hkq : ∀ n, ∀ d ∈ (setup n).support, 2 ^ k n ≤ F.order d) + (hchallenge : Negligible fun n => 1 / 2 ^ k n) {A : F.SchnorrImpersonator} (hA : A.IsPPT) : + Negligible fun n => Game.succProbability (F.schnorrDirectGame setup k A n) := by + refine negligible_of_le (hchallenge.add (Negligible.sqrt (hDL _ (isPPTOn_rewind hk hA)))) + fun n => ?_ + rw [← NNReal.coe_le_coe, Pi.add_apply, NNReal.coe_add, Real.coe_sqrt, NNReal.coe_div, + NNReal.coe_one, NNReal.coe_pow, NNReal.coe_ofNat] + exact succProbability_schnorrDirectGame_le setup k A n (hkq n) + +end Cslib.Crypto.PrimeOrderGroupFamily diff --git a/Complexity/Crypto/Protocols/SigmaProtocol/Identification.lean b/Complexity/Crypto/Protocols/SigmaProtocol/Identification.lean index 618b8d543..ea9775d02 100644 --- a/Complexity/Crypto/Protocols/SigmaProtocol/Identification.lean +++ b/Complexity/Crypto/Protocols/SigmaProtocol/Identification.lean @@ -29,10 +29,11 @@ verification key (`directAttack`, Attack Game 18.1); in an eavesdropping attack honest conversations (`eavesdropAttack`, Attack Game 18.2). `oneWayGame` is the one-way key generation experiment (Attack Game 19.2). -* **Extraction** (Theorem 19.14). If the protocol has special soundness with extractor - `extract`, rewinding an impersonator with direct-attack success probability `ε` recovers a - witness for the key with probability at least `ε ^ 2 - ε / N`, where `N` is the number of - challenges; consequently `ε ≤ 1 / N + √ε'`. No assumption on the key generator is needed. +* **Extraction** (Theorem 19.14). If `extract` is a witness extractor for the statements the key + generator produces (`SpecialSoundOn`, implied by `SpecialSoundness`), rewinding an impersonator + with direct-attack success probability `ε` recovers a witness for the key with probability at + least `ε ^ 2 - ε / N`, where `N` is the number of challenges; consequently `ε ≤ 1 / N + √ε'`. + The generated pairs need not be in the relation. * **Simulation** (Theorems 19.3 and 19.15). If the protocol is special HVZK, an eavesdropper succeeds with exactly the probability of the direct impersonator that simulates the conversations itself, provided the key generator only outputs pairs in the relation. @@ -50,6 +51,7 @@ although `SigmaProtocol` itself is universe-polymorphic. * `SigmaProtocol.Impersonator`: a two-stage prover strategy. * `SigmaProtocol.directAttack`, `SigmaProtocol.eavesdropAttack`: impersonation experiments. * `SigmaProtocol.oneWayGame`: recover a witness for a generated statement. +* `SigmaProtocol.SpecialSoundOn`: special soundness for the statements of a key generator. * `SigmaProtocol.Impersonator.rewind`: the rewinding witness extractor. * `SigmaProtocol.simulateConversation`, `SigmaProtocol.Impersonator.withSimulatedViews`: replace eavesdropped conversations by simulated ones. @@ -153,16 +155,30 @@ private theorem directAttack_eq_once (P : SigmaProtocol X Y T C Z) (keyGen : PMF variable {P : SigmaProtocol X Y T C Z} {R : X → Y → Prop} [∀ x y, Decidable (R x y)] {extract : Y → T → C → Z → C → Z → X} +/-- Special soundness for the statements a key generator can produce: from two accepting +conversations with a common commitment and distinct challenges for such a statement, `extract` +computes a witness. It follows from `SpecialSoundness`, and suffices for extraction. -/ +def SpecialSoundOn (P : SigmaProtocol X Y T C Z) (keyGen : PMF (X × Y)) (R : X → Y → Prop) + (extract : Y → T → C → Z → C → Z → X) : Prop := + ∀ key ∈ keyGen.support, ∀ t c z c' z', c ≠ c' → P.Accepts key.2 t c z → + P.Accepts key.2 t c' z' → R (extract key.2 t c z c' z') key.2 + +omit [Fintype C] [Nonempty C] [∀ x y, Decidable (R x y)] in +/-- Special soundness gives special soundness for every key generator. -/ +theorem SpecialSoundness.specialSoundOn (hP : P.SpecialSoundness R extract) + (keyGen : PMF (X × Y)) : P.SpecialSoundOn keyGen R extract := + fun key _ => hP key.2 + /-- Two accepting runs with distinct challenges lead the rewinding extractor to a witness. -/ -private theorem twice_le_oneWayGame [DecidableEq C] (hP : P.SpecialSoundness R extract) - (keyGen : PMF (X × Y)) (A : Impersonator Y T C Z) : +private theorem twice_le_oneWayGame [DecidableEq C] {keyGen : PMF (X × Y)} + (hP : P.SpecialSoundOn keyGen R extract) (A : Impersonator Y T C Z) : Rewinding.twice (directFirst keyGen A) (fun s c => A.respond s.2.2 c) (fun s c z => P.verify s.1 s.2.1 c z) true ≤ oneWayGame keyGen R (A.rewind extract) true := by simp only [Rewinding.twice, oneWayGame, Impersonator.rewind, directFirst, Probability.PMF.monad_bind_eq_bind, Probability.PMF.monad_pure_eq_pure, PMF.bind_bind, PMF.pure_bind] - refine Probability.PMF.bind_apply_mono_on_support _ _ fun key _ => ?_ + refine Probability.PMF.bind_apply_mono_on_support _ _ fun key hkey => ?_ refine Probability.PMF.bind_apply_mono_on_support _ _ fun ts _ => ?_ refine Probability.PMF.bind_apply_mono_on_support _ _ fun c _ => ?_ refine Probability.PMF.bind_apply_mono_on_support _ _ fun c' _ => ?_ @@ -170,17 +186,17 @@ private theorem twice_le_oneWayGame [DecidableEq C] (hP : P.SpecialSoundness R e refine Probability.PMF.bind_apply_mono_on_support _ _ fun z' _ => ?_ by_cases hwin : (P.verify key.2 ts.1 c z && P.verify key.2 ts.1 c' z' && c != c') = true · simp only [Bool.and_eq_true, bne_iff_ne] at hwin - have hR := hP key.2 ts.1 c z c' z' hwin.2 hwin.1.1 hwin.1.2 + have hR := hP key hkey ts.1 c z c' z' hwin.2 hwin.1.1 hwin.1.2 calc _ ≤ 1 := PMF.coe_le_one _ _ _ = _ := by simp [hR] · simp [Bool.eq_false_iff.mpr hwin] /-- **Extraction from an impersonator** ([BonehShoup2023], Theorem 19.14, Equation 19.17): with -special soundness, the rewinding extractor recovers a witness with probability at least -`ε ^ 2 - ε / N`, where `ε` is the direct-attack success probability and `N` the number of -challenges. -/ -theorem sq_sub_le_oneWayGame_rewind (hP : P.SpecialSoundness R extract) (keyGen : PMF (X × Y)) - (A : Impersonator Y T C Z) : +special soundness on the generated statements, the rewinding extractor recovers a witness with +probability at least `ε ^ 2 - ε / N`, where `ε` is the direct-attack success probability and `N` +the number of challenges. -/ +theorem sq_sub_le_oneWayGame_rewind {keyGen : PMF (X × Y)} + (hP : P.SpecialSoundOn keyGen R extract) (A : Impersonator Y T C Z) : (Game.succProbability (P.directAttack keyGen A) : ℝ) ^ 2 - Game.succProbability (P.directAttack keyGen A) / Fintype.card C ≤ Game.succProbability (oneWayGame keyGen R (A.rewind extract)) := by @@ -188,20 +204,21 @@ theorem sq_sub_le_oneWayGame_rewind (hP : P.SpecialSoundness R extract) (keyGen simp only [Game.succProbability, ENNReal.coe_toNNReal_eq_toReal] rw [directAttack_eq_once] exact (Rewinding.sq_sub_le_twice _ _ _).trans - (ENNReal.toReal_mono (PMF.apply_ne_top _ _) (twice_le_oneWayGame hP keyGen A)) + (ENNReal.toReal_mono (PMF.apply_ne_top _ _) (twice_le_oneWayGame hP A)) /-- **Security against direct attacks** ([BonehShoup2023], Theorem 19.14, Equation 19.18): with -special soundness, the direct-attack success probability is at most `1 / N + √ε'`, where `ε'` is -the success probability of the rewinding extractor in the one-way game. -/ -theorem succProbability_directAttack_le (hP : P.SpecialSoundness R extract) - (keyGen : PMF (X × Y)) (A : Impersonator Y T C Z) : +special soundness on the generated statements, the direct-attack success probability is at most +`1 / N + √ε'`, where `ε'` is the success probability of the rewinding extractor in the one-way +game. -/ +theorem succProbability_directAttack_le {keyGen : PMF (X × Y)} + (hP : P.SpecialSoundOn keyGen R extract) (A : Impersonator Y T C Z) : (Game.succProbability (P.directAttack keyGen A) : ℝ) ≤ 1 / Fintype.card C + √(Game.succProbability (oneWayGame keyGen R (A.rewind extract))) := by classical simp only [Game.succProbability, ENNReal.coe_toNNReal_eq_toReal] rw [directAttack_eq_once] exact (Rewinding.le_inv_add_sqrt_twice _ _ _).trans (add_le_add le_rfl (Real.sqrt_le_sqrt - (ENNReal.toReal_mono (PMF.apply_ne_top _ _) (twice_le_oneWayGame hP keyGen A)))) + (ENNReal.toReal_mono (PMF.apply_ne_top _ _) (twice_le_oneWayGame hP A)))) /-! ### Eavesdropping by simulation -/ @@ -250,6 +267,6 @@ theorem succProbability_eavesdropAttack_le {simulate : Y → C → PMF (T × Z)} 1 / Fintype.card C + √(Game.succProbability (oneWayGame keyGen R ((A.withSimulatedViews simulate).rewind extract))) := by rw [eavesdropAttack_eq_directAttack hzk hkey] - exact succProbability_directAttack_le hsound keyGen _ + exact succProbability_directAttack_le (hsound.specialSoundOn keyGen) _ end Cslib.Crypto.Protocols.SigmaProtocol diff --git a/Complexity/Crypto/Protocols/SigmaProtocol/SchnorrIdentification.lean b/Complexity/Crypto/Protocols/SigmaProtocol/SchnorrIdentification.lean index 6100129c8..6f1a7fc16 100644 --- a/Complexity/Crypto/Protocols/SigmaProtocol/SchnorrIdentification.lean +++ b/Complexity/Crypto/Protocols/SigmaProtocol/SchnorrIdentification.lean @@ -72,7 +72,7 @@ theorem schnorr_succProbability_directAttack_le [Fact q.Prime] (A : Impersonator (Game.succProbability ((schnorr ι g).directAttack (schnorrKeyGen g) A) : ℝ) ≤ 1 / Fintype.card C + √(Game.succProbability (oneWayGame (schnorrKeyGen g) (fun α u => α • g = u) (A.rewind (linearExtract ι)))) := - succProbability_directAttack_le schnorr_specialSoundness _ A + succProbability_directAttack_le (schnorr_specialSoundness.specialSoundOn _) A /-- **Schnorr identification against eavesdropping** ([BonehShoup2023], Theorem 19.5, exact form): an eavesdropper succeeds with exactly the probability of the direct impersonator that diff --git a/ComplexityTests.lean b/ComplexityTests.lean index 7b0cee993..b7f74fa40 100644 --- a/ComplexityTests.lean +++ b/ComplexityTests.lean @@ -104,6 +104,7 @@ import ComplexityTests.Crypto.HomomorphicLeveled import ComplexityTests.Crypto.HomomorphicRefresh import ComplexityTests.Crypto.KeyChainSecurity import ComplexityTests.Crypto.LeveledSecurity +import ComplexityTests.Crypto.SchnorrDiscreteLog import ComplexityTests.Crypto.SigmaIdentification import ComplexityTests.Crypto.SigmaProtocol import ComplexityTests.Crypto.Signature diff --git a/ComplexityTests/Crypto/SchnorrDiscreteLog.lean b/ComplexityTests/Crypto/SchnorrDiscreteLog.lean new file mode 100644 index 000000000..39983e393 --- /dev/null +++ b/ComplexityTests/Crypto/SchnorrDiscreteLog.lean @@ -0,0 +1,97 @@ +/- +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.DiscreteLog.SchnorrGroup +import Complexity.Crypto.Computational.SchnorrIdentification +import Complexity.Crypto.Negligible.Basic +import Complexity.Tactic.PolyTime +import Mathlib.Tactic.NormNum.Prime + +/-! +# Tests for Schnorr identification under the discrete-logarithm assumption + +The Schnorr group of order `11` in `(ZMod 23)ˣ`, generated by `2`, is a valid description, and +the family's operations compute on its encoded elements. The security theorem applies to the +Schnorr-group family with `n`-bit challenges, for any setup law producing groups of order at least +`2 ^ n`, and its premises are satisfiable: an impersonator that ignores its inputs is uniform +strict PPT. +-/ + +namespace ComplexityTests.Crypto.SchnorrDiscreteLog + +open Cslib Cslib.Probability Cslib.Crypto Turing.MultiTapeTM +open scoped NNReal + +/-- The Schnorr group of order `11` in `(ZMod 23)ˣ`, generated by `2`. -/ +def d23 : SchnorrGroup.Desc := + ⟨(23, 11, 2), ⟨by norm_num, by norm_num, by norm_num, by norm_num, by norm_num⟩⟩ + +example : schnorrGroups.order d23 = 11 := rfl + +/-- The encoded generator is the binary digits of `2`. -/ +example : schnorrGroups.encode d23 (schnorrGroups.generator d23) = Nat.bits 2 := + SchnorrGroup.encode_generator d23 + +/-- `2 ^ 7 = 13` in `(ZMod 23)ˣ`, computed on encodings. -/ +example : schnorrGroups.smul (d23, 7, Nat.bits 2) = Nat.bits 13 := by decide + +/-- `13 · 9 = 2` in `(ZMod 23)ˣ`, computed on encodings. -/ +example : schnorrGroups.add (d23, Nat.bits 13, Nat.bits 9) = Nat.bits 2 := by decide + +/-- An impersonator that ignores its inputs. -/ +noncomputable def silent : schnorrGroups.SchnorrImpersonator where + commit _ _ := pure ([], []) + respond _ _ := pure [] + +/-- The silent impersonator is uniform strict PPT. -/ +theorem silent_isPPT : silent.IsPPT := + ⟨ComputableTidilyInPolyTime.isPPTOn (ComputableTidilyInPolyTime.const _), + ComputableTidilyInPolyTime.isPPTOn (ComputableTidilyInPolyTime.const _)⟩ + +/-- `n`-bit challenges have negligible guessing probability `1 / 2 ^ n`. -/ +theorem negligible_inv_two_pow : Negligible fun n => (1 : ℝ≥0) / 2 ^ n := by + simpa only [one_div, inv_pow] using negligible_geometric (ratio := 2⁻¹) (by norm_num) + +/-- Under the discrete-logarithm assumption for Schnorr groups of order at least `2 ^ n`, +Schnorr identification with `n`-bit challenges resists every uniform strict PPT impersonator. -/ +example (setup : ℕ → PMF schnorrGroups.Desc) (hDL : schnorrGroups.DiscreteLog setup) + (hsize : ∀ n, ∀ d ∈ (setup n).support, 2 ^ n ≤ schnorrGroups.order d) + (A : schnorrGroups.SchnorrImpersonator) (hA : A.IsPPT) : + Negligible fun n => Game.succProbability (schnorrGroups.schnorrDirectGame setup id A n) := + PrimeOrderGroupFamily.negligible_schnorrDirectGame hDL (ComputableInPolyTime.of_eq fun _ => rfl) + hsize negligible_inv_two_pow hA + +/-- In particular, the silent impersonator succeeds with negligible probability. -/ +example (setup : ℕ → PMF schnorrGroups.Desc) (hDL : schnorrGroups.DiscreteLog setup) + (hsize : ∀ n, ∀ d ∈ (setup n).support, 2 ^ n ≤ schnorrGroups.order d) : + Negligible fun n => Game.succProbability (schnorrGroups.schnorrDirectGame setup id silent n) := + PrimeOrderGroupFamily.negligible_schnorrDirectGame hDL (ComputableInPolyTime.of_eq fun _ => rfl) + hsize negligible_inv_two_pow silent_isPPT + +/-! ### Axioms -/ + +/-- +info: 'Cslib.Crypto.PrimeOrderGroupFamily.negligible_schnorrDirectGame' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms PrimeOrderGroupFamily.negligible_schnorrDirectGame + +/-- +info: 'Cslib.Crypto.PrimeOrderGroupFamily.succProbability_schnorrDirectGame_le' depends on +axioms: [propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms PrimeOrderGroupFamily.succProbability_schnorrDirectGame_le + +/-- +info: 'Turing.MultiTapeTM.ComputableInPolyTime.binary_powMod' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms ComputableInPolyTime.binary_powMod + +end ComplexityTests.Crypto.SchnorrDiscreteLog diff --git a/ComplexityTests/Crypto/SigmaIdentification.lean b/ComplexityTests/Crypto/SigmaIdentification.lean index 03c1f227d..0eef0fc84 100644 --- a/ComplexityTests/Crypto/SigmaIdentification.lean +++ b/ComplexityTests/Crypto/SigmaIdentification.lean @@ -76,8 +76,9 @@ theorem succProbability_knower : probability at least `1 - 1 / 11`. -/ example : (10 / 11 : ℝ) ≤ Game.succProbability (oneWayGame (schnorrKeyGen (2 : ZMod 11)) (fun α u => α • (2 : ZMod 11) = u) (knower.rewind (linearExtract ι))) := by - have h := sq_sub_le_oneWayGame_rewind (schnorr_specialSoundness (ι := ι) (g := (2 : ZMod 11))) - (schnorrKeyGen 2) knower + have h := sq_sub_le_oneWayGame_rewind + ((schnorr_specialSoundness (ι := ι) (g := (2 : ZMod 11))).specialSoundOn (schnorrKeyGen 2)) + knower rw [succProbability_knower, ZMod.card] at h norm_num at h ⊢ exact h diff --git a/ROADMAP.md b/ROADMAP.md index ea11743cc..b2c04e347 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -1152,11 +1152,14 @@ Jukna coverage below is an additional target beyond the V1 port: `ε ≤ 1/N + √ε'` and HVZK ⇒ eavesdropping security are proved for [identification from Sigma protocols](Complexity/Crypto/Protocols/SigmaProtocol/Identification.lean) and [Schnorr identification](Complexity/Crypto/Protocols/SigmaProtocol/SchnorrIdentification.lean). - Open: a discrete-log assumption for a group family with native polynomial-time operations, - efficiency of the reductions and the asymptotic security of Schnorr identification, and - Fiat–Shamir/Schnorr signatures in the random-oracle model with the forking bound of - Theorem 19.16. Strict PPT samples bit strings but not `ZMod q` exactly, so those bounds will - carry explicit statistical-distance terms. + The [discrete-log assumption](Complexity/Crypto/Computational/DiscreteLog.lean) is stated for + a family of prime-order groups with plain polynomial-time operations, instantiated by + [Schnorr groups](Complexity/Crypto/Computational/DiscreteLog/SchnorrGroup.lean), and + [Schnorr identification](Complexity/Crypto/Computational/SchnorrIdentification.lean) is secure + against direct attacks by uniform strict PPT impersonators under it. Open: security against + eavesdropping in the strict-PPT model, where simulating transcripts needs approximately uniform + `ZMod q` samples and hence an explicit statistical-distance term, and Fiat–Shamir/Schnorr + signatures in the random-oracle model with the forking bound of Theorem 19.16. The current V1 port excludes the circuitized anti-checker, hardness-magnification argument and MINKT/MINCKT developments. The long-term canon above includes metacomplexity; those results should From 68e1e92d5cecd17e31b2e4a1063c832e78ac28bc Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 19:49:35 -0400 Subject: [PATCH 2/2] refactor(crypto): register the extraction certificate locally Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- Complexity/Crypto/Computational/SchnorrIdentification.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Complexity/Crypto/Computational/SchnorrIdentification.lean b/Complexity/Crypto/Computational/SchnorrIdentification.lean index b89ca6dd9..2edc35bd4 100644 --- a/Complexity/Crypto/Computational/SchnorrIdentification.lean +++ b/Complexity/Crypto/Computational/SchnorrIdentification.lean @@ -273,7 +273,6 @@ theorem succProbability_schnorrDirectGame_le (setup : ℕ → PMF F.Desc) (k : /-- The extracted witness is computable in polynomial time from the group description and the four binary numbers. -/ -@[fun_prop] private theorem computableTidilyInPolyTime_extractNat {α : Type} {input : α ↪ List Bool} {d : α → F.Desc} {c z c' z' : α → ℕ} (hd : ComputableTidilyInPolyTime d input F.encDesc) (hc : ComputableTidilyInPolyTime c input encNat) @@ -295,6 +294,8 @@ private theorem computableTidilyInPolyTime_extractNat {α : Type} {input : α (ComputableInPolyTime.of_tidy hq) fun a => (F.prime_order (d a)).pos).tidy exact .binary_mod' (.binary_mul' hpow (hdiff hz hz')) hq +attribute [local fun_prop] computableTidilyInPolyTime_extractNat + /-- **The rewinding adversary is uniform strict PPT** when the impersonator is and the challenge length is computable in polynomial time. -/ theorem isPPTOn_rewind {k : ℕ → ℕ} (hk : ComputableInPolyTime k encUnary encUnary)