Formal Verification of Authenticated, Append-Only Skip Lists in Agda: Extended Version

Authenticated Append-Only Skiplists (AAOSLs) enable maintenance and querying of an authenticated log (such as a blockchain) without requiring any single party to store or verify the entire log, or to trust another party regarding its contents. AAOSLs can help to enable efficient dynamic participation (e.g., in consensus) and reduce storage overhead. In this paper, we formalize an AAOSL originally described by Maniatis and Baker, and prove its key correctness properties. Our model and proofs are machine checked in Agda. Our proofs apply to a generalization of the original construction and provide confidence that instances of this generalization can be used in practice. Our formalization effort has also yielded some simplifications and optimizations.


Introduction
Decentralized technologies-such as blockchains [13]-that enable reliable coordination among parties that do not trust each other are of increasing interest and importance. It is common to maintain a self-authenticating log using hash chaining [20]: each entry (e.g., block or transaction) includes a cryptographic hash based on its own contents as well as on the previous entry. This technique ensures that a dishonest participant can "rewrite history" without detection only if it can find a collision for the cryptographic hash function used; it is a standard assumption that this is infeasible for a computationally bounded adversary.
Participating in consensus to add more entries to the log typically requires knowledge of the current "state", which is a function of all previous transactions. However, downloading and verifying the entire history and directly computing the state is too slow and expensive for many purposes, such as bringing a new participant online quickly.
One option is to provide a state and a quorum of signed digests for that state to a new participant . We could further enable to download only parts of the state that it needs by using more structured state types [11]. Although this enables to participate in consensus for appending new blocks to the chain, receiving and verifying the state at index does not enable to verify claims about transactions at indexes < without significant work. This is because hash-chaining typically used in blockchains is linear: to confirm a claim that a particular transaction is at index , must fetch and verify all transactions between and .
By instead using an Authenticated Append-Only Skip List [7] (AAOSL) to represent the log, an existing participant (the prover) can provide to a new participant (the verifier) an advancement proof from some previous log entry (perhaps the initial-or genesis-entry) to the new root digest that the verifier has obtained from a quorum of participants. The verifier can then receive a membership proof containing a claim about a previous log entry, and confirm that the claim is consistent with the log on which the previously verified advancement proof was based. The new participant can also construct advancement proofs and/or membership proofs pertaining to new log entries; thus it can assist another new participant to bootstrap in future. Together, these ideas enable dynamic participation without requiring any participant to possess all historical information.
To provide this functionality efficiently, the hash stored in each log entry is made to directly depend not only on the previous entry but also on selected entries further back in the log. The "hops" back to these previous entries are arranged so that advancement and membership proofs are logarithmic in the length of the log. As a result, these ideas enable dynamic participation that can be sustained over a long period of time, because the work required for a new participant to join grows only logarithmically with the length of the log.

arXiv:2103.04519v1 [cs.CR] 8 Mar 2021
These advantages come at the cost of using mechanisms that are significantly more complicated than linear hashchaining. Therefore, a formally verified model is paramount before using these techniques in practice.
Our primary contribution is a formal model of a class of AAOSLs and proofs of important properties about them in the Agda language [15]. Moreover, we prove that the original AAOSL [7] is an instance of this class and, consequently, enjoys the same properties. Finally, our formal verification work enabled us to simplify some aspects of the original AAOSL, such as the encoding of advancement proofs and the definition of authenticators.
We provide some background in Section 2 and then present a specification of the original AAOSL [7] in Section 3. In Section 4, we present our Agda model of a class of AAOSLs, proofs of key properties about them, and our proof that the original AAOSL is an instance of the class. We discuss related and future work in Section 5, and conclude in Section 6.

Background
To illustrate traditional linear hash chaining using Haskell, we define the following datatype and type synonyms. Auth a-the type of authenticated values of some type a-comprises a value of type a and its . We assume (via a type constraint ℎ a) that there is a function hash that receives an a and returns a fixed-length bytestring, which we call a digest (or hash).
The "genesis" log is represented as [ Auth a ★ h ★ ], where a ★ is agreed in advance and is used only to compute h ★ = hash a ★ ; we sometimes refer to index 0 as ★. The append function illustrates the hash chaining technique.
append :: ( ℎ a) ⇒ a → a → a append x [ ] = error " " append x (Auth y dy : l) = Auth x (hash (hash x + + dy)) : Auth y dy : l An initialized log comprises a head Auth y dy and a tail l. When appending x, the new log is constructed by hashing hash x concatenated with the latest hash in the log, dy. We chose to present append as adding an element to the front of the list for conciseness. An implementation that adds elements to the tail of a list would use the same hash chaining: the hash for the element at position + 1 depends exclusively on the hash of the element at position . Whether we interpret position 0 to be the leftmost or the rightmost element of the list is irrelevant for the remainder of our formalization.
With a traditional linear log, a client that knows the ℎ log entry can verify the ℎ entry for < only by recomputing each digest for entries + 1 to to confirm that the recomputed digest for matches. This is inefficient and requires possession of all entries between and .
(a) A skiplog with entries indexed 1 through 12 (b) The direct dependencies of ℎ 8 and ℎ 12 , needed to verify a proof of advancement from ℎ 7 to ℎ 12 assuming ℎ 7 is already known and trusted. An AAOSL [7] stores a (partial) log linearly as usual, but enables verifying earlier contents in the log, or verifying that a recent segment of the log builds on a known previous log, by verifying only a logarithmic amount of data.

