This page links to tutorial material for EasyCrypt.
- Computer-Aided Cryptography: Some tools and applications is the online version of our APPA 2014 invited paper. Our goal in this document was to demonstrate the variety of applications of formal methods and programming language techniques in cryptography, from an example EasyCrypt proof to an application of formal methods to the analysis of DH-style cryptographic assumptions in the Generic Group Model. It is accompanied by proof scripts (to come soon).
- EasyCrypt: A Tutorial is the online version of our FOSAD VII chapter. Our goal in this document is to invite cryptographers to consider the EasyCrypt language as a close relative to the informal languages they use to describe systems, cryptographic assumptions and security notions and proof sketches (intermediate games and lemmas). We do so by presenting a simple stateful random generator constructed from a pseudo-random function and sketching a proof of its security as a pseudo-random generator. The associated EasyCrypt proof script gives an idea of the amount of effort needed to formally fill the sketch into a simple – but fully formal – proof. The example is chosen to be simple, yet exercise interesting aspects of the tool, not for cryptographic realism.