Documentation

CatCryptCore.Examples.Schnorr

Schnorr's Σ-Protocol: Special Soundness and the Forking Reduction to DL #

Schnorr's identification/signature scheme, over an abstract prime-order group. Following Rosulek, The Joy of Cryptography (Σ-protocols), and the standard Schnorr → Discrete-Logarithm reduction (Pointcheval–Stern / Bellare–Neven).

We work in the group P.G₁ of a PairingGroup P — an abstract cyclic group of prime order P.p with generator g₁ and ZMod P.p-exponentiation x ^ᵍ a. No concrete curve is used.

The protocol #

A statement is a public key pk : G₁; the witness is its discrete log w : ZMod p with g₁ ^ᵍ w = pk. A transcript (a, c, s) consists of a commitment a : G₁, a challenge c : ZMod p, and a response s : ZMod p, and is accepting when

g₁ ^ᵍ s = a * (pk ^ᵍ c).

The honest prover samples r, sends a = g₁ ^ᵍ r, and answers s = r + w·c.

Main results #

References #

General zpowZMod₁ homomorphism lemmas #

PairingGroup.lean proves the exponent-homomorphism laws for the generator g₁; special soundness needs them for the arbitrary public key pk, so we lift them to a general base element. Every element of G₁ has order dividing the prime p, so x ^ᵍ is a ZMod p-module action just like g₁ ^ᵍ.

The Schnorr relation #

source
def CatCrypt.Examples.Schnorr.schnorrAccepts {P : Crypto.PairingGroup} (pk a : Crypto.PairingGroup.G₁) (c s : ZMod Crypto.PairingGroup.p) :
Prop

A Schnorr transcript (a, c, s) for public key pk is accepting when g₁ ^ᵍ s = a * (pk ^ᵍ c).

