In this talk I will introduce the QIF approach to studying secure systems, focussing on the notion of refinement which provides a robust method of comparing systems wrt Bayesian threats. I will introduce a variety of new refinement orders inspired by QIF and DP which allow us to study threats to privacy using max-case notions. We will see how to apply these orders to the task of comparing DP mechanisms, raising the question of whether the order based on epsilon provides strong privacy guarantees.

In this talk I will outline how the theory of Quantitative Information Flow which was developed to provide a rigorous framework to measure information leakage was used to probe the Brazilian Education Censuses. Using this theory applied to these datasets showed that the defences proposed by the Ministry were prone to serious vulnerabilities, in some cases leading to complete re-identification under reasonably modest attacks. The consequence is that our work has provided the agency with rigorously formalized risk analysis, which will help it make informed decisions.

In this talk I will describe some recent developments concerning how to measure the severity of information leaks based on new definitions of entropy, and how to apply them to programming language semantics. The ideas are illustrated by measuring the degree of privacy participants can rely on when they vote using some standard voting protocols.