EasyCrypt is a toolset for reasoning about relational properties of probabilistic computations with adversarial code. Its main application is the construction and verification of game-based cryptographic proofs.

This talk will consist of two parts. I will begin by introducing some standard notions used in cryptography and I will show how they are modelled using Easycrypt. I will then develop an Easycrypt proof of security under chosen plaintext-attacks of a simple encryption scheme introduced by Bellare and Rogaway in 1993. While straightforward, this proof exhibits some of the fundamental reasoning patterns used pervasively in cryptographic proofs.