My research involves the development of new mathematical analysis techniques, and the application of these techniques to cyber security problems. Some highlights are listed below (some papers appear in more than one category). A fuller list of my publications can be found here and on my google scholar profile.

• Protocol Security:

  • More is Less: Extra Features in Contactless Payments Break Security (USENIX 2025). We look at non-spec, proprietorial, ad-hoc extra features that companies have been adding to the EMV payment protocol and find that they are the cause of many vulnerabilities.
  • Who Pays Whom? Anonymous EMV-Compliant Contactless Payments (USENIX 2025). A design of an privacy protecting, backward compatible, regulation compliant EMV card payment system.
  • Symbolic modelling of remote attestation protocols for device and app integrity on Android (AsiaCCS 2023). We find attacks against Google SafetyNet and Samsung Knox2 using Tamarin modelling, which led to the deprecation of Samsung Knox v2. Models and PoC code can be found here.
  • The Closer You Look, The More You Learn: A Grey-box Approach to Protocol State Machine Learning (CCS 2022) CVE-2020-17497 CVE-2021-44718. Source code and all artifacts can be found here.
  • Practical EMV Relay Protection (S&P 2022) Attacks against ApplePay and relay protection protocols from Mastercard and Visa, plus a new proposed protocol, with models in Tamarin. More information here, press coverage here and a promotional video.
  • Security Analysis and Implementation of Relay-Resistant Contactless Payments (CCS 2020) Protection for EMV cards from rouge readers, models in ProVerif.
  • Modelling of 802.11 4-Way Handshake Attacks and Analysis of Security Properties (STM 2020) We use Tamarin to test if the official WPA security properties were sufficient to catch the KRACK attack (they weren't).
  • Modelling and Analysis of a Hierarchy of Distance Bounding Attacks (Usenix 2018). Using ProVerif, we build on the FC2015 paper to make the first automated method to test for distance bounding attacks, first models of Mastercards RRP and NXP's proximity check. More information here.
  • Extending Automated Protocol State Learning for the 802.11 4-Way Handshake (ESORICS 2018) State machine learning for WPA, tool, CVE-2018-0412.
  • An Attack Against Message Authentication in the ERTMS Train to Trackside Communication Protocols (ASIACCS 2017).
  • On the (in)security of the Latest Generation Implantable Cardiac Defibrillators and How to Secure Them, (ACSAC) 2016 CVE-2019-6538, CVE-2019-6540
  • Relay Cost Bounding for Contactless EMV Payments, (FC 2015). A relay attack and protection for EMV, more information here.
  • Analysing Unlinkability and Anonymity Using the Applied Pi Calculus (CSF 2010).
  • A Traceability Attack Against e-Passports, (FC 2010). Media coverage of this work can be found here.
  • Analysing the MUTE Anonymous File-Sharing System Using the Pi-calculus (FORTE 06) Best Paper Award. We analysed a popular (in 2006) anonymous peer to peer file sharing system using the pi-calculus and found a flaw in the design.

  
  
• Industrial Control System and Rail Systems Security:

  • Catch Me If You Can: An In-Depth Study of CVE Discovery Time and Inconsistencies for Managing Risks in Critical Infrastructures (CPSIoTSec2022)
  • Learning From Vulnerabilities - Categorising, Understanding and Detecting Weaknesses in Industrial Control Systems (CyberICPS 2020), Dataset, CVE-2020-12524, CVE-2020-7592 , CVE-2020-24686
  • An Attack Against Message Authentication in the ERTMS Train to Trackside Communication Protocols (ASIACCS 2017) An attack against the most widely used rail control protocol.
  • TRAKS: A Universal Key Management Scheme for ERTMS (ACSAC 2017) A proposal for a quantum secure key management system for rail.


• Statistical Estimation of Information Flow and Leakage: Tools and software to support these papers can be found here
  • Time Protection: The Missing OS Abstraction (EuroSys 2019), time side-channel protection for sel4. The methods below are used to measure information leakage for a range of processor types.
  • LeakWatch: Estimating Information Leakage from Java Programs (ESORICS 2014), applying the methods below to make a tool for measuring information leaks in Java programs.
  • A Tool for Estimating Information Leakage, (CAV 2013) a tool and case studies based on the methods below.
  • Probabilistic Point-to-Point Information Leakage (CSF 2013), formally defining information leakage for programs that may loop or not terminate.
  • A Statistical Test for Information Leaks Using Continuous Mutual Information (CSF 2011), leakage model and test for continuous data.
  • Statistical Measurement of Information Leakage (TACAS 2010), How to estimate mutual information based leakage measures from sampled data.


• Cyber Security Education and Games:

  • Anti-Cheat: Attacks and the Effectiveness of Client-Side Defences (CheckMATE 24), a look at how game anti-cheats and cheats work and how cheats are sold online.
  • Teaching Adversarial Thinking by Having Students Circumvent Exam Rules Advances in Teaching and Learning for Cyber Security Education. CSE 2024.
  • Phishing Attacks: Learning by Doing (ASE 18), a phishing simulation VM.
  • Jail, Hero or Drug Lord? Turning a Cyber Security Course Into an 11 Week Choose Your Own Adventure Story (ASE 17)
  • Learning From Others Mistakes: Penetration Testing IoT Devices in the Classroom, (ASE 2016)
  • An Offline Capture The Flag-Style Virtual Machine for Cyber Security Education (3GSE 15)
  • SCAIL: An integrated Starcraft AI System (CIG2012).

  
  
• BioInformatics: Before cyber security I worked on:

  • Finishing the euchromatic sequence of the human genome (Nature 431, 2004), I was one of 4000+ authors of this paper on the results of the human genome project.
  • GAZE: a generic framework for the integration of gene-prediction data by dynamic programming, a dynamic programming framework for finding genes in DNA (Genome research 12/9 2002)

I co-founded and named the Finite Number of Monkeys hacking club.