The SkipLog
In traditional skip lists [18], for each inserted index, a "height" is probabilistically chosen, and for each level up to that height, a "skip pointer" to the previous index with a height of at least that level is stored.
A skiplog is an append-only variant, enabling the use of deterministic skip pointers per power of two, as seen in Figure 1(a). These skip pointers define a dependency relation (or hop relation) between indexes, and thus a dependency graph.
When traversing the list from index 12 to index 4, the shortest path is to take the skip pointer at level 3, from 12 to 8, then the one at level 3, from 8 to 4. A skip pointer at level skips 2 −1 entries back. The maximum skip level for an index > 0 is defined as + 1 where is the largest integer such that 2 divides . We use the type synonyms and (both s) to make the role of these values evident.
maxLvl :: The maximum skip level of a given index is exactly the number of other indexes it depends on. Therefore, the maximum skip level of index 0 is defined as 0, indicating that there is no skip pointer from 0. In our skiplogs, the hash of each entry is made to depend on all the entries one skip pointer away from it.
Appending an entry is similar to the description in Section 2. This time, however, we change how the hash of the appended entry is computed, ensuring that it depends directly on every log entry one skip pointer away from it. Thus, the hash for log index 8 depends on entries for 7, 6, 4, and ★.
The auth x log call computes the authenticator [7] of x at the new position in the log. The authenticator for position j is a hash computed using the hash of the data to be stored at j and the hashes of the entries one skip pointer back from j, namely entries at indexes − 2 −1 for l = 1, 2, . . . , maxLvl j.
in Auth a (auth j (hash a) deps) The lookupHash log i function returns the authenticator for the entry at position i and the auth auxiliary function assembles the necessary data into a single hash. This hash is determined by hashing the concatenation of the partial authenticators [7] of each dependency in deps. In the original presentation, partial authenticators are computed by hashing the current index, level, data, and the authenticator of the dependency, illustrated by the following pseudo-Haskell: , hash (encode j + + encode 2 + + datumDig + + lookup 1 lvlDigs) , . . . , hash (encode j + + encode l + + datumDig + + lookup (l − 1) lvlDigs) ]) where l = maxLvl j Translating the pseudo-Haskell above to working Haskell yields: auth :: → → [ ] → auth j datumDig lvlDigs = let pauth lvl lvldig = hash (encode j + + encode lvl The encode function encodes data in a , facilitating concatenation and hashing with the rest of the data. As in Section 2, the authenticator for the last position in the log depends (directly or indirectly) on the authenticators of every prior position and thus provides a "cumulative" hash of the whole structure.
We started our work using the original auth definition [7] shown above. However, our formalization effort revealed that any definition of auth that is injective in its second and third parameters suffices. That is, any auth such that auth j h 1 ds1 ≡ auth j h 2 ds2 implies h 1 ≡ h 2 and ds1 ≡ ds2 (modulo hash collisions) can be used as the definition for authenticators. We have done the proofs in the remainder of this paper for the original definitions as well as the following, simpler, auth function.

Advancement Proofs
As more data is appended to the log, a client must be able to verify that the maintainer did not rewrite history, that is, that the appended log entries are consistent with any previous log entries that the client has already verified. For this purpose, a maintainer constructs an advancement proof, which can be checked by a client that already knows and trusts the hash (authenticator) ℎ for the th log entry in order to verify that the hash ℎ for some > is consistent with extending the log from position to position . Depending on the use case, the advancement proof could be sent in response to an explicit request, or the sender could know what the recipient already knows and therefore what advancement proof it requires. Next, we examine how the hashing strategy described above enables efficient construction and verification of these advancement proofs.
An advancement proof comprises a Merkle path [9,11] in the skiplog. For example, consider the skiplog in Figure 1(a). Suppose Alice knows and trusts a value (call it a 7 ) for the cumulative hash at position 7, but has not yet verified that the log advanced from index 7 to 12. To verify that the advancement from 7 to 12 is consistent with the log she already trusts up to index 7, Alice needs enough information in addition to the hashes she already trusts to compute a value for ℎ 12 . Figure 1(b) illustrates this information: circles represent information Alice needs, squares represents information she already has, and the bold links show the path from 12 to 7; superfluous links have been erased for clarity.
If Alice can obtain ℎ 4 , ℎ 6 , ℎ 10 , ℎ 11 and the hashes of the data in positions 12 and 8 ( 12 and 8 ), then she can compute a value for ℎ 12 using a 7 (the value for index 7 that she already trusts), along with the genesis hash ℎ ★ . Note that Alice's possession of a value for the hash at index 7 does not imply that she also knows ℎ 4 or ℎ 6 : 7 is computed by hashing a value that depends on the data at index 7 and ℎ 6 , so Alice would have to invert the hash function to get ℎ 6 from ℎ 7 . In some contexts (such as in our motivating use case), Alice may already know the expected value for ℎ 12 (e.g., because consensus has been reached on it). In this case, she can compare her computed value 12 to ℎ 12 and confirm that the advancement from index 7 to 12 is consistent with the log that led to ℎ 12 . We encode the information Alice needs in the AdvProof type.
The structure of an advancement proof mimics a traversal through the skip pointers in a skip list. For example, an advancement proof from index 7 to index 12 sent to Alice can be represented by the following value p of type AdvProof : Each carries all the information needed to build an authenticator for the hop's source index using auth. For example, p's first hop (from index 12) contains the datum hash d 12 and information sufficient to determine the authenticators for each dependency of index 12, thus enabling the verifier to compute a 12 using auth, as shown above. The advancement proof contains two lists of authenticators for each hop: one for dependencies of the hop's source that are after the hop's target index, and one for those that are before it. In the example, the first list of the hop from 12 contains authenticators for 11 and 10, which are after 8 (the hop's target index), and there are no dependencies before 8 (note that the authenticator for the genesis index ★ is not needed because it is known by all in advance).
Finally the hop provides another advancement proof from the hop's target to the final target of the advancement proof (7 in this case), enabling recursive computation of the authenticator for the hop's target (8 in the example).
This structure enables us to rebuild an authenticator from an advancement proof by recursively computing the authenticator for the hop's target, and then using auth to combine this with the supplied authenticators for the other dependencies. When the recursion reaches the base case , the authenticator value provided to the rebuild function is used (+ + is list concatenation).
One can verify that rebuild p a 7 constructs the correct hash. Note that rebuild a 7 provides the hash Alice already trusts for index 7.
Building an advancement proof is done by traversing the dependency graph of the log. The smallest advancement proof is obtained by traversing from position to < via the highest level hop such that −2 −1 ⩾ ; this is facilitated by the singleHopLevel function.
singleHopLevel :: → → singleHopLevel from to = min (1 + floor (logBase 2 (from − to))) (maxLvl from) The mkadv function uses this to traverse the dependency graph of a log and construct an advancement from j to i: mkadv :: Advancement proofs can also be used to construct membership proofs: a maintainer can prove to a client that data d i is at position , if the client trusts the cumulative hash at position , for > . The maintainer sends an advancement proof from to , along with a list of the authenticators of the dependencies of ; the client can then compute and confirm the authenticator at .
Constructing values of type MembershipProof is trivial: We construct an advancement proof and add the necessary authenticators to it. Membership proofs can also be used to establish relative order between elements. Element is at an index smaller than element iff there is a membership proof from the index of to the index of .

Well-Formed and Normalized
Proofs. It is easy to construct values of type AdvProof that are not valid advancement proofs. For example, here are two non-well-formed advancements from index 4 to index 12: In w 1 , the 8 step is missing an authenticator. Recall that the authenticator for position i depends on maxLvl i authenticators. We are supposed to compute one authenticator recursively, which leaves the other maxLvl i − 1 of them to be specified by the advancement proof. Index 8 has level 4, so the total number of authenticators in the before and after lists should be exactly 3. For w 2 , the first hop should be at level 2, from index 12 to 12 − 2 2 ≡ 8, but the proof declares that the hop lands at index 6.
Consequently, we must identify what it means for a proof to be well formed-that is, it has the correct number of authenticators and takes the correct hop at every step.
Well-formedness is a purely structural constraint that is trivial to check in practice. In our formal development, we enforce the wellformed invariant at the type level, which precludes construction of non-well-formed proofs. Now, consider the following AdvProof from 4 to 12: Although w 3 is a well-formed proof, it takes more hops than necessary. A normalized proof takes the hop determined by singleHopLevel at each step, resulting in the shortest possible advancement proof, thus reducing bandwidth and computation requirements for sending and verifying them. Note that our results hold for advancement proofs formed by composition, which are not always normalized.

Size of Advancement Proofs.
A normalized advancement proof between indexes and > has at most 2⌈log 2 (1 + − )⌉ hops (we go up hop levels to get from to the maximum-length hop that does not overshoot , and each hop makes twice as much progress as the previous; similarly, we then go down from that hop to reach , with each hop progressing at least half the way to ). Each hop references at most ⌈log 2 ⌉ digests. These observations yield a bound of at most 2⌈log 2 This bound is conservative: there may be fewer hops, fewer digests per hop (and the maximum per hop is smaller for smaller indexes), and each digest is included only once, even if it is referenced by multiple hops in an advancement proof (see the type in Section 4.1). Proving a tighter bound is left as future work. However, using our Haskell specification to examine all normalized advancement proofs between indexes less than 1,000 yields several observations. The advancement proof from i = 1 to j = 991 is both the longest (visiting 17 indexes) and the largest (85 digests). About 40 digests are included on average, which is about 1/4 of the number indicated by the conservative bound. Avoiding duplicate digests (Section 4.1) saves only about 3 digests on average, but results in a worthwhile simplification to the algorithm and proofs.

Verifying Key Properties Using Agda
The original AAOSL work [7] presents manual proofs of several properties, showing that they can be violated only by an adversary that finds a collision for the underlying cryptographic hash function, which is assumed to be infeasible for a computationally bounded adversary. We have constructed an Agda proof of the main property specified by Maniatis and Baker, called Evolutionary collision resistance of AAOSL membership proofs (Theorem 3). Following the original naming, we call this property evo-cr.
The essence of the evo-cr property is that, if two clients have advanced their logs to a point with the same digest, then it is infeasible for a computationally bounded adversary to convince them to accept different authenticators for the same earlier log position, even if the clients advanced their logs via different advancement proofs. Furthermore, if the hop relation contains a hop between every index (except the initial index) and its predecessor-as with the hop relation defined in Section 3-then there is a "degenerate" advancement proof that visits every index between 0 and j, for any j. In this case, evo-cr implies that a computationally bounded adversary cannot convince a client to accept a membership proof for index i that is inconsistent with a given log at index i if the client has rebuilt the membership proof to the same authenticator as that log at index ⩾ .
Our proof of evo-cr is based on several applications of a key property that we prove first, called AgreeOnCommon (and of a variant of this property that we introduce later). This property states that, for any two advancement proofs into a new index , if rebuilding both proofs yields the same hash, then either these proofs agree on the authenticator for every index that they both visit, or there is a hash collision.
The overall proof is divided into two parts: an abstract model of a class of authenticated skip lists, and a concrete instantiation thereof, which we prove meets the necessary requirements. The abstract model assumes a (defined below). This type implies a dependency relation satisfying several properties that are introduced below. Our concrete skiplog (described in Section 3) is defined by instantiating the abstract model with a that implies the dependency relation described in Section 3. The same could be achieved for a wide variety of such dependency relations.
The record defines the class of skiplogs for which we prove AgreeOnCommon and then evo-cr.

record
: The definition requires a maxlvl function, which should return the number of hops from a given index, and a proof that the level of 0 is 0, i.e., there are no hops out of the initial index. For every index i there are maxlvl i hops, encoded by the datatype, and these hops have targets (hop--tgt). It is important that hop--tgt is injective (hop--inj), but also that taking a hop progresses, that is, the target of a hop is always smaller than the source (hop--<). It is also important that hops never cross over each other, which is ensured by hop--no--cross. This property is illustrated in Figure 2; we examine it in more detail when we describe how we ensure our concrete hop relation respects it in Section 4.4.
Constructing an inhabitant of with maxlvl as defined in Section 3 and hop--tgt { j } h defined as − 2 ℎ is mostly straightforward. However, although one can marvel at a geometric proof of the hop--no--cross property for this hop relation on a napkin, constructing a precise, machine checked proof of this property is a substantial challenge. In the second part of our proof, presented in Section 4.4, we prove that we can instantiate the abstract model with the hop relation used by our particular implementation.

Abstract Model
Our abstract model in Agda requires an arbitrary value of type as a module parameter, so the properties in this section apply to any dependency relation implied by 's requirements. Next, we introduce base notions necessary for constructing an AAOSL.
To avoid the inconsistency issues discussed in Section 3.1.1, we represent an advancement proof using a well-formed advancement path that simply indicates which hops the proof takes, along with the datum hashes of the source of each hop.
A prover provides the authenticators associated with the indexes in an advancement path in a separate view, which we model as a function from log indexes to hashes: This way, a single authenticator is provided for each index, regardless of how many times that index appears in the proof or is a dependency of an index that appears in the proof. (A practical Haskell implementation would represent a view as a partial map: . ℎ; if the map does not include an authenticator for an index required by the advancement proof, then the advancement proof is rejected.) The rebuild function in Agda operates over s instead of receiving and returning a single hash. This is important because it enables us to lookup all rebuilt authenticators from a proof. For example, take a = d 8 3 (  d 4 3 ). Calling rebuild a t, for some view t, will return another view t ′ , where we can lookup the newly rebuilt value for 8 with t ′ 8, and also check the recursively rebuilt hash for 4, used in the computation of t ′ 8, by calling t ′ 4.
Here, insert k v f inserts a new key-value pair into a map. Note how we are computing the authenticator for j using the view that results from recursively rebuilding the proof.
Next we look at encoding membership proofs, which reuse the constructions we have just seen. Although similar, membership proofs and advancement proofs work in different "directions". An advancement proof is used to prove to someone who trusts the hash of index that the skiplog can be extended to index > in a way that is consistent with the log up to index . Membership proofs, on the other hand, prove to a verifier who trusts the hash of > , that a given datum is at index .
As described above, when rebuilding an advancement proof from to , a verifier already knows and trusts an authenticator for index . In contrast, with membership proofs, the prover must provide sufficient additional information for the verifier to compute the authenticator for index . The datum hash is provided explicitly as the second component of the membership proof. The third component ensures that we do not construct a ℎ for index 0, which does not have associated data. (Agda uses × to express product types.) In addition to a MbrPath, the prover also provides a that the verifier uses to rebuild the MbrPath: Unlike with advancement proofs, the provided must also include authenticators for each dependency of index that-together with the datum hash-enable the verifier to compute the authenticator for index . Reasoning about collision resistance. The proofs presented in the next sections establish desired properties modulo hash collisions. Hence, it is important to model the possibility that an adversary may find hash collisions. One option for doing this in a constructive setting is to carry around hash collisions evidenced in existentials [2]. We use the ℎ datatype: This becomes necessary when reasoning about injectivity of authenticators, which is central to our proofs. If two advancement proofs a 1 : ℎ j i 1 and a 2 : ℎ j i 2 rebuild using views t 1 and t 2 respectively to the same authenticator at j (i.e., rebuild a 1 t 1 j ≡ rebuild a 2 t 2 j), then unless there is a hash collision, a 1 and a 2 provide the same datum hash for j and both rebuilds use the same authenticators for all dependencies of j.
This conclusion is reached via two injectivity lemmas applied to the evidence that the rebuilt views agree at j. The first establishes that (unless ℎ ), the datum hashes passed to auth to compute the authenticators for index j for the respective advancement proofs are equal: The auth--inj--1 lemma is says that, if the datumDig values passed to two invocations of auth are different, but they return the same hash, then we have a hash collision. Its proof is somewhat more involved, though, because auth uses concatenations and encoding of natural numbers into bytestrings. Therefore the proof requires reasoning about injectivity of encoding and of concatenation of fixed-size byte strings. We make a simplifying assumption that indexes are encoded into a fixed (but unspecified) number of bits. This assumption is reasonable in practice and not difficult to relax, but this would not add significant value to our proof.
Once we have auth--inj--1 to determine that the datum hashes are equal (unless ℎ ), we define the other injectivity lemma to conclude that the lists of digests provided to the lvldigs arguments of the respective auth invocations are also equal: Where t 1 t 2 xs states that t 1 x ≡ t 2 x for every x ∈ xs and depsof returns the dependencies of a given index j by enumerating all hops from j and computing their target. In case j is zero, it has no dependencies.
We have proven that both the original definition of auth used by Maniatis and Baker [7] and the simpler variant described in Section 3 satisfy these two injectivity lemmas. In fact, any definition of auth that satisfies auth--inj--1 and auth--inj--2 could be used to construct an AAOSL that enjoys all the properties we will explore next.

Proving AgreeOnCommon
The AgreeOnCommon property states that, given two advancement proofs into index j, if both proofs rebuild to the same hash, then either these proofs agree on the authenticators of every index that they visit in common, or the adversary found a hash collision. This is stated in Agda as follows: Here, _ ap _ encodes the relation of visited indexes of a given advancement proof. A value of type k ap a exists iff index k is visited by advancement proof a: The proof of AgreeOnCommon follows by induction on the commonly visited indexes of the advancement proofs under scrutiny. We present the proof in two parts. First, we explain how we encode this induction principle in a datatype, , and why it provides sufficient information to prove AgreeOnCommon. Later we prove that we can always construct a value of type for the advancement proofs expected by AgreeOnCommon.
Using the data type to prove AgreeOnCommon. In this section we focus on how captures enough information to conclude that two advancement proofs rebuild to the same hash at every index they both visit. Intuitively, a value of type t 1 t 2 a 1 a 2 represents a list of all indexes visited by both a 1 and a 2 , along with sufficient evidence to prove that the respective views obtained by rebuilding a 1 using t 1 and rebuilding a 2 using t 2 agree at each of these indexes. This can be seen in the type of aoc--correct, below. aoc--correct The proof of aoc--correct is a long but straightforward induction on and i ap a 1 and i ap a 2 . The more intellectual step lies in defining to have the right structure to make the rest of the proof straightforward. Intuitively, is like a zip over advancement proofs: it puts in evidence the commonly visited indexes. Its type signature reveals that it is a relation between ℎs from a common index j: Each of 's constructors represents one possible situation with advancement proofs that share a common index. There are three base cases that handle pairs of advancement proofs a 1 and a 2 that have one or two common indexes: (i) both proofs are , (ii) a 1 hops over a 2 , or (iii) a 2 hops over a 1 . These are captured by the following constructors: : --symmetric The first constructor represents pairs of advancement proofs that trivially agree on their only common index because both proofs are and the two views agree at that index.
In the second constructor, , the left advancement path is not : it takes a hop d h a 1 . Moreover, h hops over a 2 (note that the constructor requires evidence that hop--tgt h ⩽ i 2 ). The diagram below illustrates this case. requires evidence that rebuild ( d h a 1 ) t 1 agrees with rebuild a 2 t 2 on j, which is sufficient to ensure that both proofs rebuild to the same hash at j. It also requires evidence that hop--tgt h ⩽ i 2 , which implies that the advancement proofs can have at most one more commonly visited index besides j, which is i 2 when hop--tgt h ≡ i 2 . In this case, because i 2 would then be a dependency of j (evidenced by the implicit hop h provided to ), applying auth--inj--1 and auth--inj--2 to the hypothesis that d h a 1 and a 2 rebuild the same authenticator at j, yields t 1 t 2 (depsof j), implying that the digests for i 2 in the two advancement proofs are equal (again, unless ℎ ). This implies that the s resulting from rebuilding the two advancement proofs used the same authenticators for index i 2 ; some simple lemmas ensure that rebuilding hops to higher indexes do not modify the views at i 2 , so the rebuilt views also agree at i 2 , as required.
is symmetric to , capturing the case in which the right advancement proof hops over the entire left advancement proof.
Next we examine the three inductive cases of . The simplest is , which is used when both proofs take the same hop. requires evidence t 1 t 2 a 1 a 2 that the rebuilt views agree at all existing common indexes, as well as sufficient evidence to conclude that rebuild ( d h a 1 ) t 1 j is equal to rebuild ( d h a 2 ) t 2 j.
Finally, the case in which a 2 is extended to index j by a hop h 2 and a 1 is extended by a different path to index j is handled by the constructor; being its symmetric counterpart. This situation is captured in the diagram below. The idea here is that we can look at the advancement proof that takes the smaller hop as a composition of two advancement proofs making evident the next common index.
and are similar to in that they all require an t 1 t 2 a 1 a 2 , which provides evidence that the smaller advancement proofs agree at each of their common indexes. They also all require sufficient evidence to prove that the authenticator computed for the new common index j is the same following either of the new advancement proofs to index j.
One important observation is that rebuilding an advancement proof never interferes with previous indexes. That is, rebuilding a path e : ℎ j 1 j 2 on a view that was obtained from rebuilding a : ℎ j 2 i on a view t will not change any authenticator already computed for any k ⩽ i. This is witnessed by the rebuild--⊕ property below, which guarantees that the inductive hypothesis provided by t 1 t 2 a 1 a 2 in is not falsified by rebuilding (e ⊕ a 1 ) on top of t 1 .
rebuild--⊕ : ∀ { j 1 j 2 i k t } (e : ℎ j 1 j 2 ) (a 1 : ℎ j 2 i) → k ap a 1 → rebuild (e ⊕ a 1 ) t k ≡ rebuild a 1 t k This property is proved by a simple induction using the fact that computing authenticators for indexes higher than j 2 does not modify the provided view at j 2 or any lower index. Because k ap a 1 and a 1 is an ℎ j 2 i, k ⩽ j 2 ; thus the two rebuilds agree at k.
Using rebuild--⊕, we prove AgreeOnCommon--∈, a variant of AgreeOnCommon that allows a 2 to be an ℎ j 2 i 2 for any index j 2 that is visited by a 1 (i.e., j 2 ap a 1 ), not just the source index of a 1 as required by AgreeOnCommon. AgreeOnCommon--∈ requires that the two advancement proofs rebuild to the same hash at their common index j 2 .

Constructing an inhabitant.
To conclude the proof of AgreeOnCommon, we must construct an t 1 t 2 a 1 a 2 given rebuild a 1 t 1 j ≡ rebuild a 2 t 2 j, where a 1 and a 2 are advancement proofs to index j. This is accomplished by the aoc lemma. aoc : ∀ { i 1 i 2 j } (t 1 t 2 : ) (a 1 : ℎ j i 1 ) (a 2 : ℎ j i 2 ) → i 1 ⩽ i 2 --w.l.o.g → rebuild a 1 t 1 j ≡ rebuild a 2 t 2 j → ℎ ℎ ( t 1 t 2 a 1 a 2 ) First, we pattern match on a 1 and a 2 and compare the hop--tgt (if any) of the hops taken. This enables us to understand which constructor of must be used. In most cases we can easily extract the evidence needed for the relevant constructor via case analysis on the structure of the two proofs and the injectivity lemmas discussed above, applied to the hypothesis that rebuild a 1 t 1 j ≡ rebuild a 2 t 2 j.
However, we face an additional challenge when the two advancement proofs take different hops, but neither hop passes the other's entire proof. These cases require the or constructor, and we must split the proof that took the shorter hop into two composable pieces in order to obtain an advancement proof between the targets of the hops taken by the respective advancement proofs. This is needed for the e argument to the constructor. Because of the hop--no--cross requirement on we can always perform this split as evidenced by the lemma below. No hop can cross from an index strictly between hop--tgt h 2 and hop--tgt h 1 to an index lower than or equal to hop--tgt h 1 without passing through hop--tgt h 1 first.

Proving evo-cr
With AgreeOnCommon out of the way, we move to the key correctness property evocr [7], which states that a computationally bounded adversary cannot produce two advancement proofs a 1 and a 2 that rebuild to the same authenticator at some index , and also provide two membership proofs from s 1 to tgt and s 2 to tgt that prove a conflicting claim at tgt, given that a 1 visits s 1 and a 2 visits s 2 .
To enable a rigorous proof of this property, we require a precise statement of it, which is provided by the type of evo-cr and illustrated in Figure 3.
ℎ j i 1 ) (a 2 : ℎ j i 2 ) → rebuild a 1 t 1 j ≡ rebuild a 2 t 2 j → ∀ { s 1 s 2 tgt } { u 1 u 2 : } → (m 1 : MbrPath s 1 tgt) (m 2 : MbrPath s 2 tgt) → s 1 ap a 1 → s 2 ap a 2 → s 1 ⩽ s 2 → i 1 ⩽ tgt → i 2 ⩽ tgt → rebuildMbr m 1 u 1 s 1 ≡ rebuild a 1 t 1 s 1 → rebuildMbr m 2 u 2 s 2 ≡ rebuild a 2 t 2 s 2 → ℎ ℎ (datum--hash m 1 ≡ datum--hash m 2 ) When translating the informal statement of this property [7] to a precise one, we originally [12] required tgt to be visited by both a 1 and a 2 . This was a mistake, because the purpose of a membership proof is to enable proving that a log entry that has not necessarily been verified previously is consistent with an advancement proof that has been verified: if tgt were required to be in the advancement proof, then it would already have been verified. Therefore, in this extended version, we present the proof of the stronger evo-cr property stated above.
The bulk of the proof of evo-cr comprises proving that the authenticators computed for index tgt when rebuilding m 1 and m 2 are equal, enabling us to invoke auth--inj--1 to establish that (unless there is a hash collision), the two membership proofs m 1 and m 2 claim the same datum at index tgt. To achieve this, we must work back from the assumptions that m 1 (respectively m 2 ) rebuilds to an index s 1 (respectively s 2 ) visited by a 1 (respectively a 2 ), consistent at these indexes with rebuilding a 1 and a 2 , and that a 1 and a 2 build to the same hash at their common index j.
The first step is to split a 1 into a 11 ⊕ a 12 , and similarly for a 2 , as depicted in Figure 3. Next, following the original manual proof [7], we identify two special indexes, each of which is common to three advancement proofs.
The first special index, which we call M (consistent with index m in [7, Fig. 4]), is required to be common to a 22 , m 2 and a 11 . If, s 1 = s 2 , then that index serves the purpose, because every ℎ contains its starting and ending indexes. Otherwise, s 1 < s 2 . In that case, M is chosen to be the last index in a 11 before s 2 (note that it exists because s 1 < s 2 , so s 1 could be M if there is no index in a 11 between s 1 and s 2 ). The function last--bef determines M: We define M as last--bef a 11 prf , where prf is evidence that s 1 < s 2 . A correctness lemma establishes that M ap a 11 : We also prove that M ap a 22 and M ap mbr--path m 2 , via two applications of the following lemma, which is based on Lemma 5 of the original manual proof [7], hence the name: Lemma 5 ensures that, given an advancement proof a from j to i and another advancement proof b from k to i 0 , where i < k ⩽ j and i 0 ⩽ i, the last index in a before index k is also in b.
The key to proving this lemma is the hop--no--cross property: because b is an ℎ k i 0 , last--bef a ik kj < k, and i 0 ⩽ i ⩽ last--bef a ik kj, b must pass index last--bef a ik kj; due to hop--no--cross, it cannot do so without visiting index last--bef a ik kj.
Similarly, we identify the second special index R (corresponding to r in [7,Fig. 4]) and prove that R ap mbr--path m 1 , R ap mbr--path m 2 and R ap a 12 . If tgt = s 1 , then that index serves the purpose of R, again because every ℎ includes its endpoints. Otherwise, tgt < s 1 , and we show that the first index in a 12 after tgt can serve as R, using similar machinery as above (first--aft, first--aft--correct and lemma5 ′ , not shown).
Having established the two special indexes M and R, and showing that each of them is common to three advancement proofs, we then proceed to prove that the authenticators computed for index tgt when rebuilding m 1 and m 2 are equal. Our proof is based on several applications of AgreeOnCommon and its variant AgreeOnCommon--∈, as well as some smaller lemmas including rebuild--⊕. Next we look at the individual proof steps together with an illustration on how they are related, in Figure 3.
1. First, we notice that a 1 = a 11 ⊕ a 12 and a 2 = a 21 ⊕ a 22 arrive and agree at j: rebuild a 1 t 2 j ≡ rebuild a 2 t 2 j. Now define M as last--bef a 11 hyp, where hyp is the hypothesis that s 1 < s 2 , we have that M ap a 22 and M ap a 11 . A first application of AgreeOnCommon yields: Here, u 2 ′ = insertAuth u 2 tgt (datum--hash m 2 ). Thus, we have established that rebuilding a 1 yields the same hash at M as rebuilding m 2 , but rebuilding only the m 22 component. (3) that a 1 = a 11 ⊕ a 12 rebuilds to the same hash as m 2 at index M, we can now show that they also agree at index R (recall that R ap a 12 and R ap m 2 ). To do so, we apply AgreeOnCommon--∈ to  Figure 3. Graphical representation evo-cr property [7]. Thick lines represent the advancement paths, thin lines represent the membership proofs, dotted lines represent points that must be visited by all proofs they intersect and the numbered dots reference the proof step that justifies the intersection. a 1 and m 22 using (4), yielding:

Having established in
This invocation of AgreeOnCommon--∈ requires evidence that R ap m 22 , which is proved using some simple lemmas (not shown) that reason about whether an index in an ℎ that is formed by composing two ℎs using ⊕ is in the first or second ℎ, depending on its index.
6. Analogous to (2), we again invoke AgreeOnCommon using the hypothesis that rebuildMbr m 1 u 1 s 1 ≡ rebuild a 1 t 1 s 1 in combination with rebuild--⊕ to show that rebuilding a 12 and m 1 yield the same hash at index R.
rebuild a 12 t 1 R ≡ rebuildMbr m 1 u 1 R 7. Next, we split m 1 at index R, resulting in mbr--path m 1 ≡ m 11 ⊕ m 12 (not labelled in Figure 3). Then, combining (5) and (6) and using rebuild--⊕ twice, we establish that rebuilding m 22 and m 12 both result in the same hash at index R: rebuild m 22 u 2 ′ R ≡ rebuild m 12 u 1 ′ R (Here, u 1 ′ is defined analogously to u 2 ′ .) At last we know that the rebuilds of m 12 and m 22 agree at an index (R) that they share; next we work back from there to show that they also agree at tgt.
8. By applying AgreeOnCommon--∈ using (7), we can conclude that the views achieved by rebuilding m 22 and m 12 agree at index tgt.
10. Finally, the observation that rebuilding an ℎ j i using view t does not modify t at i establishes that the authenticators computed for index tgt when rebuilding m 1 and m 2 are equal.
This concludes the abstract properties. We have shown how any value of will yield a skiplog that enjoys AgreeOnCommon and evo-cr. The next step is proving that we can inhabit the datatype with the skiplog described in Section 3.

Instantiating the Abstract Model
Having proved that any instantiation of enjoys the AgreeOnCommon and evo-cr properties, we now instantiate with the hop relation defined in Section 3: we define maxlvl to be equivalent to the definition presented there (see below) and define hop targets as follows.
We use Agda's . − operator, which truncates negative subtraction results to zero. Reasoning is simplified by a lemma proving that hop targets never "overshoot" zero.
In this section, we explain how we provide the remaining properties required to prove that the hop relation arising from the definitions of maxlvl and hop--tgt satisfies the requirements of . Most of them are straightforward. However, proving that this relation satisfies hop--no--cross is quite challenging. The first step towards a manageable proof is to define suitable induction principles over the hops we seek to analyze.
In our case, we want to prove a number of lemmas over the structure that arises from establishing − 2 as a dependency of , for less than the largest power of two that divides . Because − 2 +1 = ( − 2 ) − 2 , we can form hops at level l + 1 by composing adjacent hops at level l.
This structure is encoded in a simple Agda datatype: A value h of type l j i proves the existence of a hop at level l connecting j and i. The constraint that suc l < maxLvl x ensures that hops are created from index x only for levels up to maxLvl x. Without this constraint, for example, a hop from index 6 to index 2 could be constructed, which would cross the hop from 0 to 4. As neither of these hops is nested within the other, this would violate the hop--no--cross property, thus preventing a proof that our hop relation inhabits . Another aspect that complicated our earlier direct proof efforts was the difficulty of dealing inductively with the original recursive definition of the maxLvl function, defined in Agda as: We tamed this complexity by observing that every nonzero natural number can be uniquely represented as the product of a power of two and an odd number, and then using a non-inductive definition of maxLvl that is isomorphic to our original definition. This is known as a view type in the literature [8].
This enables us to write a non-inductive version of maxLvl that simply extracts this largest power of two.
The definition of maxLvl ′ is provably equivalent to the recursive version maxLvl used in the specification. The proof is an easy induction on n, and the lemma is used frequently throughout the proofs in our model and has been invaluable in helping us complete the proof. maxLvl ≡ maxLvl : ∀ n → maxLvl n ≡ maxLvl ′ (to n) Next, we must be able to inhabit the type , witnessing the existence of hops from a given index into − 2 , as long as is less than maxLvl j. This proves that the datatype is inhabited and meets the criteria we expect: i.e., it connects and its dependencies one power of two away.
h--correct : ∀ j l → l < maxLvl j → l j (j − 2 l ) Conversely, given h : l j i, we can prove that is a 2 away from , which shows that the datatype encodes exactly the required structure.
A central lemma used in the proof that our hop relation satisfies the hop--no--cross property is that all the indexes that a hop skips over have a level lower than the level of the hop. In other words, if a hop from to at level hops over index , then maxLvl k is at most .
Next, we discuss how we prove that our hop relation satisfies the hop--no--cross property required by . Recalling the definition of this property, as illustrated in Figure 2, it would suffice to prove the following property: This property captures the intuition of hops not crossing: given any two hops that do not share an index (w.l.o.g. i 2 < i 1 ), either they do not overlap or one is contained within the other. (Note that two hops that share an index do not cross.) Our earlier attempts to prove nocross ′ directly became unmanageable due to the combined effects of dealing with arithmetic nuances, seemingly minor details such as subtraction in Agda truncating to zero to ensure the result is always a natural, and the fact that recursive calls do not directly inform us about the relationship between l 1 and l 2 .
Therefore, we instead prove hopcross via a stronger property and an auxiliary lemma: nocross : ∀ { l 1 i 1 j 1 l 2 i 2 j 2 } (h 1 : l 1 j 1 i 1 ) (h 2 : l 2 j 2 i 2 ) The auxiliary lemma is proved via a straightforward induction on hops, using the following definition of ⊆. This definition establishes that every hop contains itself, and then recursively defines a hop h as being contained by another if the latter is the composition of two adjacent hops, one of which contains h. However, this simplified description is too inclusive. Observe that the left and right constructors require constraints to enable the construction of legitimate hops using the hs constructor of .
With these definitions established, we can describe the proof that our hop relation satisfies the nocross property, which proceeds by case analysis on hops. To facilitate this case analysis, we define an auxiliary relation that categorizes the relationship between two hops h 1 and h 2 into one of five possible situations, depending on the relative indexes of the hops' sources and targets: It is interesting to note that the definition of the categorization mechanism (not shown) is mutually recursive with the definition of nocross: it uses nocross to distinguish some cases. Agda's termination checker confirms there is no circular reasoning here because it can prove that such recursive uses of nocross are on lower level hops, implying that the recursion must terminate. Figure 4. There exists no p with type suc l < maxLvl j 2 when in this situation. Hence, the composite hop hs v 0 v 1 p cannot be built.
The proof of nocross h v proceeds by induction on v. If hop--tgt h ⩽ hop--tgt v, then nocross holds vacuously. Otherwise, hop--tgt v < hop--tgt h, so if one hop is nested within the other, then it is h that is contained within v, the longer hop.
If v is a hop at level zero, we are done because any hop that hops over v must contain it. In case v is a composite hop hs v 0 v 1 p, we use the categorization mechanism to determine the relationship between h and v 0 ; in some cases we then use the categorization mechanism again to determine the relationship between h and v 1 . It is straightforward in all cases except one to use information from the categorization mechanism to prove that: • the case cannot arise; or • hop--src v ⩽ hop--tgt h, implying that nocross holds via the "left" alternative; or • h ⊆ v 0 or h ⊆ v 1 , implying that h ⊆ v, so nocross holds via the "right" alternative.
The difficult case is illustrated in Figure 4. In this case, hop--tgt h coincides with the point at which v 0 and v 1 meet, so there is no opportunity for the categorization mechanism to eliminate the case using a recursive instance of nocross against v 0 or v 1 . It simply tells us that v 1 is disjoint from h and that h contains v 0 .
The h--lvl--mid lemma is invaluable here: it proves that this case is impossible. Suppose v 0 and v 1 are hops at level l, so v is at level suc l. The contradiction arises from p, which is (supposedly) a proof that suc l < maxLvl j 2 . Because h hops over j 2 , h--lvl--mid implies that maxLvl j 2 is at most suc l.
Having proved these properties about our hop relation, we are ready to use it to instantiate the abstract model with our particular definition of . The properties required by other than hop--no--cross are straightforward to prove; some of them are shown below.
For hop--no--cross, first we define a simple convenience function to witness the existence of hops: Then we prove the hop--no--cross property using getHop and nocross. We pattern match on the result of nocross and discharge the Left branch as impossible with simple arithmetic (not shown). The other branch carries a proof that one hop is entirely contained within the other, from which we extract a value of the desired type.

Related and Future Work
Pugh's original skip lists [18] supported insertion, necessitating the use of probabilistic "heights" (analogous to our deterministic maxLvl function) for elements added to the list. Authenticated skip lists proposed by Goodrich and Tamassia [4] similarly required probabilistic heights, and depended on the use of a commutative hash function. Maniatis and Baker [7] proposed an append-only authenticated skip list (AAOSL), eliminating the need for commutative hashing, and achieving a simpler structure better suited to representing tamper-evident logs such as blockchains. The concrete AAOSL achieved in Section 4.4 by instantiating our abstract model presented in Section 4.1 is essentially the same as [7], modulo our changes to eliminate the possibility of a prover providing different authenticators for the same index within an advancement proof. The "skipchains" used by Chaniac [14] use the same "hop structure" in the case of deterministic skipchains with = 2; Chaniac also maintains "forward" links built when new elements are appended. Authenticated data-structures have been studied in many different incarnations. Miller et al. [10] presents lambdaauth, a language used to write a large variety of authenticated data structures with ease. They provide pen-and-paper proofs that a prover can fool a verifier only if it finds a hash collision. Brun and Traytel [2] formalized lambda-auth in Isabelle/HOL, which corrected some issues in the original paper, strengthening the overall result and reinforcing the importance of formal verification. In authenticated data structures produced using lambda-auth, the hash of a value depends exclusively on its type structure. In our case, the hash of different indexes might have a different number of dependencies, even though each log entry carries only one recursive argument: its tail. It therefore does not seem possible to use lambda-auth to achieve encode the original AAOSL presentation [7], nor our formalization thereof.
Using trees instead of lists to enable efficient queries has also been done in the CCF framework [19], with a verified incremental Merkle tree implementation [17]. This enables logarithmic-time access to past transactions and enables peers to store only important transactions locally. However, the CCF framework does not support advancement proofs. It may be possible to extend incremental Merkle trees to support advancement proofs and to prove a property analogous to EVO-CR. However, the translation is not immediate. An important difference between incremental Merkle trees and deterministic skiplogs is in how hashes are computed. The root hash of the Merkle tree depends directly only on its immediate children, whereas skiplog hashes depend directly on previous values carefully chosen to provide logarithmicsized advancement proofs.
There have been a number of formal verification efforts related to blockchain consensus [3,5,16]. Consensus is orthogonal to proving EVO-CR. The former states a property such as there is a single chain of blocks that is consistent with every honest participant's view, and commits must extend this chain. In contrast, our work entails formal verification of AAOSLs, which can be used to enable verifying claims about past entries in the presence of partial information. In other words, Evolutionary Collision Resistance states that if two peers agree at log index , even without possessing the entire log, then it is not possible to convince them of conflicting membership claims for indexes < . The agree on common (AOC) property can be related to the universal agreement properties of Pîrlea and Sergey [16] or the common prefix property of Garay et al. [3,5]. If we consider a set of "degenerate" advancement proofs, each of which includes only hops between adjacent indexes, starting at genesis and arriving at indexes 0 , · · · , −1 , respectively, AOC implies that they all agree on all indexes ⩽ min { 0 , · · · , −1 }. In our context, AOC is more general because it applies even in the case of partial information: advancement proofs typically do not both visit all indexes.
The most important future work aspect lies in the treatment of hash collisions. We proved our results modulo finding an arbitrary hash collision, similar to Miller et al. [10] or Brun and Traytel [2]. Yet, a full fledged security proof should provide a polynomial time reduction from an authentication failure to a hash collision. We are grateful to Profs. Seny Kamara and José Carlos Bacelar Almeida for useful discussions on this direction.
One promising option to improve our development in this direction is to make our proofs return proof-relevant information about which of its branches evidenced a collision. For example, in the AgreeOnCommon lemma, we could replace the ℎ disjunct as illustrated below.
AgreeOnCommon : ∀ { j i 1 i 2 } { t 1 t 2 : } → { a 1 : ℎ j i 1 } { a 2 : ℎ j i 2 } → rebuild a 1 t 1 j ≡ rebuild a 2 t 2 j → { i : N } → i ap a 1 → i ap a 2 → ℎ (AOC--Collision t 1 t 2 a 1 a 2 ) (rebuild a 1 t 1 i ≡ rebuild a 2 t 2 i) Here, a value of type AOC--Collision t 1 t 2 a 1 a 2 would witness a hash collision from the data provided in its parameters t 1 ,t 2 ,a 1 and a 2 . The definition of AOC--Collision is directly dependent on the structure of AgreeOnCommon, and hence cannot be reused for evo-cr, for instance. The evo-cr would have its own EvoCR--Collision... datatype, which would actually use values of AOC--Collision because evo-cr calls aoc internally and needs to forward potential collisions. Consequently, every Agda function that returns ℎ ℎ will have its own collision-tracking datatype, making this a non-trivial effort. Nevertheless, with these datatypes at hand, we would explicitly construct the hash collisions and readers could convince themselves of the polynomial runtime constraint based on the structure of these datatypes.
Although the approach described above would surely work, it is labor intensive and not transferable. As a future research question, we wonder whether there might be a more automatic way of constructively keeping track of hash collisions. In fact, with a little creativity one could even imagine enforcing the polynomial runtime constraint at the type level using appropriate type systems [6].

Concluding Remarks
We have presented formal, machine-checked proofs that Authenticated Append-Only Skip Lists (AAOSLs) indeed provide the properties claimed by its original authors [7].
Our formalization effort also uncovered some improvements to the original AAOSL. For example, providing authenticators separately in s (or with partial maps, as would be done in practice) precludes representing proofs with inconsistent authenticators, eliminating the need to check that, and also results in slightly smaller advancement proofs. Our proofs also highlighted that the actual implementation of auth is a red herring. Any definition satisfying auth--inj--1 and auth--inj--2 can be used with confidence. This showcases two important aspects of a formal development. On one hand, it uncovers the foundations of the security argument. In this case, we need an injective auth function and a definition of hops that do not cross each other. On the other hand, it provides an interactive playground to study variations of the construction. After we finished the development using the definition of auth provided by Maniatis and Baker, it was trivial to change it to a simpler variant with confidence that the development is still valid.
This work provides increased confidence that AAOSLs can be used in practice to dramatically reduce the overhead of verifying a recent log state, thus enabling sustainable dynamic participation in authenticated logs such as blockchains. Our development is available in open source [1].