×

Verified interoperable implementations of security protocols. (English) Zbl 1137.68323

Broy, Manfred (ed.) et al., Software system reliability and security. Proceedings of the NATO Advanced Research Institute on software system reliability and security, Marktoberndorf, Germany, August 1–13, 2006. Amsterdam: IOS Press (ISBN 978-1-58603-731-4/hbk). NATO Security through Science Series. D: Information and Communication Security 9, 87-115 (2007).
Summary: 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.
For the entire collection see [Zbl 1123.68003].

MSC:

68M12 Network protocols
68P25 Data encryption (aspects in computer science)
PDFBibTeX XMLCite