Verifying Security of Web Service Configurations
Karthik Bhargavan

In this talk I discuss vulnerabilities in distributed systems built using the emerging specifications for web services security. I will then present formal languages and automated tools for modelling and verifying the security of specific web service deployments and of general classes of web service configurations.

XML Web Services provide a flexible API for building distributed systems as a collection of endpoints that can send and receive SOAP messages. These systems are secured using message-based cryptographic mechanisms defined in a series of specifications developed by Microsoft, IBM, and others. Such home-grown security protocols often go wrong; they are prone to a well-known class of attacks, formalized by Dolev and Yao, where an attacker can intercept, modify, and replay messages. The vulnerability is only increased by the flexible message formats and complex trust configurations allowed by the standards. Our goal is to verify the security of families of protocol configurations, such as those deployed for Microsoft's WSE and Indigo web services implementations.

I will begin the talk by describing a few simple configurations and discuss subtle attacks we have found using our tools. I will then present a language, TulaFale, for modelling SOAP security protocols, and show how we use Blanchet's protocol analyzer for verifying them. I will describe a formal language for modelling web service security configurations, and demonstrate a tool that can automatically generate and analyze security policy deployments for web services written using WSE. This is the first tool we know of that can automatically analyze cryptographic configurations to find real errors and demonstrable attacks. I will end by extending the correctness results to families of configurations. This work was done as part of the Samoa Project with C. Fournet and A.D. Gordon, with contributions from R. Puccella and R. Corin.