Summer School Program Target Audience Venue and Registration Workshop Accommodation Acknowledgments

Announcement

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.

School

The first EasyCrypt summer school will take 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.

Program

July 16th

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

July 17th

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

July 18th

9:00 - 9:45Probability Computations, Failure Events
10:00 - 12:00Tutorial Session 3 - Probability computations and reasoning up to failure
13:30 - 14:15Case Study
14:30 - 16:30Tutorial Session 4 - Case Study-related proofs [Corrected exercises]
The material linked is also available from the public repository used during the school at http://ci.easycrypt.info/ec-school.git/ using
git clone http://ci.easycrypt.info/ec-school.git
We will do our best to update the tutorial exercises and slides if (when) syntax changes occur.

Target audience

Participants are expected to have a basic understanding of the following topics: Background material can be obtained by visiting http://www.easycrypt.info.
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 http://www.easycrypt.info/ 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@imdea.org) if the space constraints allow it.

Workshop

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.

Program

July 19th

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

Accommodation

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.

Acknowledgments

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.