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

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

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

陈力琼¹⁺,陈贤²

1. 上海交通大学计算机科学与工程系，上海 200240
2. 西安电子科技大学通信工程系，西安 710071

收稿日期:1900-01-01 修回日期:1900-01-01 出版日期:2008-02-20 发布日期:2008-02-20
通讯作者: 陈力琼

Improvement and application of authentication test

CHEN Liqiong¹⁺, CHEN Xian²

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

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

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

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

陈力琼1+ ,陈贤2 . 认证测试方法的改进及应用[J]. 计算机科学与探索, 2008, 2(1): 104-109.

CHEN Liqiong¹⁺, CHEN Xian². Improvement and application of authentication test[J]. Journal of Frontiers of Computer Science and Technology, 2008, 2(1): 104-109.

[1]	魏杰林，袁申，李永明，梁常建. 具有DP的广义可能性模糊时态CTL模型检测[J]. 计算机科学与探索, 2019, 13(10): 1781-1792.
[2]	祝义，黄志球，周航. 采用函数式语言的BPEL模型形式化验证方法[J]. 计算机科学与探索, 2018, 12(2): 185-196.
[3]	朱晔，袁红娟，钱俊彦，潘海玉. 模糊交互时态逻辑的一些标记[J]. 计算机科学与探索, 2018, 12(12): 2033-2040.
[4]	鱼先锋，李超，李永明. 直觉模糊测度的计算树逻辑[J]. 计算机科学与探索, 2017, 11(9): 1523-1530.
[5]	赵杰，李永明. 广义可能性计算树逻辑的两种范式[J]. 计算机科学与探索, 2016, 10(10): 1475-1481.
[6]	余鹏，魏欧，韩兰胜，牛耘. 模型检测网络传播干预策略[J]. 计算机科学与探索, 2014, 8(8): 906-918.