计算机工程 ›› 2010, Vol. 36 ›› Issue (2): 144-146.doi: 10.3969/j.issn.1000-3428.2010.02.051

• 安全技术 • 上一篇    下一篇

TA4SP的认证性扩展

朱文也,祝跃飞,刘 楠,陈 晨   

  1. (信息工程大学信息工程学院,郑州 450002)
  • 收稿日期:1900-01-01 修回日期:1900-01-01 出版日期:2010-01-20 发布日期:2010-01-20

Certification Expansion of TA4SP

ZHU Wen-ye, ZHU Yue-fei, LIU Nan, CHEN Chen   

  1. (College of Information Engineering, Information Engineering University, Zhengzhou 450002)
  • Received:1900-01-01 Revised:1900-01-01 Online:2010-01-20 Published:2010-01-20

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

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

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

中图分类号: