Canton and the underlying theory is described in the following research publications:
Extended abstract presented at Computer Security Foundations 2019.
CantonCoin: Gaining Horizontal Scalability and Privacy with Distributed Commits Instead of Global Consensus explains how Canton’s distributed commit protocol enables a scalable and privacy-preserving coin design.
Abstract: Bitcoin sought to create a trustless and censorship-resistant paymentsystem. However, to obtain a practical day-to-day payment systemcapable of serving the global needs, these goals must be balanced with many other properties, such as scalability and privacy. In this paper, we show that replacing state machine replication (the mechanism underlying Bitcoin and most other blockchains) with a distributed commit protocol over private local ledgers removes the scalability bottlenecks and enhances privacy. We demonstrate our approach usingthe Canton commit protocol, resulting in the CantonCoin prototype cryptocurrency.
Authenticated Data Structures As Functors in Isabelle/HOL formalizes Canton’s Merkle tree data structures in the theorem prover Isabelle/HOL.
- Andreas Lochbihler and Ognjen Maric. Authenticated Data Structures As Functors in Isabelle/HOL. In: Bruno Bernardo and Diego Marmsoler (eds.) Formal Methods for Blockchain 2020. OASIcs vol. 84, 5:1-5:14, 2020.
- DOI (to appear).
- Preprint PDF
- Pre-reecorded talk
- Live presentation (1:48 to 12:50)
Abstract: Merkle trees are ubiquitous in blockchains and other distributed ledger technologies (DLTs). They guarantee that the involved systems are referring to the same binary tree, even if each of them knows only the cryptographic hash of the root. Inclusion proofs allow knowledgeable systems to share subtrees with other systems and the latter can verify the subtrees’ authenticity. Often, blockchains and DLTs use data structures more complicated than binary trees; authenticated data structures generalize Merkle trees to such structures.
We show how to formally define and reason about authenticated data structures, their inclusion proofs, and operations thereon as datatypes in Isabelle/HOL. The construction lives in the symbolic model, i.e., we assume that no hash collisions occur. Our approach is modular and 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.