Verified Interoperable Implementations of Security Protocols

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

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


We present an architecture and tools for verifying implementations of security protocols. Our implementations can run with both concrete and symbolic implementations of cryptographic algorithms. The concrete implementation is for production and interoperability testing. The symbolic implementation is for debugging and formal verification. We develop our approach for protocols written in F#, a dialect of ML, and verify them by compilation to ProVerif, a resolution-based theorem prover for cryptographic protocols. We establish the correctness of this compilation scheme, and we illustrate our approach with protocols for Web Services security.
Original languageEnglish
Title of host publication19th IEEE Computer Security Foundations Workshop, (CSFW-19 2006), 5-7 July 2006, Venice, Italy
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Number of pages14
ISBN (Print)0-7695-2615-2
Publication statusPublished - 2006


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

Cite this