
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: 
20200416 
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_FunctorAFP,
author = {Andreas Lochbihler and Ognjen MariÄ‡},
title = {Authenticated Data Structures As Functors},
journal = {Archive of Formal Proofs},
month = apr,
year = 2020,
note = {\url{http://isaafp.org/entries/ADS_Functor.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
