Name
Abstract | ||
|---|---|---|
We present EasyCrypt, an automated tool for elaborating security proofs of cryptographic systems from proof sketches-compact, formal representations of the essence of a proof as a sequence of games and hints. Proof sketches are checked automatically using off-the-shelf SMT solvers and automated theorem provers, and then compiled into verifiable proofs in the CertiCrypt framework. The tool supports most common reasoning patterns and is significantly easier to use than its predecessors. We argue that EasyCrypt is a plausible candidate for adoption by working cryptographers and illustrate its application to security proofs of the Cramer-Shoup and Hashed ElGamal cryptosystems. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1007/978-3-642-22792-9_5 | CRYPTO |
Keywords | Field | DocType |
automated theorem provers,security proof,hashed elgamal cryptosystems,working cryptographer,cryptographic system,certicrypt framework,computer-aided security proof,verifiable proof,proof sketches-compact,common reasoning pattern,automated tool,proof sketch,theorem prover,provable security,elgamal encryption | Computer-assisted proof,Cramer–Shoup cryptosystem,Cryptography,Computer science,Automated proof checking,Theoretical computer science,Mathematical proof,ElGamal encryption,Provable security,Proof assistant | Conference |
Volume | ISSN | Citations |
6841 | 0302-9743 | 97 |
PageRank | References | Authors |
2.45 | 26 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Gilles Barthe | 1 | 2337 | 152.36 |
| Benjamin Grégoire | 2 | 817 | 48.93 |
| Sylvain Heraud | 3 | 120 | 4.69 |
| Santiago Zanella Béguelin | 4 | 114 | 6.28 |