Paper 2018/941

A tutorial introduction to CryptHOL

Andreas Lochbihler and S. Reza Sefidgar

Abstract

This tutorial demonstrates how cryptographic security notions, constructions, and game-based security proofs can be formalized using the CryptHOL framework. As a running example, we formalize a variant of the hash-based ElGamal encryption scheme and its IND-CPA security in the random oracle model. This tutorial assumes familiarity with Isabelle/HOL basics and standard cryptographic terminology.

Note: This paper explains how to use the CryptHOL framework to formalize game-based security proofs. It complements the theoretical CryptHOL paper (e-print 2017/753), which focues on the theoretical foundations.

Metadata
Available format(s)
PDF
Category
Foundations
Publication info
Preprint.
Keywords
Game-based ProofsTheorem ProvingHigher-order LogicIsabelleHOLCryptHOL
Contact author(s)
mail @ andreas-lochbihler de
History
2018-10-05: received
Short URL
https://ia.cr/2018/941
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2018/941,
      author = {Andreas Lochbihler and S.  Reza Sefidgar},
      title = {A tutorial introduction to CryptHOL},
      howpublished = {Cryptology ePrint Archive, Paper 2018/941},
      year = {2018},
      note = {\url{https://eprint.iacr.org/2018/941}},
      url = {https://eprint.iacr.org/2018/941}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.