1 | | = The [wiki:WikiStart EasyCrypt] Tool: A Tutorial = |

| 1 | = [wiki:WikiStart EasyCrypt] Tutorials = |

| 2 | |

| 3 | This page links to tutorial material for !EasyCrypt. |

| 4 | |

| 5 | * [https://www.easycrypt.info/downloads/tutorial/tutorial-prg.pdf The EasyCrypt Tool: A Tutorial] |

| 6 | is the online version of our FOSAD VII chapter. Our goal in |

| 7 | this document is to invite cryptographers to consider the |

| 8 | !EasyCrypt language as a close relative to the informal |

| 9 | languages they use to describe systems, cryptographic |

| 10 | assumptions and security notions and proof |

| 11 | sketches (intermediate games and lemmas). We do so by |

| 12 | presenting a simple stateful random generator constructed from |

| 13 | a pseudo-random function and sketching a proof of its security |

| 14 | as a pseudo-random generator. The associated !EasyCrypt proof |

| 15 | script (to come) gives an idea of the amount of effort needed |

| 16 | to formally fill the sketch into a simple – but fully formal – |

| 17 | proof. |