Abstract: In view of the deficiency of no specific formal construction rules for authentication test theory on the construction of test component, according to the characteristics of the roles which protocol principal plays in the authentication test of some message, along with the role and nature of the message components which contain the message coming from the only one source in the test, message components are reclassified and defined，as well the concept of authentication test model is proposed on the basis of message components’ new classification and new definition, and then the propositions for the property of principals’ keys on the construction of authentication test components are given based on authentication test model. The correctness proof for these propositions is carried on by using basis theory of authentication test at the same time, thus the formal rules which can be applied to the construction of authentication test components are determined.

Key words: security protocol, formal analysis method, strand space model, authentication test, message component；authentication test component

摘要： 针对认证测试理论在测试组件构造方面缺少具体形式化构造规则的不足，根据协议主体在认证测试中的角色特点，以及包含惟一源发消息的消息组件在认证测试中的作用和性质，对消息组件进行分类和定义并提出认证测试模型的概念，基于认证测试模型给出协议主体密钥在测试组件构造上的性质命题，同时运用认证测试基础理论对命题进行正确性证明，从而确定测试组件构造的形式化规则。

关键词: 安全协议, 形式化分析方法, 串空间模型, 认证测试, 消息组件, 测试组件