国防科学技术大学计算机学院410073

【摘要】形式化方法是分析和验证安全协议的有效手段。AVISPA工具集是一套建立和分析安全协议模型的形式化自动分析工具，结合SPAN可以对安全协议进行直观而全面的分析并得出结论。本文通过将CAS+规范引入到AVISPA工具集中来对协议进行安全性的分析，利用AVISPA分析发现，使用CAS+规范可以更加直观、简便地对协议进行形式化语言建模，快速准确的推导出分析结果和入侵者轨迹。
【关键词】：安全协议  AVISPA  CAS+  SPAN  
One Formal Analysis Method for Security Protocol based on AVISPA
Xin Zhang, Yongjun Wang, Shaojing Fu
National University of Defense Technology 410073
Abstract：The formal methods have been proved to be the analysis and verification of the effective means of security protocols. AVISPA is a set of formalized automatic analysis tool for building and analyzing security protocols. In this paper, we introduce the CAS+ specification to the AVISPA tool sets for security protocol analysis. By combined with AVISPA tool sets, we can find a fact. With CAS+ specification, it is more intuitive and easier to model with formal language, faster to see the intruder trajectory and to deduce accurate results.
Key words: security protocol  AVISPA  CAS+  SPAN

参考文献
[1]薛锐,冯登国．安全协议的形式化分析技术与方法[J]．计算机学报．2006(29)：1-20
[2]冯登国,范红．安全协议形式化分析理论与方法研究综述[J]．中国科学院研究生院学报. 2003.12(4)：389-406．
[3]李建华.网络安全协议的形式化分析与验证[M].北京：机械工业出版社.2010.3:14-18.
[4]王聪,刘军,王孝国,于振伟. 安全协议原理与验证[M].北京：北京邮电大学出版社.2011.8:3-13.
[5]徐梦茗,肖聪,唐六华,黄金涛.安全协议和网络攻击分析[J]．信息安全与通信保密．2007(2)：50-54
[6] AVISPA Team. AVISPA V1.0 User Manual．European Community under the Information Society Technologies Program．(2005-10-1)．http：//www.avispa-project.org.
[7]徐梦茗,肖聪,李斌.安全协议形式化分析的研究和实现[J]．信息安全与通信保密．2008(8)：76-78
[8]徐梦茗,李斌,肖聪. 怎样用好AVISPA工具[J].信息安全与通信保密. 2009(8) :155-158
[9] The AVISPA team. AVISPA v1.1 user Manual. Document Version: 1.1.June 30, 2006
[10] Yann GLOUCHE,Thomas GENET,Erwan HOUSSAY.SPAN：a security Protocol Animator for AVISPA. 2008.9
[11] CAS+, Ronan Saillard and Thomas Genet, March 21, 2011
[12 ]卫剑钒,陈钟. 安全协议分析与设计[M]. 北京：人民邮电出版社.2010.11:30-31

作者简介：
张鑫，女，1988生，河南南阳人，在读工程硕士，
项目来源于教育部高等学校博士学科点专项科研基金资助课题，NO20124307110014。