Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Automation in Computer-Aided Cryptography: proofs, attacks and designs

Gilles Barthe, Benjamin Grégoire, César Kunz, Yassine Lakhnech, and Santiago Zanella-Béguelin

Abstract

CertiCrypt and EasyCrypt are machine-checked frameworks for proving the security of cryptographic constructions. Both frameworks adhere to the game-based approach to provable security, but revisit its realization from a formal verification perspective. More specifically, CertiCrypt and EasyCrypt use a probabilistic programming language pWHILE for expressing cryptographic constructions, security properties, and computational assumptions, and a probabilistic relational Hoare logic pRHL for justifying reasoning in cryptographic proofs. While both tools coincide in their foundations, they differ in their underlying technologies: CertiCrypt is implemented as a set of libraries in the Coq proof assistant, whereas EasyCrypt uses a verification condition generator for pRHL in combination with off-the-shelf SMT solvers and automated theorem provers. Over the last six years, we have used both tools to verify prominent examples of public-key encryption schemes, modes of operation, signature schemes, hash function designs, zero-knowledge proofs. Recently, we have also used both tools to certify the output of a zero-knowledge compiler.

Details

Publication typeInproceedings
Published in2nd International Conference on Certified Programs and Proofs, CPP 2012
URLhttp://dx.doi.org/10.1007/978-3-642-35308-6_3
Pages7-8
Volume7679
SeriesLecture Notes in Computer Science
PublisherSpringer
> Publications > Automation in Computer-Aided Cryptography: proofs, attacks and designs