Paper 2017/753

CryptHOL: Game-based Proofs in Higher-order Logic

David A. Basin, Andreas Lochbihler, and 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 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.

Available format(s)
Publication info
Published by the IACR in JOC 2020
Provable SecurityGame-based ProofsTheorem ProvingHigher-order LogicIsabelleHOL
Contact author(s)
mail @ andreas-lochbihler de
2020-05-16: last of 2 revisions
2017-08-07: received
See all versions
Short URL
Creative Commons Attribution


      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},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.