Open access
Date
2005Type
- Report
ETH Bibliography
yes
Altmetrics
Abstract
Many security protocols fundamentally depend on the algebraic properties of cryptographic operators. It is however difficult to handle these properties when formally analyzing protocols, since basic problems like the equality of terms that represent cryptographic messages are undecidable, even for relatively simple algebraic theories. We present a framework for security protocol analysis that can handle algebraic properties of cryptographic operators in a uniform and modular way. Our framework is based on two ideas: the use of modular rewriting to formalize a generalized equational deduction problem for the Dolev- Yao intruder, and the introduction of two parameters that control the complexity of the equational unification problems that arise during protocol analysis by bounding the depth of message terms and the operations that the intruder can perform when analyzing messages.We motivate the different restrictions made in our model by highlighting different ways in which undecidability arises when incorporating algebraic properties of cryptographic operators into formal protocol analysis. Show more
Permanent link
https://doi.org/10.3929/ethz-a-006787620Publication status
publishedJournal / series
Technical Report / ETH Zurich, Department of Computer ScienceVolume
Publisher
ETH, Department of Computer ScienceEdition / version
Extended VersionSubject
NETWORK PROTOCOLS + COMMUNICATION PROTOCOLS (COMPUTER SYSTEMS); CRYPTOGRAPHY (INFORMATION THEORY); NETZWERKPROTOKOLLE + KOMMUNIKATIONSPROTOKOLLE (COMPUTERSYSTEME); KRYPTOGRAPHIE (INFORMATIONSTHEORIE)Organisational unit
02150 - Dep. Informatik / Dep. of Computer Science03634 - Basin, David / Basin, David
Notes
Technical Reports D-INFK.More
Show all metadata
ETH Bibliography
yes
Altmetrics