Abstract: In view of the problem of higher complexity and lower automation which lies in the basic theory of authentication test, generates for the lack of judgment rules used in the consistence analysis on the strands parameters of protocol principals, through formalizing the structure of message component, as well as analyzing the common grounds on the structure of authentication test, the formal modeling for the structure of authentication test is made based on the basic theory of authentication test. Upon the authentication test model, by using the construction rules in the keys of protocol principals, the analysis is carried on the conditions which need to be met when the strands of protocol principals keep consistence on different types of parameter, as the judgment rules existing in the consistence of the strand parameters are found, the formal method used in the consistence analysis on the strand parameters of the protocol principals is gave out. Analyzing practice of protocols indicates that the method is more concise and more effective, easier to be automated, compared to hypothetical deduction method, and can provide the corresponding correction scheme for the flaws which it accurately locates.

Key words: security protocol, formal analysis method, strand space model, authentication test, strand parameters

摘要： 针对认证测试基础理论在协议主体串参数一致性分析方面，因形式化判定规则不足所产生的分析复杂度较高和自动化程度较低问题，通过对消息组件结构的形式化，以及认证测试结构的共性分析，基于认证测试基础理论对认证测试结构进行形式化建模；在认证测试结构模型上，运用协议主体密钥的认证测试构造规则，分析协议主体串在不同类型参数上满足一致性的条件，在明确参数一致性判定规则的同时，给出协议主体串参数一致性分析的形式化方法。协议分析实践表明，该方法较传统方法不仅具有简洁高效、易于自动化实现的优点，而且能够准确定位协议缺陷并给出相应的修正方案。

关键词: 安全协议, 形式化分析, 串空间模型, 认证测试, 串参数