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
-
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},
url = {https://eprint.iacr.org/2018/941}
}
