IKE的分析及其基于CPK的改进

论文摘要

在众多的安全协议中,IPSec是因特网的基础协议,IPSec是IPv6中负责数据通信安全的部分,而IKE又是IPSec协议簇的重要内容,负责密钥的协商和管理。因此对IKE的安全性进行分析不仅具有理论意义,而且具有实用价值。鉴于IKE的重要性,论文的主要工作是对其进行的分析和改进。首先,对各种协议分析方法作了比较,并选择逻辑化方法作为分析工具。而后对逻辑化方法作了改进——增加和修改了若干公理,并证明了新的定理。其次,用逻辑化方法详细地分析了IKE(IKEv1和IKEv2)的安全性——对IKEv1第一阶段主模式的三种认证模式(预共享密钥模式、数字签名模式、公钥加密模式)、第二阶段的快速模式和IKEv2都进行了详细的形式化分析。分析表明,IKEv1和IKEv2协议都是安全的。同时,也指出了IKE在效率方面的弱点。最后,为了提高IKE的效率,给出了基于CPK的IKE的改进方案。CPK的用户公钥由用户名来确定,证书与用户名之间存在一一对应关系。由于私钥是面对面分发,或由单位统一申请、分发,是一种直接的信任关系,可信度较高。而且,用户公钥的确认除了查询黑名单列表时需要访问中心外,其它的验证只需用户有本地主机上作一次查表即可,因而效率较之原协议有明显的提高。此外,逻辑化分析也表明,改进的协议具有较高的安全性。诚然,IPSec有其自身的优势——更好的开放性。所以,我们的方案并不是要完全取代IPSec协议。一般而言,在无边界的开放网络中,更适合用现有的IPSec协议。但在封闭的网络,如军事网、电子政务网中,我们方案则具有明显的优势。

论文目录

• 目录
• 表目录
• 摘要
• ABSTRACT
• 第一章 概论
• 1.1 引言
• 1.2 协议的若干基本概念
• 1.2.1 协议和协议的分类
• 1.2.2 通信协议及其分类
• 1.2.3 安全协议及其安全性
• 1.3 IPSEC协议简介
• 1.3.1 IPSec的框架
• 1.3.2 IPSec的主要内容
• 1.3.3 IPSec的简要评述及其研究意义
• 1.4 协议安全性研究概述
• 1.4.1 协议安全性分析的几种基本途径
• 1.4.2 串空间方法
• 1.4.3 逻辑化方法
• 1.4.4 串空间方法与逻辑化方法的比较
• 1.5 本文的主要内容及成果
• 第二章 SPALL方法及其改进
• 2.1 SPALL方法的产生背景——BAN类逻辑概述
• 2.2 SPALL方法的若干概念和符号
• 2.2.1 若干基本概念和记号
• 2.2.2 消息及其相关概念
• 2.2.3 公式及其相关概念
• 2.2.4 其它符号和公式
• 2.3 SPALL系统的公理
• 2.3.1 系统公理集
• 2.3.2 系统规则
• 2.4 SPALL系统的定理
• 2.4.1 K的常用定理、由定义或公理直接得到的定理
• 2.4.2 关于集合和BMP的常用定理
• 2.4.3 关于密钥和共享秘密的常用定理
• 2.4.4 关于一阶认证谓词的常用定理
• 2.5 对SPALL系统的一点改进
• 2.5.1 对公理的改进
• 2.5.2 几个新定理及其证明
• 第三章 IKEV1和IKEV2分析
• 3.1 IKEv1简介
• 3.1.1 IKEv1的基本内容
• 3.1.2 IKE协商的两个阶段
• 3.1.3 IKEv1中的若干记号
• 3.2 IKEv1模式的详细介绍
• 3.2.1 几种模式所使用的认证方法
• 3.2.2 阶段1的主模式交换
• 3.2.3 阶段1的野蛮模式交换
• 3.2.4 阶段2的快速模式交换
• 3.3 IKEv1的分析
• 3.3.1 预共享密钥主模式的分析
• 3.3.2 数字签名主模式的分析
• 3.3.3 公钥加密认证主模式的分析
• 3.3.4 快速模式的分析
• 3.4 IKEv2简介与分析
• 3.4.1 IKEv2对于IKEv1主要的改进
• 3.4.2 IKEv2的协商过程
• 3.4.3 密钥的衍生
• 3.4.4 AUTH载荷的产生
• 3.4.5 IKEv2的分析
• 第四章 基于CPK的IPSEC协议的改进及分析
• 4.1 CPK简介
• 4.2 基于CPK的IKE协议改进
• 4.2.1 改进协议的必要性
• 4.2.2 对协议的改进
• 4.3 改进协议的分析
• 4.3.1 协议目标
• 4.3.2 初始假设
• 4.3.3 协议目标的分析
• 第五章 结束语
• 参考文献
• 附录 数理逻辑基础
• 1. 非形式的命题逻辑
• 2. 形式的命题逻辑
• 3. 非形式的谓词逻辑
• 4. 形式的谓词逻辑
• 作者简历 攻读硕士学位期间完成的主要工作
• 致谢