Differential Privacy: Theory and Verification in EasyCrypt

Location: Chalmers
Instructors: Marco Gaboardi and Alley Stoughton
e-mail: gaboardi@bu.edu and stough@bu.edu

Reading material:
  • The Algorithmic Foundations of Differential Privacy (DR)
  • The Complexity of Differential Privacy (SV)
  • Programming Differential Privacy
  • https://differentialprivacy.org

  • Overview

    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
    Tue 10/25 Basic Mechanisms and Some Proofs
    Tue 11/1 Basic Properties
    Wed 11/2 Report Noisy Max and Exponential Mechanism
    Tue 11/8 Other Mechanisms
    Wed 11/9 Beyond Global Sensitivity and Verification
    Tue 11/15 Introduction to EasyCrypt; EasyCrypt's Ambient Logic
    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
    Fri 12/2, 5pm Assignment 2
    Assignment 2
    ex1-fill.ec ex1.ec
    ex2-fill.ec ex2.ec
    ex3-fill.ec ex3.ec