Aaron Coble



Aaron received a Bachelor's of Science degree with Honours in Computer Science from the Pennsylvania State University in 2005.

Afterwards he began research towards his PhD at the University of Cambridge Computer Laboratory. That research, supervised by Prof. Lawrence Paulson, brought together the domains of mechanised theorem-proving and computer security in order to develop methods for analysing the privacy and information leakage of software systems. Mechanisms for preserving privacy in modern communications systems often use probabilistic algorithms and can only practically provide partial protection; therefore, it is vital to have high-assurance techniques for quantifying and verifying the security provided by those complex systems.

Aaron's research resulted in the formalisation of numerous foundational theories in the HOL4 theorem prover (HOL4), including: measure theory, probability theory, Lebesgue integration, and (Shannon's) information theory. He then applied those theories to create a quantitative framework for analysing information leakage using HOL4. Using that framework, Aaron produced the first machine-verified proof of anonymity for the dining cryptographers protocol, for an unbounded number of participants, thereby demonstrating the applicability of the framework in the privacy domain.

Since the completion of his PhD research, Aaron has been working as a Product Development Engineer at CMCL Innovations in Cambridge and is a Visiting Fellow at the CoMo Group.

Research Themes

  Theme icon

Contact Details

Telephone: +44 (0)1223 767866
Address: CMCL Innovations, Sheraton House, Castle Park, Cambridge CB3 0AX, United Kingdom