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

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