Verifying policy-based security for web services

WS-SecurityPolicy is a declarative configuration language for driving web services security mechanisms. We describe a formal sefor WS-SecurityPolicy, and propose a more abstract link language for specifying the security goals of web services and their clients. Hence, we present the architecture and implementation of fully automatic 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, as we can verify policies when first compiled from link specifications, and also reverify policies against their original goals after any modifications during deployment. Categories and Subject Descriptors: F.3.2 [The...

• Type: Conference
• Year: 2004
• Where: CCS
• Authors: Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon
• Keywords: Abstract Link Language, CCS 2004, Link Specifications, Security Privacy, Web Services