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
© Springer-Verlag
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-)