Biography

I am an Associate Professor in the Cryptography Research group and School of Computer Science at the University of Bristol (UK).

I received my PhD from the Open University in 2013, for my research on “Proving Cryptographic C Programs Secure with General-Purpose Verification Tools”. It was conducted under the supervision of Andy Gordon, Jan Jürjens and Bashar Nuseibeh, and was supported by a Microsoft Research PhD Scholarship. I spent most of my PhD time at the MSR lab in Cambridge, with internships in MSR’s labs in Aachen, Cambridge and Redmond, and some brief stays at the Open University in Milton Keynes.

I then went on to do some work on EasyCrypt and on using it to machine-check increasingly out-of-reach cryptographic proofs (including some with more “real-world” adversary models) while a post-doctoral research at the IMDEA Software Institute. This has been my research focus since, also through my stay as a lecturer (and senior lecturer) at the University of Surrey.

Research

My research revolves around proving cryptographic and side-channel security properties of concrete realizations and implementations of cryptographic primitives and protocols, in the presence of partial compromise. This involves tackling problems in modelling adversaries and systems, designing and applying proof methodologies and verification tools, and generally finding less tedious ways of verifying complex properties of important (but not vast) quantities of code.

Check out my publications on the topic.

Other research-related information

I serve as Head of the Cryptography research group—representing and supporting Chloe Martindale and Dan Page and their labs.

I am associated with the Bristol Programming Languages research group.

I am a core developer for the EasyCrypt proof assistant, focusing on its libraries of cryptographic definitions and game transformations, and finding new and exciting ways to use it to do things it’s not designed to do.

I am a core member of the Formosa Crypto project, federating activities around machine-checked cryptography and verifiable cryptographic engineering to enable practical adoption of the techniques and tools.

Supervision

If you are interested in research positions on machine-checked cryptography, high-assurance cryptography, or verified software-security, please take a look through my recent publications and contact me with a proposal for a short project that relates to them (essentially the first year of your PhD, but shorter if you’re only interested in an internship).

I tend to expect and encourage independence in students I supervise: a PhD is a joint enterprise in co-discovery, and I will be learning only slightly less than you in the process of guiding you through it.