The Joint EasyCrypt-F*-CryptoVerif School 2014
Dates: 24-28 November
Precise location TBA
The school is aimed at teaching participants how to use three state-of-the-art security verification tools: EasyCrypt, F*, and CryptoVerif, as well as give participants a glimpse of the formal foundations behind these tools.
EasyCrypt is a toolset for reasoning about relational properties of probabilistic computations with adversarial code. Its main application is the construction and verification of game-based cryptographic proofs. EasyCrypt was used to prove the security of complex cryptographic constructions, including the Cramer-Shoup encryption scheme, the Merkle-Damgaard iterative hash function design, and the ZAEP encryption scheme. More recently, it has been used for proving the security of protocols based on garbled circuits, and for the proof of security for authenticated key-exchange protocols and derived proofs under weaker assumptions.
CryptoVerif is an automatic protocol prover sound in the computational model. It can prove secrecy and correspondences (e.g. authentication). The generated proofs are by sequences of games, as used by cryptographers. CryptoVerif was successfully used for security proofs of FDH signatures, Kerberos, OEKE, and the SSH transport layer protocol.
Lecturers and tutorial aides
Participants will attend lectures and hands-on tutorials, under the guidance of members from the tools' developer teams:
- EasyCrypt: Gilles Barthe, François Dupressoir, Benjamin Grégoire, Benedikt Schmidt, Pierre-Yves Strub
- F*: Karthik Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Cătălin Hriţcu, Chantal Keller, Alfredo Pironti, Pierre-Yves Strub, Nikhil Swamy
While the school is targeted mostly at explaining the three tools, we're also planning two sessions of invited talks, one on Wednesday and one on Friday.
- Hubert Comon (LSV, CNRS & ENS de Cachan) - Computationally Complete Symbolic Attacker
- Véronique Cortier (CNRS & LORIA Nancy) - Using F* to Verify E-Voting Protocols
- Matteo Maffei (Saarland University) - Linear Refinement Type Systems
- Dominique Unruh (University of Tartu) - Computational Soundness for Refinement Types
- Monday, 24 November: EasyCrypt
- Tuesday, 25 November: EasyCrypt
- Wednesday, 26 November: F* + Invited speakers: Cortier & Comon (afternoon)
- Thursday, 27 November: Lectures on F* + CryptoVerif (morning) + F* tutorial (afternoon)
- Friday, 28 November: Invited speakers: Maffei & Unruh (morning) + CryptoVerif lecture + tutorial
Hardware and software
Roughly half of the time of the school is devoted to hands-on exercise sessions and tutorials. Participants are expected to bring their own laptop with EasyCrypt, F*, and CryptoVerif installed. More details e.g. about precise versions and setup will be communicated by email to the participants.
- There are no registration fees for participants.
- Registration deadline has passed (1 September, 2014).
- The number of participants is limited.
- Registrants will be informed of the outcome of the selection process shortly after the registration deadline.
- We try to offer grants covering the travel and/or accommodation costs of the participants who need it.
- The accommodation support is for double hotel rooms we will directly book and which will be shared by two participants each.
- The travel support comes in the form of reimbursement for the costs of a trip participants plan and initially pay themselves, provided these costs stay within certain bounds we establish in advance.
- Participants can apply for financial support via the registration form above.
- A number of the grants for UK attendees are subsidized by CryptoForma; the application process is the same for all grants (part of the normal registration form above).
We will organize a social dinner and a social lunch that are free for all registered participants.
Travel, food, and accommodation
Participants are expected to make their own travel, food, and accommodation arrangements. Paris offers many good alternatives. The only exceptions are for invited speakers, for the shared hotel rooms (see financial support above), and for the social events (see above).
This school is financially supported by the Prosecco team at INRIA Paris-Rocquencourt. The EPSRC CryptoForma network on formal methods and cryptography sponsors a number of grants for UK attendees.