My research is in the formal modelling and verification of communication protocols. Generally, our process is:
- Identify a real-world protocol or usecase
- Create a mathematical model which represents the requirements of this protocol
- Prove results about this model, often with the assistance of automated proving tools such as Tamarin
- Claim (usually in a useful way!) that our findings are relevant to the “real” protocol
Luckily, it seems that this is a good approach to getting useful results in the domain of cybersecurity. Thanks in no small part to my wonderful coauthors, we have had multiple publications in top-level conferences relating to several highly relevant topics, such as TLS, distance-bounding protocols and even RFID-enabled passports. See my Publications for more.