Merkle trees as authenticated data structures: verification and position binding

Cslib.Crypto.merkleRoot hashes a list of leaves and Cslib.Crypto.merklePath opens one position. This module adds the verifier and the security notion of an authenticated data structure scheme ([BS23], Section 8.9.1): a verifier merkleVerify with completeness, binding and a polynomial-time certificate, the game of Attack Game 8.2, and the security of Theorem 8.8, reduced to collision resistance with no loss.

• The verifier. merkleVerify H k d root i leaf path accepts when path has d labels, i < 2 ^ d, and the root recomputed from leaf at position i along path is root (the V of [BS23], Definition 8.3). These are the checks that the module documentation of Complexity.Crypto.Computational.MerkleTree requires of a verifier, under "What a verifier must check"; without them binding fails. Honest openings are accepted (merkleVerify_merklePath, merkleVerify_merklePath_of_clog_eq), the correctness requirement of Definition 8.3. An opening has one label per level, each of at most k.length bits when H k returns k.length bits (length_le_of_mem_merklePath).
• Binding of the verifier. Two openings of one position to different leaves, both accepted at the same depth, give a collision of H k, found by extractMerkleCollision (isCollision_of_merkleVerify).
• The game. In merkleBindingGame the adversary receives the security parameter and a uniform key k, and outputs a root, a position and two openings. It wins when both openings are accepted at the depth of the first path and their leaves differ (merkleBreaksBinding). MerklePositionBinding H asks that every uniform strict PPT adversary win with negligible probability.
• The reduction. merkleCollisionFinder runs the adversary and applies extractMerkleCollision to its two openings. Every win yields a collision, so the binding advantage is at most the collision advantage at every parameter (succProbability_merkleBindingGame_le), and the reduction is strict PPT (isPPT_merkleCollisionFinder). Hence every collision-resistant HashFamily gives position binding (HashFamily.merklePositionBinding).

Differences from [BS23]. Attack Game 8.2 is stated for a scheme over (X^n, Y) with a fixed number n of items; here:

• the hash is a keyed family with a uniform n-bit key, and adversaries are uniform strict PPT programs, as in CollisionResistant;
• the adversary chooses the depth d, the length of its first path, and must open both leaves at that depth, which makes the game stronger than one with a fixed depth;
• positions are 0 ≤ i < 2 ^ d, the padding positions included, rather than 1 ≤ i ≤ n;
• the adversary writes its position in unary (encMerkleBindingOutput), so the game covers polynomially bounded positions: enough for trees with polynomially many leaves, but not for trees whose leaves are indexed by superpolynomially many positions.

Kilian's construction. Kilian's succinct arguments commit to a PCP proof with a hash tree and open the queried positions (Barak and Goldreich, Construction 3.4, steps P1.3 and V3). That tree differs from this one, which is [BS23]'s Figure 8.12: its leaf labels are the proof bits themselves, not their hashes, and an internal label hashes the plain concatenation ℓ_γ0 ℓ_γ1 of its children's labels, not their encPair pairing. Its prover sends both child labels at every level of a path rather than only the siblings, and the verifier checks the same hash equations along the path. Barak and Goldreich's hashing family resists non-uniform circuits.

Main definitions

• Cslib.Crypto.merkleVerify: accepting an opening at a given depth.
• Cslib.Crypto.MerkleBindingOutput, Cslib.Crypto.encMerkleBindingOutput, Cslib.Crypto.MerkleBindingAdversary: the adversary's output, its encoding, and adversaries.
• Cslib.Crypto.merkleBreaksBinding, Cslib.Crypto.merkleBindingGame, Cslib.Crypto.MerklePositionBinding: the position-binding game and security notion.
• Cslib.Crypto.merkleCollisionFinder: the reduction to collision finding.

Main results

• Cslib.Crypto.merkleVerify_merklePath, Cslib.Crypto.merkleVerify_merklePath_of_clog_eq: honest openings are accepted.
• Cslib.Crypto.length_of_mem_merkleLevel, Cslib.Crypto.length_le_of_mem_merklePath: tree nodes have k.length bits, and the labels of an opening at most k.length bits.
• Cslib.Crypto.computableInPolyTime_merkleVerify: verification takes polynomial time.
• Cslib.Crypto.isCollision_of_merkleVerify: two accepted openings of one position to different leaves yield a collision.
• Cslib.Crypto.isCollision_of_merkleBreaksBinding, Cslib.Crypto.succProbability_merkleBindingGame_le, Cslib.Crypto.isPPT_merkleCollisionFinder: the certified reduction, with no loss.
• Cslib.Crypto.MerklePositionBinding.negligible, Cslib.Crypto.MerklePositionBinding.of_negligible: position binding as negligible success.
• Cslib.Crypto.HashFamily.merklePositionBinding: collision-resistant hash families give position binding.

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Section 8.9.1, Definitions 8.3 and 8.4, Attack Game 8.2 and Theorem 8.8.
• B. Barak, O. Goldreich, Universal Arguments and their Applications, Construction 3.4.

