Tom Chothia

Tom Chothia

Professor of Cyber Security · University of Birmingham

I build mathematical methods for analysing security: formal verification of protocols, and statistical measurement of information leakage. I then use them to break and fix real systems. Work from my group has changed contactless payment standards, broken the Windows secure kernel, deprecated an Android attestation platform, and produced fixes in Wi-Fi, cardiac defibrillators and rail signalling.

Tom Chothia holding out a hand to two monkeys sitting on a railing in a forest.
I co-founded and named Birmingham’s student hacking club, A Finite Number of Monkeys.

Research

Six threads of work

Each thread runs from a formal model through to a working attack on deployed hardware, and where possible to a fix in the standard. Every badge below is a link.

Contactless payments

Breaking and fixing EMV

A decade of work on contactless card payments: relay attacks that let a payment be made from a card that is nowhere near the terminal, a bypass of the Apple Pay and Visa lock screen, and a study showing that the non-standard extra features banks bolt onto EMV are the source of most of its vulnerabilities. We also designed relay-resistant and privacy-preserving protocols that stay backward compatible with the deployed estate.

How easy is it to steal $10,000 from a locked phone? Veritasium · explains our IEEE S&P 2022 Apple Pay result All payment papers →

Protocol analysis

State learning and verification

Automatically recovering a protocol implementation's state machine and checking it against the specification. The grey-box method finds bugs black-box learning misses; our Tamarin models of Android remote attestation led Samsung to deprecate Knox v2.

All protocol papers →

Critical infrastructure

Rail and industrial control

An attack against message authentication in ERTMS, the most widely deployed rail control protocol, a quantum-secure key management scheme to replace it, and a systematic study of how long ICS vulnerabilities take to surface as CVEs.

All rail & ICS papers →

Quantitative security

Measuring information leakage

How much does a system actually leak? We built the statistical theory for estimating mutual information and min-entropy leakage from sampled executions, then the tools that apply it to Java programs and to processor timing channels in seL4: LeakiEst, LeakWatch and CH-IMP.

Tools →

Education

Teaching adversarial thinking

Security is learned by doing. An offline capture-the-flag virtual machine, a phishing simulator students attack in a sandbox, an eleven-week course run as a choose-your-own-adventure story, and an exam students are invited to cheat on.

All education papers →