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

TL;DR

This paper formalizes and verifies the correctness of authenticated, append-only skip lists in Agda, ensuring their reliability for use in secure, efficient logging systems like blockchains.

Contribution

It provides the first formal, machine-checked proof of AAOSL correctness, generalizes the original construction, and offers simplified, optimized formalization.

Findings

Proof of key correctness properties in Agda

Generalization of the original AAOSL construction

Simplifications and optimizations in formalization

Abstract

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.