Verifying policy-based web services security

Karthikeyan Bhargavan, Cedric Fournet, Andrew D. Gordon

Research output: Contribution to journalArticlepeer-review


WS-SecurityPolicy is a declarative language for configuring web services security mechanisms. We describe a formal semantics for WS-SecurityPolicy and propose a more abstract language for specifying secure links between web services and their clients. We present the architecture and implementation of tools that (1) compile policy files from link specifications, and (2) 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; our tools help prevent such vulnerabilities. We can verify policies when first compiled from link specifications, and also re-verify policies against their original goals after any modifications during deployment. Moreover, we present general security theorems for all configurations that rely on compiled policies.
Original languageEnglish
Article number30
Number of pages59
JournalACM Letters on Programming Languages and Systems
Issue number6
Publication statusPublished - Oct 2008


Dive into the research topics of 'Verifying policy-based web services security'. Together they form a unique fingerprint.

Cite this