This course is intended for graduate students interested in data privacy, with a particular focus on differential privacy. Differential privacy offers a strong guaranteed bound on the increase in harm that a user may incur as a result of participating in a data analysis. The first part of this course will focus on some fundamental results about the theory of differential privacy and how to use it in concrete applications. The second part of the class will introduce students to EasyCrypt, a proof assistant designed for the verification of cryptographic primitives, and how to use it to verify cryptographic protocols and differential privacy algorithms.
We will also experiment practically with these topics on different examples by using the EasyCrypt tool, which you can find here. Detailed instructions for installing EasyCrypt, and configuring Emacs to work with EasyCrypt, can be found here. There is an (incomplete and somewhat out of date) EasyCrypt Reference Manual.| Date | Topic | Notes |
|---|---|---|
| Mon 10/24 | Privacy Attacks and Definition |
Slides |
| Tue 10/25 | Basic Mechanisms and Some Proofs |
Slides |
| Tue 11/1 | Basic Properties |
Slides |
| Wed 11/2 | Report Noisy Max and Exponential Mechanism |
Slides |
| Tue 11/8 | Other Mechanisms |
Slides |
| Wed 11/9 | Beyond Global Sensitivity and Verification |
Slides |
| Tue 11/15 | Introduction to EasyCrypt; EasyCrypt's Ambient Logic |
Slides EasyCrypt's Ambient Logic logic-examp-fill.ec logic-examp.ec primes-fill.ec primes.ec |
| Wed 11/16 | Using EasyCrypt's Program Logics |
EasyCrypt's While Language and Hoare Logic EasyCrypt's Relational Hoare Logic EasyCrypt's Probabilistic Relational Hoare Logic rnd-fill.ec rnd.ec |
| Thu 11/17 | Using EasyCrypt's Program Logics / Proving Cryptographic Security using EasyCrypt> |
EasyCrypt's While Language and Hoare Logic EasyCrypt's Relational Hoare Logic EasyCrypt's Probabilistic Relational Hoare Logic smc-fill.ec smc.ec Slides on Cryptographic Security |
| Tue 11/22 | Proving Cryptographic Security using EasyCrypt |
Presentation of Assignment 2 phoare-fill.ec phoare.ec Slides on Cryptographic Security |
| Wed 11/23 | Proving Cryptographic Security using EasyCrypt / Differential Privacy in EasyCrypt (aprhl branch) |
Slides on Cryptographic Security |
| Thu 11/24 | Help on Assignment 2 | |
| Due Date | Name | File |
|---|---|---|
| Fri 11/11, 5pm | Assignment 1 |
assignment_1.txt |
| Fri 12/2, 5pm | Assignment 2 |
Assignment 2 ex1-fill.ec ex1.ec ex2-fill.ec ex2.ec ex3-fill.ec ex3.ec |