Aaron Coble

Biography

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 ReSolutions Ltd. in Cambridge and is a Visiting Fellow at the CoMo Group.