Home News About Us Contact Contributors Disclaimer Privacy Policy Help FAQ

Home
Search
Quick Search
Advanced
Fulltext
Browse
Collections
Persons
My eDoc
Session History
Login
Name:
Password:
Documentation
Help
Support Wiki
Direct access to
document ID:


          Institute: MPI für Informatik     Collection: Static Analysis Group     Display Documents



ID: 520663.0, MPI für Informatik / Static Analysis Group
Verification of Cryptographic Protocols: Tagging Enforces Termination
Authors:Blanchet, Bruno; Podelski, Andreas
Language:English
Date of Publication (YYYY-MM-DD):2005
Title of Journal:Theoretical Computer Science
Volume:333
Issue / Number:1-2
Start Page:67
End Page:90
Review Status:Peer-review
Audience:Experts Only
Intended Educational Use:No
Abstract / Description:We investigate a resolution-based verification method for
secrecy and authentication properties of cryptographic protocols.
In experiments, 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.
Last Change of the Resource (YYYY-MM-DD):2005-05-01
External Publication Status:published
Document Type:Article
Communicated by:to be appointed
Affiliations:MPI für Informatik/Static Analysis Group
Identifiers:LOCALID:C1256BDD001D715B-493A49D4190D93BCC1256FB00051F267-...
URL:http://dx.doi.org/10.1016/j.tcs.2004.10.018
ISSN:0304-3975
The scope and number of records on eDoc is subject to the collection policies defined by each institute - see "info" button in the collection browse view.