Easy intruder deduction problems with homomorphisms

We present complexity results for the verification of security protocols. Since the perfect cryptography assumption is unrealistic for cryptographic primitives with visible algebraic properties, we extend the classical Dolev-Yao model by permitting the intruder to exploit these properties. More precisely, we are interested in theories such as Exclusive or and Abelian groups in combination with the homomorphism axiom. We show that the intruder deduction problem is in PTIME in both cases, improving the EXPTIME complexity results presented in [10]. Key words: automatic theorem proving, formal methods, security protocols

• Type: Journal
• Year: 2006
• Where: IPL
• Authors: Stéphanie Delaune
• Keywords: IPL 2006, Perfect Cryptography Assumption, Security Protocols, Visible Algebraic Properties