Merkle Binding (Collision Lemma)

The structural collision lemma for inductive Merkle trees, often called the "Collision Lemma": two distinct leaf values that verify against the same Merkle root — under possibly different sibling proofs — entail a collision in the underlying hash function.

The hypothesis x ≠ y captures that the adversary equivocates on the committed value, which is what binding requires; the case x = y with different sibling proofs is not a binding break, since the committer is allowed to know multiple valid proofs of the same value.

The hash function is taken in curried form α → α → α, matching the convention used by getPutativeRootWithHash and the rest of the Merkle tree API.

The proof is constructive: findCollision is a computable function that walks two Merkle branches and returns a hash collision as data, rather than merely asserting its existence.

Main Definitions

• InductiveMerkleTree.Collision — specification: a hash collision under h : α → α → α.
• InductiveMerkleTree.findCollision — constructive search: given two branches with the same leaf index, look for a hash collision along the path.

Main Results

• InductiveMerkleTree.findCollision_sound — if findCollision returns a tuple, that tuple satisfies Collision.
• InductiveMerkleTree.getPutativeRootWithHash_binding — from any two distinct leaf values producing the same root at the same leaf index under (possibly different) sibling proofs, findCollision returns some.
• InductiveMerkleTree.getPutativeRootWithHash_binding_collision — the user-facing Collision Lemma: the tuple returned by findCollision is a genuine hash collision.

References

• Dan Boneh and Victor Shoup. A Graduate Course in Applied Cryptography. §8.9 (Merkle-Damgård and Merkle trees).

def InductiveMerkleTree.Collision {α : Type u_1} (h : α → α → α) (l₁ r₁ l₂ r₂ : α) : Prop

Two distinct input pairs producing the same hash output: a collision for the curried hash h : α → α → α.

def InductiveMerkleTree.findCollision {α : Type u_1} [DecidableEq α] (h : α → α → α) {s : BinaryTree.Skeleton} (idx : BinaryTree.SkeletonLeafIndex s) (proof₁ proof₂ : List.Vector α idx.depth) (x y : α) : Option (α × α × α × α)

Walk two Merkle branches with the same leaf index, looking for a hash collision. Returns some (l₁, r₁, l₂, r₂) if a collision is found (two distinct input pairs that hash to the same value), or none if the branches agree everywhere they are compared.

This is the constructive kernel of the Collision Lemma. Instead of merely asserting ∃ l₁ r₁ l₂ r₂, Collision h l₁ r₁ l₂ r₂, we compute the collision explicitly.

theorem InductiveMerkleTree.findCollision_sound {α : Type u_1} [DecidableEq α] (h : α → α → α) {s : BinaryTree.Skeleton} (idx : BinaryTree.SkeletonLeafIndex s) (proof₁ proof₂ : List.Vector α idx.depth) (x y l₁ r₁ l₂ r₂ : α) (hfind : findCollision h idx proof₁ proof₂ x y = some (l₁, r₁, l₂, r₂)) : Collision h l₁ r₁ l₂ r₂

Soundness: if findCollision returns a tuple, that tuple is a hash collision according to Collision.

theorem InductiveMerkleTree.getPutativeRootWithHash_binding {α : Type u_1} [DecidableEq α] (h : α → α → α) {s : BinaryTree.Skeleton} (idx : BinaryTree.SkeletonLeafIndex s) (proof₁ proof₂ : List.Vector α idx.depth) (x y : α) (hne : x ≠ y) (heq : getPutativeRootWithHash idx x proof₁ h = getPutativeRootWithHash idx y proof₂ h) : ∃ (l₁ : α) (r₁ : α) (l₂ : α) (r₂ : α), findCollision h idx proof₁ proof₂ x y = some (l₁, r₁, l₂, r₂)

Merkle binding: from two distinct leaf values x ≠ y that produce the same putative root at the same leaf index under (possibly different) sibling proofs, the constructive search findCollision returns some.

Note that idx is shared — this is binding at a fixed position. The distinct-position case requires walking down both paths to the lowest common ancestor and is handled separately.

Proof strategy: induction on idx. At each non-leaf step, the recursion of getPutativeRootWithHash exposes a top-level hash. Either the two pairs (subL, proof₁.head) and (subR, proof₂.head) it consumes already differ (top-level collision, so findCollision returns them) or they agree component-wise — in which case the inputs to the inner recursive calls disagree, so we recurse.

theorem InductiveMerkleTree.getPutativeRootWithHash_binding_collision {α : Type u_1} [DecidableEq α] (h : α → α → α) {s : BinaryTree.Skeleton} (idx : BinaryTree.SkeletonLeafIndex s) (proof₁ proof₂ : List.Vector α idx.depth) (x y : α) (hne : x ≠ y) (heq : getPutativeRootWithHash idx x proof₁ h = getPutativeRootWithHash idx y proof₂ h) : ∃ (l₁ : α) (r₁ : α) (l₂ : α) (r₂ : α), findCollision h idx proof₁ proof₂ x y = some (l₁, r₁, l₂, r₂) ∧ Collision h l₁ r₁ l₂ r₂

Collision Lemma for Merkle trees: from two distinct leaf values that produce the same putative root at the same leaf index under (possibly different) sibling proofs, findCollision returns a tuple that is a genuine hash collision.

Combines getPutativeRootWithHash_binding (the search succeeds) with findCollision_sound (its output satisfies Collision) into a single witness suitable for collision-resistance reductions.