形式化验证认证协议的研究

The Research of Using Formal Methods to Verify Authentication Protocols

认证协议设计和实现的安全性分析是网络安全的重要课题，越来越多的人关注这个方向的发展。在此系统地讨论了认证协议形式验证研究的前沿课题和发展趋势，并介绍了基于时序逻辑的认证协议研究成果和基于时序逻辑的ModelChecking的构想。

It is impoTtpni to analyze autheniication protocols of designing and implement by formal methods in network security,more andmore people resoarch it.This paper presents a general approach for analysis and verification of authentication properties using the theory offormal methods.We attompt to outline some of major threads of research in the area and else to document some emerging treads.Also weintroduced our research in verifying authentication protocols using temporal logic,and Provided our plan about model checking.