BlanchetSAS01

Back to ProVerif

Bruno Blanchet. Abstracting Cryptographic Protocols by Prolog Rules (invited talk). In Patrick Cousot, editor, 8th International Static Analysis Symposium (SAS'2001), volume 2126 of Lecture Notes in Computer Science, pages 433-436, Paris, France, July 2001. Springer. Survey

Copyright

Get the paper

.ps.gz, 35 Kb

Links

LNCS series home page. LNCS Volume 2126 at Springer

Abstract

Most current cryptographic protocol verifiers meet the state space explosion problem, and have to limit the number of executions of the considered protocol during the verification. To solve these problems, we introduce an abstract representation of cryptographic protocols, based on Prolog rules, and use it to verify secrecy properties of protocols.

Bibtex


@INPROCEEDINGS{BlanchetSAS01,
  AUTHOR = {Bruno Blanchet},
  TITLE = {Abstracting {C}ryptographic {P}rotocols by {P}rolog {R}ules (invited talk)},
  BOOKTITLE = {8th International Static Analysis Symposium (SAS'2001)},
  PAGES = {433--436},
  YEAR = 2001,
  EDITOR = {Patrick Cousot},
  VOLUME = 2126,
  SERIES = {Lecture Notes in Computer Science},
  ADDRESS = {Paris, France},
  MONTH = JUL,
  PUBLISHER = {Springer}
}