TulaFale A Security Tool for Web Services.pdfVIP

TulaFale: A Security Tool for Web Services Karthikeyan Bhargavan, C´edric Fournet, Andrew D. Gordon, and Riccardo Pucella Microsoft Research 4 0 0 2 Abstract. Web services security specifications are typically expressed c as a mixture of XML schemas, example messages, and narrative expla- e nations. We propose a new specification language for writing comple- D mentary machine-checkable descriptions of SOAP-based security pro- tocols and their properties. Our TulaFale language is based on the pi 0 1 calculus (for writing collections of SOAP processors running in paral- lel), plus XML syntax (to express SOAP messaging), logical predicates ] (to construct and filter SOAP messages), and correspondence assertions R (to specify authentication goals of protocols). Our implementation com- C piles TulaFale into the applied pi calculus, and then runs Blanchet’s . resolution-based protocol verifier. Hence, we can automatically verify s authentication properties of SOAP protocols. c [ 1 1 Verifying Web Services Security v 4 4 Web services are a wide-area distributed systems technology, based on asyn- 0 chronous exchanges of XML messages conforming to the SOAP message for- 2 mat [BEK+00,W3C03]. The WS-Sec