We are delighted to announce the first EasyCrypt school and workshop, to be held at the Computer and Information Science Department, University of Pennsylvania, Philadelphia, USA, on July 16-19, 2013.


The first EasyCrypt summer school took place from July 16th to July 18th 2013 at the University of Pennsylvania.

The goal of this Summer School is to give a working understanding of computer-aided cryptographic proofs, as embodied in the EasyCrypt tool, to cryptographers of all levels. Lectures discussing the theoretical aspects of computer-aided cryptography will be complemented by hands-on lab sessions, covering all aspects of the tool, from the basic aspects of formalizing cryptographic schemes and properties to advanced code-based proof techniques.

Lectures will be assured by Gilles Barthe, François Dupressoir, Benjamin Grégoire (INRIA), César Kunz, Alley Stoughton (MITLL), and Pierre-Yves Strub. Juan Manuel Crespo, Guillaume Davy and Santiago Zanella-Béguelin (MSRC) will help during the tutorial sessions.

You can download the school material (slides, tutorials).


July 16th

9:30 - 12:00
Introductory Lectures
13:30 - 16:30
Tutorial Session 1 - Basic Proofs and Formalizations

July 17th

9:00 - 9:45
Modules and Instantiation
10:00 - 12:00
Tutorial Session 2 - Modules, advanced pRHL proofs
13:30 - 14:15
Sections, Theories and Cloning
14:30 - 16:30
Tutorial Session 3 - Sessions, Theories, advanced instantiation

July 18th

9:00 - 9:45
Probability Computations, Failure Events
10:00 - 12:00
Tutorial Session 3 - Probability computations and reasoning up to failure
13:30 - 14:15
Case Study
14:30 - 16:30
Tutorial Session 4 - Case Study-related proofs [Corrected exercises]

Target audience

Participants are expected to have a basic understanding of the following topics:

  • semantics of pWhile, and basics of Hoare logic,
  • basic understanding of provable crypto and game-based proofs.

Background material can be obtained by visiting

In addition, each participant is expected to bring his or her own computer, with the latest version of EasyCrypt installed and working in interactive mode. Some documentation and help will be made available on in advance of the school.

Venue and Registration

The summer school will be held at the University of Pennsylvania between the 16th and 18th of July. Registration is now closed. People from UPenn wishing to attend are encouraged to check with the organizers (francois.dupressoir@…) if the space constraints allow it.


The summer school will be followed (on July 19th) by a workshop. Summer school participants should let us know if they plan on attending the workshop when registering. The aim of the workshop is to allow researchers working with EasyCrypt to present their ongoing work and to exchange their experiences with using the system. Participants interested in presenting their work should send a title and abstract, with an indication of the intended length of the talk to François Dupressoir.


July 19th

9:30 - 11:00
MITLL - NRL Panel EasyCrypt 0.2 feedback and opinions
  • Jonathan Herzog (MITLL) (pdf),
  • Catherine Meadows (NRL),
  • Aaron Jaggard (NRL),
  • Alley Stoughton (MITLL) (pdf), and
  • Jonathan Katz (U. of Maryland) (pdf)
11:20 - 11:50
An EasyCrypt Formalization of Garbled Circuits
Guillaume Davy (IMDEA Software and ÉNS Cachan) (pdf)
12:30 - 13:30
Certified Machine Code from Provably Secure C-like Code
François Dupressoir (IMDEA Software) (pdf)
Adam Petcher (MITLL and Harvard)


We cannot arrange accommodation for summer school participants, and UPenn does not appear to provide on-campus accommodation for visitors. If nearby hotels are not an option, please take a look at UPenn's page on temporary housing.


The school will be hosted by the University of Pennsylvania, USA. Thanks to Andre Scedrov and Benjamin Pierce for their kind help. EasyCrypt and the school are partially funded by ONR Grant N000141210914, Spanish project TIN2009-14599 DESAFIOS 10, and Madrid Regional project S2009TIC-1465 PROMETIDOS.

Last modified 3 years ago Last modified on 18 Mar 2014, 16:39:37

Attachments (13)