DocumentCode :
2173130
Title :
Verified interoperable implementations of security protocols
Author :
Bhargavan, Karthikeyan ; Fournet, Cedric ; Gordon, Andrew D. ; Tse, Stephen
Author_Institution :
Microsoft Res., Microsoft Corp., Redmond, WA
fYear :
0
fDate :
0-0 0
Lastpage :
152
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
Keywords :
cryptography; formal verification; program debugging; protocols; F# language; ProVerif; Web services security; cryptographic algorithms; cryptographic protocols; formal verification; interoperability testing; production testing; resolution-based theorem prover; security protocols; verified interoperable implementations; Concrete; Cryptographic protocols; Cryptography; Debugging; Libraries; Production systems; Security; Testing; Web services; Writing;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Computer Security Foundations Workshop, 2006. 19th IEEE
Conference_Location :
Venice
ISSN :
1063-6900
Print_ISBN :
0-7695-2615-2
Type :
conf
DOI :
10.1109/CSFW.2006.32
Filename :
1648714
Link To Document :
بازگشت