Equations
Instances For
    source
    noncomputable def CatCrypt.Examples.Schnorr.schnorrVerify {P : Crypto.PairingGroup} (pk a : Crypto.PairingGroup.G₁) (c s : ZMod Crypto.PairingGroup.p) :
    Bool

    Boolean acceptance test (decidable, for use as a forking-lemma predicate).

    Equations
    Instances For
      source
      @[simp]
      theorem CatCrypt.Examples.Schnorr.schnorrVerify_eq_true {P : Crypto.PairingGroup} {pk a : Crypto.PairingGroup.G₁} {c s : ZMod Crypto.PairingGroup.p} :
      schnorrVerify pk a c s = true ↔ schnorrAccepts pk a c s

      Completeness #

      source
      theorem CatCrypt.Examples.Schnorr.schnorr_honest_accepts {P : Crypto.PairingGroup} (w r c : ZMod Crypto.PairingGroup.p) :
      schnorrAccepts (Crypto.PairingGroup.zpowZMod₁ Crypto.PairingGroup.g₁ w) (Crypto.PairingGroup.zpowZMod₁ Crypto.PairingGroup.g₁ r) c (r + w * c)

      Completeness. The honest transcript (g₁ ^ᵍ r, c, r + w·c) for the public key pk = g₁ ^ᵍ w always verifies.

      Special soundness #

      source
      theorem CatCrypt.Examples.Schnorr.schnorr_special_soundness {P : Crypto.PairingGroup} (pk a : Crypto.PairingGroup.G₁) (c₁ c₂ s₁ s₂ : ZMod Crypto.PairingGroup.p) (hv₁ : schnorrAccepts pk a c₁ s₁) (hv₂ : schnorrAccepts pk a c₂ s₂) (hne : c₁ ≠ c₂) :
      pk = Crypto.PairingGroup.zpowZMod₁ Crypto.PairingGroup.g₁ ((s₁ - s₂) * (c₁ - c₂)⁻¹)

      Special soundness. Two accepting transcripts that share the commitment a but use distinct challenges c₁ ≠ c₂ reveal the witness: pk = g₁ ^ᵍ ((s₁ - s₂) / (c₁ - c₂)).

      This is the algebraic heart of Schnorr's knowledge soundness — and, in the ROM/forking reduction, the discrete-log extractor. Pure group algebra: no probability.

      source
      theorem CatCrypt.Examples.Schnorr.schnorr_special_soundness_bool {P : Crypto.PairingGroup} (pk a : Crypto.PairingGroup.G₁) (c₁ c₂ s₁ s₂ : ZMod Crypto.PairingGroup.p) (hv₁ : schnorrVerify pk a c₁ s₁ = true) (hv₂ : schnorrVerify pk a c₂ s₂ = true) (hne : c₁ ≠ c₂) :
      pk = Crypto.PairingGroup.zpowZMod₁ Crypto.PairingGroup.g₁ ((s₁ - s₂) * (c₁ - c₂)⁻¹)

      Boolean-hypothesis form of special soundness, matching the forking-lemma acceptance predicate.

      Forking reduction to Discrete Log #

      The forking reduction exercises the core forking lemma. A Fiat–Shamir Schnorr forger making a single random-oracle query decomposes into a probabilistic coins phase (choose a message and commitment a) and a deterministic respond phase (given the challenge c from the oracle, produce the response s). Replaying the forger on the same coins but a fresh challenge yields two accepting transcripts that share the commitment — exactly the hypothesis of schnorr_special_soundness.

      source
      structure CatCrypt.Examples.Schnorr.SchnorrForger (P : Crypto.PairingGroup) (Msg S : Type) :
      Type

      A decomposed Schnorr forger (single random-oracle query).

      Instances For
        source
        noncomputable def CatCrypt.Examples.Schnorr.SchnorrForger.toForkable {P : Crypto.PairingGroup} {Msg S : Type} (A : SchnorrForger P Msg S) :
        Crypto.ForkingLemma.ForkableAdversary Crypto.PairingGroup.G₁ (S × Msg × Crypto.PairingGroup.G₁) (ZMod Crypto.PairingGroup.p) (Crypto.PairingGroup.G₁ × ZMod Crypto.PairingGroup.p × ZMod Crypto.PairingGroup.p)

        View a SchnorrForger as a core ForkableAdversary. The response type carries (a, c, s) so the acceptance predicate can run verification.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def CatCrypt.Examples.Schnorr.romAccept {P : Crypto.PairingGroup} (pk : Crypto.PairingGroup.G₁) :
          Crypto.PairingGroup.G₁ × ZMod Crypto.PairingGroup.p × ZMod Crypto.PairingGroup.p → Bool

          Acceptance predicate for the forking lemma: run Schnorr verification.

          Equations
          Instances For
            source
            theorem CatCrypt.Examples.Schnorr.schnorr_forking_bound {P : Crypto.PairingGroup} {Msg S : Type} (A : SchnorrForger P Msg S) (pk : Crypto.PairingGroup.G₁) :
            Crypto.ForkingLemma.forkSuccProb A.toForkable pk (romAccept pk) ≥ Crypto.ForkingLemma.acceptProb A.toForkable pk (romAccept pk) ^ 2 - Crypto.ForkingLemma.acceptProb A.toForkable pk (romAccept pk) / ↑(Fintype.card (ZMod Crypto.PairingGroup.p))

            Forking bound. For any public key, the fork-success probability is at least acc² - acc / |ZMod p| — a direct instantiation of the core forking lemma fork_success_ge. Two successful runs share the commitment and (with probability accounted for by the - acc/|R| term) use distinct challenges, so special soundness extracts the discrete log.

            source
            noncomputable def CatCrypt.Examples.Schnorr.dlFromForking {P : Crypto.PairingGroup} {Msg S : Type} (A : SchnorrForger P Msg S) :
            Crypto.PairingGroup.G₁ → Core.SPComp (ZMod Crypto.PairingGroup.p)

            A discrete-log solver built from a Schnorr forger: fork, and on success extract via special soundness; otherwise fall back to a random guess.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem CatCrypt.Examples.Schnorr.dlFromForking_correct {P : Crypto.PairingGroup} {Msg S : Type} (A : SchnorrForger P Msg S) (pk a : Crypto.PairingGroup.G₁) (st : S) (c₁ c₂ : ZMod Crypto.PairingGroup.p) (hv₁ : schnorrVerify pk a c₁ (A.respond st c₁) = true) (hv₂ : schnorrVerify pk a c₂ (A.respond st c₂) = true) (hne : c₁ ≠ c₂) :
              Crypto.PairingGroup.zpowZMod₁ Crypto.PairingGroup.g₁ ((A.respond st c₁ - A.respond st c₂) * (c₁ - c₂)⁻¹) = pk

              Extraction correctness. On a successful fork — both transcripts accept and the challenges differ — the extracted scalar is the true discrete log of pk. This is exactly schnorr_special_soundness applied to the two replayed transcripts.