Research

Automated protocol analysis tools such as the Tamarin Prover offer a compelling alternative to traditional cryptographic techniques. These tools ingest a protocol description and its security properties and aim to analyse it entirely automatically, producing a proof that the properties hold or a counterexample. Unlike traditional approaches which can take months of expert analysis, Tamarin allows for rapid feedback and prototyping whilst a protocol is in the design stage.

However, automated tools can only find (or verify the absence of) attacks that are within the scope of their cryptographic model. One of my main areas of research has been improving the fidelity of this model and widening its scope to include more cryptographic primitives. My recent work has extended Tamarin to capture the complex cryptographic behaviours of non-prime order groups, invalid elliptic curve points and subtle signature properties. Using these extensions, we’ve:

• discovered a new attack on Secure Scuttlebutt’s authenticated key exchange.
• formally verified the Noise Protocol Framework.
• broken the WS-Security Mutual Authentication handshake.

In 2020, I helped design the DP3T Contact Tracing Protocols and analyse their security, privacy and performance characteristics. Our work, alongside other proposals such as PACT and TCN, inspired the Google and Apple Exposure Notification framework which is now deployed all over the world.