Verifying openings

def Cslib.Crypto.merkleVerify (H : List Bool → List Bool → List Bool) (k : List Bool) (d : ℕ) (root : List Bool) (i : ℕ) (leaf : List Bool) (path : List (List Bool)) : Bool

Accept path as an opening of position i of a depth-d tree with root root to leaf: the path has d labels, i < 2 ^ d, and the recomputed root is root. This is the verifier V of the Merkle tree as an authenticated data structure ([BS23], Definition 8.3), with the depth as an explicit argument.

theorem Cslib.Crypto.merkleVerify_merklePath {H : List Bool → List Bool → List Bool} {k : List Bool} (leaves : List (List Bool)) {i : ℕ} (hi : i < 2 ^ Nat.clog 2 leaves.length) : merkleVerify H k (Nat.clog 2 leaves.length) (merkleRoot H k leaves) i (leaves.getD i []) (merklePath H k leaves i) = true

Honest openings are accepted: every position i < 2 ^ Nat.clog 2 leaves.length of the tree over leaves, opened by its authentication path, is accepted against the root (the correctness requirement of [BS23], Definition 8.3).

theorem Cslib.Crypto.merkleVerify_merklePath_of_clog_eq {H : List Bool → List Bool → List Bool} {k : List Bool} {leaves : List (List Bool)} {d i : ℕ} (hd : Nat.clog 2 leaves.length = d) (hi : i < 2 ^ d) : merkleVerify H k d (merkleRoot H k leaves) i (leaves.getD i []) (merklePath H k leaves i) = true

Honest openings are accepted at any depth d equal to the tree's depth, for instance d = Nat.clog 2 N for N leaves.

theorem Cslib.Crypto.length_of_mem_merkleLevel {H : List Bool → List Bool → List Bool} {k : List Bool} (hlen : ∀ (k x : List Bool), (H k x).length = k.length) {leaves : List (List Bool)} {j : ℕ} {y : List Bool} (hy : y ∈ merkleLevel H k leaves j) : y.length = k.length

Every node of the tree has k.length bits when H k returns k.length bits.

theorem Cslib.Crypto.length_le_of_mem_merklePath {H : List Bool → List Bool → List Bool} {k : List Bool} (hlen : ∀ (k x : List Bool), (H k x).length = k.length) {leaves : List (List Bool)} {i : ℕ} {s : List Bool} (hs : s ∈ merklePath H k leaves i) : s.length ≤ k.length

Openings are short: the labels of an authentication path have at most k.length bits (a sibling outside the tree reads as []), so an opening of the tree over leaves has at most Nat.clog 2 leaves.length * k.length bits of labels.

theorem Cslib.Crypto.isCollision_of_merkleVerify {H : List Bool → List Bool → List Bool} {k : List Bool} {d : ℕ} {root : List Bool} {i : ℕ} {leaf₁ leaf₂ : List Bool} {path₁ path₂ : List (List Bool)} (h₁ : merkleVerify H k d root i leaf₁ path₁ = true) (h₂ : merkleVerify H k d root i leaf₂ path₂ = true) (hne : leaf₁ ≠ leaf₂) (n : ℕ) : isCollision H (fun (x : ℕ) (x_1 : List Bool) => true) n k (extractMerkleCollision H k leaf₁ leaf₂ i path₁ path₂).1 (extractMerkleCollision H k leaf₁ leaf₂ i path₁ path₂).2 = true

Binding of the verifier: two openings of position i to different leaves, both accepted against root at depth d, contain a collision of H k, which extractMerkleCollision finds. The length check makes the two paths equally long, as isCollision_extractMerkleCollision requires.

theorem Cslib.Crypto.computableInPolyTime_merkleVerify {H : List Bool → List Bool → List Bool} (hH : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool) => H p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hlen : ∀ (k x : List Bool), (H k x).length = k.length) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (List Bool × ℕ) × (List Bool × ℕ) × List Bool × List (List Bool)) => merkleVerify H p.1.1 p.1.2 p.2.1.1 p.2.1.2 p.2.2.1 p.2.2.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)))) Turing.MultiTapeTM.encBool

Verifying an opening takes polynomial time: the key, the depth in unary, the root, the position in unary, the leaf and the path.

Position binding

@[reducible, inline]

abbrev Cslib.Crypto.MerkleBindingOutput : Type

The output of a position-binding adversary: a root and a position, then two openings of that position, each a leaf and its path. The depth is the length of the first path.

@[reducible, inline]

abbrev Cslib.Crypto.encMerkleBindingOutput : MerkleBindingOutput ↪ List Bool

