EasyCrypt swMATH ID: 9738 Software Authors: Barthe, Gilles; Grégoire, Benjamin; Heraud, Sylvain; Béguelin, Santiago Zanella Description: 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. Homepage: http://link.springer.com/chapter/10.1007%2F978-3-642-22792-9_5 Source Code: https://github.com/EasyCrypt/easycrypt Keywords: provable security; verifiable security; game-based proofs; Cramer-Shoup cryptosystem; ElGamal encryption Related Software: Coq; F*; AVISPA; CryptHOL; Isabelle/HOL; ProVerif; z3; TAMARIN; Archive Formal Proofs; Zoo Probabilistic Systems; Lifting; Transfer; Autoref; Helios; ASPIER; pGCL; CoSP; Plutus; NRL; Ynot Cited in: 32 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year EasyCrypt: a tutorial. Zbl 1448.68184Barthe, Gilles; Dupressoir, François; Grégoire, Benjamin; Kunz, César; Schmidt, Benedikt; Strub, Pierre-Yves 2014 all top 5 Cited by 65 Authors 13 Barthe, Gilles 8 Grégoire, Benjamin 5 Strub, Pierre-Yves 5 Zanella Béguelin, Santiago 3 Hsu, Justin 3 Kunz, César 3 Lochbihler, Andreas 2 Blanchet, Bruno 2 Cortier, Véronique 2 Crespo, Juan Manuel 2 Dal Lago, Ugo 2 Espitau, Thomas 2 Heraud, Sylvain 2 Olmedo, Federico 1 Aspinall, David 1 Austin, Evan 1 Ayala-Rincón, Mauricio 1 Baillot, Patrick 1 Basin, David A. 1 Batson, Scott C. 1 Betarte, Gustavo 1 Bloem, Roderick 1 Campo, Juan Diego 1 Comon-Lundh, Hubert 1 Curry, Peter 1 Dupressoir, François 1 Fournet, Cédric 1 Gaboardi, Marco 1 Gagné, Martin 1 Gallego Arias, Emilio Jesús 1 Gascón, Adrià 1 Gaudry, Pierrick 1 Glondu, Stéphane 1 Grellois, Charles 1 Groß, Hannes 1 Herzberg, Amir 1 Iusupov, Rinat 1 Jager, Tibor 1 Koblitz, Neal I. 1 Kohlar, Florian 1 Könighofer, Bettina 1 Lafourcade, Pascal 1 Lakhnech, Yassine 1 Leibowitz, Hemi 1 Luna, Carlos 1 Mangard, Stefan 1 Meadows, Catherine A. 1 Nowak, David E. 1 Pavlović, Duško 1 Pichardie, David 1 Rego, Yuri Santos 1 Roth, Aaron Leon 1 Safavi-Naini, Reihaneh 1 Scerri, Guillaume 1 Schäge, Sven 1 Schmidt, Benedikt 1 Schwenk, Jorg 1 Sefidgar, S. Reza 1 Stefanesco, Léo 1 Swamy, Nikhil 1 Syta, Ewa 1 Winter, Johannes 1 Wrótniak, Sara 1 Zdancewic, Steve 1 Zhang, Yu Cited in 5 Serials 4 Journal of Automated Reasoning 2 Information and Computation 2 Journal of Cryptology 1 Journal of Mathematical Cryptology 1 Journal of Formalized Reasoning all top 5 Cited in 6 Fields 27 Computer science (68-XX) 24 Information and communication theory, circuits (94-XX) 11 Mathematical logic and foundations (03-XX) 3 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 1 Number theory (11-XX) 1 Category theory; homological algebra (18-XX) Citations by Year