Verifying Policy-Based Web Services Security

WS-SecurityPolicy is a declarative language for configuring web services security mechanisms. The authors describe a formal semantics for WS-SecurityPolicy and propose a more abstract language for specifying secure links between web services and their clients. They present the architecture and implementation of tools that compile policy files from link specifications, and verify by invoking a theorem prover whether a set of policy files run by any number of senders and receivers correctly implements the goals of a link specification, in spite of active attackers. Policy-driven web services implementations are prone to the usual subtle vulnerabilities associated with cryptographic protocols; their tools help prevent such vulnerabilities.