Paper 2018/941 Original: eprint.iacr.org/2018/941 ↗
A tutorial introduction to CryptHOL
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.
Metadata
- Available format(s)
PDF- Category
- Foundations
- Publication info
- Preprint.
- History
- 2018-10-05: last updated
- 2018-10-05: published
- Short URL
- https://ia.cr/2018/941
- License
- https://creativecommons.org/licenses/by/4.0/
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}
}