de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Conference Paper

Verification of Cryptographic Protocols: Tagging Enforces Termination

MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44141

Blanchet,  Bruno
Static Analysis, MPI for Informatics, Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons45201

Podelski,  Andreas
Programming Logics, MPI for Informatics, Max Planck Society;

Locator
There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available
Citation

Blanchet, B., & Podelski, A. (2003). Verification of Cryptographic Protocols: Tagging Enforces Termination. In A. D. Gordon (Ed.), Foundations of software science and computation structures: 6th International Conference, FOSSACS 2003 (pp. 136-152). Berlin, Germany: Springer.


Cite as: http://hdl.handle.net/11858/00-001M-0000-000F-2EA4-E
Abstract
In experiments with a resolution-based verification method for cryptographic protocols, we could enforce its termination by \emph{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.