Source-pinned research

Research proof index

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 1 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic
Project-declaredLean 4.32.0

Binding Advantage to Commitment le keyed CRAdvantage

CollisionResistance.bindingAdvantage_toCommitment_le_keyedCRAdvantage

Plain-language statement

Binding ≤ keyed-CR (standard model): for any binding adversary A against the hash-based commitment scheme H.toCommitment, the binding advantage is bounded by the keyed-CR advantage of H against the natural reduction adversary bindingAdv_toCRAdv A. A binding-game win has m₁ ≠ mā‚‚ together with both openings verifying: `H k (m₁, s₁) = c = H k (...

program verificationseparation logiccryptography

Source project: VCVio

Person-level attribution pending.

View proof record