本文介绍了安全协议的基本概念和安全协议的安全性;研究了安全协议逻辑分析方法的途径和技术的发展历程;介绍了安全协议形式化分析的三种思路;AVISPA是一个用于自动验证安全协议的工具。我们介绍了高级协议规范语言和中间格式,分析了AVISPA工具的整体结构,特别深入研究了AVISPA的后台OFMC.我们用AVISPA,分析了H.530协议