國防科學技術大學計算機學院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。