中文摘要：

协议安全是确保网络数据安全的基础。传统的基于观察的人工分析协议安全性分析已不能满足安全需求。如何研究安全协议及安全属性的性质，使两者在统一框架下实现可分析和验证是亟待解决的问题，形式化分析为解决这一问题提供了精确的数学手段和强大的分析工具。对已有的安全协议形式化分析方法进行了归纳和总结，并从等价验证、协议优化和增强分析准确度三方面提出了未来的研究设想。

英文摘要：

Protocol security is the foundation for ensuring of network data security. Traditional methods based on manual analysis could no longer meet the requirements of data security. How to research, analyze and verify the security protocol and its security properties in the same formal framework is now a problem demanding prompt solution. Formal analysis provides an exact mathematical method and automatic tool for solving this peoblem. In this paper, the existing formal analysis methods for security protocol are reviewed and summarized. In addition, the future researches in the three fields of equivalence verification, protocol optimization, and accuracy enhancement are also suggested.