CryptoDB
CryptHOL: Game-Based Proofs in Higher-Order Logic
| Authors: | |
|---|---|
| Download: | |
| 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 formalising different game-based proofs from the literature and comparing the results with existing formal-methods tools. |
BibTeX
@article{jofc-2020-30105,
title={CryptHOL: Game-Based Proofs in Higher-Order Logic},
journal={Journal of Cryptology},
publisher={Springer},
doi={10.1007/s00145-019-09341-z},
author={David A. Basin and Andreas Lochbihler and S. Reza Sefidgar},
year=2020
}