Schnorr identification under the discrete-logarithm assumption

Schnorr's identification scheme ([BS23], 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, Section 19.1.
• C.-P. Schnorr, Efficient Signature Generation by Smart Cards

structure Cslib.Crypto.PrimeOrderGroupFamily.SchnorrImpersonator (F : PrimeOrderGroupFamily) : Type

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.

• commit : ℕ → F.Desc × List Bool → ProbComp (List Bool × List Bool)

  Commit, keeping a state word.

• respond : ℕ → List Bool × List Bool → ProbComp (List Bool)

  Respond to a challenge word from the state word.

def Cslib.Crypto.PrimeOrderGroupFamily.SchnorrImpersonator.IsPPT {F : PrimeOrderGroupFamily} (A : F.SchnorrImpersonator) : Prop

Both stages of an impersonator are uniform strict PPT in their whole inputs.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.schnorrDirectGame (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (k : ℕ → ℕ) (A : F.SchnorrImpersonator) (n : ℕ) : Game

The direct impersonation attack on Schnorr identification ([BS23], Attack Game 18.1), with challenges of k n bits. The verifier accepts when the commitment encodes z • g - c • u.

def Cslib.Crypto.PrimeOrderGroupFamily.extractNat (q c z c' z' : ℕ) : ℕ

The extracted witness (c - c')⁻¹ (z - z') modulo q, computed on natural numbers with the inverse as a (q - 2)nd power.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.SchnorrImpersonator.rewind {F : PrimeOrderGroupFamily} (k : ℕ → ℕ) (A : F.SchnorrImpersonator) (n : ℕ) (input : F.Desc × List Bool) : ProbComp (List Bool)

The rewinding discrete-logarithm adversary (proof of [BS23], 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.

The exact bound

theorem Cslib.Crypto.PrimeOrderGroupFamily.succProbability_schnorrDirectGame_le {F : PrimeOrderGroupFamily} (setup : ℕ → PMF F.Desc) (k : ℕ → ℕ) (A : F.SchnorrImpersonator) (n : ℕ) (hkq : ∀ d ∈ (setup n).support, 2 ^ k n ≤ F.order d) : ↑(F.schnorrDirectGame setup k A n).succProbability ≤ 1 / 2 ^ k n + √↑(F.discreteLogGame setup (SchnorrImpersonator.rewind k A) n).succProbability

Schnorr identification against direct attacks, exact form ([BS23], 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.

Efficiency of the rewinding adversary

theorem Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_rewind {F : PrimeOrderGroupFamily} {k : ℕ → ℕ} (hk : Turing.MultiTapeTM.ComputableInPolyTime k Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) {A : F.SchnorrImpersonator} (hA : A.IsPPT) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits fun (input : ℕ × F.Desc × List Bool) => SchnorrImpersonator.rewind k A input.1 input.2

The rewinding adversary is uniform strict PPT when the impersonator is and the challenge length is computable in polynomial time.

Security under the discrete-logarithm assumption

theorem Cslib.Crypto.PrimeOrderGroupFamily.negligible_schnorrDirectGame {F : PrimeOrderGroupFamily} {setup : ℕ → PMF F.Desc} (hDL : F.DiscreteLog setup) {k : ℕ → ℕ} (hk : Turing.MultiTapeTM.ComputableInPolyTime k Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.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 : ℕ) => (F.schnorrDirectGame setup k A n).succProbability

Schnorr identification is secure against direct attacks under the discrete-logarithm assumption ([BS23], 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.