# Merkle Trees

A Merkle tree is a cryptographic data structure designed by Ralph Merkle in the late 1970s and has grown dramatically in prominence in the last few years, inasmuch as variants of Merkle trees are at the core of most blockchain systems.

A Merkle tree makes use of cryptographic hashes to enable efficient cryptographic proofs of the authenticity of data stored in the tree. In particular, for a Merkle tree containing \(2^n\) data items, it only takes \(n\) hash computations to prove that a particular item is in the tree.

In this section, we build a very simple, but canonical, Merkle tree and prove it correct and cryptographically secure. And we’ll use several indexed inductive types to do it. Thanks to Aseem Rastogi for this example!

## Setting

Merkle trees have many applications. To motivate our presentation here, consider the following simple scenario.

A content provider (someone like, say, the New York Times) has a large archive of digital artifacts—documents, multimedia files, etc. These artifacts are circulated among users, but when receiving an artifact one may question its authenticity. One way to ensure the authenticity of received artifacts is for the content provider to use a digital signature based on a public-key cryptosystem and for users to verify these signatures upon receiving an artifact. However, signatures can be quite heavyweight for certain applications.

Instead, the content provider can organize their archive into a Merkle
tree, a tree of hashes with the artifacts themselves stored at the
leaves, such that a single hash associated with the root node of the
tree authenticates *all* the artifacts in the tree. By publishing just
this root hash, and associating with each artifact a path in the tree
from the root to it, a skeptical client can quickly check using a
small number of hash computations (logarithmic in the size of the
entire archive) whether or not a given artifact is authentic (by
recomputing the root hash and checking if it matches the known
published root hash).

## Intuitions

Our Merkle tree will be a full binary tree of height \(n\) storing
\(2^n\) data items and their corresponding hashes at the
nodes. The main idea of a Merkle tree is for each internal node to
also maintain a *hash of the hashes* stored at each of its
children. If the hash algorithm being used is cryptographically
secure, in the sense that it is collision resistant (i.e., it is
computationally hard to find two strings that hash to the same value),
then the hash associated with the root node authenticates the content
of the entire tree.

Informally, a Merkle tree is an authenticated data structure in that
it is computationally hard to tamper with any of the data items in the
tree while still producing the same root hash. Further, to prove that
a particular data item `d`

is in the tree, it suffices to provide
the hashes associated with the nodes in the path from the root to that
the leaf containing that item `d`

, and one can easily check by
comparing hashes that the claimed path is accurate. In fact, we can
prove that if a claimed path through the tree attests to the presence
of some other item `d' <> d`

, then we can construct a collision on
the underlying hash algorithm—this property will be our main proof of
security.

## Preliminaries

We’ll model the resources and the hashes we store in our tree as
strings of characters. F* standard library `FStar.String`

provides
some utilities to work with strings.

In the code listing below, we define the following

`lstring n`

, the type of strings of length`n`

. Like the`vec`

type,`lstring`

is a length-indexed type; unlike`vector`

it is defined using a refinement type rather than an indexed inductive type. Defining indexed types using refinements is quite common in F*.

`concat`

, a utility to concatenate strings, with its type proving that the resulting string’s length is the sum of the lengths of the input strings.

`hash_size`

and`hash`

, a parameter of our development describing the length in characters of a`hash`

function. The F* keyword`assume`

allows you to assume the existence of a symbol at a given type. Use it with care, since you can trivially prove anything by including an`assume nonsense : False`

.The type of resources we store in the tree will just be

`resource`

, an alias for`string`

.

```
//Length-indexed strings
let lstring (n:nat) = s:string{String.length s == n}
//Concatenating strings sums their lengths
let concat #n #m (s0:lstring n) (s1:lstring m)
: lstring (m + n)
= FStar.String.concat_length s0 s1;
s0 ^ s1
//A parameter, length of the hash in characters,
//e.g., this would be 32, if a character is 1 byte
//and we're using SHA-256
assume
val hash_size:nat
//The type of a hashed value
let hash_t = lstring hash_size
//The hash function itself
assume
val hash (m:string) : hash_t
//The type of resources stored in the tree
let resource = string
```

## Defining the Merkle tree

The inductive type `mtree`

below defines our Merkle tree. The type
has *two* indices, such that `mtree n h`

is the type of a Merkle
tree of height `n`

whose root node is associated with the hash
`h`

.

Leaves are trees of height `0`

and are constructed using `L res`

,
where the hash associated with this node is just `hash res`

, the
hash of the resource stored at the leaf.

Internal nodes of the tree are constructed using `N left right`

,
where both the `left`

and `right`

trees have the same height
`n`

, producing a tree of height `n + 1`

. More interestingly, the
hash associated with `N left right`

is `hash (concat hl hr)`

, the
hash of the concatenation of hashes of the left and right subtrees.

