Email Gateway (Aug 22 2022 at 19:51): Email Gateway (Aug 22 2022 at 19:51):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,
there is a new AFP entry by Matthias Brun and Dmitriy Traytel:
Formalization of Generic Authenticated Data Structures
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. Miller et al. introduced λ• (pronounced
lambda auth)—a functional programming language with a built-in primitive
authentication construct, which supports a wide range of user-specified
authenticated data structures while guaranteeing certain correctness and
security properties for all well-typed programs. We formalize λ• and prove its
correctness and security properties. With Isabelle's help, we uncover and repair
several mistakes in the informal proofs and lemma statements. Our findings are
summarized in a paper draft.
See https://www.isa-afp.org/entries/LambdaAuth.html for more details.
Enjoy,
René
Last updated: Apr 25 2024 at 16:19 UTC