The IACR School on Computer-aided Cryptography will take place at University of Maryland, College Park, USA on June 1- 4 2015.
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 firstname.lastname@example.org. 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.
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|
- Slides for Lecture 1.
- EasyCrypt tutorial: exercises, a cleaner version of BR93, and a version with proofs filled in
- Slides for the lecture on implementation security
- Slides for "Stoughton: Towards Information-theoretic Security Proofs in EasyCrypt for Multi-party Protocols"
- Scripts for proofs of Stoughton's lecture
- René Peralta on Small Circuits for Cryptographic Applications (abstract). You can also have a look at René's circuits page.
- François Dupressoir
- Alex Malozemoff
- Benedikt Schmidt
- Alley Stoughton
You can get EasyCrypt via our public git repository (browse):
git clone https://github.com/EasyCrypt/easycrypt.git
We are also providing binary packages (last update: 27/05/2015)
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.
Small Circuits for Cryptographic Applications
Consider the function
f(x1,x2,x3,x4,x5) = x1x2x3 + x1x2x4 + x1x2x5 + x1x3x4 + x1x3x5 + x1x4x5 + x2x3x4 + x2x3x5 + x2x4x5 + x3x4x5 + x1x2x3x4 + x1x2x3x5 + x1x2x4x5 + x1x3x4x5 + x2x3x4x5
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 http://cvs.umd.edu/visitors/offcampus.html.
lecture1.pdf (262.9 KB) - added by 2 years ago.
tutorials-day-1.tgz (7.7 KB) - added by 2 years ago.
BR93_erased.ec (7.4 KB) - added by 2 years ago.
Erased version of BR93
BR93_filled.ec (9.4 KB) - added by 2 years ago.
Filled in proofs for BR93.
lecture-implementations.pdf (132.2 KB) - added by 2 years ago.
Lecture slides on implementation security
Stoughton-PCR.pdf (160.0 KB) - added by 2 years ago.
Stoughton: Towards Information-theoretic Security Proofs in EasyCrypt for Multi-party Protocols
PCR-proof-scripts.tar.gz (43.4 KB) - added by 2 years ago.
Stoughton: PCR EasyCrypt proof scripts