The Joint EasyCrypt-F*-CryptoVerif School 2014
Dates: 24-28 November
Place: Paris
Because the interest was so big, the school location has changed; we now have two locations:
- Monday, Tuesday, and Friday are at: Maison Internationale, Salon David Weill, Cité internationale universitaire de Paris (Cite Universitaire), 17 Boulevard Jourdan, 75014 Paris
- Wednesday and Thursday we are at: UPMC - Campus des Cordeliers, Amphitheatre Roussy, 15 Rue de l'École de Médecine, 75006 Paris
Abstract
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.
F* is a new ML-like functional programming language designed with program verification in mind. It has a powerful refinement type-checker that discharges verification conditions using the Z3 SMT solver. F* has been successfully used to verify nearly 50,000 lines of code, ranging from cryptographic protocol implementations to web browser extensions, and from cloud-hosted web applications to key parts of the F* compiler itself. The newest version on F* erases to both F# and OCaml, on which it is based. It also compiles securely to JavaScript, enabling safe interoperability with arbitrary, untrusted JavaScript libraries.
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.
The presented tools have been developed at
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, Aseem Rastogi, Pierre-Yves Strub, Nikhil Swamy
Invited speakers
While the school is targeted mostly at explaining the three tools, we're also planning two sessions of invited talks, a longer one Wednesday morning and a short one Friday morning.
- Hubert Comon (LSV, CNRS & ENS de Cachan) - Computationally Complete Symbolic Attacker
- Véronique Cortier (CNRS & LORIA Nancy) - Type-Based Verification of Electronic Voting Protocols
- Matteo Maffei (Saarland University) - Affine Refinement Types for Secure Distributed Programming
- Dominique Unruh (University of Tartu) - Computational Soundness for Refinement Types
Organization
Anna Bednarik, Cătălin Hriţcu (contact), Pierre-Yves Strub
Registration
- The school has filled up completely, we have no space for additional participants.
Schedule
Monday, November 24th 2014
| Time | Maison Internationale, Cite Universitaire | Room |
|---|---|---|
| 09.15 - 10.15 | EasyCrypt lecture - Introduction to Game-Based Proofs | Salon David Weill |
| 10.15 - 10.30 | break | |
| 10.30 - 11.30 | EasyCrypt lecture - Introduction to EasyCrypt | |
| 11.30 - 11.45 | break | |
| 11.45 - 12.45 | EasyCrypt lecture - Probabilistic Relational Hoare Logic and the EasyCrypt proof engine | |
| 12.45 - 14.15 | lunch | Restaurant Universitaire |
| 14.15 - 15.45 | EasyCrypt tutorial | Salon David Weill + Salle Orange at INRIA (25 minutes walk) |
| 15.45 - 16.15 | break | |
| 16.00 - 17.30 | EasyCrypt tutorial |
Tuesday, November 25th 2014
| Time | Maison Internationale, Cite Universitaire | Room |
|---|---|---|
| 09.15 - 10.15 | EasyCrypt lecture - Theories, Cloning and Modules | Salon David Weill |
| 10.15 - 10.30 | break | |
| 10.30 - 11.30 | EasyCrypt lecture - High-Level Cryptographic Proof Principles | |
| 11.30 - 11.45 | break | |
| 11.45 - 12.45 | EasyCrypt lecture - EasyCrypt in the Real-World | |
| 12.45 - 14.15 | lunch | Restaurant Universitaire |
| 14.15 - 15.45 | EasyCrypt tutorial | Salon David Weill + Salle Orange at INRIA (25 minutes walk) |
| 15.45 - 16.15 | break | |
| 16.00 - 17.30 | EasyCrypt tutorial | |
| 18.00 - 20:00 | Cryptosense Reception | Le Vin Qui Danse, Gobelins (25 minutes walk from CiteU) |
Wednesday, November 26th 2014 (Tentative!)
| Time | UPMC - Campus des Cordeliers | Room |
|---|---|---|
| 09:00 - 10:00 | F* lecture: High-level introduction (Nikhil) | Amphitheatre Roussy |
| 10:00 - 10:15 | short break | |
| 10:15 - 10:45 | Véronique Cortier: Type-Based Verification of Electronic Voting Protocols (Invited Talk) | |
| 10:45 - 11:15 | Matteo Maffei: Affine Refinement Types for Secure Distributed Programming (Invited Talk) | |
| 11:15 - 11:30 | short break | |
| 11:30 - 12:00 | Hubert Comon: Computationally Complete Symbolic Attacker (Invited Talk) | |
| 12:00 - 12:30 | CryptoVerif lecture: sneak preview (Bruno) | |
| 12:30 - 14:30 | lunch break | |
| 14:30 - 16:00 | F* lecture: Basics | |
| 16:00 - 16:30 | break | |
| 16.30 - 19:00 | F* lecture and/or tutorial (TBD) | Amphitheatre Roussy + Rooms Déjerine and Leroux (35 people each) |
| 19:00 - 21:00 | Social dinner | Bouillon Racine (2 minutes walk) |
Thursday, November 27th 2014
| Time | UPMC - Campus des Cordeliers | Room |
|---|---|---|
| 09:00 - 10:00 | F* lecture | Amphitheatre Roussy |
| 10:00 - 10:15 | short break | |
| 10:15 - 11:15 | F* lecture | |
| 11:15 - 11:30 | short break | |
| 11:30 - 12:30 | F* lecture | |
| 12:30 - 14:30 | lunch break | |
| 14:30 - 16:00 | F* tutorial | Rooms Déjerine and Leroux (35 people each) |
| 16:00 - 16:30 | break | |
| 16.30 - 18:00 | F* tutorial |
Friday, November 28th 2014
| Time | Maison Internationale, Cite Universitaire | Room |
|---|---|---|
| 09:00 - 10:30 | CryptoVerif lecture | Salon Salon David Weill |
| 10:30 - 11:00 | break | |
| 11:00 - 12:30 | CryptoVerif lecture | |
| 12:30 - 13:00 | Dominique Unruh: Computational Soundness for Refinement Types (Invited talk) | |
| 13:00 - 14:30 | lunch break | Restaurant Universitaire |
| 14:30 - 16:00 | CryptoVerif tutorial | Salon Salon David Weill |
| 16:00 - 16:30 | break | |
| 16.30 - 18:00 | CryptoVerif 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 on the participants' mailing list.
Social dinner
- The social dinner is free for all registered participants and takes place Wednesday at 7pm at Bouillon Racine.
- Bouillon Racine is located at 3 rue Racine, 75006 Paris, a 2 minutes walk from UPMC - Campus des Cordeliers.
- The social dinner is sponsored by the MSR-Inria Joint Centre.
Cryptosense reception
- The Cryptosense reception takes place Tuesday 6-8pm at Le Vin Qui Danse, Gobelins.
- We have a reserved area at the back of the bar. There will be a wine, juice, water, and nibbles available, paid for by Cryptosense, and the possibility of buying beer or cocktails at the bar. Afterwards it's a reasonable area for people to split up and go for dinner in smaller groups.
- Le Vin Qui Danse, Gobelins is located at 69 Rue Broca, 75013 Paris. That's a 25 minutes walk from Cité Universitaire (15 minutes walk from Place d'Italie). From Cité Universitaire one can also take RER B, get off at Port Royal, and then walk for 10 minutes.
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 dinner (see above).
Sponsors
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. The MSR-Inria Joint Centre sponsors the social dinner. Cryptosense organizes and sponsors the reception.
