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. 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 an ITP'19 paper.