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.

References in zbMATH (referenced in 33 articles , 1 standard article )

Showing results 1 to 20 of 33.
Sorted by year (citations)

1 2 next

  1. Butler, D.; Lochbihler, A.; Aspinall, D.; Gascón, A.: Formalising (\varSigma)-protocols and commitment schemes using crypthol (2021)
  2. Herzberg, Amir; Leibowitz, Hemi; Syta, Ewa; Wrótniak, Sara: MoSS: modular security specifications framework (2021)
  3. Barthe, Gilles; Betarte, Gustavo; Campo, Juan Diego; Luna, Carlos; Pichardie, David: System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory (2020)
  4. Basin, David A.; Lochbihler, Andreas; Sefidgar, S. Reza: CryptHOL: game-based proofs in higher-order logic (2020)
  5. Baillot, Patrick; Barthe, Gilles; Dal Lago, Ugo: Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs (2019)
  6. Cortier, Véronique; Gaudry, Pierrick; Glondu, Stéphane: Belenios: a simple private and verifiable electronic voting system (2019)
  7. Austin, Evan; Batson, Scott; Curry, Peter; Williams, Bryan: Finding a middle ground for computer-aided cryptography (2018)
  8. Bloem, Roderick; Gross, Hannes; Iusupov, Rinat; Könighofer, Bettina; Mangard, Stefan; Winter, Johannes: Formal verification of masked hardware implementations in the presence of glitches (2018)
  9. Barthe, Gilles; Espitau, Thomas; Grégoire, Benjamin; Hsu, Justin; Strub, Pierre-Yves: Proving uniformity and independence by self-composition and coupling (2017)
  10. Dal Lago, Ugo; Grellois, Charles: Probabilistic termination by monadic affine sized typing (2017)
  11. Jager, Tibor; Kohlar, Florian; Schäge, Sven; Schwenk, Jörg: Authenticated confidential channel establishment and the security of TLS-DHE (2017)
  12. Barthe, Gilles; Gaboardi, Marco; Arias, Emilio Jesús Gallego; Hsu, Justin; Roth, Aaron; Strub, Pierre-Yves: Computer-aided verification for mechanism design (2016)
  13. Gagné, Martin; Lafourcade, Pascal; Lakhnech, Yassine; Safavi-Naini, Reihaneh: Automated proofs of block cipher modes of operation (2016)
  14. Lochbihler, Andreas: Probabilistic functions and cryptographic oracles in higher order logic (2016)
  15. Barthe, Gilles; Espitau, Thomas; Grégoire, Benjamin; Hsu, Justin; Stefanesco, Léo; Strub, Pierre-Yves: Relational reasoning via probabilistic coupling (2015)
  16. Meadows, Catherine: Emerging issues and trends in formal methods in cryptographic protocol analysis: twelve years later (2015)
  17. Nowak, David; Zhang, Yu: Formal security proofs with minimal fuss: implicit computational complexity at work (2015)
  18. Rand, Robert; Zdancewic, Steve: VPHL: a verified partial-correctness logic for probabilistic programs (2015)
  19. Barthe, Gilles; Dupressoir, François; Grégoire, Benjamin; Kunz, César; Schmidt, Benedikt; Strub, Pierre-Yves: EasyCrypt: a tutorial (2014)
  20. Barthe, Gilles; Fournet, Cédric; Grégoire, Benjamin; Strub, Pierre-Yves; Swamy, Nikhil; Zanella-Béguelin, Santiago: Probabilistic relational verification for cryptographic implementations (2014)

1 2 next