= [wiki:WikiStart EasyCrypt] Tutorials =
This page links to tutorial material for !EasyCrypt.
* [https://www.easycrypt.info/downloads/tutorial/tutorial-prg.pdf 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.