Computer-Aided Security Proofs for the Working Cryptographer - Crypto 2011

Explore a conference talk from Crypto 2011 on computer-aided security proofs for cryptographers. Delve into the presentation of EasyCrypt, an automated tool designed to streamline the process of creating and verifying security proofs for cryptographic systems. Learn about the tool's ability to transform proof sketches into verifiable proofs using SMT solvers and automated theorem provers. Discover how EasyCrypt supports common reasoning patterns and offers a more user-friendly experience compared to its predecessors. Gain insights into its potential adoption by working cryptographers and examine its application to security proofs of the Cramer-Shoup and Hashed ElGamal cryptosystems. The talk covers an introduction, background information, the proof framework, how EasyCrypt functions, and concludes with a Q&A session.