### 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.

### License

BSD License

### Topics

- Computer science/Data structures

### Session ADS_Functor

- Merkle_Interface
- ADS_Construction
- Generic_ADS_Construction
- Inclusion_Proof_Construction
- Canton_Transaction_Tree

## Cite

×

ADS_Functor-AFP

    @article{ADS_Functor-AFP,
      author  = {Andreas Lochbihler and Ognjen Marić},
      title   = {Authenticated Data Structures As Functors},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2020},
      note    = {\url{https://isa-afp.org/entries/ADS_Functor.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 27, 2020 : Isabelle2020