《计算机应用研究》|Application Research of Computers

一种基于通道的AVISPA扩展方法研究

Extension of AVISPA based on concept of channels

免费全文下载 (已被下载 次)  
获取PDF全文
作者 刘威,郭渊博
机构 解放军信息工程大学 a.网络空间安全学院;b.数学工程与先进计算国家重点实验室,郑州 450001
统计 摘要被查看 次,已被下载
文章编号 1001-3695(2013)12-3783-03
DOI 10.3969/j.issn.1001-3695.2013.12.068
摘要 针对AVISPA工具在分析某些消息需要依靠具有特定属性的信道传递的安全协议或服务中存在的问题, 提出了一种基于抽象通道的扩展方法。抽象通道具有相关的安全性质保证如认证性, 能够对提供安全性质保证的底层服务建模, 并基于密码机制和标签等实现了抽象通道。利用扩展后的AVISPA工具分析有无消息源认证机制的Diffie-Hellman密钥交换协议的安全性, 表明了方法的有效性, 并且能够简化协议建模过程和增强AVISPA工具协议描述分析能力。
关键词 安全协议;形式化分析;安全属性;抽象通道
基金项目 国家部委基金资助项目(9140C130103120C13062)
本文URL http://www.arocmag.com/article/01-2013-12-068.html
英文标题 Extension of AVISPA based on concept of channels
作者英文名 LIU Wei, GUO Yuan-bo
机构英文名 a. Institute of Cyberspace Security, b. State Key Laboratory of Mathematical Engineering & Advanced Computing, PLA Information Engineering University, Zhengzhou 450001, China
英文摘要 For the transmission of some of protocol messages relies on channels with particular security properties, this paper proposed an extension of AVISPA based on abstract channels. It supplied security guarantees such as authentication by abstract channels, and with which it could model the underlying services providing security guarantees. It realized abstract channels with cryptography schemes and labels, and validated the model by verifying Diffie-Hellman key exchange protocol with message origin authentication using extended AVISPA automatically. The extension can simplify protocol modeling and enhance the power of the mechanized tool AVISPA.
英文关键词 security protocols; formal analysis; security properties; abstract channels
参考文献 查看稿件参考文献
  [1] VIGANO L. Automated security protocol analysis with the AVISPA tool[J] . Electronic Notes in Theoretical Computer Science, 2006, 155:61-86.
[2] ARMANDO A, BASIN D, BOICHUT Y, et al. The AVISPA tool for the automated validation of Internet security protocols and applications[C] //Lecture Notes in Computer Science, vol 3576. Berlin:Springer-Verlag, 2005:281-285.
[3] DOLEV D, YAO A C. On the security of public-key protocols[J] . IEEE Trans on Information Theory, 1983, 29(2):198-208.
[4] BRADNER S, MANKIN A, SCHILLER J. A framework for purpose-built keys (PBK)[EB/OL] . [2013-01-20] . http://tools. ietf. org/search/draft-bradner-pbk-frame-06.
[5] The AVISPA Team. The HLPSL tutorial:a beginner's guide to mode-ling and analysing Internet security protocols[EB/OL] . [2013-01-20] . http://www. avispa-project. org.
[6] The AVISPA Team. AVISPA v1. 1 user manual[EB/OL] . [2013-01-20] . http://www. avispa-project. org.
[7] DILLOWAY C, LOWE G. On the specification of secure channels[C] //Proc of the 7th International Workshop on Issues in the Theory of Security. 2007:118-123.
[8] CERVESATO I, JAGGARD A D, SCEDROV A, et al. Breaking and fixing public-key Kerberos[J] . Information and Computation, 2008, 206(2-4):402-424.
[9] 冯超, 张权, 唐朝京. 计算可靠的Diffie-Hellman密钥交换协议自动证明[J] . 通信学报, 2011, 32(10):118-121.
[10] 徐恒, 陈恭亮, 杨福祥. 密钥交换中中间人攻击的防范[J] . 信息安全与通信保密, 2009(2):90-92.
收稿日期
修回日期
页码 3783-3785,3803
中图分类号 TP393
文献标志码 A