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

Adding some comments.

EasyCrypt Tutorials

This page links to tutorial material for EasyCrypt.

  • 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 (to come) 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.