基于攻击者和秘密的安全协议验证算法的研究与实现

网络的普及便得网络安全问题日益重要，协议的安全性和密码算法的安全性是网络数据安全的两个最基本的概念。本文介绍了几种有代表性的安全协议的形式化验证工具，研究并使用了JAVA语言实现了基于攻击者和秘密的安全协议验证算法。我们提出了身份验证协议必须交换秘密的概念，还为协议的形式化验证过程设计了框架。框架是指针对攻击者和其冒充的角色对原安全协议的改造。我们实现的验证工具是证伪的，即如果攻击者能够成功冒充某主体，则该安全协议是有漏洞的，反之则该协议的安全性得到某种程度的保证。本文还给出了该算法的攻击实例，并且对以后的研究工作进行了展望。

RESEARCH ON FORMAL AUTHENTICATION ALGORITHM BASED ON INTRUDER AND SECURITY

Protocol security and algorithm security are two fundamental aspects of network data security. In this paper we introduce some classical formal authentication tools of security protocol, and we have implemented an authentication algorithm of security protocol based on intruder and security using JAVA. We raised an important idea that an authentication protocol must exchange some secrets. We also constructed frame for the process of protocol authentication. Frame is an alteration of a security protocol based on the idea of the intruder and the role he is pretending. The authentication tool implements a falsification job, that is, if the intruder can successfully impersonate another legal principal of the protocol, then we can make a decision that the security protocol is not safe, if contrarily, then the security of the protocol is guaranteed to some certain degree. We finally presented an instance of the algorithm, and made some expectation of the future work in this area.