IKEv2的实现及形式语言逻辑分析

发布时间：2021-07-29 16:48

　　因特网密钥交换（Internet Key Exchange IKE）协议是IPSec（IP Security）协议簇的重要组成部分，负责动态协商和管理安全联盟。由于IKE协议的复杂性，导致它存在很多问题。所以提出IKEv2作为IKE协议的替代者，目的在于简化协议，并解决IKE中存在的问题。 论文首先简要介绍了IKE协议，并分析了IKE协议中存在的安全缺陷，然后详细介绍了IKEv2协议。IKEv2作为一个密码协议，安全性是非常重要的。论文中使用一种形式化的方法——WK逻辑对IKEv2协议的安全性进行分析。在使用WK逻辑的过程中发现逻辑的有些语法存在问题，针对这些问题提出一些改进意见。根据对IKEv2的分析，论文中提出一种协议的实现方案，并介绍了方案中各部分的主要功能和实现方法。在论文的最后是关于IKEv2协议的一些扩展功能，这些扩展功能是为了满足不同环境下的使用要求而提出来的，论文中对扩展功能的基本原理及如何在IKEv2中的实现做了介绍，并提出一种方法协商即将过期的IKE SA。 

【文章来源】：西安电子科技大学陕西省 211工程院校 教育部直属院校

【文章页数】：68 页

【学位级别】：硕士

【文章目录】：
第一章 绪论
第二章 IKE协议简介
    2.1 IKE和密码协议中的基本概念
        2.1.1 安全联盟(SA)
        2.1.2 协商阶段和模式
        2.1.3 认证方法
        2.1.4 Diffie-Hellman交换
        2.1.5 密码协议
    2.2 协议描述使用的符号
    2.3 密钥生成
    2.4 第一阶段交换
        2.4.1 使用数字签名的验证方法
        2.4.2 使用公钥加密的验证方法
        2.4.3 使用改进的公钥加密的验证方法
        2.4.4 使用预共享密钥的认证方法
    2.5 第二阶段交换
    2.6 新群模式
    2.7 ISAKMP信息交换
第三章 IKE协议缺陷分析
    3.1 不能抵御DoS攻击
    3.2 存在中间人攻击
        3.2.1 修改协商提案的中间人攻击
        3.2.2 修改身份标识符的中间人攻击
    3.3 关于身份保护
    3.4 小结
第四章 IKEv2协议简介
    4.1 初始交换(The Initial Exchange)
        4.1.1 初始交换过程
        4.1.2 IKE SA中密钥的计算
        4.1.3 AUTH载荷的计算
    4.2 产生子SA交换(The CREATE_CHILD_SA Exchange)
        4.2.1 CREATE_CHILD_SA交换过程
        4.2.2 CHILD SA中密钥的计算
    4.3 信息交换(INFORMATIONAL Exchange)
        4.3.1 INFORMATIONAL交换过程
        4.3.2 删除SAs的INFORMATIOANL交换过程
    4.4 IKEv2保证协议可靠的措施
        4.4.1 超时重传和Message ID的作用
        4.4.2 错误处理
    4.5 使用Cookie防御DoS攻击
第五章 IKEv2协议的形式语言分析
    5.1 BAN逻辑
        5.1.1 BAN逻辑的介绍
        5.1.2 扩展的BAN逻辑
    5.2 WK逻辑
        5.2.1 语法
        5.2.2 公理和推理规则
        5.2.3 分析步骤
    5.3 IKEv2的WK逻辑分析
        5.3.1 协议处理
        5.3.2 前提条件
        5.3.3 目标
        5.3.4 证明
第六章 IKEv2协议的实现
    6.1 总体框架
    6.2 IKE管理服务模块
    6.3 消息和事件处理模块
        6.3.1 管理消息处理子模块
        6.3.2 网络消息处理子模块
        6.3.3 时钟事件处理子模块
    6.4 IKE状态库
    6.5 IKE交换消息处理模块
第七章 IKEv2扩展功能
    7.1 重新协商SA(Rekey)
    7.2 IP载荷压缩(IPComp)
    7.3 NAT Traversal
        7.3.1 NAT的原理
        7.3.2 NAT和IPSec之间的不兼容
        7.3.3 支持NAT Traversal的IKEv2
    7.4 扩展认证(Extended Authentication)
    7.5 获得内部IP地址
    7.6 小结
第八章 结论
致谢
参考文献
作者在读期间的研究成果
附录A


【参考文献】：
期刊论文
[1]一种改进的适用于空间网络的密钥交互协议[J]. 张亚航,庞波,程博文.  航天器工程. 2011(04)

硕士论文
[1]TD-SCDMA Femto基站鉴权与加密过程的研究与实现[D]. 林忠杰.华南理工大学 2011
[2]JFK协议的研究及改进[D]. 黄欣.南昌大学 2009
[3]IKEv2协议安全机制的研究和实现[D]. 权乐.解放军信息工程大学 2007
[4]IKE/IKEv2的安全性分析及实现[D]. 章春宇.河海大学 2007
[5]快速密钥交换协议JFK的改进与实现[D]. 林鹏.重庆大学 2006



本文编号：3309691