NB I have moved to the Laboratoire Spécification et Vérification at ENS-Cachan near Paris to take up a permanent position as an INRIA chargé de recherche. I have a homepage there.

From October 2004 to September 2007, I was engaged on the EPSRC-funded project "Automated Analysis of Security Critical Systems". The project involved applying formal tools to the problem of analysing the APIs of hardware security modules. These devices are used, for example, in ATM (cash machine) networks and electronic payment systems. The final report and assessment by EPSRC are available.

From July 2006 to January 2007, I carried out a security review of ATM Software for KAL, with part funding from the Scottish Executive's SCORE scheme.

My PhD work concerned the automated discovery of cryptographic security protocol attacks by refutation of inductive conjectures. This lead to the development of the Coral system, and the discovery of several previously unknown attacks on group protocols.

I previously worked at the Università degli Studi di Genova, and the Universität Karlsruhe.