公共无线局域网安全体系研究及其可验安全性形式化分析

论文题目: 公共无线局域网安全体系研究及其可验安全性形式化分析

论文类型: 博士论文

论文专业: 信号与信息处理

作者: 宋宇波

导师: 胡爱群

关键词: 公共无线局域网,安全体系,预言机模型,模型,认证协议,密钥交换,加密机制,形式化分析

文献来源: 东南大学

发表年度: 2005

论文摘要: 公共无线局域网（PWLAN）是目前无线网络技术发展的热点之一,旨在给用户提供随时随地高效率、高质量、低成本的移动接入,其安全性直接影响到公共无线局域网技术的推广应用。如何设计和实现公共无线局域网的安全体系,为其安全协议的设计与分析提供理论指导,从而确保公共无线局域网的安全是目前迫切需要解决的问题。本文采用形式化分析手段,对当前公共无线局域网安全协议的安全性进行证明,并比较不同协议的安全性能,从而为选择合适的安全协议提供依据。为此,本文开展了以下几个方面的研究:1.通过对公共无线局域网现有应用模式和体系结构的分析,将公共无线局域网归纳为:WISP-owned PWLAN、Operator PWLAN以及PWLAN for Enterprise三种类型。在此基础上,提出了一个可以基本满足各种类型公共无线局域网需求的基于接入控制器模式的通用公共无线局域网安全体系结构,给出了该体系设计的合理性分析。2.根据预言机模型,从协议的机密性和可靠性两方面,对WEP、TKIP以及CCMP密码协议进行了精确量化的可验安全性形式化分析;推导出WEP、TKIP和CCMP协议的安全量化函数,该函数采用攻击成功率的优势函数来衡量加密机制的安全性能。分析表明,当攻击RC4算法的成功率为O（n2） * 2-128（密钥长度为128比特）时,WEP的攻击成功率约为O（n2） * 2-24,TKIP的攻击成功率约为O（n3） * 2-48,这两个加密协议都没有达到提供预期的安全强度。3.提出了TKIP算法的一种改进算法。在该算法中把TKIP序列计数器（TSC）值由原来的48比特扩大到128比特,使其安全强度比RC4算法提高了约3个数量级。4.证明了CCMP加密协议的安全性和可靠性。分析表明,当AES算法的攻击成功率为O（n2） * 2-128时,CCMP的可靠性和机密性对应的攻击成功率分别为O（n） * 2-64和O（n2） * 2-128,达到了预期的设计目标,可以满足公共无线局域网的安全需求。5.利用Bellare-Rogoway模型,对密码交换协议进行了可验安全性分析。证明了公共无线局域网采用的四步握手密钥交换机制的保密性和认证正确性;6.提出了一种增强的Bellare-Rogoway模型。采用该模型对802.1X认证协议进行了可验安全性分析,发现了该协议存在安全缺陷,容易遭受中间人攻击。在此基础上提出了一种攻击方法及改进措施。7.设计和实现了符合公共无线局域网技术规范的无线接入点和接入控制器。

论文目录:

摘要

Abstract

主要符号对照表

第一章绪论

1.1 公共无线局域网及其安全

1.2 安全协议的形式化分析

1.3 论文的工作和组织结构

第二章公共无线局域网安全体系结构

2.1 公共无线局域网的架构

2.2 公共无线局域网的安全体系

2.2.1 公共无线局域网安全威胁

2.2.2 安全体系结构

2.2.3 公共无线局域网安全业务

2.2.4 无线局域网安全业务

2.3 公共无线局域网认证架构

2.3.1 IEEE802.11认证

2.3.2 公共无线局域网的多方式认证体系

2.3.3 可信凭证类型

2.3.4 基于WEB方式的认证模型

2.4 公共无线局域网加密架构

2.4.1 802.11加密机制

2.4.2 802.11i/WPA加密机制

2.4.3 IPSEC VPN加密机制

2.5 公共无线局域网密钥管理

第三章形式化可验证安全模型

3.1 形式化可验安全性

3.1.1 计算复杂度

3.1.2 多项式时间不可区分性

3.1.3 预言机(Oracle Machine)

3.1.4 安全性证明的随机预言机模型

3.1.5 精确量化的可验证安全性理论

3.2 PWLAN加密机制的可验安全性分析模型

3.2.1 基本概念

3.2.2 计算模型

3.3 PWLAN认证和密钥交换机制的可验安全性分析模型

3.3.1 密钥交换分析模型－Bellare-Rogaway模型

3.3.1.1 合法用户的形式化

3.3.1.2 密钥交换通信的形式化

3.3.1.3 密钥交换安全目标的形式化

3.3.2 认证协议分析模型－增强的Bellare-Rogaway模型

