Document Open Access Logo

Generic Authenticated Data Structures, Formally

Authors Matthias Brun, Dmitriy Traytel

PDF
Thumbnail PDF

File

LIPIcs.ITP.2019.10.pdf
  • Filesize: 0.49 MB
  • 18 pages

Document Identifiers

Author Details

Matthias Brun
  • Department of Computer Science, ETH Zürich, Switzerland
Dmitriy Traytel
  • Institute of Information Security, Department of Computer Science, ETH Zürich, Switzerland

Acknowledgements

We thank David Basin for supporting this work and Andrew Miller for discussing our counterexamples and proposing a remedy to the issue with type soundness. Joshua Schneider and the anonymous ITP reviewers helped to improve the presentation through numerous comments.

Cite AsGet BibTex

Matthias Brun and Dmitriy Traytel. Generic Authenticated Data Structures, Formally. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ITP.2019.10

Abstract

Authenticated data structures are a technique for outsourcing data storage and maintenance to an untrusted server. The server is required to produce an efficiently checkable and cryptographically secure proof that it carried out precisely the requested computation. Recently, Miller et al. [https://doi.org/10.1145/2535838.2535851] demonstrated how to support a wide range of such data structures by integrating an authentication construct as a first class citizen in a functional programming language. In this paper, we put this work to the test of formalization in the Isabelle proof assistant. With Isabelle’s help, we uncover and repair several mistakes and modify the small-step semantics to perform call-by-value evaluation rather than requiring terms to be in administrative normal form.

Subject Classification

ACM Subject Classification
  • Security and privacy → Logic and verification
Keywords
  • Authenticated Data Structures
  • Verifiable Computation
  • Isabelle/HOL
  • Nominal Isabelle

Metrics

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

Supplementary Materials

References

  1. Henk P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 40 of Studies in Logic. Elsevier, 1984. Google Scholar
  2. Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, and Dmitriy Traytel. Bindings as bounded natural functors. PACMPL, 3(POPL):22:1-22:34, 2019. URL: https://doi.org/10.1145/3290335.
  3. Joachim Breitner. The adequacy of Launchbury’s natural semantics for lazy evaluation. J. Funct. Program., 28:e1, 2018. URL: https://doi.org/10.1017/S0956796817000144.
  4. Matthias Brun. Authenticated Data Structures in Isabelle/HOL. B.Sc. thesis, ETH Zürich, 2019. Google Scholar
  5. Premkumar T. Devanbu, Michael Gertz, Charles U. Martel, and Stuart G. Stubblebine. Authentic third-party data publication. In Bhavani M. Thuraisingham, Reind P. van de Riet, Klaus R. Dittrich, and Zahir Tari, editors, DBSec 2000, volume 201 of IFIP Conference Proceedings, pages 101-112. Kluwer, 2000. URL: https://doi.org/10.1007/0-306-47008-X_9.
  6. Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with continuations. In Robert Cartwright, editor, PLDI 1993, pages 237-247. ACM, 1993. URL: https://doi.org/10.1145/155090.155113.
  7. Murdoch Gabbay and Andrew M. Pitts. A new approach to abstract syntax with variable binding. Formal Asp. Comput., 13(3-5):341-363, 2002. URL: https://doi.org/10.1007/s001650200016.
  8. Brian Huffman and Christian Urban. A new foundation for Nominal Isabelle. In Matt Kaufmann and Lawrence C. Paulson, editors, ITP 2010, volume 6172 of LNCS, pages 35-50. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14052-5_5.
  9. Ralph C. Merkle. A digital signature based on a conventional encryption function. In Carl Pomerance, editor, CRYPTO 1987, volume 293 of LNCS, pages 369-378. Springer, 1987. URL: https://doi.org/10.1007/3-540-48184-2_32.
  10. Andrew Miller, Michael Hicks, Jonathan Katz, and Elaine Shi. Authenticated data structures, generically. In Suresh Jagannathan and Peter Sewell, editors, POPL 2014, pages 411-424. ACM, 2014. URL: https://doi.org/10.1145/2535838.2535851.
  11. Julian Nagele, Vincent van Oostrom, and Christian Sternagel. A short mechanized proof of the Church-Rosser theorem by the Z-property for the λβ-calculus in Nominal Isabelle. CoRR, abs/1609.03139, 2016. Google Scholar
  12. Mizuhito Ogawa, Eiichi Horita, and Satoshi Ono. Proving properties of incremental Merkle trees. In Robert Nieuwenhuis, editor, CADE 2005, volume 3632 of LNCS, pages 424-440. Springer, 2005. URL: https://doi.org/10.1007/11532231_31.
  13. Lawrence C. Paulson. A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle. J. Autom. Reasoning, 55(1):1-37, 2015. URL: https://doi.org/10.1007/s10817-015-9322-8.
  14. Benjamin C. Pierce. Types and programming languages. MIT Press, 2002. Google Scholar
  15. George Pîrlea and Ilya Sergey. Mechanising blockchain consensus. In June Andronick and Amy P. Felty, editors, CPP 2018, pages 78-90. ACM, 2018. URL: https://doi.org/10.1145/3167086.
  16. Roberto Tamassia. Authenticated data structures. In Giuseppe Di Battista and Uri Zwick, editors, ESA 2003, volume 2832 of LNCS, pages 2-5. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-39658-1_2.
  17. Christian Urban and Cezary Kaliszyk. General bindings and alpha-equivalence in Nominal Isabelle. Logical Methods in Computer Science, 8(2), 2012. URL: https://doi.org/10.2168/LMCS-8(2:14)2012.
  18. Christian Urban and Julien Narboux. Formal SOS-proofs for the lambda-calculus. Electr. Notes Theor. Comput. Sci., 247:139-155, 2009. URL: https://doi.org/10.1016/j.entcs.2009.07.053.
  19. Christian Urban and Christine Tasson. Nominal techniques in Isabelle/HOL. In Robert Nieuwenhuis, editor, CADE 2005, volume 3632 of LNCS, pages 38-53. Springer, 2005. URL: https://doi.org/10.1007/11532231_4.
  20. Bill White. A theory for lightweight cryptocurrency ledgers. Accessed on 30.03.2019, 2015. URL: https://github.com/input-output-hk/qeditas-ledgertheory.
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 Imprint Privacy Contact