计算机科学与探索 ›› 2008, Vol. 2 ›› Issue (1): 104-109.

• 学术研究 • 上一篇    下一篇

认证测试方法的改进及应用

陈力琼1+,陈 贤2   

  1. 1. 上海交通大学 计算机科学与工程系,上海 200240
    2. 西安电子科技大学 通信工程系,西安 710071
  • 收稿日期:1900-01-01 修回日期:1900-01-01 出版日期:2008-02-20 发布日期:2008-02-20
  • 通讯作者: 陈力琼

Improvement and application of authentication test

CHEN Liqiong1+, CHEN Xian2   

  1. 1. Department of Computer Science and Engineering, Shanghai Jiao Tong University, Shanghai 200240, China
    2. Department of Communication Engineering, Xidian University, Xi’an 710071, China
  • Received:1900-01-01 Revised:1900-01-01 Online:2008-02-20 Published:2008-02-20
  • Contact: CHEN Liqiong

摘要: 基于串空间模型的认证测试方法被证明是一种分析认证协议的有效工具,为了使之适用于类型更多、规模更大的安全协议,并提高其在协议的认证性、可达性、机密性、非否认性、会话密钥的新鲜性及主体间的关联度上的分析能力,对原有的认证测试方法进行改进,充分利用消息格式,细化分析步骤,增添相关符号以分析复杂协议的更多安全特性。利用该方法能缩减模型检测自动化工具的搜索范围,在解决空间爆炸问题的同时有效地找到多方协议的具体攻击路径,而且它对安全协议的设计和验证也具有一定的指导作用。

关键词: 串空间, 认证测试, 主体关联度, 模型检测

Abstract: Authentication test was proved to be an effective tool of protocol analysis based on strand space. In order to make it to be suitable for analyzing more kinds of protocols and their authentication, security, freshness, non-repudiation and correspondence of principals, authentication test can be improved by making full use of the format of message, fining the procedure of analysis and adding more symbols to represent more goals of security. This improved authentication test combining with model checking automatic tools can solve the problem of space explosion and find detailed attacks as well. It also provides guidance for the design and validation of the protocols.

Key words: strand space, authentication test, correspondence of principals, model checking