EasyCrypt-F*-CryptoVerif School 2014
The school website has been disbanded.
You will find on this page the materials relative to the EasyCrypt part.
- Lecture 1 -- Introduction and Game-Based Proofs
- Lecture 2 -- Types, Operators, Modules
- Lecture 3 -- Ambient Logic and pRHL
- Lecture 4 -- Theories, Cloning and Sections
- Lecture 5 -- High-level Proof Principles
- Lecture 6 -- Overview and perspectives
EasyCrypt Installation Instructions
We provide binary packages for EasyCrypt. You can download them at the following URL
Download the tarball corresponding to your system, untar it (this will create an
easycrypt folder) and run the script
run-easycrypt. The Emacs
editor should pop-up. You can then open any EasyCrypt
file (ending with the
.ec extension) and start hacking it.
- Note for Linux users:
- you must have emacs installed on your system.
- Note for Windows users:
- EasyCrypt support under Windows is beta.
- Under Windows 8, calls to SMT solvers might pop-up some console window that should get closed when the solver is done.
- the SMT prover
eproveris not available on your platform.
Note that you might have to redownload the binary package on Monday. If you installed EasyCrypt before the 23rd (exclusive) of November, redownload the binary packages or update your source tree and reinstall it.
In case you come to the EasyCrypt tutorials without EasyCrypt installed, you will be able to get it from USB keys.
A source distribution of EasyCrypt is also available. Installation instructions can be found in the README file. We strongly suggest that you try using the binary packages first.
refman.pdf (430.6 KB) - added by 2 years ago.
Ref Man: Description of most ambient and program tactics
lecture1.pdf (292.5 KB) - added by 2 years ago.
Introduction and Game-Based Proofs
lecture2.pdf (276.5 KB) - added by 2 years ago.
Types, Operators, Modules
lecture3.pdf (330.5 KB) - added by 2 years ago.
Ambient Logic and pRHL
lecture4.pdf (237.8 KB) - added by 2 years ago.
Theories, Cloning and Sections
lecture5.pdf (112.7 KB) - added by 2 years ago.
High-level Proof Principles
lecture6.pdf (347.5 KB) - added by 2 years ago.
Overview and perspectives
day1.tgz (3.8 KB) - added by 2 years ago.
Exercices for day 1
day2.tgz (7.2 KB) - added by 2 years ago.
Exercices for day 2