Computer Science and Privacy
Prof. Frédéric Prost. IMAG, Francia.
Abstract
The aim of the course is to provide theoretical tools to handle privacy issues in computer science. Privacy issues take a more and more important place in the public debate since the revelations of E. Snowden. Nevertheless, bare concepts related to privacy are difficult to precisely define from a scientific point of view. The very definition of what is privacy is an active research subject. Moreover, by nature, privacy issues involve many aspects of computer science at many levels: typically it goes from cryptography to formal methods mixed together with network engineering and operating system considerations.
The main objective of the course is to provide a "tour d'horizon" of techniques and theoretical tools used to reason about privacy in our information technology society. We will first show how standard cryptographic tools are not sufficient to cope with privacy. We will present several mathematical definitions of privacy (notably the non-interference property studied in various settings), discuss their relevance and how they can be analysed. We will also adress the ideas behind zero-knowledge proofs that are stepping stones for a mathematical approach to privacy. Finally, we will show how formal methods can be applied to complex situations like electronic cash, anonymous blacklisting or electronic vote. The course is mainly based on research papers. Prerequisites Students are expected to have basic notions in computability and complexity notions. It is also supposed that students have followed a basic course in logic, and on theory of programming.
Indicative plan of the course
- 1- Introduction :
- 1.1- Cryptography is not enough : historical examples (enigma code breaking, various attacks on cryptographic protocols, de-anonymisation).
- 1.2- Shamir secret sharing protocol and applications.
- 1.3- Information theory and cryptography.
- 2- Formalizing identity and anonymity :
- 2.1- Identity certification schemes.
- 2.2- Measuring anonymity.
- 2.3- Differential privacy.
- 2.4- Chaum's algorithm for anonymous communications (oignon routing).
Attacks on anonymous schemes in theory and in practice.
- 3- Non interference property :
- 3.1- Formalizing information flow in programs : different definitions of non-interference Static analyses of non-interference in different paradigms (functional, imperative and concurrent calucli).
- 4- Zero-Knowledge proofs :
- 4.1- Interactive proofs of identiy without revealing id.
- 4.2- Non-interactive zero knowledge proofs.
- 4.3- Static analysis of zero knowledge protocols.
- 5- Formal proofs for elaborated protocols :
- 5.1- Electronic vote.
- 5.2- Electronic cash.
- 5.3- Anonymous blacklisting.
Examination
The evaluation mode will be Take-Home.
Slides
Exam
