International Association for Cryptologic Research

International Association
for Cryptologic Research


Andreas Lochbihler


CryptHOL: Game-Based Proofs in Higher-Order Logic
David A. Basin Andreas Lochbihler S. Reza Sefidgar
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.


David Basin (1)
S. Reza Sefidgar (1)