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
Creative Commons Attribution
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.