```
type mtree: nat -> hash_t -> Type =
| L:
res:resource ->
mtree 0 (hash res)
| N:
#n:nat ->
#hl:hash_t ->
#hr:hash_t ->
left:mtree n hl ->
right:mtree n hr ->
mtree (n + 1) (hash (concat hl hr))
```

In our previous examples like vectors, the index of the type
abstracts, or summarizes, some property of the type, e.g., the
length. This is also the case with `mtree`

, where the first index is
an abstraction summarizing only the height of the tree; the second
index, being a cryptographic hash, summarizes the entire contents of
the tree.

## Accessing an element in the tree

A resource identifier `resource_id`

is a path in the tree from the
root to the leaf storing that resource. A path is just a list of
booleans describing whether to descend left or right from a node.

Just like a regular binary tree, it’s easy to access an element in the
tree by specifying its `resource_id`

.

### Exercise

Implement a function to access an element in a `mtree`

in given a
`rid : list bool`

. Figuring out its type, including its decreases
clause, is the most interesting part. The function itself is
straightforward.

**Answer**

```
let resource_id = list bool
let rec get #h
(ri:resource_id)
(tree:mtree (L.length ri) h)
: Tot resource (decreases ri)
= match ri with
| [] -> L?.res tree
| b::ri' ->
if b then
get ri' (N?.left tree)
else
get ri' (N?.right tree)
```

## The Prover

Unlike the ordinary `get`

function, we can define a function
`get_with_evidence`

that retrieves a resource from the tree together
with some evidence that that resource really is present in the tree.
The evidence contains the resource identifier and the hashes of
sibling nodes along the path from root to that item.

First, we define `resource_with_evidence n`

, an indexed type that
packages a `res:resource`

with its `rid:resource_id`

and
`hashes:list hash_t`

—both `rid`

and `hashes`

have the same
length, which is the index of the constructed type.

The function `get_with_evidence`

is similar to `get`

, except as it
returns from descending into a child node, it adds the hash of the
other child node to the list of hashes.

```
type resource_with_evidence : nat -> Type =
| RES:
res:resource ->
ri:resource_id ->
hashes:list hash_t { L.length ri == L.length hashes } ->
resource_with_evidence (L.length ri)
/// Retrieves data references by the path, together with the hashes
/// of the sibling nodes along that path
let rec get_with_evidence (#h:_)
(rid:resource_id)
(tree:mtree (L.length rid) h)
: Tot (resource_with_evidence (L.length rid))
(decreases rid)
= match rid with
| [] ->
RES (L?.res tree) [] []
| bit::rid' ->
let N #_ #hl #hr left right = tree in
let p = get_with_evidence rid' left in
if bit then
let p = get_with_evidence rid' left in
RES p.res rid (hr :: p.hashes)
else
let p = get_with_evidence rid' right in
RES p.res rid (hl :: p.hashes)
```

In the cryptographic literature, this function is sometimes called
*the prover*. A `RES r ri hs`

is a claimed proof of the membership
of `r`

in the tree at the location specified by `ri`

.

Going back to our motivating scenario, artifacts distributed by our
content provider would be elements of the type
`resource_with_evidence n`

, enabling clients to verify that a given
artifact is authentic, as shown next.

## The Verifier

Our next step is to build a checker of claimed proofs, sometimes
called *a verifier*. The function `verify`

below takes a
`p:resource_with_evidence n`

, re-computes the root hash from the
evidence presented, and checks that that hash matches the root hash of
a given Merkle tree. Note, the `tree`

itself is irrelevant: all
that’s needed to verify the evidence is *the root hash* of the Merkle
tree.

```
let verify #h #n (p:resource_with_evidence n)
(tree:mtree n h)
: bool
= compute_root_hash p = h
```

The main work is done by `compute_root_hash`

, shown below.

In the first branch, we simply hash the resource itself.

In the second branch, we recompute the hash from the tail of the path, and then based on which direction was taken, we either concatenate sibling hash on the left or the right, and hash the result.

```
let tail #n (p:resource_with_evidence n { n > 0 })
: resource_with_evidence (n - 1)
= RES p.res (L.tail p.ri) (L.tail p.hashes)
let rec compute_root_hash (#n:nat)
(p:resource_with_evidence n)
: hash_t
= let RES d ri hashes = p in
match ri with
| [] -> hash p.res
| bit::ri' ->
let h' = compute_root_hash (tail p) in
if bit then
hash (concat h' (L.hd hashes))
else
hash (concat (L.hd hashes) h')
```

Convince yourself of why this is type-correct—refer back to the
description of vectors, if needed. For example,
why is it safe to call `L.hd`

to access the first element of
`hashes`

?

## Correctness

Now, we can prove our main correctness theorem, namely that
`get_with_evidence`

returns a resource with verifiable
evidence.

