A New Algorithm for Solving the Intruder Deduction Problem

The intruder deduction problem is the key of formal analysis of crytographical protocol. Because many security protocols are based on the algebraic properties of original operation, so it must analyze the problem under the equational theory which is inducted by the set of equations that expressed the algebraic properties, then it becomes more difficult. A new algorithm for solving the intruder deduction problem which under the Dolev-Yao model is given, it is based on two ideas, one is dividing the equational theory into finite equivalence theory and cancellation equivalence theory, another is choosing representative element. The algorithm is same with most protocols, reduces the complexity of basic algorithm which adopted in usual. The result has been verified in related task.