Physicien théorique de formation, il obtient son doctorant sur la gravité quantique à Queen Mary College l'Université de Londres, et intègre le GCHQ. Rapidement fasciné par les protocoles cryptographiques, mais critique des approches principalement basées sur la logique BAN alors répandues, il lance l’application de l'algèbre des processus à la sécurité. Un projet avec Oxford et Royal Holloway démontre vite l'efficacité de ces outils, en particulier menant à la découverte par Gavin Lowe de d’une célèbre attaque sur le protocole Needham-Schoeder. Un autre sujet sur lequel il a beaucoup travaillé est la caractérisation des flux d'information. Il est, en particulier, l’auteur de la première formulation d'algèbre de processus de "non-interférence" caractérisant l'absence d'information sur interface dans un cadre non-déterministe.
Depuis 2004, il a été fasciné par la sécurisation des élections, ce qui a conduit au développement, avec l'aide de ses collègues, d'un certain nombre de schémas vérifiables : Pret à Voter, Pretty Good Democracy, OpenVote et plus récemment Selene.
Plus récemment, il a étudié l'assurance quantique, en particulier les protocoles d’établissement de clés authentifiés. Son intérêt s'est également étendu aux aspects humains de l'assurance de l'information: comment les humains peuvent contribuer ou compromettre la sécurité et la robustesse d'un système sociotechnique (dont les systèmes de vote sont un excellent exemple).
