Schnorr identification

Schnorr's identification scheme ([BS23], Section 19.1) is Schnorr's Sigma protocol with the key generator that draws α uniformly from ZMod q and publishes u = α • g. The one-way game for this key generator is the discrete-logarithm experiment for g: the adversary wins when it outputs some α' with α' • g = u. When g generates a group of prime order q, this α' is the sampled α.

The two theorems here are the exact forms of Boneh and Shoup's Theorems 19.1 and 19.5 at a fixed group. They make no efficiency or hardness claim; the discrete-logarithm assumption and the asymptotic security statement need a group family with efficient operations. As for the identification experiments they instantiate, the group and challenge types are in Type.

Main definitions

• SigmaProtocol.schnorrKeyGen: a uniform secret α and the public key α • g.

Main results

• SigmaProtocol.schnorr_succProbability_directAttack_le: ε ≤ 1 / N + √ε', with ε' the rewinding extractor's discrete-logarithm success probability (Theorem 19.1).
• SigmaProtocol.schnorr_eavesdropAttack_eq_directAttack: an eavesdropper is no stronger than the direct impersonator that simulates its views (Theorem 19.5).

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Section 19.1.
• C.-P. Schnorr, Efficient Signature Generation by Smart Cards

noncomputable def Cslib.Crypto.Protocols.SigmaProtocol.schnorrKeyGen {q : ℕ} [NeZero q] {G : Type} [AddCommGroup G] [Module (ZMod q) G] (g : G) : PMF (ZMod q × G)

Schnorr key generation ([BS23], Section 19.1): a uniform secret α and the verification key α • g.

theorem Cslib.Crypto.Protocols.SigmaProtocol.mem_support_schnorrKeyGen {q : ℕ} [NeZero q] {G : Type} [AddCommGroup G] [Module (ZMod q) G] {g : G} {key : ZMod q × G} (h : key ∈ (schnorrKeyGen g).support) : key.1 • g = key.2

Every Schnorr key pair is in Schnorr's relation.

theorem Cslib.Crypto.Protocols.SigmaProtocol.schnorr_succProbability_directAttack_le {q : ℕ} [NeZero q] {G C : Type} [AddCommGroup G] [Module (ZMod q) G] [DecidableEq G] [Fintype C] [Nonempty C] {ι : C ↪ ZMod q} {g : G} [Fact (Nat.Prime q)] (A : Impersonator G G C (ZMod q)) : ↑((schnorr ι g).directAttack (schnorrKeyGen g) A).succProbability ≤ 1 / ↑(Fintype.card C) + √↑(oneWayGame (schnorrKeyGen g) (fun (α : ZMod q) (u : G) => α • g = u) (A.rewind (linearExtract ι))).succProbability

Schnorr identification against direct attacks ([BS23], Theorem 19.1, exact form): an impersonator's success probability is at most 1 / N + √ε', where ε' is the probability that rewinding it computes a discrete logarithm of the key and N is the number of challenges.

theorem Cslib.Crypto.Protocols.SigmaProtocol.schnorr_eavesdropAttack_eq_directAttack {q : ℕ} [NeZero q] {G C : Type} [AddCommGroup G] [Module (ZMod q) G] [DecidableEq G] [Fintype C] [Nonempty C] {ι : C ↪ ZMod q} {g : G} {Q : ℕ} (A : Impersonator (G × (Fin Q → G × C × ZMod q)) G C (ZMod q)) : (schnorr ι g).eavesdropAttack (schnorrKeyGen g) Q A = (schnorr ι g).directAttack (schnorrKeyGen g) (Impersonator.withSimulatedViews (linearSimulate (fun (x : G) => LinearMap.toSpanSingleton (ZMod q) G g) id ι) A)

Schnorr identification against eavesdropping ([BS23], Theorem 19.5, exact form): an eavesdropper succeeds with exactly the probability of the direct impersonator that simulates its Q conversations.