Brun, Matthias ;
Traytel, Dmitriy
Generic Authenticated Data Structures, Formally
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.
BibTeX - Entry
@InProceedings{brun_et_al:LIPIcs:2019:11065,
author = {Matthias Brun and Dmitriy Traytel},
title = {{Generic Authenticated Data Structures, Formally}},
booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)},
pages = {10:1--10:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-122-1},
ISSN = {1868-8969},
year = {2019},
volume = {141},
editor = {John Harrison and John O'Leary and Andrew Tolmach},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2019/11065},
URN = {urn:nbn:de:0030-drops-110657},
doi = {10.4230/LIPIcs.ITP.2019.10},
annote = {Keywords: Authenticated Data Structures, Verifiable Computation, Isabelle/HOL, Nominal Isabelle}
}
|
Keywords: |
|
Authenticated Data Structures, Verifiable Computation, Isabelle/HOL, Nominal Isabelle |
|
Seminar: |
|
10th International Conference on Interactive Theorem Proving (ITP 2019)
|
|
Issue date: |
|
2019 |
|
Date of publication: |
|
2019 |
2019
