Verified Reference Implementations of WS-Security Protocols

Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We describe a new reference implementation of the web services security specifications. The implementation is structured as a library in the functional programming language F#. Applications written using this library can interoperate with other compliant web services, such as those written using Microsoft WSE and WCF frameworks. Moreover, the security of such applications can be automatically verified by translating them to the applied pi calculus and using an automated theorem prover. We illustrate the use of our reference implementation through examples drawn from the sample applications included with WSE and WCF. We formally verify their security properties. We also experimentally evaluate their interoperability and performance.
Original languageEnglish
Title of host publicationWeb Services and Formal Methods
Subtitle of host publicationThird International Workshop, WS-FM 2006 Vienna, Austria, September 8-9, 2006, Proceedings
PublisherSpringer Berlin Heidelberg
Number of pages19
ISBN (Electronic) 978-3-540-38865-4
ISBN (Print) 978-3-540-38862-3
Publication statusPublished - 2006


Dive into the research topics of 'Verified Reference Implementations of WS-Security Protocols'. Together they form a unique fingerprint.

Cite this