| 摘要 | 第3-4页 |
| abstract | 第4页 |
| 符号说明 | 第7-8页 |
| 第一章 绪论 | 第8-12页 |
| 1.1 研究背景及意义 | 第8-9页 |
| 1.2 研究现状 | 第9-10页 |
| 1.3 研究内容 | 第10-11页 |
| 1.4 论文结构 | 第11-12页 |
| 第二章 形式化方法与模型检测技术理论基础 | 第12-18页 |
| 2.1 形式化方法概述 | 第12-14页 |
| 2.2 模型检测工具SPIN | 第14-18页 |
| 2.2.1 SPIN工作机理 | 第14-15页 |
| 2.2.2 建模语言Promela | 第15-17页 |
| 2.2.3 线性时态逻辑LTL | 第17-18页 |
| 第三章 超轻量级RFID双向认证协议 | 第18-22页 |
| 3.1 超轻量级双向认证协议分类 | 第18-19页 |
| 3.2 典型的超轻量级认证协议 | 第19-21页 |
| 3.2.1 RCIA协议 | 第19-20页 |
| 3.2.2 RAPP协议 | 第20-21页 |
| 3.3 超轻量级双向认证协议安全问题 | 第21-22页 |
| 第四章 超轻量级双向认证协议的形式化分析与验证 | 第22-40页 |
| 4.1 协议抽象建模方法 | 第22页 |
| 4.2 协议形式化表示 | 第22-24页 |
| 4.2.1 RCIA形式化表示 | 第22-23页 |
| 4.2.2 RAPP形式化表示 | 第23-24页 |
| 4.3 协议安全属性刻画 | 第24-25页 |
| 4.4 基于SPIN的RCIA协议模型检测 | 第25-34页 |
| 4.4.1 诚实主体建模 | 第25-27页 |
| 4.4.2 攻击者建模 | 第27-31页 |
| 4.4.3 验证结果与分析 | 第31-34页 |
| 4.5 基于SPIN的RAPP协议模型检测 | 第34-40页 |
| 4.5.1 诚实主体建模 | 第35-36页 |
| 4.5.2 攻击者建模 | 第36-38页 |
| 4.5.3 验证结果与分析 | 第38-40页 |
| 第五章 基于G-UMAP密钥同步机制的改进协议模型检测 | 第40-47页 |
| 5.1 超轻量级双向认证协议通用交互模型G-UMAP | 第40-41页 |
| 5.2 G-UMAP中的去同步攻击漏洞 | 第41-43页 |
| 5.3 密钥同步机制改进方案 | 第43页 |
| 5.4 基于密钥同步机制的改进协议模型检测 | 第43-47页 |
| 5.4.1 改进的RCIA协议建模与验证分析 | 第43-45页 |
| 5.4.2 改进的RAPP协议建模与验证分析 | 第45-47页 |
| 第六章 总结与展望 | 第47-49页 |
| 6.1 工作总结 | 第47-48页 |
| 6.2 未来工作展望 | 第48-49页 |
| 参考文献 | 第49-52页 |
| 附录 基于密钥同步机制的RAPP协议模型检测Promela代码 | 第52-60页 |
| 个人简历 在读期间发表的学术论文 | 第60-61页 |
| 致谢 | 第61页 |
