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