Hash-Based Commitment Schemes — Binding via Collision Resistance

Hash-based commitment scheme construction and the standard-model reduction from binding to keyed collision resistance.

Given a keyed hash family H : KeyedHashFamily K (M × S) C, the scheme H.toCommitment commits to m : M by sampling a uniform opening s : S and returning (H k (m, s), s). Verification recomputes the hash and compares.

A binding adversary outputting two openings (c, m₁, s₁, m₂, s₂) with m₁ ≠ m₂ and both verifications passing yields a keyed-CR collision at (m₁, s₁) ≠ (m₂, s₂) with H k (m₁, s₁) = c = H k (m₂, s₂). Bound: bindingAdvantage H.toCommitment A ≤ keyedCRAdvantage H (bindingAdv_toCRAdv A).

This is the standard-model layer of the #284 consolidation chain binding ≤ keyed-CR ≤ birthday.

Main Definitions

• KeyedHashFamily.toCommitment — hash-based commitment scheme.
• bindingAdv_toCRAdv — reduction adversary from binding to keyed-CR.
• bindingAdvantage_toCommitment_le_keyedCRAdvantage — the binding bound.

def CollisionResistance.KeyedHashFamily.toCommitment {K M S C : Type} [SampleableType S] [DecidableEq C] (H : KeyedHashFamily K (M × S) C) : CommitmentScheme K M C S

Hash-based commitment scheme: commit to m by sampling a uniform opening s ← $ᵗ S and returning (H k (m, s), s). Verification recomputes the hash and compares to the committed value.

def CollisionResistance.bindingAdv_toCRAdv {K M S C : Type} (A : CommitmentScheme.BindingAdv K M C S) : KeyedCRAdversary K (M × S)

Reduction adversary: a binding adversary against H.toCommitment becomes a keyed-CR adversary against H by forgetting the commitment value and forwarding the two opening pairs ((m₁, s₁), (m₂, s₂)).

theorem CollisionResistance.bindingAdvantage_toCommitment_le_keyedCRAdvantage {K M S C : Type} [SampleableType S] [DecidableEq M] [DecidableEq S] [DecidableEq C] (H : KeyedHashFamily K (M × S) C) (A : CommitmentScheme.BindingAdv K M C S) : H.toCommitment.bindingAdvantage A ≤ keyedCRAdvantage H (bindingAdv_toCRAdv A)

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 (m₂, s₂). Since m₁ ≠ m₂ implies (m₁, s₁) ≠ (m₂, s₂), this is exactly a keyed-CR win for the reduction adversary, by transitivity through the common commitment c.