Research proof index

CMA-to-NMA reduction for Fiat-Shamir signatures built from a Sigma protocol. The reduction runs the CMA adversary with simulated signing transcripts and a managed random oracle, then appends a single explicit live random-oracle query for the forgery's hash point so that the verification challenge is part of the forkable transcript (the `nmaAdvFromCmaWithF...

Running the inner unifForward + roImpl simulator against a source computation with an nmaHashQueryBound Q can grow the internal queryLog by at most Q. Each source Sum.inr step consumes one unit of the nmaHashQueryBound budget, while roImpl appends to queryLog only on a cache miss, hence at most once per such step.

If two successful contextual forks select the same fork index, their forgery targets agree.

NMA-to-extraction via the forking lemma and special soundness. The parameter qH is the fork slot parameter passed to Fork.forkPoint qH, i.e., the number of Fin (qH + 1) candidate target positions over which the replay-forking lemma sums. It is not required to be a valid query bound on the adversary: callers may supply a wrapped adversary with up...

Completeness of the Fiat-Shamir signature scheme follows from completeness of the underlying Σ-protocol.

Fiat-Shamir signing has expected weighted query cost equal to the expectation of the queried commitment cost over the output signature distribution.