Document Open Access Logo

Generic Authenticated Data Structures, Formally

Authors Matthias Brun, Dmitriy Traytel

Thumbnail 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


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)


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. [] 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
  • Authenticated Data Structures
  • Verifiable Computation
  • Isabelle/HOL
  • Nominal Isabelle


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail