Internet的应用己从军事、科研与学术领域进入商业、传播和娱乐等领域,成为发展最快的传播媒介。然而许多企业的局域网与Internet互联带来了重大的安全问题,虚拟专用网(VirtualPrivate Network,VPN)技术能够很好地解决这一安全问题,虚拟专用网技术是指在公共网络中建立专用网络,数据通过安全的“加密通道”在公共网络中传播的技术。IPSec(IP Security协议)是构建VPN的主流协议之一,它是IETF组织为在IP层提供安全通信而制定的网络安全标准,是一个与IP协议栈紧密结合的安全协议族,能为IP及其上层协议提供安全保证。两台计算机在交换数据之前必须首先建立安全关联SA(Secruity Association),就双方需要如何保护信息、如何交换信息等公用的安全设置达成一致。因特网密钥交换(IKE,Internet Key Exchange)协议是IPSec协议簇的重要组成部分。目前,IKE已经成为IPSec实现中首选的密钥交换协议。它负责动态协商、身份验证和管理安全关联。IKE协议的安全性决定了通信双方协商的共享密钥的可靠性以及通信的安全性。然而由于它是一种混合型的协议,其自身的复杂性不可避免带来一些缺陷,导致它在安全性、效率和实现方面都存在很多问题。近年来,对IKE协议的分析和改进己成为网络安全领域的一个研究热点。所以提出IKEv2协议和JFK(Just Fast Keying)协议作为IKE协议的替代协议,目的在于简化协议,并尽量解决IKE中存在的问题。从实用和简便的角度,JFK协议比IKE协议更加安全、高效和简单。然而无论是基础版本IKEv1还是改进版本IKEv2及JFK,都还存在着很多漏洞和安全问题。本文首先介绍DoS攻击。在其基础上,引出分布式的拒绝服务攻击(DDoS)。DDOS是近年来出现的一种特殊形式的拒绝服务(DoS)攻击。它采用了分布、协作的大规模攻击方式。DDoS攻击和普通DoS的攻击原理是一样的,但是与早期的DoS攻击由单台攻击发起,单兵作战相比较,DDoS实现是借助数百台,甚至数千台被植入攻击守护进程的攻击主机同时发起的集团作战行为。主要目标是较大的站点,像商业公司、搜索引擎和政府部门的站点。由于DDoS攻击拥有更多攻击源,破坏力更大,因此检测和防御工作也更加困难。DDoS攻击已经严重威胁Internet的安全,成为目前网络安全界研究的热点。其次介绍了IKE协议的结构及原理,研究了密钥交换协议IKEv1、IKEv2及JFK的工作机制,重点介绍了基于预共享密钥认证的IKEv1主模式协议的认证和协商机制,并阐述了IKEv2针对IKEv1存在的问题做出的改进。然后简要介绍了BAN类逻辑形式化的逻辑分析方法,说明了逻辑方法在密钥安全性分析上的重要性。在对SVO逻辑的分析研究中发现了SVO逻辑形式化证明复杂密钥交换协议的缺陷和不足,针对SVO逻辑的这些缺陷和不足,本文对其进行了必要的修改和扩展,使其逻辑关系更为严格,同时重新定义了一种新的适用于分析复杂密钥交换协议的形式化验证方法——SVO+逻辑。接着再利用改进的SVO+逻辑分析了IKEv1、IKEv2及JFK协议存在的安全问题,通过实例分析验证,SVO+逻辑是实用和有效的。本文重点针对现有密钥交换协议在保护通信双方身份信息和防御DDoS攻击方面的不足,提出了基于可信任第三方的辅助认证下实现的新型密钥交换协议,称为TKE(Trusted KeyExchange可信任密钥交换协议)。在文中较为详细地定义了可信任密钥交换协议要达到的安全预期目标、协议的消息格式和报文的具体内容以及交换方式等,并对提出的可信任密钥交换协议进行了可行性及安全性论证:同时利用SVO+逻辑形式化语言分析证明了该TKE协议除了能达到密钥交换协议所要求的一般安全目标外还能有效地保护双方通信实体的身份信息和防御DDoS攻击,因此达到了密钥交换协议TKE设计的预期目的。