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.
cryptographical protocol formal analysis algebraic properties equational theory
Chen Chen Chen Weihong
Institute of Information Engineering, Information Engineering University, Zhengzhou 450002, China
国际会议
重庆
英文
825-828
2009-12-25(万方平台首次上网日期,不代表论文的发表时间)