基于认证测试的一种安全协议一致性分析方法

认证测试^1]技术是串空间（strand space）理论的进一步发展，不仅用于认证协议的安全性分析而且还用于指导认证协议的设计^2]。但在分析安全协议为何不正确以及如何改进方面，与其他的形式化验证方法一样，也不能提供更深入有效的分析。本文提出了参数一致性矩阵的概念并运用参数一致性矩阵对协议的一致性进行分析，说明了协议失败的原因并给出改进的方向。分析过程的形式化有利于协议分析自动化工具的实现。

An Agreement Analysis Method of Security Protocol Based on Authentication Test

Authentication Test is the further development of strand space, it can be used not only for analyzing protocols, but also for guiding the design of protocol. However in the aspect of why a protocol is incorrect and how to improve it,Authentication Test can not offer deeper and more effective analysis as other formal methods. This paper put forward the concept of the parameter-agreement-matrix, carry on deep analysis to the agreement property of protocol, well solve this problem. In addition, the formal process make protocol analysis automatically.