Authenticated Data Structures As Functors

Title:	Authenticated Data Structures As Functors
Authors:	Andreas Lochbihler and Ognjen Marić (ogi /dot/ afp /at/ mynosefroze /dot/ com)
Submission date:	2020-04-16
Abstract:	Authenticated data structures allow several systems to convince each other that they are referring to the same data structure, even if each of them knows only a part of the data structure. Using inclusion proofs, knowledgeable systems can selectively share their knowledge with other systems and the latter can verify the authenticity of what is being shared. In this article, we show how to modularly define authenticated data structures, their inclusion proofs, and operations thereon as datatypes in Isabelle/HOL, using a shallow embedding. Modularity allows us to construct complicated trees from reusable building blocks, which we call Merkle functors. Merkle functors include sums, products, and function spaces and are closed under composition and least fixpoints. As a practical application, we model the hierarchical transactions of Canton, a practical interoperability protocol for distributed ledgers, as authenticated data structures. This is a first step towards formalizing the Canton protocol and verifying its integrity and security guarantees.
BibTeX:	@article{ADS_Functor-AFP, author = {Andreas Lochbihler and Ognjen Marić}, title = {Authenticated Data Structures As Functors}, journal = {Archive of Formal Proofs}, month = apr, year = 2020, note = {\url{http://isa-afp.org/entries/ADS_Functor.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Proof outline
Proof document

Browse theories

Download this entry