Algebraic Intruder Deductions

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

• Type: Conference
• Year: 2005
• Where: LPAR
• Authors: David A. Basin, Sebastian Mödersheim, Luca Viganò
• Keywords: Algebraic Properties, Cryptographic Operators, LPAR 2005, Security Protocol