Interactive Proofs in Higher-Order Logic with Errors and Application to Concrete Cryptography
TL;DR
This paper introduces a proof term calculus with dedicated features for bounds, for which an elaborator can automatically infer bound-related manipulations, improving usability and reducing user inputs, and theoretically argues for its usability through an erasability theorem.
Abstract
Computer-aided cryptography (CAC) provides strong guarantees through mechanized proofs of security. SquirREL is a proof assistant specialized in CAC, but is restricted to the asymptotic setting, which limits its applicability. Recent theoretical work [1] adapted Squirrel’s underlying logic to the concrete setting through the introduction of a higher-order logic with errors. While this allows to prove precise security bounds on paper, it only provides a low-level logical calculus which lacks an implementation. Thus, it falls short of the CAC aims.In this paper, we use this low-level calculus to build the full-fledged set of features used in a proof assistant such as Squirrel, with a focus on reachability reasoning. We design higher-level logical mechanisms on top of this logic, including proof context management, introduction patterns, and boundannotated tactics. To do so, we introduce a proof term calculus with dedicated features for bounds, for which we design an elaborator. This elaborator can automatically infer bound-related manipulations, improving usability and reducing user inputs, and we theoretically argue for its usability through an erasability theorem. All these improvements have been implemented as an extension of Squirrel, and we provide empirical evidence of the applicability of our framework through case studies.