Version 2 (modified by François Dupressoir, 5 years ago) (diff)

Adding link to the first version of the cryptographer-oriented tutorial

EasyCrypt Tutorials

This page links to tutorial material for EasyCrypt.

  • The EasyCrypt Tool: 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 (to come) gives an idea of the amount of effort needed to formally fill the sketch into a simple – but fully formal – proof.