TulaFale: A Security Tool for Web Services
Karthikeyan Bhargavan, Cedric Fournet, Andrew D. Gordon, Riccardo, Pucella

TL;DR
TulaFale is a new specification language that enables automatic verification of SOAP-based web service security protocols by combining pi calculus, XML syntax, and logical assertions.
Contribution
It introduces a novel language for specifying and verifying security properties of SOAP protocols, integrating formal methods with XML-based messaging.
Findings
Automated verification of authentication properties for SOAP protocols.
Implementation compiles TulaFale into applied pi calculus for analysis.
Uses Blanchet's verifier to ensure protocol security.
Abstract
Web services security specifications are typically expressed as a mixture of XML schemas, example messages, and narrative explanations. We propose a new specification language for writing complementary machine-checkable descriptions of SOAP-based security protocols 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. Hence, we can automatically verify authentication properties of SOAP protocols.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Authentication Protocols Security · User Authentication and Security Systems · Access Control and Trust
