Abstract: Certification is important properties of security protocols, but Tree Automata based on Automatic Approximation for the Analysis of Security Protocols(TA4SP) can not detect certification of security protocols. To solove the above problem, this paper proposes a certification detection method for TA4SP. Based on the analysis of TA4SP, the method introduces the hierarchical certification, and achieves the expanding of certification for TA4SP. The method is a clear structure and easy to foamal. Examples show that the adoption of impoved method can detect certification of security protocols effectively.

Key words: TA4SP system, Term Rewriting System(TRS), tree automata, certification

摘要： 认证性是安全协议检测的重要特性之一，但TA4SP自动协议证明器无法对安全协议的认证性进行检测。针对该问题，提出一种TA4SP的认证性检测方法。该方法基于对TA4SP设计原理的分析，采用分层认证思想，实现对其认证性的理论扩展，其结构清晰、易于形式化。实例表明，通过该方法改进后的TA4SP能有效检测安全协议的认证性。

关键词: TA4SP系统, 项重写系统, 树自动机, 认证性

CLC Number: 

• TP309