The Joint EasyCrypt-F*-CryptoVerif School 2014

Place: INRIA office in Paris

23 Avenue d'Italie, 75013 Paris

Abstract:

Formal verification tools for cryptographic constructions and protocols are slowly reaching maturity. This school is aimed at teaching you how to use three state of the art cryptographic verification tools: EasyCrypt, F*, and CryptoVerif, as well as give you a glimpse of the beautiful theoretical foundations behind these tools.

[wiki:WikiStart 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, and more recently the formalization of secure function evaluation, verifiable computation and key-exchange protocols.

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.

Lecturers and tutorial aides:

• EasyCrypt:

 Gilles Barthe,
 François Dupressoir,
 Benjamin Grégoire,
 Benedikt Schmidt,
 Pierre-Yves Strub,
 Santiago Zanella-Béguelin

• F*:

 Karthik Bhargavan,
 Antoine Delignat-Lavaud,
 Cédric Fournet,
 Cătălin Hriţcu,
 Chantal Keller,
 Alfredo Pironti,
 Pierre-Yves Strub

• CryptoVerif:

 Bruno Blanchet

Invited speakers:

TBA

Organization:

Anna Bednarik, Cătălin Hriţcu, Pierre-Yves Strub

Schedule:

• Monday, 24 November: !EasyCrypt
• Tuesday, 25 November: !EasyCrypt
• Wednesday, 26 November: F*
• Thursday, 27 November: Lectures on F* + !CrytoVerif (morning) + F* tutorial (afternoon)
• Friday, 28 November: Invited speakers (morning) + !CrytoVerif 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 registered participants.

Registration:

• There are no registration fees for participants.
• Please fill in this registration form

Financial support:

• 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.

Social events:

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).

Sponsors:

This school is financially supported by the Prosecco team at INRIA Paris-Rocquencourt.