Computer-aided security proofs for the working cryptographer. 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.
Keywords for this software
References in zbMATH (referenced in 12 articles )
Showing results 1 to 12 of 12.
- Gagné, Martin; Lafourcade, Pascal; Lakhnech, Yassine; Safavi-Naini, Reihaneh: Automated proofs of block cipher modes of operation (2016)
- Nowak, David; Zhang, Yu: Formal security proofs with minimal fuss: implicit computational complexity at work (2015)
- Barthe, Gilles; Fournet, Cédric; Grégoire, Benjamin; Strub, Pierre-Yves; Swamy, Nikhil; Zanella-Béguelin, Santiago: Probabilistic relational verification for cryptographic implementations (2014)
- Barthe, Gilles; Crespo, Juan Manuel; Kunz, César: Beyond 2-safety: asymmetric product programs for relational program verification (2013)
- Barthe, Gilles; Olmedo, Federico: Beyond differential privacy: composition theorems and relational logic for $f$-divergences between probabilistic programs (2013)
- Comon-Lundh, Hubert; Cortier, Véronique; Scerri, Guillaume: Tractable inference systems: an extension with a deducibility predicate (2013)
- Barthe, Gilles; Grégoire, Benjamin; Heraud, Sylvain; Olmedo, Federico; Zanella Béguelin, Santiago: Verified indifferentiable hashing into elliptic curves (2012)
- Barthe, Gilles; Grégoire, Benjamin; Kunz, César; Lakhnech, Yassine; Zanella Béguelin, Santiago: Automation in computer-aided cryptography: proofs, attacks and designs (2012)
- Barthe, Gilles; Grégoire, Benjamin; Zanella Béguelin, Santiago: Probabilistic relational Hoare logics for computer-aided security proofs (2012)
- Blanchet, Bruno: Security protocol verification: symbolic and computational models (2012)
- Barthe, Gilles; Grégoire, Benjamin; Heraud, Sylvain; Béguelin, Santiago Zanella: Computer-aided security proofs for the working cryptographer (2011)
- Koblitz, Neal: Another look at automated theorem-proving. II (2011)