EUF-CMA security of the Fiat-Shamir Σ-protocol transform

End-to-end security reduction, packaged as three theorems:

• euf_cma_to_nma: CMA-to-NMA via HVZK simulation, absorbing the signing-query loss into a statistical term qS · ζ_zk + ζ_col;
• euf_nma_bound: NMA-to-extraction via Fork.replayForkingBound and special soundness, producing a reduction to hardRelationExp;
• euf_cma_bound: the combined bound, instantiating euf_cma_to_nma into euf_nma_bound.

theorem FiatShamir.euf_cma_to_nma {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} [SampleableType Stmt] [SampleableType Wit] (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (M : Type) [DecidableEq M] [DecidableEq Commit] [SampleableType Chal] (simTranscript : Stmt → ProbComp (Commit × Chal × Resp)) (ζ_zk ζ_col : ℝ) (_hζ_zk : 0 ≤ ζ_zk) (_hζ_col : 0 ≤ ζ_col) (_hhvzk : σ.HVZK simTranscript ζ_zk) (adv : (FiatShamir σ hr M).unforgeableAdv) (qS qH : ℕ) (_hQ : ∀ (pk : Stmt), signHashQueryBound M (adv.main pk) qS qH) : ∃ (nmaAdv : (FiatShamir σ hr M).managedRoNmaAdv), (∀ (pk : Stmt), nmaHashQueryBound M (nmaAdv.main pk) qH) ∧ SignatureAlg.unforgeableAdv.advantage (runtime M) adv ≤ Fork.advantage σ hr M nmaAdv qH + ENNReal.ofReal (↑qS * ζ_zk + ζ_col)

CMA-to-NMA reduction via HVZK simulation.

For any EUF-CMA adversary A making at most qS signing-oracle queries and qH random-oracle queries, there exists a managed-RO NMA adversary B such that:

Adv^{EUF-CMA}(A) ≤ Adv^{fork-NMA}_{qH}(B) + qS · ζ_zk + ζ_col

The NMA adversary B is constructed by:

• Forwarding A's hash queries to the external oracle (visible to Fork.fork)
• Simulating A's signing queries using the HVZK simulator, programming the simulated challenge into the cache
• Returning A's forgery together with the accumulated QueryCache

Each of the qS signing simulations introduces at most ζ_zk total-variation distance. The ζ_col term accounts for collisions where A queries a hash that B later programs.

This step is independent of special soundness and the forking lemma; those are handled by euf_nma_bound.

The Lean bound matches Firsov-Janku's pr_koa_cma at fsec/proof/Schnorr.ec:943: the CMA-to-KOA reduction uses eq_except (signed qs) LRO.m{1} LRO.m{2} as the RO-cache invariant, swaps real signing with simulator_equiv (per-query HVZK cost), handles RO reprogramming via lro_redo_inv + ro_get_eq_except, and absorbs the late-programming collision event through the bad flag, bounded by pr_bad_game at fsec/proof/Schnorr.ec:793 as QS · (QS+QR) / |Ω|, matching our ζ_col.

theorem FiatShamir.euf_nma_bound {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} [SampleableType Wit] (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (M : Type) [DecidableEq M] [DecidableEq Commit] [SampleableType Chal] (hss : σ.SpeciallySound) (hss_nf : ∀ (ω₁ : Chal) (p₁ : Resp) (ω₂ : Chal) (p₂ : Resp), Pr[⊥ | σ.extract ω₁ p₁ ω₂ p₂] = 0) [Fintype Chal] [Inhabited Chal] (nmaAdv : (FiatShamir σ hr M).managedRoNmaAdv) (qH : ℕ) (_hQ : ∀ (pk : Stmt), nmaHashQueryBound M (nmaAdv.main pk) qH) : ∃ (reduction : Stmt → ProbComp Wit), Fork.advantage σ hr M nmaAdv qH * (Fork.advantage σ hr M nmaAdv qH / (↑qH + 1) - challengeSpaceInv Chal) ≤ Pr[= true | hardRelationExp hr reduction]

NMA-to-extraction via the forking lemma and special soundness.

For any managed-RO NMA adversary B making at most qH random-oracle queries, there exists a witness-extraction reduction such that:

Adv^{fork-NMA}_{qH}(B) · (Adv^{fork-NMA}_{qH}(B) / (qH + 1) - 1/|Ω|) ≤ Pr[extraction succeeds]

Runs B.main pk twice with shared randomness up to a randomly chosen fork point, then re-samples the oracle answer. Programmed cache entries are part of B's deterministic computation given the seed, so they are identical across both fork runs. The reduction extracts only from fork outputs whose two forged transcripts share a commitment and whose cached challenges are distinct. The remaining proof obligation is to show that successful forks satisfy exactly those compatibility checks, after which special soundness applies.

Here Adv^{fork-NMA}_{qH}(B) is Fork.advantage: it counts exactly the managed-RO executions whose forgery already verifies from challenge values present in the adversary's managed cache or in the live hash-query log recorded by Fork.runTrace. This is the precise success event that the forking lemma can rewind.

This matches Firsov-Janku's schnorr_koa_secure at fsec/proof/Schnorr.ec:448, which applies forking_lemma_ro with the single-run postcondition verify plus the extractor correctness lemma extractor_corr at fsec/proof/Schnorr.ec:87. Our version uses Fork.replayForkingBound for the RO-level packaging and _hss for special soundness, with σ.extract playing the role of EC's extractor.

Currently conditional on the two B1 prefix-faithfulness sorrys (evalDist_uniform_bind_fst_replayRunWithTraceValue_takeBeforeForkAt and tsum_probOutput_replayFirstRun_weight_takeBeforeForkAt in ReplayFork.lean), which feed the Jensen/Cauchy-Schwarz step that powers Fork.replayForkingBound.

theorem FiatShamir.euf_cma_bound {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} [SampleableType Stmt] [SampleableType Wit] (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (M : Type) [SampleableType Chal] (hss : σ.SpeciallySound) (hss_nf : ∀ (ω₁ : Chal) (p₁ : Resp) (ω₂ : Chal) (p₂ : Resp), Pr[⊥ | σ.extract ω₁ p₁ ω₂ p₂] = 0) [Fintype Chal] [Inhabited Chal] (simTranscript : Stmt → ProbComp (Commit × Chal × Resp)) (ζ_zk ζ_col : ℝ) (hζ_zk : 0 ≤ ζ_zk) (hζ_col : 0 ≤ ζ_col) (hhvzk : σ.HVZK simTranscript ζ_zk) (adv : (FiatShamir σ hr M).unforgeableAdv) (qS qH : ℕ) (hQ : ∀ (pk : Stmt), signHashQueryBound M (adv.main pk) qS qH) : ∃ (reduction : Stmt → ProbComp Wit), have eps := SignatureAlg.unforgeableAdv.advantage (runtime M) adv - ENNReal.ofReal (↑qS * ζ_zk + ζ_col); eps * (eps / (↑qH + 1) - challengeSpaceInv Chal) ≤ Pr[= true | hardRelationExp hr reduction]

Combined EUF-CMA bound (Pointcheval-Stern with quantitative HVZK).

Composes euf_cma_to_nma and euf_nma_bound:

1. Replace the signing oracle with the HVZK simulator, losing qS · ζ_zk + ζ_col.
2. Apply the forking lemma to the resulting forkable managed-RO NMA experiment.

The combined bound is:

(ε - qS·ζ_zk - ζ_col) · ((ε - qS·ζ_zk - ζ_col) / (qH+1) - 1/|Ω|) ≤ Pr[extraction succeeds]

where ε = Adv^{EUF-CMA}(A). The ENNReal subtraction truncates at zero, so the bound is trivially satisfied when the simulation loss exceeds the advantage.

Currently conditional on two open obligations:

1. euf_cma_to_nma (this file, still sorry): CMA-to-NMA reduction via HVZK simulator.
2. The two B1 prefix-faithfulness sorrys in ReplayFork.lean (evalDist_uniform_bind_fst_replayRunWithTraceValue_takeBeforeForkAt and tsum_probOutput_replayFirstRun_weight_takeBeforeForkAt), which feed the Jensen/Cauchy-Schwarz step inside Fork.replayForkingBound; transitively inherited from euf_nma_bound.