Samoa: Formal Tools for Securing Web Services

Speaker: Andy Gordon

26th January 2006 , 2pm , 701 Claremont Tower

Abstract

Based on joint work with K. Bhargavan and C. Fournet Microsoft Research, Cambridge.

Securing.WS

An XML web service is, to a first approximation, a wide-area RPC service in which requests and responses are encoded in XML as SOAP envelopes, and transported over HTTP. Applications exist on the internet (for programmatic access to search engines and retail), on intranets (for enterprise systems integration), and are emerging between intranets (for the e-science Grid and for e-business). Specifications (such as WS-Security, now standardized at OASIS) and toolkits (such as the Microsoft WSE product) exist for securing web services by applying cryptographic transforms to SOAP envelopes.

The underlying principles, and indeed the difficulties, of using cryptography to secure RPC protocols have been known for many years, and there has been a sustained and successful effort to devise formal methods for specifying and verifying the security goals of such protocols. One line of work, embodied in the spi calculus of Abadi and Gordon and the applied pi calculus of Abadi and Fournet, has been to represent protocols as symbolic processes, and to apply techniques from the theory of the pi calculus, including equational reasoning, type-checking, and resolution theorem-proving, to attempt to verify security properties such as confidentiality and authenticity, or to uncover bugs.

The goal of the Samoa Project is to exploit these recent theoretical advances in the analysis of security protocols in the practical setting of XML web services. This talk will present some of the outcomes of our research, including: automatic analysis of hand-written pi-calculus descriptions of WS-Security protocols; automatic generation of pi-calculus descriptions from WSE config and policy files; and tools to help review the security of WSE installations.