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

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

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