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. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Basin, D., Mödersheim, S., & Viganò, L. (2005). Algebraic intruder deductions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3835 LNAI, pp. 549–564). https://doi.org/10.1007/11591191_38
Mendeley helps you to discover research relevant for your work.