Document Open Access Logo

Authenticated Data Structures as Functors in Isabelle/HOL

Authors Andreas Lochbihler , Ognjen Marić

PDF
Thumbnail PDF

File

OASIcs.FMBC.2020.6.pdf
  • Filesize: 433 kB
  • 15 pages

Document Identifiers

Author Details

Andreas Lochbihler
  • Digital Asset, Zurich, Switzerland
Ognjen Marić
  • Digital Asset, Zurich, Switzerland

Cite As Get BibTex

Andreas Lochbihler and Ognjen Marić. Authenticated Data Structures as Functors in Isabelle/HOL. In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/OASIcs.FMBC.2020.6

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Higher order logic
  • Theory of computation → Cryptographic primitives
Keywords
  • Merkle tree
  • functor
  • distributed ledger
  • datatypes
  • higher-order logic

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. Jeremy Avigad, Mario Carneiro, and Simon Hudon. Data types as quotients of polynomial functors. In John Harrison, John O'Leary, and Andrew Tolmach, editors, ITP 2019, volume 141 of LIPIcs, pages 6:1-6:19. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.ITP.2019.6.
  2. Stefan Berghofer and Markus Wenzel. Inductive datatypes in HOL - lessons learned in formal-logic engineering. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Théry, editors, TPHOLs 1999, volume 1690 of LNCS, pages 19-36. Springer, 1999. URL: https://doi.org/10.1007/3-540-48256-3_3.
  3. Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, and Dmitriy Traytel. Truly modular (co)datatypes for Isabelle/HOL. In Interactive Theorem Proving (ITP 2014), pages 93-110, 2014. Google Scholar
  4. Sören Bleikertz, Andreas Lochbihler, Ognjen Marić, Simon Meier, Matthias Schmalz, and Ratko G. Veprek. A structured semantic domain for smart contracts. Computer Security Foundations poster session (CSF 2019), https://www.canton.io/publications/csf2019-abstract.pdf, 2019.
  5. Matthias Brun and Dmitriy Traytel. Generic authenticated data structures, formally. In Interactive Theorem Proving (ITP 2019), pages 10:1-–10:18, 2019. Google Scholar
  6. Canton: A private, scalable, and composable smart contract platform. https://www.canton.io/publications/canton-whitepaper.pdf, 2019.
  7. Canton: Global synchronization beyond blockchain. https://www.canton.io/, 2020.
  8. Corda: Open source blockchain platform for business. https://www.corda.net/, 2020.
  9. Rasmus Dahlberg, Tobias Pulls, and Roel Peeters. Efficient sparse merkle trees: Caching strategies and secure (non-)membership proofs. Cryptology ePrint Archive, Report 2016/683, 2016. URL: https://eprint.iacr.org/2016/683.
  10. Digital Asset. Daml programming language. https://daml.com, 2020.
  11. D. Dolev and A. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, 29(2):198-208, 1983. Google Scholar
  12. Basil Fürer, Andreas Lochbihler, Joshua Schneider, and Dmitriy Traytel. Quotients of bounded natural functors. In N. Peltier and V. Sofronie-Stokkermans, editors, Automated Reasoning (IJCAR 2020), volume 12167 of LNAI, pages 58-78. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51054-1_4.
  13. Hacl^∗ verified merkle tree library. https://github.com/project-everest/hacl-star/tree/master/secure_api/merkle_tree, 2020.
  14. Ralf Hinze and Johan Jeuring. Weaving a web. J. Funct. Program., 11(6):681-–689, 2001. URL: https://doi.org/10.1017/S0956796801004129.
  15. Gérard Huet. The zipper. Journal of Functional Programming, 7(5):549-–554, 1997. Google Scholar
  16. Brian Huffman and Ondřej Kuncar. Lifting and transfer: A modular design for quotients in Isabelle/HOL. In Certified Programs and Proofs (CPP 2013), pages 131–-146, 2013. Google Scholar
  17. Oleg Kiselyov. Zippers with several holes. http://okmij.org/ftp/Haskell/Zipper2.lhs, 2011.
  18. Andreas Lochbihler and Ognjen Marić. Authenticated data structures as functors. Archive of Formal Proofs, April 2020. URL: http://isa-afp.org/entries/ADS_Functor.html.
  19. Conor McBride. The derivative of a regular type is its type of one-hole contexts, 2001. Google Scholar
  20. Ralph C. Merkle. A digital signature based on a conventional encryption function. In Advances in Cryptology (CRYPTO 1987), pages 369-378, 1987. Google Scholar
  21. Andrew Miller, Michael Hicks, Jonathan Katz, and Elaine Shi. Authenticated data structures, generically. In Principles of Programming Languages (POPL 2014), pages 411-–423, 2014. Google Scholar
  22. Mizuhito Ogawa, Eiichi Horita, and Satoshi Ono. Proving properties of incremental Merkle trees. In Automated Deduction (CADE 2005), pages 424-440, 2005. Google Scholar
  23. Sean Seefried. Merkle proofs for free! Functional Programming Sydney, http://code.ouroborus.net/fp-syd/past/2017/2017-04-Seefried-Merkle.pdf, 2017.
  24. D. B. Skillicorn. Parallel implementation of tree skeletons. Journal of Parallel and Distributed Computing, 39(2):115-125, 1996. URL: https://doi.org/10.1006/jpdc.1996.0160.
  25. Bill White. A theory for lightweight cryptocurrency ledgers. https://github.com/input-output-hk/qeditas-ledgertheory, 2015.
  26. Jiangshan Yu, Vincent Cheval, and Mark Ryan. DTKI: a new formalized PKI with no trusted parties. The Computer Journal, 59(11):1695-1713, November 2016. arXiv: 1408.1023. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact