License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2019.10
URN: urn:nbn:de:0030-drops-110657
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11065/
Go to the corresponding LIPIcs Volume Portal

Brun, Matthias ; Traytel, Dmitriy

Generic Authenticated Data Structures, Formally

pdf-format:
LIPIcs-ITP-2019-10.pdf (0.5 MB)

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
Collection: 10th International Conference on Interactive Theorem Proving (ITP 2019)
Issue Date: 2019
Date of publication: 05.09.2019
Supplementary Material: https://isa-afp.org/entries/LambdaAuth.html

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI