Quantitative Analysis of Information Leakage in Probabilistic and Nondeterministic Systems

TL;DR

This thesis introduces cpCTL, a temporal logic for specifying and verifying quantitative information leakage in anonymity protocols, along with algorithms for leakage computation and techniques for protocol debugging.

Contribution

It presents cpCTL, the first logic for conditional probabilities in security, and algorithms for quantifying information leakage in anonymity protocols.

Findings

Developed cpCTL for formal security property specification.

Created algorithms to compute and approximate information leakage.

Proposed a debugging technique for security protocol flaws.

Abstract

This thesis addresses the foundational aspects of formal methods for applications in security and in particular in anonymity. More concretely, we develop frameworks for the specification of anonymity properties and propose algorithms for their verification. Since in practice anonymity protocols always leak some information, we focus on quantitative properties, which capture the amount of information leaked by a protocol. The main contribution of this thesis is cpCTL, the first temporal logic that allows for the specification and verification of conditional probabilities (which are the key ingredient of most anonymity properties). In addition, we have considered several prominent definitions of information-leakage and developed the first algorithms allowing us to compute (and even approximate) the information leakage of anonymity protocols according to these definitions. We have also studied a well-known problem in the specification and analysis of distributed anonymity protocols, namely full-information scheduling. To overcome this problem, we have proposed an alternative notion of scheduling and adjusted accordingly several anonymity properties from the literature. Our last major contribution is a debugging technique that helps on the detection of flaws in security protocols.