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.

We propose a new specification language for writing machine-checkable descriptions of SOAP-based security protocol configurations and their properties. Our TulaFale language is based on the pi calculus (for writing collections of SOAP processors running in parallel), plus XML syntax (to express SOAP messaging), logical predicates (to construct and filter SOAP messages), and correspondence assertions (to specify authentication goals of protocols). Our implementation compiles TulaFale into the applied pi calculus, and then runs Blanchet’s resolution-based protocol verifier. The TulaFale implementation is available for download.

We also describe a high-level link language for describing security configurations, and demonstrate a tool that can automatically generate and analyze executable 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.

Download pdf Verifying Web Services Security Configurations