LIPIcs.ITP.2019.10.pdf
- Filesize: 0.49 MB
- 18 pages
Document
Generic Authenticated Data Structures, Formally
Authors
Dmitriy Traytel 
-
Part of:
Volume:
10th International Conference on Interactive Theorem Proving (ITP 2019)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 3.0 Unported license
- Publication date: 2019-09-05
File
Document Identifiers
Author Details
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
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)
0PDF Downloads