Technical reports

Anonymity, information, and machine-assisted proof

Aaron R. Coble

July 2010, 171 pages

This technical report is based on a dissertation submitted January 2010 by the author for the degree of Doctor of Philosophy to the University of Cambridge, King’s College.

DOI: 10.48456/tr-785

Abstract

This report demonstrates a technique for proving the anonymity guarantees of communication systems, using a mechanised theorem-prover. The approach is based on Shannon’s theory of information and can be used to analyse probabilistic programs. The information-theoretic metrics that are used for anonymity provide quantitative results, even in the case of partial anonymity. Many of the developments in this text are applicable to information leakage in general, rather than solely to privacy properties. By developing the framework within a mechanised theorem-prover, all proofs are guaranteed to be logically and mathematically consistent with respect to a given model. Moreover, the specification of a system can be parameterised and desirable properties of the system can quantify over those parameters; as a result, properties can be proved about the system in general, rather than specific instances.

In order to develop the analysis framework described in this text, the underlying theories of information, probability, and measure had to be formalised in the theorem-prover; those formalisations are explained in detail. That foundational work is of general interest and not limited to the applications illustrated here. The meticulous, extensional approach that has been taken ensures that mathematical consistency is maintained.

A series of examples illustrate how formalised information theory can be used to analyse and prove the information leakage of programs modelled in the theorem-prover. Those examples consider a number of different threat models and show how they can be characterised in the framework proposed.

Finally, the tools developed are used to prove the anonymity of the dining cryptographers (DC) protocol, thereby demonstrating the use of the framework and its applicability to proving privacy properties; the DC protocol is a standard benchmark for new methods of analysing anonymity systems. This work includes the first machine-assisted proof of anonymity of the DC protocol for an unbounded number of cryptographers.

Full text

PDF (1.1 MB)

BibTeX record

@TechReport{UCAM-CL-TR-785,
  author =	 {Coble, Aaron R.},
  title = 	 {{Anonymity, information, and machine-assisted proof}},
  year = 	 2010,
  month = 	 jul,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-785.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-785},
  number = 	 {UCAM-CL-TR-785}
}