安全协议形式化自动验证工具AVISPA的研究
发布时间：2021-02-20 10:00
近年来，网络技术的飞速发展给人类带来众多便利的同时也存在着越来越多的网络信息安全问题。据统计，到2010年为止，我国网民总数超过4.2亿，但具有独立网络安全意识的网民不到40%。2012年我国电子商务交易金额有望突破8万亿元，网络购物金额超过4000亿元。2013年美国提交的2014年国防预算草案中，网络安全经费大幅增至47亿，用来拦截来自他国的网络攻击。网络信息安全不仅关系着个人信息安全还关系着国家安全。为了保证网络信息安全，用建立在复杂密码体系基础上的安全协议担任网络中的重要通信协议。这些安全的通信协议被应用于广泛的计算机网络和分布式系统中，已经成为电子商务和计算机通信的一个重要环节。但是，虽然这些安全协议使用了加密算法，但不能保证网络一直处于安全状态，只要黑客找到适当的工具，该网络安全协议很快就被攻破，信息很容易被窃取，篡改等受到恶意的破坏。通常采用攻击检验方法和形式化分析方法确保安全协议的安全性。攻击检验方法是基于已知的各种攻击对安全协议进行分析，分析前必须已知各种攻击，但在实际应用中大多数攻击在分析前是不可知的。另一种安全协议分析方法形式化分析在分析前不需要已知攻击，因此形式...
【文章来源】：吉林大学吉林省 211工程院校 985工程院校 教育部直属院校
【文章页数】：47 页
【学位级别】：硕士
【部分图文】：
丫ahalom协议交互过程图
26图 4-2 Yahalom 协议的协议模拟4.2.3 Yahalom 协议的攻击模拟运行 AVISPA 安全协议自动化验证工具对 Yahalom.hlpsl 分析验证，其中Yahalom.hlpsl，是上述的协议描述文件。通过 OFMC 分析终端对 Yahalom 协议的分析，得出了此协议是不安全的结论并给出攻击的轨迹如图 4-3 所示：
27图 4-3 结论及攻击轨迹攻击轨迹：1. i -> (b，3): a.x2532. (b,3) -> i: b.{a.x253.Nb(1)}_kbs3. i -> (s,3): b.{a.x253.Nb(1)}_kbs4. (s,3) -> i: {b.Kab(2).x253.Nb(1)}_kas.{a.Kab(2)}_kbs5. i -> (s,7): b.{a.x253.Nb(1)}_kbs6. (s,7) -> i: {b.Kab(3).x253.Nb(1)}_kas.{a.Kab(3)}_kbs攻击者 Intruder 最先冒充 B 为 I(B)，接收原本 A 发给 B 的消息，导致 B 接收不到需要消息，然后攻击者又冒充 B 把从 A 获得的消息发送给 S。在整个过程
【参考文献】：
期刊论文
[1]安全协议形式化分析的研究和实现[J]. 徐梦茗,肖聪,李斌,杜彪. 信息安全与通信保密. 2008(08)
[2]Efficient Protocol-Proving Algorithm Based on Improved Authentication Tests[J]. 李谢华,杨树堂,李建华,诸鸿文. Journal of Shanghai Jiaotong University. 2007(01)
[3]安全协议和网络攻击分析[J]. 徐梦茗,肖聪,唐六华,黄金涛. 信息安全与通信保密. 2007(02)
[4]串空间理论在网络安全协议形式化分析中应用[J]. 孙海波,林东岱,黄寄洪. 大连理工大学学报. 2003(S1)
[5]安全协议形式化分析理论与方法研究综述[J]. 冯登国,范红. 中国科学院研究生院学报. 2003(04)
[6]基于串空间的安全协议形式化验证模型及算法[J]. 周宏斌,黄连生,桑田. 计算机研究与发展. 2003(02)
[7]认证协议的一些新攻击方法[J]. 王贵林,卿斯汉,周展飞. 软件学报. 2001(06)
博士论文
[1]安全协议代数证明方法研究[D]. 李援.合肥工业大学 2007
硕士论文
[1]密码协议符号分析方法的计算可靠性研究[D]. 朱玉娜.解放军信息工程大学 2008
[2]无线传感器网络安全定向扩散路由协议研究[D]. 赵浩浩.武汉理工大学 2008
本文编号：3042608
【文章来源】：吉林大学吉林省 211工程院校 985工程院校 教育部直属院校
【文章页数】：47 页
【学位级别】：硕士
【部分图文】：
丫ahalom协议交互过程图
26图 4-2 Yahalom 协议的协议模拟4.2.3 Yahalom 协议的攻击模拟运行 AVISPA 安全协议自动化验证工具对 Yahalom.hlpsl 分析验证，其中Yahalom.hlpsl，是上述的协议描述文件。通过 OFMC 分析终端对 Yahalom 协议的分析，得出了此协议是不安全的结论并给出攻击的轨迹如图 4-3 所示：
27图 4-3 结论及攻击轨迹攻击轨迹：1. i -> (b，3): a.x2532. (b,3) -> i: b.{a.x253.Nb(1)}_kbs3. i -> (s,3): b.{a.x253.Nb(1)}_kbs4. (s,3) -> i: {b.Kab(2).x253.Nb(1)}_kas.{a.Kab(2)}_kbs5. i -> (s,7): b.{a.x253.Nb(1)}_kbs6. (s,7) -> i: {b.Kab(3).x253.Nb(1)}_kas.{a.Kab(3)}_kbs攻击者 Intruder 最先冒充 B 为 I(B)，接收原本 A 发给 B 的消息，导致 B 接收不到需要消息，然后攻击者又冒充 B 把从 A 获得的消息发送给 S。在整个过程
【参考文献】：
期刊论文
[1]安全协议形式化分析的研究和实现[J]. 徐梦茗,肖聪,李斌,杜彪. 信息安全与通信保密. 2008(08)
[2]Efficient Protocol-Proving Algorithm Based on Improved Authentication Tests[J]. 李谢华,杨树堂,李建华,诸鸿文. Journal of Shanghai Jiaotong University. 2007(01)
[3]安全协议和网络攻击分析[J]. 徐梦茗,肖聪,唐六华,黄金涛. 信息安全与通信保密. 2007(02)
[4]串空间理论在网络安全协议形式化分析中应用[J]. 孙海波,林东岱,黄寄洪. 大连理工大学学报. 2003(S1)
[5]安全协议形式化分析理论与方法研究综述[J]. 冯登国,范红. 中国科学院研究生院学报. 2003(04)
[6]基于串空间的安全协议形式化验证模型及算法[J]. 周宏斌,黄连生,桑田. 计算机研究与发展. 2003(02)
[7]认证协议的一些新攻击方法[J]. 王贵林,卿斯汉,周展飞. 软件学报. 2001(06)
博士论文
[1]安全协议代数证明方法研究[D]. 李援.合肥工业大学 2007
硕士论文
[1]密码协议符号分析方法的计算可靠性研究[D]. 朱玉娜.解放军信息工程大学 2008
[2]无线传感器网络安全定向扩散路由协议研究[D]. 赵浩浩.武汉理工大学 2008
本文编号：3042608
本文链接：https://www.wllwen.com/guanlilunwen/ydhl/3042608.html
