My time in the Computer Science department at Oxford has been focussed on understanding the state-of-the-art in the automated verification of stateful security protocols. Stateful security protocols are those where at least some of the participants must retain a certain amount of "state" to ensure the desired security properties hold. This state often takes the form of a counter, or fixing the identities of other participants with some cryptographic material (such as a public key), and can often prevent attackers from performing otherwise trivial attacks. Historically, automated verification of security protocols has avoided these cases, since they are harder to model and verify than stateless protocols.
My work so far has been two-fold:
- Comprehending the internal model used by Tamarin (a multiset term rewriting system, designed around the verification of security protocols), especially around its modelling of "injective facts" - those facts which cannot be replicated and therefore stolen by the attacker, which are traditionally used to model a participant storing state.
- Understanding why extensions such as SAPIC (built-upon Tamarin and designed especially for stateful protocols) are necessary and exploring whether they can be fully integrated into Tamarin.
My academic career began with discovering and exploring Computer Science at Durham University (2006-2009). There I focussed on the theoretical side of CS - particularly complexity theory and algorithms, writing a thesis with Stefan Dantchev that explored the practical implications of the then recent work of Reingold and his proof of undirected ST-connectivity being L-complete, with some side interests of AI, logic, and knowledge representation.
I left Durham and took a job in the civil service, where I had completed a internship during the previous summer and found the challenges equally intriguing. There I took on several different roles, often involving some form of software engineering expertise. I was fortunate as they could fund me to do a part-time MSc at the University of Bristol (2010-2012), where I explored Data Mining and Machine Learning, and my thesis with Peter Flach was on the use of subgroup discovery (a form of ML algorithm that sits in-between classification and association rule learning) in a distributed MapReduce environment. After six years with the civil service, I found my interest waning and non-managerial opportunities inexistent, and as such as I decided to leave, and make my way back into the arms of academia.
I was fortunate enough to find the CDT in Cyber Security here at the University of Oxford, which offered the practical motivation that I often felt the more theoretical elements of CS lacked, whilst still providing an intellectual challenge. During my first taught year of the CDT, I rediscovered my interest in formal modelling and verification, especially within the context of computer security protocols, an area I developed some expertise with during my time as a civil servant. And thus, I started my DPhil with Cas Cremers as my supervisor, working on the formal verification of security protocols.