密码学报ISSN2095．7025CN10一1195厂rNE-mail：jcr@eacmet．org．cnJournalofCryptologicResearch，2014，1(6)：568-577http：／／www．jcr．cacmetorg．crl@《密码学报》编辑部版权所有．Te汗ax：+86—10—8103310l安全协议形式化分析工具比较研究木陆思奇1,2，程庆丰1,2，赵进华31．洛阳外国语学院，洛阳4710032．中国科学院信息工程研究所，信息安全国家重点实验室，北京1000933．信息保障技术重点实验室，北京100072通讯作者：程庆丰，E-mail：qingfengc2008@sina．com摘要：形式化分析方法已经成为协议分析的主流方法之一．目前，国内针对形式化分析工具的研究很少，工具之间的比较研究也不够充分．一方面，当前比较研究存在参比工具较少以及参比性能不全面的问题，另一方面，大部分比较研究仅停留在理论比较，并没有提供实验数据．因此，本文首先对AVISPA、ProVerif、Maude．NPA、Scyther、Tamarin等当前主流形式化分析工具的背景、5-具性能、应用范围等方面进行介绍，然后以SSH协议为目标协议，利用不同的形式化工具对SSH协议进行分析．根据实验分析结果，对比研究工具在运行性能、运行效率、底层算法、使用界面、安全模型等方面的优势和劣势．在对比研究结果的基础上，从形式化分析5．-具的使用和开发两方面进行讨论：在工具使用方面，通过工具比较研究，用户可以根据目标协议特性挑选合适的工具，对协议实现准确高效的分析；在工具开发方面，通过工具比较研究，指出代数性质扩展以及状态空间的限制和搜索算法是当前工具性能提升的重点和难点，突出了工具开发者需要掌握的用户需求，为工具开发提供理论基础．关键词：形式化分析工具；比较研究；SSH协议：安全模型中图法分类号：TN918．1文献标识码：ADOI：10．13868／j．cnki．jcr．000052中文引用格式：陆思奇，程庆丰，赵进华．安全协议形式化分析工具比较研究【J】．密码学报，2014，1(6)：568—577．英文引用格式：LuSQ，ChengQF，ZhaoJH．Comparisonstudyofformalverificationtoolsforsecurityprotocols[J】JournalofCryptologicResearch，2014，1(6)：568-577．ComparisonStudyofFormalVerificationToolsforSecurityProtocolsLUSi—Qil”，CHENGQing-Fen91，一，ZHAOJin．Hua31．LuoyangUniversityofForeignLanguages，Luoyang471003，China2．StateKeyLaboratoryofInformationSecurity，InstituteofInformationEngineering，ChineseAcademyofSciences，Beijing100093，China3．ScienceandTechnologyonInformationAssuranceLaboratory，Beijing100072，ChinaCorrespondingauthor：CHENGQing·Feng，E·mail：qingfengc2008@sina．comAbstract：Theformalmethodforveillyingsecurityprotocolshasbeenoneofthemostpopularmethodsofprotocolverification．Uptonow,verylittleworkhasbeenpublishedonformalverificationtools，andthe·基金项目：信息保障技术重点实验室开放基金(U一13—109)；信息安全国家重点实验室资助开放课题(2014—11)---本文来源于网络，仅供参考，勿照抄，如有侵权请联系删除---陆思奇等：安全协议形式化分析工具比较研究569comparisonstudyofthetoolsisnotenough．Ononehand,Sincethecurrentexistingcomparisonstudyisnotcomprehensive，andontheotherhand，mostofthecomparisonsarelackofexperimentaldata．Thispaperf'n'stbrieflyintroducessomepopulartools，includingAVISPA、ProVerif、Maude—NPA、Scyther、TamarinandSOon，includingtheirbackground,effectiveness，andareaofapplications，thentheSSHprotocolisverifiedbythesetoolsandtheresultsarecompared，SOthatacomprehensivecomparisonstudy，includingthetoolfeatures，efficiency,underlyingalgorithm，userinterfaceandthesecuritymodels，ispresented．Basedonthiscomparisonstudy,wediscussboththeapplicationanddesignofformalverificationtools．Ononehand,userscanchoosetheappropriatetoolaccordingtothetargetprotocol，makingtheuseofthetoolsmoreaccurateandeffective．Ontheotherhand，wefindthatthee...