Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 169 research declarations. Search 10,000 more complete Mathlib declarations.
169 results
Clear filtersFiatShamir.sign_expectedQueryCost_eq_outputExpectation
Plain-language statement
Fiat-Shamir signing has expected weighted query cost equal to the expectation of the queried commitment cost over the output signature distribution.
Source project: VCVio
Person-level attribution pending.
FiatShamir.simulatedNmaAdv_hashQueryBound
Plain-language statement
Hash-query bound for simulatedNmaAdv: if the CMA adversary makes at most qS signing-oracle queries and qH random-oracle queries, the NMA reduction makes at most qH live hash queries. The qS signing queries are absorbed into the managed cache rather than issued live.
Source project: VCVio
Person-level attribution pending.
FiatShamir.Stateful.cma_advantage_le_fork_bound_of_h5
Project documentation
Native stateful top-level chain, assuming the H5 replay-forking boundary. This theorem carries the H1/H2/H3/H4 arithmetic directly in the stateful chain. The bound is in terms of the verify-wrapped adversary nmaAdvFromCmaWithFinalQuery at fork slot parameter qH.
Source project: VCVio
Person-level attribution pending.
FiatShamir.Stateful.cmaH3ExpectedLoss_le_queryBounds
Plain-language statement
Expected H3 loss from direct signing and hash query bounds. If the adversary makes at most qS signing queries and at most qH random oracle queries, the accumulated state-dependent signing slack is bounded by the standard qS * ζ + qS * (qS + qH) * β expression.
Source project: VCVio
Person-level attribution pending.
FiatShamir.Stateful.cmaReal_cmaSim_tv_sign_le_cmaSignEpsCore_of_valid
Plain-language statement
On a valid keypair state, the total-variation distance between the real and simulated signing oracle on a single signing query is bounded by cmaSignEpsCore.
Source project: VCVio
Person-level attribution pending.
FiatShamir.Stateful.cmaSignLogImpl_cmaSignHashQueryBound
Plain-language statement
Logging signing inputs while forwarding all queries preserves the joint signing/hash query bound.
Source project: VCVio
Person-level attribution pending.