TA4SP的认证性扩展  

Certification Expansion of TA4SP

作　　者：朱文也[1] 祝跃飞[1] 刘楠[1] 陈晨[1] 

机构地区：[1]信息工程大学信息工程学院,郑州450002

出　　处：《计算机工程》2010年第2期144-146,共3页Computer Engineering

基　　金：国家"863"计划基金资助项目(2007AA01471)

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

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

分 类 号：TP309[自动化与计算机技术—计算机系统结构]