Skip to main content


There is an increasing variety of computer security research at Oxford, bridging Theory and Automated Verification and Software Engineering. Lowe and Roscoe continue to refine their seminal protocol analysis and verification techniques, which are now capable of verifying or refuting most protocols very rapidly using FDR in conjunction with front ends to support protocol notations, including SOAP. This work has been further expanded by Cremers' arrival. We also work in protocol development and information flow analysis. Achievements include discovery of attacks and other flaws in many protocols, including several which were standardised or at advanced stages of standardisation, such as ISO/IEC 9798, ISO/IEC 11770, and Webservice SecureConversation. Our protocol analysis tools, Casper and Cremers' Scyther, have become widely used in industry and international research. Roscoe's group developed a new family of protocols for bootstrapping ad-hoc networks, leading to three patent applications. Cremers' work includes further tool development including the Tamarin prover, as well as bridging the gap between symbolic analysis tools and computational/cryptographic analysis of protocols. Ker has recently proved a fundamental new result: that steganographic capacity grows as N0.5 rather than linearly.




Past Members

Selected Publications

View All