物联网传感网络安全协议形式化研究
| 摘要 | 第1-5页 |
| Abstract | 第5-6页 |
| 目录 | 第6-9页 |
| 第1章 绪论 | 第9-19页 |
| 引言 | 第9页 |
| ·研究背景 | 第9-10页 |
| ·研究内容和方法 | 第10-14页 |
| ·研究原则和思路 | 第14-16页 |
| ·研究流程及成功标准 | 第16-17页 |
| ·论文创新点 | 第17页 |
| ·论文组织结构 | 第17-18页 |
| ·本章小结 | 第18-19页 |
| 第2章 物联网及安全协议形式化研究综述 | 第19-31页 |
| 引言 | 第19页 |
| ·物联网的发展 | 第19-20页 |
| ·物联网的定义 | 第20页 |
| ·物联网的体系结构 | 第20-23页 |
| ·应用层 | 第21-22页 |
| ·感知层 | 第22页 |
| ·网络层 | 第22-23页 |
| ·物联网的研究现状 | 第23-24页 |
| ·无线传感网络综述及研究现状 | 第24-25页 |
| ·安全协议形式化研究综述 | 第25-30页 |
| ·安全协议设计的困难性 | 第26页 |
| ·形式化方法设计 | 第26-28页 |
| ·形式化方法分析 | 第28-29页 |
| ·形式化方法验证 | 第29页 |
| ·形式化方法定理证明 | 第29-30页 |
| ·本章小结 | 第30-31页 |
| 第3章 相关研究基础 | 第31-45页 |
| 引言 | 第31页 |
| ·Dolev-Yao模型 | 第31-33页 |
| ·攻击者的知识和能力 | 第32页 |
| ·攻击者的行为 | 第32-33页 |
| ·通信顺序进程 | 第33-35页 |
| ·CSP基本定义 | 第33-35页 |
| ·CSP运算符 | 第35页 |
| ·攻击者模型 | 第35-37页 |
| ·运行环境模型 | 第37-38页 |
| ·CK模型 | 第38-40页 |
| ·CSP模型验证 | 第40-41页 |
| ·串空间定理证明 | 第41-43页 |
| ·基于密钥的单向杂凑函数 | 第43-44页 |
| ·异或运算 | 第44页 |
| ·本章小结 | 第44-45页 |
| 第4章 物联网传感网络建模 | 第45-53页 |
| 引言 | 第45页 |
| ·物联网传感网络的特点 | 第45-46页 |
| ·物联网传感网络结构建模 | 第46-49页 |
| ·物联网传感网络建模分析 | 第49-50页 |
| ·物联网传感网络通信主体的抽象 | 第50-52页 |
| ·本章小结 | 第52-53页 |
| 第5章 基于SNIT的协议元库构建方法 | 第53-60页 |
| 引言 | 第53页 |
| ·协议元库的构建目标 | 第53页 |
| ·协议元库的构建思路 | 第53-54页 |
| ·协议元的选取标准 | 第54页 |
| ·协议元库的构建 | 第54-59页 |
| ·协议的自动化生成 | 第59页 |
| ·本章小结 | 第59-60页 |
| 第6章 SNIT协议建模 | 第60-83页 |
| 引言 | 第60页 |
| ·相关符号及术语 | 第60-61页 |
| ·SNIT协议设计目标 | 第61页 |
| ·SNIT协议设计 | 第61-63页 |
| ·SNIT协议的安全分析 | 第63-69页 |
| ·AM模型中的攻击者行为能力模型 | 第63页 |
| ·SNIT协议在AM模型下的SK安全 | 第63-66页 |
| ·SNIT协议的模型认证器 | 第66页 |
| ·SNIT协议在AM模型到UM模型的转化 | 第66-68页 |
| ·SNIT协议的安全分析 | 第68-69页 |
| ·SNIT协议建模分析 | 第69-71页 |
| ·SNIT_C协议建模 | 第71-73页 |
| ·SNIT_M协议建模 | 第73-76页 |
| ·SNIT_S协议建模 | 第76-79页 |
| ·SNIT协议自动化分析 | 第79-82页 |
| ·本章小结 | 第82-83页 |
| 第7章 SNIT协议模型验证 | 第83-120页 |
| 引言 | 第83页 |
| ·攻击者行为模型 | 第83-85页 |
| ·SNIT保密性分析 | 第85-105页 |
| ·SNIL_C的保密性 | 第87-94页 |
| ·SNIT_M的保密性 | 第94-99页 |
| ·SNIT_S的保密性 | 第99-105页 |
| ·SNIT认证性验证 | 第105-119页 |
| ·M对S的认证 | 第107-113页 |
| ·S对M的认证 | 第113-119页 |
| ·CSP自动验证工具 | 第119页 |
| ·本章小结 | 第119-120页 |
| 第8章 SNIT协议定理证明 | 第120-150页 |
| 引言 | 第120页 |
| ·对串空间的改进 | 第120-122页 |
| ·协议正确性条件 | 第122-123页 |
| ·攻击者能力模型 | 第123页 |
| ·SNIT协议的证明 | 第123-148页 |
| ·SNIT_C | 第126-133页 |
| ·SNIT_M | 第133-140页 |
| ·SNIT_S | 第140-148页 |
| ·证明结果 | 第148-149页 |
| ·本章小结 | 第149-150页 |
| 第9章 总结与展望 | 第150-154页 |
| 引言 | 第150页 |
| ·研究成功标准的确认 | 第150-151页 |
| ·总结 | 第151-152页 |
| ·未来工作展望 | 第152-153页 |
| ·本章小结 | 第153-154页 |
| 参考文献 | 第154-158页 |
| 附录A 攻读博士学位期间主持和参与的项目 | 第158-159页 |
| 附录B 攻读博士学位期间发表和录用的论文 | 第159-160页 |
| 附录C 攻读博士学位期间获得的奖励 | 第160-161页 |
| 附录D 攻读博士学位期间获得的证书 | 第161-162页 |
| 致谢 | 第162-164页 |
| 告别语 | 第164页 |
