Name : Graham Steel

Institution : INRIA project 'SECSI', Laboratoire Specification et Verification, Ecole Normale Superieure de Cachan


Graham Steel holds a degree in Mathematics form the University of Cambridge and a PhD in Automated Reasoning from the University of Edinburgh. His thesis concerned the analysis of group key management protocols, which are short programs used to securely exchange cryptographic key material over an insecure network. His work lead to the discovery of several previously unknown security flaws in existing designs, and the development of a novel tool for finding counterexamples to inductive conjectures in first order logic, the formal language he used to model the protocols and the network intruder.


After completing his thesis, Graham held post-doctoral research positions in Germany, Italy, Scotland and France. At the universities of Karlsruhe (Germany) and Genoa (Italy), he worked on EU projects in algebraic deduction and security protocols analysis, while on returning to the University of Edinburgh (Scotland), he studied the analysis of security of APIs for cryptographic modules used in the cash machine network. This work produced new tools and new vulnerabilities, results which lead to both scientific publications and, more recently, coverage in the popular press, including an interview for the Wired magazine `Threat Level' blog.


Graham then moved to the Specification and Verification Laboratory (LSV) at the ENS-Cachan for a further post-doc studying the analysis of key management APIs. He was ranked first in the INRIA competitive selection for full-time research fellows, and took up his position in September 2008. His recent work has included the discovery of a family of flaws in the RSA PKCS#11 standard API, widely used in cryptographic USB security tokens and smartcards. This work was published at the IEEE Computer Security Foundations Symposium in 2008. Again these flaws were found by the application of formal tools. A paper to appear at the security conference ESORICS in September 2009 gives an alternative design for an API for these devices for which formal security properties have been proved.


When not working, Graham enjoys running, playing football, working on his foreign languages, and eating in small out-of-the-way Parisian bistros.


Publications :


G. Steel. Formal analysis of PIN block attacks. Theoretical Computer Science, 367(1-2) :257-270, November 2006.


S. Delaune, S. Kremer, and G. Steel. Formal analysis of PKCS#11. In Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF21), pages 331-344, Pittsburgh, PA, USA, June 2008.




Trustworthy Endpoints for the Next Generation Internet


The Next Generation Internet will be composed of heterogeneous devices - not just computers, PDAs and mobile  phones, but smart tags, wearable computing, and embedded devices in vehicles, roadside units, and buildings. This presents tremendous opportunities for new applications, both optimising our use of existing infrastructure, and offering new possibilities for previously unimagined services. However, given the security problems of the Internet as we know it, we know we will have to design for security from the start. The threat models and countermeasures for these new scenarios are in a state of flux, but one point is clear : the Next Generation Internet will require a greater degree of endpoint security, i.e. integrity of networked devices, and integrity of the software they are running, in order to provide a secure platform for the envisaged applications. Proposed solutions typically leverage a tamper-resistant device that contains some secure storage, and is capable of basic cryptographic operations. However,

designing the security-critical API by which the trusted device communicates with the untrusted, possibly malicious application code, and in particular, combining this with the protocols by which the devices will communicate in a secure application, is known to be extremely difficult to get right. The aim of my research project is to develop reasoning techniques and tools for the development of trustworthy endpoints for the Next Generation Internet. This will involve reasoning about the design of APIs for a new generation of tamper proof devices, and inferring the required properties of these APIs from the protocols they are supposed to securely implement.