Relation between Unification Problem and Intruder Deduction Problem
Pascal Lafourcade · 2008
Intruder deduction problem constitutes the first step in cryptographic protocols verification for a passive intruder. In the case of an active intruder, we know that undecidability of the unification problem implies undecidability of the secrecy problem. In this paper, we analyze the link between the unification problem and the intruder deduction problem. Through examples using equational theories, we show that these two problems are not linked. We present situations where one problem is decidable and the other one is not, or the both are decidable or not. All these examples prove that the two problems are independent for a passive intruder.