Easy Intruder Deductions

摘要

We investigate extensions of the Dolev-Yao model of a passive intruder into a cryptographic protocol by some algebraic properties of cryptographic primitives. We provide sufficient conditions under which the intruder deduction problem is decidable in polynomial time. We apply this result to the equational theory of homomorphism, and show that in this case the intruder deduction problem is linear, provided that the messages are in normal form.