Revision as of 12:08, 4 November 2014 by Chritcu (talk | contribs) (Wednesday, November 26th 2014 (Tentative!))

The Joint EasyCrypt-F*-CryptoVerif School 2014

From prosecco

Dates: 24-28 November

Place: Paris

Because the interest was so big, the school location has changed; we now have two locations:

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.

Lecturers and tutorial aides

Participants will attend lectures and hands-on tutorials, under the guidance of members from the tools' developer teams:

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 on Wednesday afternoon and a short one on Friday morning.

  • 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

Organization

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

Schedule (Work in progress)

Monday, November 24th 2014

Time Maison Internationale, Cite Universitaire Room
09.15 - 10.45 EasyCrypt lecture - TBA Salon David Weill
10.45 - 11.15 break
11.15 - 12.45 EasyCrypt lecture - TBA
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.45 EasyCrypt lecture - TBA Salon David Weill
10.45 - 11.15 break
11.15 - 12.45 EasyCrypt lecture - TBA
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

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: Using F* to Verify E-Voting Protocols (Invited Talk)
10:45 - 11:15 Matteo Maffei: Linear Refinement Type Systems (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 Amphitheatre Roussy
16:00 - 16:30 break
16.30 - 18:00 F* lecture or tutorial (TBD) Amphitheatre Roussy
+ 2 rooms for 40 people
19:00 - 21:00 Social dinner' Bouillon Racine

Thursday, November 27th 2014

Time UPMC - Campus des Cordeliers Room
09:00 - 10:30 F* lecture Amphitheatre Roussy
10:30 - 11:00 break
11:00 - 12:30 F* lecture
12:30 - 14:30 lunch break
14:30 - 16:00 F* tutorial 2 rooms for 40 people
16:00 - 16:30 break
16.30 - 18:00 F* tutorial

Friday, November 28th 2014

Time Maison Internationale, Cite Universitaire Room
09:00 - 09:30 Dominique Unruh (Invited talk) Salon David Weill
09:30 - 10:30 CryptoVerif lecture
10:30 - 11:00 break
11:00 - 13:00 CryptoVerif lecture
13:00 - 14:30 lunch break
14:30 - 16:00 CryptoVerif tutorial
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.

Registration

  • There are no registration fees for participants.
  • Registration deadline has passed (1 September, 2014).
  • The number of participants is limited.
  • Registrants were informed of the outcome of the selection process on 16 September, 2014.
  • The school has filled up completely, we have no space for additional participants.

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.
  • Most of these grants are supported by the Prosecco team at INRIA Paris-Rocquencourt. 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).

Social dinner

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.

Institutions

The presented tools have been developed at

CNRS      ENS      IMDEA    INRIA    Microsoft Research      Microsoft Research Inria Joint Centre