无线网络安全协议的形式化分析方法

摘要

随着无线网络应用的迅速发展，网络安全的问题日益重要，采用形式化方法设计及分析无线环境下的安全协议得到快速的发展以及广泛的应用。本论文对于安全协议的形式化分析方法从技术特点上做了分类和分析，对于安全协议分析技术的发展历史、目前的状况以及将来的趋势作了总体的介绍和总结。具体内容包括： ·对形式化分析方法-BAN类逻辑进行了研究，利用BAN类逻辑(WK逻辑)，对中国无线局域网安全标准WAPI及其实施方案的认证基础设施WAI进行了形式化分析，指出其中存在的安全隐患，以及能够实现的安全目标。 ·对基于计算复杂性的方法进行了深入研究；重点研究内容包括：Canetti— Krawczyk模型和通用可组合模型，主要工作包括： 1.通过Canetti-Krawczyk(CK)安全模型对IEEE802.1 1 i四步握手协议模块进行了安全性证明。证明表明四步握手协议不仅满足CK模型下提出的会话密钥(SK)安全的定义，并且可以满足更高安全级别的通用可组合(UC)安全的定义，因此该协议可以作为无线局域网中安全的认证和密钥协商基础模块使用。 2.利用CK模型，对中国无线局域网安全标准WAPI的认证模型进行了深入分析，针对WAPI中的安全缺陷，提出了一种增强的无线认证协议EWAP。该方案采用模块化及可组合的设计方法，在CK模型下提供了可证明的安全性，并具有相应的安全属性。 3.提出了一个适合无线环境下使用的基于双重加密机制的会话密钥分发协议，该协议作为四步握手协议的上层协议，可以保证STA与AP安全共享PMK的目的。利用CK模型，在双重加密机制满足适应性选择密文攻击(CCA2)安全的定义下，对该会话密钥分发协议进行了安全性分析。 4.供应链管理是RFID技术主要的应用领域之一，但是目前对该领域基于RFID技术的安全机制还没有较深入的研究。供应链环境对于RFID技术的特定安全需求决定了无法直接应用已有的各种RFID安全机制。定义了供应链环境下RFID通信协议必须满足的安全需求，提出了一个可以满足这些安全需求的通用可组合安全模型，并且设计了一个可以实现该模型的轻量级RFID通信协议。 5.利用通用可组合安全模型定义并实现了一种适用于无线网络的匿名Hastl认证理想函数，并在此基础上定义了一个具有普遍意义的Hash证书权威模型。定义了匿名卜lash认证机制的安全需求和安全概念，并且证明在标准模型(非随机预言机模型)下所提匿名Hash认证机制的安全属性可以通过安全对称加密机制、安全数据签名机制、伪随机函数以及单向无碰撞Hash函数的组合得到保证。·最后，本文对安全协议的形式化分析方法的最新进展一协议组合逻辑PCL进行了深入研究，设计了一个基于RFID的供应链通信协议可以实现所定义的安全需求和可见性要求，并且用PCL给出了形式化的安全证明。

目录

文摘

英文文摘

声明

第一章无线网络安全协议的形式化分析方法综述

1.1无线网络

1.1.1无线网络的分类

1.1.2移动设备的特点

1.2无线网络安全需求分析

1.3无线网络的安全威胁及其具体表现

1.4无线局域网安全问题现状

1.4.1 WEP

1.4.2 IEEE 802.11i

1.4.3 WPA

1.4.4 WAPI及其实施指南

1.5攻击类型及安全密码协议的形式化分析

1.5.1安全密码协议的形式化分析

1.5.2安全密码协议形式化方法的发展

1.5.3基于计算复杂性的形式化方法-可证明安全性

1.5.4形式化方法的进一步发展

1.6本文主要工作及结构安排

1.6.1主要工作与主要贡献

1.6.2本文结构安排

第二章基于逻辑证明的协议分析

2.1 BAN逻辑的构成

2.2利用BAN类逻辑分析WAPI协议

2.2.1 WAPI认证机制

2.2.2用WK逻辑分析WAI的安全性

2.2.3认证和密钥协商目标

2.2.4初始化假设集

2.2.5协议分析

2.2.6 WAI的其它安全缺陷

2.2.7 WAPI与IEEE 802.11i的比较

2.2.8小结

2.3 WAPI实施方案的安全性分析

2.3.1实施方案中的密钥协商协议

2.3.2 AUTLOG逻辑介绍

2.3.3 WAPI实施方案的鉴别过程的安全性分析

2.3.4小结

2.4本章小结

第三章基于Canetti-Krawczyk模型的协议设计与分析

3.1 Canetti-Krawczyk模型及相关知识

3.1.1非认证链路攻击模型(UM)

3.1.2认证链路模型(AM)

3.1.3认证器(authenticator)

3.1.4测试会话查询

3.1.5密钥交换协议(KE)对手

3.1.6会话密钥安全(SK-secure)

3.1.7通用可组合安全

3.2利用CK模型分析IEEE802.11i四步握手协议的安全性

3.2.1 IEEE 802.11i及四步握手协议

3.2.2四步握手协议的形式化证明

3.2.3小结

3.3利用CK模型设计增强的无线认证基础设施EWAP

3.3.1 WAPI的安全性分析

3.3.2基于无证书公钥技术的无线认证方案EWAP

3.3.3协议分析

3.3.4小结

3.4利用CK模型设计无线环境下可证安全的会话密钥分发协议

3.4.1双重加密方案的安全性

3.4.2基于双重加密机制的密钥分发协议DEKD

3.4.3小结

3.5本章小结

第四章基于通用可组合(UC)模型的协议设计与分析

4.1通用可组合安全

4.2利用UC模型设计安全的RFID供应链协议

4.2.1研究现状

4.2.2基于RFID的供应链模型和安全需求

4.2.3基于RFID的供应链管理通用可组合安全模型

4.2.4基于RFID的供应链轻量级通信协议

4.2.5安全证明

4.2.6协议实现的批处理方式

4.2.7小结

4.3通用可组合的无线匿名Hash认证模型

4.3.1定义及预备知识

4.3.2匿名Hash认证理想函数Fcred

4.3.3构造UC安全的匿名Hash认证真实协议

4.3.4安全证明

4.3.5小结

4.4本章小结

第五章基于协议组合逻辑PCL模型的协议设计与分析

5.1协议组合逻辑

5.1.1组合证明方法

5.1.2抽象改进的方法

5.2利用PCL模型构造安全的RFID供应链通信协议

5.3安全需求

5.4安全可见的基于RFID的供应链通讯协议

5.4.1系统设置

5.4.2基于RFID的供应链通信协议

5.5安全分析

5.5.1 RFID读/写子协议

5.5.2 RFID密钥分发和更新子协议

5.5.3 RFID可见性子协议

5.5.4协议组合

5.6本章小结

第六章结束语

6.1形式化分析方法

6.2基于计算复杂性的安全证明方法

6.2.1 UC模型与PCL模型的区别

6.2.2可组合安全的发展趋势

6.3结束语

6.3.1论文工作总结

6.3.2未来的研究方向

致谢

参考文献

在学期间的研究成果