Skip to main content

Tutorial Overview

This tutorial takes you from "I've heard enough about EasyCrypt to end up here" to "I've proved a thing."

It assumes you are confidently in control of your computer (we can only cover installation and setup generically), and that you have had minimal exposure (as would be suffered in a good undergraduate degree in computer science with cryptography) to functional programming, program logics, and cryptographic proofs.

Getting Started​

To get started, we'll first install EasyCrypt and set it up for interactive use.

We'll then go through a top-to-bottom formalisation, which will cover modelling, simple proofs, and the use of some of the core libraries of datatypes and generic arguments.

An advanced tutorial covers some of the deeper proof tactics and some common proof tricks.

What you'll need​

  • A reasonable computer: in interactive mode, your brain and fingers are a lot more limiting than your CPU. (I am writing this on an 2GHz CPU from 2019, and have not had any issues even when checking proofs non-interactively, where the CPU is the bottleneck.) That being said, EasyCrypt does consume some memory and you should probably expect things to go wrong, slow, or both if you have less than 4GB of RAM. Having multiple cores helps, but we typically won't use more than 4 at a time unless you choose to install more SMT solvers than those we recommend.

  • Ideally, a Unix-y operating system (Linux, BSD, MacOS, WSL). You can probably make things work on Windows or on stranger operating systems, but we can't help you do it, and likely won't even try.