BlanchetPodelskiFOSSACS03

Bruno Blanchet Back to publications

Bruno Blanchet and Andreas Podelski. Verification of Cryptographic Protocols: Tagging Enforces Termination. In Andrew Gordon, editor, Foundations of Software Science and Computation Structures (FoSSaCS'03), volume 2620 of Lecture Notes in Computer Science, pages 136-152, Warsaw, Poland, April 2003. Springer.

Copyright

Get the paper

.ps.gz, 87 Kb

Links

LNCS series home page. LNCS Volume 2620 at Springer.

Slides of the talk.

Abstract

In experiments with a resolution-based verification method for cryptographic protocols, we could enforce its termination by tagging, a syntactic transformation of messages that leaves attack-free executions invariant. In this paper, we generalize the experimental evidence: we prove that the verification method always terminates for tagged protocols.

Bibtex


@INPROCEEDINGS{BlanchetPodelskiFOSSACS03,
  AUTHOR = {Bruno Blanchet and Andreas Podelski},
  TITLE = {Verification of Cryptographic Protocols: Tagging Enforces Termination},
  BOOKTITLE = {Foundations of Software Science and Computation Structures (FoSSaCS'03)},
  PAGES = {136--152},
  YEAR = 2003,
  EDITOR = {Andrew Gordon},
  VOLUME = 2620,
  SERIES = {Lecture Notes in Computer Science},
  ADDRESS = {Warsaw, Poland},
  MONTH = APR,
  PUBLISHER = {Springer}
}

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