3.3.2.1 认证参与者的的形式化

3.3.2.2 802.1X协议通信的形式化

3.3.2.3 802.1X协议安全目标的形式化

第四章公共无线局域网加密技术

4.1 WEP算法

4.2 TKIP算法

4.2.1 TKIP加密过程

4.2.2 TKIP解密过程

4.2.3 TKIP MIC函数

4.2.4 TKIP混合函数

4.2.4.1 S-box

4.2.4.2 混合函数第一阶段

4.2.4.3 混合函数第二阶段

4.3 CCMP算法

4.3.1 AES算法

4.3.1.1 AES数学基础

4.3.1.2 AES的基本结构

4.3.2 CCM模式

4.3.2.1 CTR加密模式

4.3.2.2 CBC-MAC模式

4.3.2.3 CCMP密码协议

4.4 加密算法的可验证安全分析

4.4.1 WEP的形式化安全分析

4.4.1.1 数学模型的建立和描述

4.4.1.2 安全性能分析

4.4.2 TKIP协议的形式化安全分析

4.4.2.1 数学模型的建立与描述

4.4.2.2 安全性能分析

4.4.3 WEP,TKIP安全性能比较与分析

4.4.4 TKIP改进算法

4.4.4.1 密钥混合函数设计

4.4.4.2 改进函数安全性能分析

4.4.5 CCMP协议的形式化安全分析

4.4.5.1 数学模型的建立和描述

4.4.5.2 安全性能分析

第五章公共无线局域网认证技术

5.1 IEEE802.1X认证协议

5.1.1 802.1x的体系结构

5.1.2 端口控制原理

5.2 RADIUS协议

5.2.1 RADIUS协议特点

5.2.2 RADIUS服务器的工作过程

5.3 EAP扩展认证协议

5.3.1 EAP协议在802.1x中的应用

5.3.2 EAPOL消息的封装

5.3.2.1 EAPOL数据包的格式

5.3.2.2 EAPOL数据包的格式

5.4 EAP-TLS认证协议

5.4.1 TLS传输层安全协议

5.4.1.1 握手协议

5.4.1.2 记录协议

5.4.2 EAP-TLS认证过程

5.5 EAP-SIM认证协议

5.5.1 SIM卡中的保密算法及密钥

5.5.2 EAP-SIM认证过程

5.6 802.1X协议的可验证安全分析

5.6.1 EAP-TLS协议的形式化分析

5.6.1.1 EAP-TLS协议的形式化描述

5.6.1.2 EAP-TLS协议的形式化分析

5.6.1.3 中间人攻击

5.6.2 802.1X协议的进一步考虑和改进

第六章公共无线局域网密钥管理技术

6.1 802.11i/WPA密钥管理

6.2 密钥层次

6.3 密钥协商机制

6.3.1 四步握手协议

6.3.2 组密钥握手协议

6.4 密钥管理的可验证安全分析

6.4.1 四步握手协议的形式化描述

6.4.2 四步握手协议的形式化分析

第七章公共无线局域网系统关键设备的设计与实现

7.1 无线接入点设计与实现

7.1.1 基于MPC852T的嵌入式系统平台

7.1.2 无线物理层模块

7.1.3 MAC层软件模块

7.1.4 802.1X认证者模块的实现

7.1.5 无线接入点性能测试

7.2 PWLAN接入控制器的研究与实现

第八章论文总结与展望

8.1 论文总结

8.2 改进与展望

参考文献

个人简历、在学期间的研究成果及发表的论文

发布时间: 2007-06-11

参考文献

[1].IEEE 802.11无线局域网媒质接入控制技术研究[D]. 刘吉龙.西安电子科技大学2016
[2].大规模无线局域网性能优化的关键技术研究[D]. 王浩.武汉大学2013
[3].公用无线局域网关键技术的研究[D]. 赵力强.西安电子科技大学2003
[4].低密度校验码与无线局域网研究[D]. 徐志江.浙江大学2004
[5].分布式无线局域网的自适应MAC技术研究[D]. 严少虎.电子科技大学2005
[6].无线局域网MAC层的准入控制与调度机制的研究[D]. 宣孝英.华中科技大学2005
[7].无线局域网多址接入技术研究[D]. 李长乐.西安电子科技大学2005
[8].无线局域网中妥善安排传输的多址接入协议的研究[D]. 刘静.西安电子科技大学2005
[9].无线局域网多址技术的研究[D]. 何宏.西安电子科技大学2006
[10].IEEE 802.11无线局域网业务流特性研究及预报[D]. 冯慧芳.天津大学2006

公共无线局域网安全体系研究及其可验安全性形式化分析

猜你喜欢