Fiat–Shamir signatures

The Fiat–Shamir transform ([BS23], Section 19.6.1) turns a Sigma protocol into a signature scheme in the random-oracle model: to sign m, the prover commits to t, takes the challenge c := H(m, t) and responds with z; the signature (t, z) verifies when (t, H(m, t), z) is an accepting conversation.

Honest signatures verify (fiatShamir_correct). With special soundness, special HVZK and δ-unpredictable commitments ([BS23], Definition 19.7), a forger making at most Qs signing calls and Qro hash calls wins the random-oracle EUF-CMA experiment with probability ε bounded by

ε ≤ Qs · (Qs + Qro) · δ + (Qro + 1) / N + √((Qro + 1) · ε'),

where N is the number of challenges and ε' the success probability of an explicit adversary in the one-way game for the key generator (succProbability_eufCmaGame_le). This is [BS23], Equation 19.21, with Qs · (Qs + Qro) · δ in place of the slightly larger Qs · (Qs + Qro + 1) · δ.

The proof follows [BS23], Theorems 19.7 and 19.16, with the general forking lemma of [BN06] in place of the reduction through impersonation:

1. The signer is replaced by one that programs the oracle at (m, t) with a fresh challenge. The two agree until the signer's commitment hits a point already in the oracle's table, which has probability at most Qs · (Qs + Qro) · δ (the difference lemma, OracleComp.IdenticalUntilBad.bind_apply_le, and OracleComp.toOuterMeasure_bad_le).
2. Special HVZK replaces the programming signer by the simulator, which needs no witness.
3. The simulated transcripts are drawn in advance, one per call (OracleComp.IsQueryBounded.run_interpret_presample).
4. The result is a program over the hash oracle alone, with explicit coins (FiatShamir.forkingProgram), that names the hash query of the forgery whenever the forger wins. The forking lemma (OracleComp.le_add_sqrt_fork) and special soundness turn it into the one-way adversary FiatShamir.reduction.

These are exact probability laws for one Sigma protocol, key generator and forger; there is no efficiency claim. The forger has explicit coins, so the reduction can rerun it.

Main definitions

• Cslib.Crypto.Protocols.SigmaProtocol.fiatShamir: the Fiat–Shamir signature scheme.
• Cslib.Crypto.Protocols.SigmaProtocol.FiatShamir.forkingProgram: the forger with simulated signing, as a program over the hash oracle.
• Cslib.Crypto.Protocols.SigmaProtocol.FiatShamir.reduction: the one-way adversary.

Main results

• Cslib.Crypto.Protocols.SigmaProtocol.fiatShamir_correct: honest signatures verify.
• Cslib.Crypto.Protocols.SigmaProtocol.succProbability_eufCmaGame_le: the security bound.

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Sections 19.2 and 19.6.1.
• M. Bellare, G. Neven, Multi-Signatures in the Plain Public-Key Model and a General Forking Lemma, Lemma 1.
• A. Fiat, A. Shamir, How to Prove Yourself: Practical Solutions to Identification and Signature Problems.

noncomputable def Cslib.Crypto.Protocols.SigmaProtocol.fiatShamir {X Y T C Z M : Type} (P : SigmaProtocol X Y T C Z) (keyGen : PMF (X × Y)) : ROMSignature.Scheme Y (X × Y) M (T × Z) (M × T) C

The Fiat–Shamir signature scheme ([BS23], Section 19.6.1): the public key is the statement and the secret key the witness-statement pair. To sign m, commit to t, query the oracle at (m, t) for the challenge and respond; a signature (t, z) verifies when (t, H(m, t), z) is accepting.

theorem Cslib.Crypto.Protocols.SigmaProtocol.fiatShamir_correct {X Y T C Z M : Type} [DecidableEq M] [DecidableEq T] [Fintype C] [Nonempty C] {P : SigmaProtocol X Y T C Z} {keyGen : PMF (X × Y)} {R : X → Y → Prop} (hP : P.Complete R) (hkey : ∀ key ∈ keyGen.support, R key.1 key.2) : (P.fiatShamir keyGen).Correct

Correctness of Fiat–Shamir signatures: with a complete Sigma protocol and keys in the relation, every honest signature verifies.

The reduction

structure Cslib.Crypto.Protocols.SigmaProtocol.FiatShamir.ReductionState (M T C Z : Type) : Type

The state of the reduction while it runs the forger: the oracle table, each point with its challenge and, when the reduction asked its own oracle for the point, the position of that query; the messages signed so far; the number of queries asked so far; and the simulated transcripts not used yet.

• table : List ((M × T) × C × Option ℕ)

  The oracle table.

• signed : List M

  The messages signed so far.

• count : ℕ

  The number of queries asked so far.

• transcripts : List (T × C × Z)

  The simulated transcripts not used yet.

noncomputable def Cslib.Crypto.Protocols.SigmaProtocol.FiatShamir.reductionHandler {T C Z M : Type} [DecidableEq M] [DecidableEq T] [Nonempty C] [Nonempty T] [Nonempty Z] (q : M ⊕ M × T) : StateT (ReductionState M T C Z) (OracleComp fun (x : M × T) => C) (ROMSignature.ForgerSpec M (M × T) (T × Z) C q)

Answer the forger's calls without the witness, consuming one simulated transcript (t, c, z) per call. A signing call on m returns (t, z) and programs the table at (m, t) with c. A hash call returns the table's challenge, or asks the reduction's own oracle and records the answer with the position of the query.

def Cslib.Crypto.Protocols.SigmaProtocol.FiatShamir.verdict {X Y T C Z M : Type} [DecidableEq M] (P : SigmaProtocol X Y T C Z) (y : Y) (forged : (M × T × Z) × ReductionState M T C Z) (c : C) (position : Option ℕ) : Option ℕ × Bool × (M × T) × C × Z

The verdict on a forgery (m, (t, z)) whose point (m, t) has challenge c: the forgery wins when (t, c, z) is accepting and m was never signed, and then the reduction names position, the position of the query for (m, t). The verdict records the point, the challenge and the response.

noncomputable def Cslib.Crypto.Protocols.SigmaProtocol.FiatShamir.finish {X Y T C Z M : Type} [DecidableEq M] [DecidableEq T] (P : SigmaProtocol X Y T C Z) (y : Y) (forged : (M × T × Z) × ReductionState M T C Z) : OracleComp (fun (x : M × T) => C) (Option ℕ × Bool × (M × T) × C × Z)

Check a forgery, querying its point when the table lacks it.

noncomputable def Cslib.Crypto.Protocols.SigmaProtocol.FiatShamir.forkingProgram {X Y T C Z M : Type} [DecidableEq M] [DecidableEq T] [Nonempty C] [Nonempty T] [Nonempty Z] (P : SigmaProtocol X Y T C Z) (A : ROMSignature.Forger Y M (T × Z) (M × T) C) (s : Y × A.Coins × List (T × C × Z)) : OracleComp (fun (x : M × T) => C) (Option ℕ × Bool × (M × T) × C × Z)

The forger, with simulated signing, as a program over the hash oracle with explicit coins: the statement, the forger's coins and the simulated transcripts. It names the query of the forgery's point when the forger wins.

noncomputable def Cslib.Crypto.Protocols.SigmaProtocol.FiatShamir.coins {Y T C Z M : Type} [Fintype C] [Nonempty C] (simulate : Y → C → PMF (T × Z)) (A : ROMSignature.Forger Y M (T × Z) (M × T) C) (Q : ℕ) (y : Y) : PMF (Y × A.Coins × List (T × C × Z))

The coins of the forking program for the statement y: the forger's coins and Q simulated transcripts.

noncomputable def Cslib.Crypto.Protocols.SigmaProtocol.FiatShamir.reduction {X Y T C Z M : Type} [DecidableEq M] [DecidableEq T] [Fintype C] [Nonempty C] [Nonempty T] [Nonempty Z] [DecidableEq C] [Nonempty X] (P : SigmaProtocol X Y T C Z) (simulate : Y → C → PMF (T × Z)) (extract : Y → T → C → Z → C → Z → X) (A : ROMSignature.Forger Y M (T × Z) (M × T) C) (Qs Qro : ℕ) (y : Y) : PMF X

The one-way adversary built from a forger making at most Qs signing and Qro hash calls: draw one simulated transcript per call, fork the forking program with the Qro + 1 answers of its hash oracle, and extract a witness from the two forgeries.

Game hops

The reduction simulates the game

The reduction's runs on fixed answers

theorem Cslib.Crypto.Protocols.SigmaProtocol.succProbability_eufCmaGame_le {X Y T C Z M : Type} [DecidableEq M] [DecidableEq T] [Fintype C] [Nonempty C] [Nonempty X] [Nonempty T] [Nonempty Z] [DecidableEq C] {P : SigmaProtocol X Y T C Z} {keyGen : PMF (X × Y)} {R : X → Y → Prop} [(x : X) → (y : Y) → Decidable (R x y)] {extract : Y → T → C → Z → C → Z → X} {simulate : Y → C → PMF (T × Z)} {δ : NNReal} (hkey : ∀ key ∈ keyGen.support, R key.1 key.2) (hsound : P.SpecialSoundOn keyGen R extract) (hzk : P.SpecialHVZK R simulate) (hcommit : ∀ key ∈ keyGen.support, ∀ (t : T), (PMF.map Prod.fst (P.commit key.1 key.2)) t ≤ ↑δ) (A : ROMSignature.Forger Y M (T × Z) (M × T) C) {Qs Qro : ℕ} (hA : A.CallBounded Qs Qro) : ↑(Game.succProbability (ROMSignature.eufCmaGame (P.fiatShamir keyGen) A)) ≤ ↑Qs * (↑Qs + ↑Qro) * ↑δ + (↑Qro + 1) / ↑(Fintype.card C) + √((↑Qro + 1) * ↑(oneWayGame keyGen R (FiatShamir.reduction P simulate extract A Qs Qro)).succProbability)

Security of Fiat–Shamir signatures ([BS23], Theorem 19.16 with Equation 19.21, via [BN06], Lemma 1). Let the Sigma protocol be special sound on the generated keys with extractor extract, special HVZK with simulator simulate, and have δ-unpredictable commitments, and let the key generator produce pairs in the relation. A forger making at most Qs signing calls and Qro hash calls wins the random-oracle EUF-CMA experiment with probability at most Qs · (Qs + Qro) · δ + (Qro + 1) / N + √((Qro + 1) · ε'), where N is the number of challenges and ε' is the probability that the reduction outputs a witness for a generated statement.