The encoding of MerkleBindingOutput: bit strings as themselves, the position in unary, as in computableInPolyTime_extractMerkleCollision. An efficient adversary therefore outputs only polynomially bounded positions.

@[reducible, inline]

abbrev Cslib.Crypto.MerkleBindingAdversary : Type

A position-binding adversary receives the unary security parameter n and the hash key, and outputs a root, a position and two openings.

def Cslib.Crypto.merkleBreaksBinding (H : List Bool → List Bool → List Bool) (k : List Bool) (out : MerkleBindingOutput) : Bool

out breaks position binding under the key k: both openings are accepted at the same position of the same root, at the depth of the first path, and their leaves differ.

noncomputable def Cslib.Crypto.merkleBindingGame (H : List Bool → List Bool → List Bool) (adversary : MerkleBindingAdversary) (n : ℕ) : ProbComp Bool

The position-binding experiment ([BS23], Attack Game 8.2, for a keyed hash): sample a uniform n-bit key k, run the adversary on (n, k), and accept when its output breaks binding under k.

def Cslib.Crypto.MerklePositionBinding (H : List Bool → List Bool → List Bool) : Prop

Position binding of Merkle trees over H ([BS23], Definition 8.4): every uniform strict PPT adversary breaks binding with negligible probability. Adversaries write positions in unary, so this covers polynomially bounded positions.

def Cslib.Crypto.merkleCollisionFinder (H : List Bool → List Bool → List Bool) (adversary : MerkleBindingAdversary) : CollisionFinder

The collision finder built from a position-binding adversary: run it, and extract a collision from its two openings with extractMerkleCollision.

theorem Cslib.Crypto.isCollision_of_merkleBreaksBinding {H : List Bool → List Bool → List Bool} {k : List Bool} {out : MerkleBindingOutput} (h : merkleBreaksBinding H k out = true) (n : ℕ) : isCollision H (fun (x : ℕ) (x_1 : List Bool) => true) n k (extractMerkleCollision H k out.2.1.1 out.2.2.1 out.1.2 out.2.1.2 out.2.2.2).1 (extractMerkleCollision H k out.2.1.1 out.2.2.1 out.1.2 out.2.1.2 out.2.2.2).2 = true

A binding break yields a collision: if out breaks position binding under k, then extractMerkleCollision finds two different inputs with the same hash under k.

theorem Cslib.Crypto.succProbability_merkleBindingGame_le {H : List Bool → List Bool → List Bool} (adversary : MerkleBindingAdversary) (n : ℕ) : Game.succProbability (merkleBindingGame H adversary n).eval ≤ Game.succProbability (collisionGame H (fun (x : ℕ) (x_1 : List Bool) => true) (merkleCollisionFinder H adversary) n).eval

The reduction loses nothing: at every security parameter, a position-binding adversary succeeds at most as often as its collision finder.

theorem Cslib.Crypto.isPPT_merkleCollisionFinder {H : List Bool → List Bool → List Bool} (hH : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool) => H p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hlen : ∀ (k x : List Bool), (H k x).length = k.length) {adversary : MerkleBindingAdversary} (hadversary : Probability.IsPPT encMerkleBindingOutput adversary) : Probability.IsPPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (merkleCollisionFinder H adversary)

The reduction is efficient: the collision finder of a strict PPT binding adversary is strict PPT, for a polynomial-time H that returns k.length bits.

theorem Cslib.Crypto.MerklePositionBinding.negligible {H : List Bool → List Bool → List Bool} (h : MerklePositionBinding H) (adversary : MerkleBindingAdversary) (hadversary : Probability.IsPPT encMerkleBindingOutput adversary) : Negligible fun (n : ℕ) => Game.succProbability (merkleBindingGame H adversary n).eval

Position binding gives negligible success probability to every strict PPT adversary.

theorem Cslib.Crypto.MerklePositionBinding.of_negligible {H : List Bool → List Bool → List Bool} (h : ∀ (adversary : ℕ → List Bool → ProbComp MerkleBindingOutput), Probability.IsPPT encMerkleBindingOutput adversary → Negligible fun (n : ℕ) => Game.succProbability (merkleBindingGame H adversary n).eval) : MerklePositionBinding H

Establish position binding by bounding every strict PPT adversary's success probability.

theorem Cslib.Crypto.HashFamily.merklePositionBinding {H : List Bool → List Bool → List Bool} (hH : HashFamily H) : MerklePositionBinding H

Collision-resistant hash families give position-binding Merkle trees ([BS23], Theorem 8.8, for keyed families and uniform adversaries): no uniform strict PPT adversary can open a position of a Merkle tree over a HashFamily to two different leaves, except with negligible probability. The reduction is merkleCollisionFinder, with no loss (succProbability_merkleBindingGame_le).