Formal certification of ElGamal encryption. A gentle introduction to CertiCrypt

Gilles Barthe, Benjamin Gr├ęgoire, Sylvain Heraud, and Santiago Zanella-B├ęguelin

Abstract

CertiCrypt is a framework that assists the construction of machine-checked cryptographic proofs that can be automatically verified by third parties. To date, CertiCrypt has been used to prove formally the exact security of widely studied cryptographic systems, such as the OAEP padding scheme and the Full Domain Hash digital signature scheme. The purpose of this article is to provide a gentle introduction to CertiCrypt. For concreteness, we focus on a simple but illustrative example, namely the semantic security of the Hashed ElGamal encryption scheme in both, the standard and the random oracle model.

Details

Publication typeInproceedings
Published in5th International Workshop on Formal Aspects in Security and Trust, FAST 2008
URLhttp://dx.doi.org/10.1007/978-3-642-01465-9_1
Pages1-19
Volume5491
SeriesLecture Notes in Computer Science
ISBN978-3-642-01464-2
PublisherSpringer
> Publications > Formal certification of ElGamal encryption. A gentle introduction to CertiCrypt