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 Pavlovic's 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 at advanced stages of standardisation, such as GDOI and Webservice SecureConversation. Our protocol analysis tools, Casper and Pavlovic's Protocol Derivation Assistant, 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. Ker has recently proved a fundamental new result: that steganographic capacity grows as N0.5 rather than linearly.
