### 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.

Available format(s)
Category
Foundations
Publication info
Keywords
Provable SecurityGame-based ProofsTheorem ProvingHigher-order LogicIsabelleHOL
Contact author(s)
mail @ andreas-lochbihler de
History
2020-05-16: last of 2 revisions
See all versions
Short URL
https://ia.cr/2017/753

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},
note = {\url{https://eprint.iacr.org/2017/753}},
url = {https://eprint.iacr.org/2017/753}
}

Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.