Intruder deduction for AC-like equational theories with homomorphisms. (English) Zbl 1078.68034
Giesl, Jürgen (ed.), Term rewriting and applications. 16th international conference, RTA 2005, Nara, Japan, April 19–21, 2005. Proceedings. Berlin: Springer (ISBN 3-540-25596-6/pbk). Lecture Notes in Computer Science 3467, 308-322 (2005).
Summary: Cryptographic protocols are small programs which involve a high level of concurrency and which are difficult to analyze by hand. The most successful methods to verify such protocols rely on rewriting techniques and automated deduction in order to implement or mimic the process calculus describing the protocol execution.
We focus on the intruder deduction problem, that is the vulnerability to passive attacks, in presence of several variants of AC-like axioms (from AC to abelian groups, including the theory of exclusive or) and homomorphism which are the most frequent axioms arising in cryptographic protocols. Solutions are known for the cases of exclusive or, of abelian groups, and of homomorphism alone. In this paper we address the combination of these AC-like theories with the law of homomorphism which leads to much more complex decision problems.
We prove decidability of the intruder deduction problem in all cases considered. Our decision procedure is in EXPTIME, except for a restricted case in which we have been able to get a PTIME decision procedure using a property of one-counter and pushdown automata.
For the entire collection see [Zbl 1070.68002].
We focus on the intruder deduction problem, that is the vulnerability to passive attacks, in presence of several variants of AC-like axioms (from AC to abelian groups, including the theory of exclusive or) and homomorphism which are the most frequent axioms arising in cryptographic protocols. Solutions are known for the cases of exclusive or, of abelian groups, and of homomorphism alone. In this paper we address the combination of these AC-like theories with the law of homomorphism which leads to much more complex decision problems.
We prove decidability of the intruder deduction problem in all cases considered. Our decision procedure is in EXPTIME, except for a restricted case in which we have been able to get a PTIME decision procedure using a property of one-counter and pushdown automata.
For the entire collection see [Zbl 1070.68002].
MSC:
| 68P25 | Data encryption (aspects in computer science) |
| 68Q42 | Grammars and rewriting systems |
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 94A60 | Cryptography |
