Schnorr signatures

Schnorr signatures ([BS23], 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, [BS23], 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, Section 19.2.
• C.-P. Schnorr, Efficient Signature Generation by Smart Cards

theorem Cslib.Crypto.Protocols.SigmaProtocol.schnorr_commit_map_fst_le {q : ℕ} [Fact (Nat.Prime q)] {G C : Type} [AddCommGroup G] [Module (ZMod q) G] [DecidableEq G] {ι : C ↪ ZMod q} {g : G} (hg : g ≠ 0) (x : ZMod q) (y t : G) : (PMF.map Prod.fst ((schnorr ι g).commit x y)) t ≤ (↑q)⁻¹

Unpredictable Schnorr commitments ([BS23], 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 Cslib.Crypto.Protocols.SigmaProtocol.schnorr_succProbability_eufCmaGame_le {q : ℕ} [Fact (Nat.Prime q)] {G C : Type} [AddCommGroup G] [Module (ZMod q) G] [DecidableEq G] {ι : C ↪ ZMod q} {g : G} [Fintype C] [Nonempty C] [DecidableEq C] {M : Type} [DecidableEq M] (hg : g ≠ 0) (A : ROMSignature.Forger G M (G × ZMod q) (M × G) C) {Qs Qro : ℕ} (hA : A.CallBounded Qs Qro) : ↑(Game.succProbability (ROMSignature.eufCmaGame ((schnorr ι g).fiatShamir (schnorrKeyGen g)) A)) ≤ ↑Qs * (↑Qs + ↑Qro) / ↑q + (↑Qro + 1) / ↑(Fintype.card C) + √((↑Qro + 1) * ↑(oneWayGame (schnorrKeyGen g) (fun (α : ZMod q) (u : G) => α • g = u) (FiatShamir.reduction (schnorr ι g) (linearSimulate (fun (x : G) => LinearMap.toSpanSingleton (ZMod q) G g) id ι) (linearExtract ι) A Qs Qro)).succProbability)

Security of Schnorr signatures ([BS23], 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.