形式化分析方法已经成为协议分析的主流方法之一.目前,国内针对形式化分析工具的研究很少,工具之间的比较研究也不够充分.一方面,当前比较研究存在参比工具较少以及参比性能不全面的问题,另一方面,大部分比较研究仅停留在理论比较,并没有提供实验数据.因此,本文首先对AVISPA、Pro Verif、Maude-NPA、Scyther、Tamarin等当前主流形式化分析工具的背景、工具性能、应用范围等方面进行介绍,然后以SSH协议为目标协议,利用不同的形式化工具对SSH协议进行分析.根据实验分析结果,对比研究工具在运行性能、运行效率、底层算法、使用界面、安全模型等方面的优势和劣势.在对比研究结果的基础上,从形式化分析工具的使用和开发两方面进行讨论:在工具使用方面,通过工具比较研究,用户可以根据目标协议特性挑选合适的工具,对协议实现准确高效的分析;在工具开发方面,通过工具比较研究,指出代数性质扩展以及状态空间的限制和搜索算法是当前工具性能提升的重点和难点,突出了工具开发者需要掌握的用户需求,为工具开发提供理论基础.