loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
19th IEEE Computer Security Foundations Workshop (CSFW'06)
Verified Interoperable Implementations of Security Protocols
Venice, Italy
July 05-July 07
ISBN: 0-7695-2615-2
ASCII Text
x 
 
Karthikeyan Bhargavan, Cedric Fournet, Andrew D. Gordon, Stephen Tse, "Verified Interoperable Implementations of Security Protocols," Computer Security Foundations Workshop, IEEE, pp. 139-152, 19th IEEE Computer Security Foundations Workshop (CSFW'06), 2006.
 
 
BibTex
x
 
@article{ 10.1109/CSFW.2006.32,
author = {Karthikeyan Bhargavan and Cedric Fournet and Andrew D. Gordon and Stephen Tse},
title = {Verified Interoperable Implementations of Security Protocols},
journal ={Computer Security Foundations Workshop, IEEE},
volume = {0},
year = {2006},
issn = {1063-6900},
pages = {139-152},
doi = {http://doi.ieeecomputersociety.org/10.1109/CSFW.2006.32},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Computer Security Foundations Workshop, IEEE
TI - Verified Interoperable Implementations of Security Protocols
SN - 1063-6900
SP139
EP152
A1 - Karthikeyan Bhargavan,
A1 - Cedric Fournet,
A1 - Andrew D. Gordon,
A1 - Stephen Tse,
PY - 2006
KW - null
VL - 0
JA - Computer Security Foundations Workshop, IEEE
ER -
 
Karthikeyan Bhargavan, Microsoft Research, USA
Cedric Fournet, Microsoft Research, USA
Andrew D. Gordon, Microsoft Research, USA
Stephen Tse, University of Pennsylvania, USA
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.
Citation:
Karthikeyan Bhargavan, Cedric Fournet, Andrew D. Gordon, Stephen Tse, "Verified Interoperable Implementations of Security Protocols," csfw, pp.139-152, 19th IEEE Computer Security Foundations Workshop (CSFW'06), 2006
Usage of this product signifies your acceptance of the Terms of Use.