Computer Science – Cryptography and Security
Scientific paper
2004-12-10
Computer Science
Cryptography and Security
26 pages, 4 figures. Appears in Proceedings of the 2nd International Symposium on Formal Methods for Components and Objects (F
Scientific paper
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.
Bhargavan Karthikeyan
Fournet Cedric
Gordon Andrew D.
Pucella Riccardo
No associations
LandOfFree
TulaFale: A Security Tool for Web Services does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with TulaFale: A Security Tool for Web Services, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and TulaFale: A Security Tool for Web Services will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-263516