```
// Correctness theorem:
//
// Using get_with_evidence's with compute_root_hash correctly
// reconstructs the root hash
let rec correctness (#h:hash_t)
(rid:resource_id)
(tree:mtree (L.length rid) h)
: Lemma (ensures (verify (get_with_evidence rid tree) tree))
(decreases rid)
= match rid with
| [] -> ()
| bit::rid' ->
let N left right = tree in
if bit then
correctness rid' left
else
correctness rid' right
```

The proof is a simple proof by induction on the height of the tree, or equivalently, the length of the resource id.

In other words, evidence constructed by a honest prover is accepted by our verifier.

## Security

The main security theorem associated with this construction is the
following: if the verifier can be convinced to accept a resource with
evidence of the form `RES r rid hs`

, and if the resource in the
Merkle tree associated with `rid`

is *not* `r`

, then we can easily
construct a collision on the underlying cryptographic hash. Since the
hash is meant to be collision resistant, one should conclude that it
is at least as hard to convince our verifier to accept incorrect
evidence as it is to find collisions on the underlying hash.

We start by defining the type of a `hash_collision`

, a pair of
distinct strings that hash to the same value.

```
type hash_collision =
| Collision :
s1:string ->
s2:string {hash s1 = hash s2 /\ not (s1 = s2)} ->
hash_collision
```

The `security`

theorem shown below takes a `tree`

and
`p:resource_with_evidence n`

, where the refinement on `p`

states
that the verifier accepts the evidence (`verify p tree`

) although
the resource associated with `p.ri`

is not `p.res`

: in this case,
we can build a function, by induction on the height of the tree, that
returns a hash collision.

```
(*
* If [verify] can be tricked into accepting the evidence of [p] when
* [p.res] is not actually present in the tree at [p.ri], then
* we can exhibit a hash collision
*)
let rec security (#n:nat) (#h:hash_t)
(tree:mtree n h)
(p:resource_with_evidence n {
verify p tree /\
not (get p.ri tree = p.res)
})
: hash_collision
= match p.ri with
| [] -> Collision p.res (L?.res tree)
| bit::rid' ->
let N #_ #h1 #h2 left right = tree in
let h' = compute_root_hash (tail p) in
let hd :: _ = p.hashes in
if bit then
if h' = h1 then
security left (tail p)
else (
String.concat_injective h1 h' h2 hd;
Collision (concat h1 h2) (concat h' hd)
)
else
if h' = h2 then
security right (tail p)
else (
String.concat_injective h1 hd h2 h';
Collision (concat h1 h2) (concat hd h')
)
```

We look at its cases in detail:

In the base case, it’s easy to construct a hash collision directly from the differing resources.

Otherwise, we recompute the hash associate with the current node from the tail of the evidence presented, and the two cases of the left and right subtrees are symmetric.

If the recomputed hash matches the hash of the node, then we can generate a collision just by the induction hypothesis on the left or right subtree.

Otherwise, we can build a hash collision, relying on

`String.concat_injective`

, a lemma from the library stating that the concatenation of two pairs of equal length strings are equal only if their components are. Knowing that`h' <> h1`

(or, symmetically,`h' <> h2`

) this allows us to prove that the concatenations are unequal, although their hashes are, by assumption, equal.

## Exercise

Implement a function to update an `mtree`

at a given
`rid:resource_id`

with a new resource `res:resource`

. The
resulting tree will have a new root hash, so you will have to return
the new hash along with the updated tree.

**Hint**

One type of the `update`

function could be as follows:

```
type mtree' (n:nat) =
| MTree : h:hash_t -> mtree n h -> mtree' n
val update_mtree' (#h:hash_t)
(rid:resource_id)
(res:resource)
(tree:mtree (L.length rid) h)
: mtree' (L.length rid)
```

**Answer**

```
let rec update_mtree' #h
(rid:resource_id)
(res:resource)
(tree:mtree (L.length rid) h)
: Tot (mtree' (L.length rid))
(decreases rid)
= match rid with
| [] -> MTree _ (L res)
| hd :: rid' ->
if hd
then (
let MTree _ t = update_mtree' rid' res (N?.left tree) in
MTree _ (N t (N?.right tree))
)
else (
let MTree _ t = update_mtree' rid' res (N?.right tree) in
MTree _ (N (N?.left tree) t)
)
```

One interesting part of our solution is that we never explicitly
construct the hash of the nodes. Instead, we just use `_`

and
let F* infer the calls to the hash functions.

## Summary and Further Reading

In summary, we’ve built a simple but powerful authenticated data structure with a proof of its correctness and cryptographic security.

In practice, Merkle trees can be much more sophisticated than our the most basic one shown here. For instance, they can support incremental updates, contain optimizations for different kinds of workloads, including sparse trees, and be implemented using high-performance, mutable structures.

You can read more about various flavors of Merkle trees implemented in F* in the following papers.

EverCrypt, Section VII (B), describes a high-performance Merkle tree with fast incremental updates.

FastVer describes the design and use of hybrid authenticated data strutures, including sparse Merkle trees, for applications such as verificable key-value stores.