| 摘要 | 第1-7页 |
| Abstract | 第7-9页 |
| 目录 | 第9-13页 |
| 第一章 无线网络安全协议的形式化分析方法综述 | 第13-29页 |
| ·无线网络 | 第13-14页 |
| ·无线网络的分类 | 第13-14页 |
| ·移动设备的特点 | 第14页 |
| ·无线网络安全需求分析 | 第14-16页 |
| ·无线网络的安全威胁及其具体表现 | 第16-17页 |
| ·无线局域网安全问题现状 | 第17-18页 |
| ·WEP | 第17页 |
| ·IEEE 802.11i | 第17页 |
| ·WPA | 第17-18页 |
| ·WAPI及其实施指南 | 第18页 |
| ·攻击类型及安全密码协议的形式化分析 | 第18-26页 |
| ·安全密码协议的形式化分析 | 第19-20页 |
| ·安全密码协议形式化方法的发展 | 第20-22页 |
| ·基于计算复杂性的形式化方法-可证明安全性 | 第22-26页 |
| ·形式化方法的进一步发展 | 第26页 |
| ·本文主要工作及结构安排 | 第26-29页 |
| ·主要工作与主要贡献 | 第27-28页 |
| ·本文结构安排 | 第28-29页 |
| 第二章 基于逻辑证明的协议分析 | 第29-47页 |
| ·BAN逻辑的构成 | 第29-30页 |
| ·利用BAN类逻辑分析WAPI协议 | 第30-38页 |
| ·WAPI认证机制 | 第31-32页 |
| ·用WK逻辑分析WAI的安全性 | 第32-33页 |
| ·认证和密钥协商目标 | 第33页 |
| ·初始化假设集 | 第33-34页 |
| ·协议分析 | 第34-36页 |
| ·WAI的其它安全缺陷 | 第36-37页 |
| ·WAPI与IEEE 802.11i的比较 | 第37-38页 |
| ·小结 | 第38页 |
| ·WAPI实施方案的安全性分析 | 第38-46页 |
| ·实施方案中的密钥协商协议 | 第38-39页 |
| ·AUTLOG逻辑介绍 | 第39-41页 |
| ·WAPI实施方案的鉴别过程的安全性分析 | 第41-46页 |
| ·小结 | 第46页 |
| ·本章小结 | 第46-47页 |
| 第三章 基于Canetti-Krawczyk模型的协议设计与分析 | 第47-73页 |
| ·Canetti-Krawczyk模型及相关知识 | 第47-51页 |
| ·非认证链路攻击模型(UM) | 第48页 |
| ·认证链路模型(AM) | 第48页 |
| ·认证器(authenticator) | 第48-49页 |
| ·测试会话查询 | 第49页 |
| ·密钥交换协议(KE)对手 | 第49页 |
| ·会话密钥安全(SK-secure) | 第49-50页 |
| ·通用可组合安全 | 第50-51页 |
| ·利用CK模型分析IEEE802.11i四步握手协议的安全性 | 第51-59页 |
| ·IEEE802.11i及四步握手协议 | 第51-52页 |
| ·四步握手协议的形式化证明 | 第52-58页 |
| ·小结 | 第58-59页 |
| ·利用CK模型设计增强的无线认证基础设施EWAP | 第59-66页 |
| ·WAPI的安全性分析 | 第59页 |
| ·基于无证书公钥技术的无线认证方案EWAP | 第59-64页 |
| ·协议分析 | 第64-66页 |
| ·小结 | 第66页 |
| ·利用CK模型设计无线环境下可证安全的会话密钥分发协议 | 第66-72页 |
| ·双重加密方案的安全性 | 第67页 |
| ·基于双重加密机制的密钥分发协议DEKD | 第67-71页 |
| ·小结 | 第71-72页 |
| ·本章小结 | 第72-73页 |
| 第四章 基于通用可组合(UC)模型的协议设计与分析 | 第73-99页 |
| ·通用可组合安全 | 第73-75页 |
| ·利用UC模型设计安全的RFID供应链协议 | 第75-87页 |
| ·研究现状 | 第77页 |
| ·基于RFID的供应链模型和安全需求 | 第77-79页 |
| ·基于RFID的供应链管理通用可组合安全模型 | 第79-80页 |
| ·基于RFID的供应链轻量级通信协议 | 第80-83页 |
| ·安全证明 | 第83-86页 |
| ·协议实现的批处理方式 | 第86页 |
| ·小结 | 第86-87页 |
| ·通用可组合的无线匿名Hash认证模型 | 第87-97页 |
| ·定义及预备知识 | 第87-88页 |
| ·匿名Hash认证理想函数F_(Cred) | 第88-90页 |
| ·构造UC安全的匿名Hash认证真实协议 | 第90-93页 |
| ·安全证明 | 第93-96页 |
| ·小结 | 第96-97页 |
| ·本章小结 | 第97-99页 |
| 第五章 基于协议组合逻辑PCL模型的协议设计与分析 | 第99-123页 |
| ·协议组合逻辑 | 第99-102页 |
| ·组合证明方法 | 第100-101页 |
| ·抽象改进的方法 | 第101-102页 |
| ·利用PCL模型构造安全的RFID供应链通信协议 | 第102-103页 |
| ·安全需求 | 第103页 |
| ·安全可见的基于RFID的供应链通讯协议 | 第103-107页 |
| ·系统设置 | 第104页 |
| ·基于RFID的供应链通信协议 | 第104-107页 |
| ·安全分析 | 第107-122页 |
| ·RFID读/写子协议 | 第108-112页 |
| ·RFID密钥分发和更新子协议 | 第112-115页 |
| ·RFID可见性子协议 | 第115-121页 |
| ·协议组合 | 第121-122页 |
| ·本章小结 | 第122-123页 |
| 第六章 结束语 | 第123-129页 |
| ·形式化分析方法 | 第123页 |
| ·基于计算复杂性的安全证明方法 | 第123-124页 |
| ·UC模型与PCL模型的区别 | 第123-124页 |
| ·可组合安全的发展趋势 | 第124页 |
| ·结束语 | 第124-129页 |
| ·论文工作总结 | 第124-127页 |
| ·未来的研究方向 | 第127-129页 |
| 致谢 | 第129-131页 |
| 参考文献 | 第131-139页 |
| 在学期间的研究成果 | 第139-141页 |
