Research
Before entering industry, I completed a PhD in theoretical computer science, with applications in cybersecurity. My main area of research was in reasoning about the security of communication protocols (e.g. TLS, RFID payment systems) by embedding them within mathematical models.
Bibliography
I am listed as a (co-)author on the following papers. Links are to the associated publisher page (e.g. IEEE).
| Link | Description |
|---|---|
|
(arXiv - 2022)
|
Collaboration with Hugo Jonker, Sjouke Mauw and Hyunwoo Lee, based on the final work in my PhD thesis. A major class of multi-party communication protocols are those in which a message is passed up a chain of participants, rather than them communicating mutually between each other. In several scenarios -- including TLS and the Bitcoin Lightning network -- adversarial agents may benefit from artificially removing participants from the chain by sending messages out-of-band. We develop a framework for describing these protocols and appropriate security goals, including modelling classic attacks on the Lightning Network and multiparty TLS protocols |
|
(EuroS&P - 2020)
|
Supporting work with Steve Wesemeyer, Ioana Boureanu and Helen Treharne at the University of Surrey. The LoRaWAN protocol is used in a variety of IoT devices, typically to connect to a home server. This protocol involves an establishment phase in which a relay server brokers the channel between the endpoint and application server, under an implicit trust model. A high-fidelity model was created and analysed with Tamarin, and vulnerabilities identified (and confirmed by the security team at LoRa) |
|
(CCS - 2019)
|
Followup to previous work with Sjouke Mauw, Jorge Toro-Pozo and Rolando Trujillo-Rasua. We developed a framework for analysing collusion in security protocols -- agents temporarily deviating from their specification in order to break security roles. Informally, a protocol is deemed 'collusion-resistant' if it's not possible to temporarily break the protocol; the smallest violation you can make is essentially equivalent to disclosing your secret encryption keys. We use this model to find vulnerabilities in RFID card payment protocols |
|
(NDSS - 2019)
|
Collaboration with Seoul National University -- Hyunwoo Lee, Junghwan Lim, Gyeongjae Choi, Selin Chun, Taejoong Chung and Ted Taekyoung Kwon. Despite TLS being a 2-party protocol, in real-world deployments it is frequently used to bridge multiple agents together. This results in insecure practices by creators of so-called 'middleboxes'. We propose a scheme for implementing a multi-party version of TLS, with relevant security properties and a discussion of some of the previous proposals |
|
(ESORICS - 2019)
|
Collaboration with Ihor Filimonov, Ross Horne and Sjouke Mauw at the University of Luxembourg. A security property known as 'unlinkability', despite being informally understood for some time, possesses several different definitions that are seen as broadly equivalent. We show that a new approach for checking process equivalence, which is faithful to the original definitions of unlinkability, gives surprising results when applied to an RFID protocol used by passports that is traditionally assumed to be secure |
|
(S&P - 2018)
|
Work with Sjouke Mauw, Jorge Toro-Pozo and Rolando Trujillo-Rasua at the University of Luxembourg. Distance Bounding protocols are communication protocols with a unique requirement -- physical proximity between participants, usually measured by ping. Modelling these within a mathematical framework which would prefer to abstract details such as location is thus a challenge. We develop such a framework -- and use it to model all of the major protocols in the literature |
|
(ESORICS - 2018)
|
Work with Sjouke Mauw, Jorge Toro-Pozo and Rolando Trujillo-Rasua at the University of Luxembourg. Rolling key updates are used as a mechanism in certain protocols -- never re-using an encryption key is a simple way to prevent replay attacks, especially in devices with limitated cryptographic capability. However, this leads to new attacks in which the adversary can trick participants into desynchronisation; a state in which they can no longer communicate, because their views of the shared state are no longer compatible. We build a framework for defining these protocols and their security |