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

Abstract

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)
Pages139-152
Number of pages14
ISBN (Print)0-7695-2615-2
DOIs
Publication statusPublished - 2006

Fingerprint

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

Cite this