Merkle trees

A Merkle tree hashes a list of leaves to a single root so that each leaf can later be opened against the root with a short authentication path ([Mer90], Section 6; [BS23], Section 8.9). Here the hash is a keyed function H : List Bool → List Bool → List Bool, as in CollisionResistant. As in both sources, a leaf x becomes the node H k x, and the parent of nodes l and r is H k (encPair encBits encBits (l, r)). The pairing encPair is injective, so nodes of any length can be paired without ambiguity.

The tree over leaves has depth Nat.clog 2 leaves.length, the least d with leaves.length ≤ 2 ^ d. Missing leaves read as the empty word, padding the tree to 2 ^ d leaves as [BS23] suggests. For 2 ^ d leaves this is Merkle's H(1, 2 ^ d, Y), with his Y_i as leaves.getD (i - 1) []. For other leaf counts it differs from Merkle's recursion, which splits at the midpoint without padding.

An authentication path for position i lists the sibling of each node on the way from leaf i to the root. merkleRootOfPath recomputes a root from a leaf, a position and a path. Its correctness is merkleRootOfPath_merklePath. Binding is isCollision_extractMerkleCollision: two openings of the same position to different leaves, along paths of equal length and with the same recomputed root, contain a collision of H k, found deterministically by extractMerkleCollision. This is the reduction behind [BS23], Theorem 8.8.

What a verifier must check. Leaves and internal nodes are hashed with the same H k, with no domain separation, so a recomputed root alone binds nothing. A verifier must fix the path length to the depth d and check i < 2 ^ d:

• with a shorter path, an internal node's hash input opens as a leaf; for leaves [a, b], the "leaf" encPair encBits encBits (H k a, H k b) at position 0 with path [] recomputes the root;
• merkleRootOfPath reads only the low path.length bits of i, so positions wrap modulo 2 ^ path.length;
• the root does not fix the number of leaves: [a, b, c] and [a, b, c, []] have the same root.

The root, the path, root recomputation and extraction have plain polynomial-time certificates for hash families whose digests have the length of the key. Positions are unary in these certificates, which suits trees with polynomially many leaves.

Main definitions

• Cslib.Crypto.merkleParents, Cslib.Crypto.merkleLevel: one level of the tree from the one below, and level j counted from the hashed leaves.
• Cslib.Crypto.merkleRoot, Cslib.Crypto.merklePath: the root and the authentication path of a position.
• Cslib.Crypto.merkleInputs, Cslib.Crypto.merkleRootOfPath: the hash inputs met while recomputing a root from an opening, and the recomputed root.
• Cslib.Crypto.extractMerkleCollision: the first differing pair of hash inputs of two openings.

Main results

• Cslib.Crypto.length_merkleLevel, Cslib.Crypto.length_merklePath: level sizes and path length.
• Cslib.Crypto.merkleRootOfPath_merklePath: an honest opening recomputes the root.
• Cslib.Crypto.isCollision_extractMerkleCollision: a second opening of a position yields a collision.
• Cslib.Crypto.computableInPolyTime_merkleRoot, Cslib.Crypto.computableInPolyTime_merklePath, Cslib.Crypto.computableInPolyTime_merkleRootOfPath, Cslib.Crypto.computableInPolyTime_extractMerkleCollision: plain polynomial-time certificates.

References

• R. C. Merkle, A Certified Digital Signature, Section 6.
• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Section 8.9, Figure 8.12 and Theorem 8.8.

The tree

def Cslib.Crypto.merkleLeafLevel (H : List Bool → List Bool → List Bool) (k : List Bool) (leaves : List (List Bool)) : List (List Bool)

The hashed leaves of the tree over leaves, padded with the empty word to 2 ^ d leaves for d = Nat.clog 2 leaves.length.

def Cslib.Crypto.merkleParents (H : List Bool → List Bool → List Bool) (k : List Bool) (level : List (List Bool)) : List (List Bool)

The parents of a level: node i hashes the pair of nodes 2 * i and 2 * i + 1.

def Cslib.Crypto.merkleLevel (H : List Bool → List Bool → List Bool) (k : List Bool) (leaves : List (List Bool)) (j : ℕ) : List (List Bool)

Level j of the tree over leaves, counted from the hashed leaves at level 0.

def Cslib.Crypto.merkleRoot (H : List Bool → List Bool → List Bool) (k : List Bool) (leaves : List (List Bool)) : List Bool

The root of the Merkle tree over leaves ([BS23], Section 8.9).

def Cslib.Crypto.merkleSibling (p : ℕ) : ℕ

The position of the sibling of node p within its level.

def Cslib.Crypto.merklePathStep (H : List Bool → List Bool → List Bool) (k : List Bool) (state : List (List Bool) × ℕ × List (List Bool)) : List (List Bool) × ℕ × List (List Bool)

One step of merklePath: record the sibling of the current node, then move to the parent level and position.

def Cslib.Crypto.merklePath (H : List Bool → List Bool → List Bool) (k : List Bool) (leaves : List (List Bool)) (i : ℕ) : List (List Bool)

The authentication path of position i: the sibling of each node on the way from leaf i up to the root, starting at the leaves ([BS23], Figure 8.12).

Recomputing a root from an opening

def Cslib.Crypto.merkleInputsStep (H : List Bool → List Bool → List Bool) (k : List Bool) (state : List (List Bool) × ℕ) (sibling : List Bool) : List (List Bool) × ℕ

One step of merkleInputs: hash the current input to a node and pair it with sibling, putting the node on the left when the current position is even.

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

The hash inputs met while recomputing a root from leaf at position i along path, from the input of the root down to leaf itself.

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

