Paper 2017/753
CryptHOL: Game-based Proofs in Higher-order Logic
David A. Basin, Andreas Lochbihler, and S. Reza Sefidgar
Abstract
Game-based proofs are a well-established paradigm for structuring security arguments and simplifying their understanding. We present a novel framework, CryptHOL, for rigorous game-based proofs that is supported by mechanical theorem proving. CryptHOL is based on a new semantic domain with an associated functional programming language for expressing games. We embed our framework in the Isabelle/HOL theorem prover and, using the theory of relational parametricity, we tailor Isabelle’s existing proof automation to game-based proofs. By basing our framework on a conservative extension of higher-order logic and providing automation support, the resulting proofs are trustworthy and comprehensible, and the framework is extensible and widely applicable. We evaluate our framework by formalizing different game-based proofs from the literature and comparing the results with existing formal-methods tools.
Note: This is the revised version that has been accepted at the Journal of Cryptology.
Metadata
- Available format(s)
-
PDF
- Category
- Foundations
- Publication info
- Published by the IACR in JOC 2020
- Keywords
- Provable SecurityGame-based ProofsTheorem ProvingHigher-order LogicIsabelleHOL
- Contact author(s)
- mail @ andreas-lochbihler de
- History
- 2020-05-16: last of 2 revisions
- 2017-08-07: received
- See all versions
- Short URL
- https://ia.cr/2017/753
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2017/753,
author = {David A. Basin and Andreas Lochbihler and S. Reza Sefidgar},
title = {{CryptHOL}: Game-based Proofs in Higher-order Logic},
howpublished = {Cryptology {ePrint} Archive, Paper 2017/753},
year = {2017},
url = {https://eprint.iacr.org/2017/753}
}
