The IACR School on Computer-aided Cryptography will take place at University of Maryland, College Park, USA on June 1- 4 2015.

The school is sponsored by the International Association for Cryptologic Research (IACR), IMDEA Software Institute, Inria and University of Maryland.

The goal of the school is to provide participants with an overview of computer-aided cryptography with a special focus on computer-aided cryptographic proofs using the EasyCrypt tool. 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. Invited lectures will cover more specialized computer-aided cryptography techniques and tools.


The school is free of charge for participants, but the number of places is limited. To register, send an email to We provide a limited number of travel stipends to America-based students. Please indicate in your registration if you want to apply for a stipend.

Tentative Program

The school will take place in room CSIC (computer science instructional center) 2107.

Monday (10.00am - 1.00pm and 2.00pm - 5.00pm)
Lecture 3h Introduction to game-based cryptographic proofs (see attachment for slides)
Tutorial 3h EasyCrypt: Introduction, Security definitions and Simple Proofs
Tuesday (10.00am - 1.00pm and 2.00pm - 5.00pm)
Tutorial 3h EasyCrypt: Reasoning about Failure Events
Tutorial 3h EasyCrypt: Modules, Theories and Instantiation
Wednesday (10.00am - 1.00pm and 2.00pm - 5.00pm)
Lecture 90m Computer-Aided Cryptographic Proofs for Low-Level Implementations (F. Dupressoir)
Lecture 90m Towards Information-theoretic Security Proofs in EasyCrypt for Multi-party Protocols (A. Stoughton)
Tutorial 3h ZooCrypt: Automated proofs for pairing and RSA-based cryptography (B. Schmidt)
Thursday (10.00am - 1.00pm)
Tutorial 60m Automated analysis of assumptions and constructions in generic group models (B. Schmidt)
Talk 30m Automated analysis and synthesis of modes of operation for CPA and AE (A. Malozemoff, UMD)
Talk 45m Small Circuits for Cryptographic Applications (R. Peralta, NIST)
Talks 45m Slots for participants of the school


Contributed Talks

Confirmed Speakers

  • François Dupressoir
  • Alex Malozemoff
  • Benedikt Schmidt
  • Alley Stoughton

Installing EasyCrypt

You can get EasyCrypt via our public git repository (browse):

git clone

Installation instructions can be found in the README file, and some tutorial material is available. You can also download a draft version of the reference manual.

We are also providing binary packages (last update: 27/05/2015)

You can also download a VirtualBox appliance

Target audience

The main objective of the school will be to give participants with some background in cryptography the necessary knowledge in formal methods to formalize cryptographic definitions and perform computer-aided cryptographic proofs in EasyCrypt. Furthermore, the school can also serve as an introduction to provable security for participants with a strong background in formal methods.

Contributed Talks

Small Circuits for Cryptographic Applications

René Peralta, NIST

Consider the function

f(x1,x2,x3,x4,x5) = x1x2x3 + x1x2x4 + x1x2x5 + x1x3x4 +
x1x3x5 + x1x4x5 + x2x3x4 + x2x3x5 +
x2x4x5 + x3x4x5 + x1x2x3x4 +
x1x2x3x5 + x1x2x4x5 + x1x3x4x5 +

over GF(2).

Using only addition and multiplication modulo 2, we would like to find good circuits under a variety of metrics. For example: how many multiplications are required? Take a guess and come to the talk.


We cannot arrange accommodation for summer school participants, UMD lists a number of options at

Last modified 20 months ago Last modified on 6 Jun 2015, 15:07:21

Attachments (7)