The root recomputed from leaf at position i along the authentication path path ([BS23], (8.16)). Only the low path.length bits of i are read, and nothing checks the path length: a verifier must fix path.length to the depth d and check i < 2 ^ d (see the module documentation).

def Cslib.Crypto.extractMerkleCollision (H : List Bool → List Bool → List Bool) (k leaf₁ leaf₂ : List Bool) (i : ℕ) (path₁ path₂ : List (List Bool)) : List Bool × List Bool

The first pair of differing hash inputs, from the root down, of two openings of position i, or ([], []) if there is none.

Shape of the tree

@[simp]

theorem Cslib.Crypto.length_merkleLeafLevel {H : List Bool → List Bool → List Bool} {k : List Bool} (leaves : List (List Bool)) : (merkleLeafLevel H k leaves).length = 2 ^ Nat.clog 2 leaves.length

The tree over leaves has 2 ^ Nat.clog 2 leaves.length hashed leaves.

@[simp]

theorem Cslib.Crypto.length_merkleParents {H : List Bool → List Bool → List Bool} {k : List Bool} (level : List (List Bool)) : (merkleParents H k level).length = level.length / 2

A level has half as many parents as nodes, rounded down.

theorem Cslib.Crypto.getD_merkleParents {H : List Bool → List Bool → List Bool} {k : List Bool} {level : List (List Bool)} {i : ℕ} (hi : i < level.length / 2) : (merkleParents H k level).getD i [] = H k ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (level.getD (2 * i) [], level.getD (2 * i + 1) []))

Parent i hashes the pair of nodes 2 * i and 2 * i + 1.

theorem Cslib.Crypto.length_merkleLevel {H : List Bool → List Bool → List Bool} {k : List Bool} (leaves : List (List Bool)) (j : ℕ) : (merkleLevel H k leaves j).length = 2 ^ Nat.clog 2 leaves.length / 2 ^ j

Level j of the tree of depth d = Nat.clog 2 leaves.length has 2 ^ d / 2 ^ j nodes.

theorem Cslib.Crypto.merkleLevel_succ {H : List Bool → List Bool → List Bool} {k : List Bool} (leaves : List (List Bool)) (j : ℕ) : merkleLevel H k leaves (j + 1) = merkleParents H k (merkleLevel H k leaves j)

Each level consists of the parents of the level below.

theorem Cslib.Crypto.merklePath_eq {H : List Bool → List Bool → List Bool} {k : List Bool} (leaves : List (List Bool)) (i : ℕ) : merklePath H k leaves i = List.map (fun (t : ℕ) => (merkleLevel H k leaves t).getD (merkleSibling (i / 2 ^ t)) []) (List.range (Nat.clog 2 leaves.length))

The authentication path of position i lists, for each level t below the root, the sibling of the ancestor of leaf i at level t.

@[simp]

theorem Cslib.Crypto.length_merklePath {H : List Bool → List Bool → List Bool} {k : List Bool} (leaves : List (List Bool)) (i : ℕ) : (merklePath H k leaves i).length = Nat.clog 2 leaves.length

An authentication path has one sibling per level below the root.

theorem Cslib.Crypto.length_of_mem_merkleLeafLevel {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)} {y : List Bool} (hy : y ∈ merkleLeafLevel H k leaves) : y.length = k.length

Hashed leaves have the length of the key when the hash's digests do.

theorem Cslib.Crypto.length_of_mem_merkleParents {H : List Bool → List Bool → List Bool} {k : List Bool} (hlen : ∀ (k x : List Bool), (H k x).length = k.length) {level : List (List Bool)} {y : List Bool} (hy : y ∈ merkleParents H k level) : y.length = k.length

Parents have the length of the key when the hash's digests do.

Correctness of honest openings

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

Correctness: opening leaf i with its authentication path recomputes the root.

Binding

theorem Cslib.Crypto.isCollision_extractMerkleCollision {H : List Bool → List Bool → List Bool} {k leaf₁ leaf₂ : List Bool} {i : ℕ} {path₁ path₂ : List (List Bool)} (n : ℕ) (hlen : path₁.length = path₂.length) (hne : leaf₁ ≠ leaf₂) (hroot : merkleRootOfPath H k leaf₁ i path₁ = merkleRootOfPath H k leaf₂ i path₂) : 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, the deterministic reduction behind [BS23], Theorem 8.8: two openings of position i to different leaves, along paths of equal length and with the same recomputed root, contain a collision of H k, which extractMerkleCollision finds. Equal path lengths are essential, since leaves and internal nodes are not domain-separated; a verifier that fixes the path length to the depth d and checks i < 2 ^ d gives this hypothesis.

Polynomial time

theorem Cslib.Crypto.computableInPolyTime_merkleRoot {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 (List Bool)) => merkleRoot H p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits

Computing the root of a Merkle tree is polynomial-time for a polynomial-time keyed hash whose digests have the length of the key.

theorem Cslib.Crypto.computableInPolyTime_merklePath {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 (List Bool) × ℕ) => merklePath H p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encUnary)) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)

Computing an authentication path is polynomial-time for a polynomial-time keyed hash whose digests have the length of the key.

theorem Cslib.Crypto.computableInPolyTime_merkleRootOfPath {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 (List Bool)) => merkleRootOfPath H p.1 p.2.1 p.2.2.1 p.2.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)))) Turing.MultiTapeTM.encBits

Recomputing a root from an opening is polynomial-time for a polynomial-time keyed hash whose digests have the length of the key.

theorem Cslib.Crypto.computableInPolyTime_extractMerkleCollision {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) × List (List Bool)) => extractMerkleCollision H p.1 p.2.1.1 p.2.1.2 p.2.2.1 p.2.2.2.1 p.2.2.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits))))) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)

Extracting a collision from two openings is polynomial-time for a polynomial-time keyed hash whose digests have the length of the key.