EasyCrypt

I did an internship at IMDEA Software under the supervision of Gilles Barthe and Benedikt Schmidt. I implemented some tactics for their project: EasyCrypt.

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.

My task was to implement ring and field equation tactics, plus some automatic tactics such as optimistic sampling.