loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
14th IEEE Computer Security Foundations Workshop (CSFW'01)
An Efficient Cryptographic Protocol Verifier Based on Prolog Rules
Cape Breton, Novia Scotia, Canada
June 11-June 13
ISBN: 0-7695-1146-5
ASCII Text
x 
 
Bruno Blanchet, "An Efficient Cryptographic Protocol Verifier Based on Prolog Rules," Computer Security Foundations Workshop, IEEE, pp. 0082, 14th IEEE Computer Security Foundations Workshop (CSFW'01), 2001.
 
 
BibTex
x
 
@article{ 10.1109/CSFW.2001.930138,
author = {Bruno Blanchet},
title = {An Efficient Cryptographic Protocol Verifier Based on Prolog Rules},
journal ={Computer Security Foundations Workshop, IEEE},
volume = {0},
year = {2001},
isbn = {0-7695-1146-5},
pages = {0082},
doi = {http://doi.ieeecomputersociety.org/10.1109/CSFW.2001.930138},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Computer Security Foundations Workshop, IEEE
TI - An Efficient Cryptographic Protocol Verifier Based on Prolog Rules
SN - 0-7695-1146-5
SP
EP
A1 - Bruno Blanchet,
PY - 2001
VL - 0
JA - Computer Security Foundations Workshop, IEEE
ER -
 
Bruno Blanchet, INRIA Rocquencourt
Abstract: We present a new automatic cryptographic protocol verifier based on a simple representation of the protocol by Prolog rules, and on a new efficient algorithm that determines whether a fact can be proved from these rules or not. This verifier proves secrecy properties of the protocols. Thanks to its use of unification, it avoids the problem of the state space explosion. Another advantage is that we do not need to limit the number of runs of the protocol to analyze it. We have proved the correctness of our algorithm, and have implemented it. The experimental results show that many examples of protocols of the literature, including Skeme [24], can be analyzed by our tool with very small resources: the analysis takes from less than 0.1 s for simple protocols to 23 s for the main mode of Skeme. It uses less than 2 Mb of memory in our tests.
Citation:
Bruno Blanchet, "An Efficient Cryptographic Protocol Verifier Based on Prolog Rules," csfw, pp.0082, 14th IEEE Computer Security Foundations Workshop (CSFW'01), 2001
Usage of this product signifies your acceptance of the Terms of Use.