BlanchetCSFW01

Bruno Blanchet Back to publications

Bruno Blanchet. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In 14th IEEE Computer Security Foundations Workshop (CSFW-14), pages 82-96, Cape Breton, Nova Scotia, Canada, June 2001. IEEE Computer Society. This paper received a test of time award at the CSF'23 conference.

Copyright

© 2001 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

If you accept this copyright notice, you can get the paper:

Get the paper

.ps.gz, 78 Kb

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, 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.

Bibtex


@INPROCEEDINGS{BlanchetCSFW01,
  AUTHOR = {Bruno Blanchet},
  TITLE = {An {E}fficient {C}ryptographic {P}rotocol {V}erifier {B}ased on {P}rolog {R}ules},
  BOOKTITLE = {14th IEEE Computer Security Foundations Workshop (CSFW-14)},
  PAGES = {82--96},
  YEAR = 2001,
  ADDRESS = {Cape Breton, Nova Scotia, Canada},
  MONTH = JUN,
  PUBLISHER = {IEEE Computer Society},
  NOTE = {This paper received a {\bf test of time award} at the CSF'23 conference}
}

E-mail/Courrier électronique : Bruno.Blanchet@trap-inria.fr (remove trap-)