| 摘要 | 第5-6页 |
| ABSTRACT | 第6-7页 |
| 第一章 绪论 | 第11-16页 |
| 1.1 研究工作的背景与意义 | 第11页 |
| 1.2 形式化验证方法的国内外研究历史与现状 | 第11-13页 |
| 1.3 本文的主要贡献与创新 | 第13-15页 |
| 1.3.1 GSTE理论的相关扩充 | 第13页 |
| 1.3.2 模型检测技术和归纳证明法的结合 | 第13页 |
| 1.3.3 使用随机图法和归纳法验证分析OSK协议及VOSK协议 | 第13-15页 |
| 1.4 本文的结构安排 | 第15-16页 |
| 第二章 形式化分析方法中的相关技术及背景知识介绍 | 第16-26页 |
| 2.1 广义符号轨迹赋值 | 第16-20页 |
| 2.1.1 模型的定义 | 第16-17页 |
| 2.1.2 断言图的定义 | 第17-18页 |
| 2.1.3 满足性的定义 | 第18-19页 |
| 2.1.4 强满足性算法 | 第19页 |
| 2.1.5 一般满足性算法 | 第19-20页 |
| 2.2 RFID系统中认证协议的形式化验证 | 第20-25页 |
| 2.2.1 安全认证协议的形式化模型 | 第22页 |
| 2.2.2 通信信道的形式化模型 | 第22-23页 |
| 2.2.3 敌手可以采用的手段 | 第23-24页 |
| 2.2.4 随机图法 | 第24页 |
| 2.2.5 归纳法 | 第24-25页 |
| 2.3 本章小结 | 第25-26页 |
| 第三章 广义符号轨迹赋值中的终端满足性 | 第26-48页 |
| 3.1 问题的引入 | 第26-27页 |
| 3.2 终端满足性相关定义 | 第27-29页 |
| 3.2.1 有限长度路径和终端路径之间的区别 | 第28-29页 |
| 3.3 终端满足性算法 | 第29-30页 |
| 3.4 终端满足性算法的应用 | 第30-39页 |
| 3.4.1 终端满足性算法可以解决强满足性的一些限制 | 第33-35页 |
| 3.4.2 使用TMC验证轮询仲裁器 | 第35-39页 |
| 3.5 终端满足性算法合理性的证明 | 第39-46页 |
| 3.5.1 TMC算法的逻辑推理 | 第39-40页 |
| 3.5.2 TMC算法是合理的 | 第40-43页 |
| 3.5.3 TMC算法是完备的 | 第43-46页 |
| 3.6 本章小结 | 第46-48页 |
| 第四章 射频识别中的隐私性与安全性研究 | 第48-73页 |
| 4.1 问题的引入 | 第48页 |
| 4.2 RFID系统中的安全问题的定义 | 第48-49页 |
| 4.3 RFID系统中协议的形式化验证 | 第49-71页 |
| 4.3.1 使用随机图法验证OSK协议及VOSK协议 | 第49-53页 |
| 4.3.1.1 敌手行为的形式化描述 | 第49-50页 |
| 4.3.1.2 建立敌手及阅读器的状态迁移模型 | 第50-52页 |
| 4.3.1.3 建立敌手和阅读器及敌手和电子标签之间的交互模型 | 第52-53页 |
| 4.3.2 OSK协议 | 第53页 |
| 4.3.3 建立OSK协议的随机图模型 | 第53-55页 |
| 4.3.4 建立VOSK协议的随机图模型 | 第55-58页 |
| 4.3.5 使用归纳法验证OSK协议及VOSK协议 | 第58-71页 |
| 4.3.5.1 电子标签的形式化描述 | 第59页 |
| 4.3.5.2 阅读器的形式化描述 | 第59-60页 |
| 4.3.5.3 电子标签和阅读器两者之间通信机制的形式化描述 | 第60页 |
| 4.3.5.4 敌手计算能力的形式化描述 | 第60-61页 |
| 4.3.5.5 设计隐私性实验 | 第61-63页 |
| 4.3.5.6 RFID系统隐私性定义 | 第63页 |
| 4.3.5.7 (r,s,t)-隐私性的合理性及相关假设说明 | 第63-64页 |
| 4.3.5.8 设计交叉RFID系统 (r,s,t)-隐私性实验 | 第64-67页 |
| 4.3.5.9 OSK协议及VOSK协议不具有(r,s,t)-隐私性 | 第67-69页 |
| 4.3.5.10 VOSK协议具有(r,s,t)-安全性 | 第69-71页 |
| 4.4 本章小结 | 第71-73页 |
| 第五章 全文总结与展望 | 第73-74页 |
| 5.1 全文总结 | 第73页 |
| 5.2 后续工作展望 | 第73-74页 |
| 致谢 | 第74-75页 |
| 参考文献 | 第75-78页 |
| 攻读硕士学位期间取得的成果 | 第78-79页 |
