IPv6协议的安全性分析与验证
| 摘要 | 第1-5页 |
| ABSTRACT | 第5-10页 |
| 第一章 引言 | 第10-15页 |
| ·论文背景及意义 | 第10页 |
| ·论文的国内外研究状况 | 第10-13页 |
| ·论文主要研究内容 | 第13-14页 |
| ·论文的组织结构 | 第14-15页 |
| 第二章 IPv6 协议介绍 | 第15-35页 |
| ·IPv6 地址结构及数据包格式 | 第15-18页 |
| ·IPv6 地址结构 | 第15-16页 |
| ·IPv6 数据报结构 | 第16-17页 |
| ·IPv6 数据报的扩展报头 | 第17-18页 |
| ·ICMPv6 及邻居发现协议 | 第18-19页 |
| ·ICMPv6 报文 | 第18-19页 |
| ·邻居发现过程 | 第19页 |
| ·IPv6 单播路由选择协议 | 第19-24页 |
| ·路由信息协议 RIPng | 第20-21页 |
| ·开放最短路径优先协议 OSPFv3 | 第21-23页 |
| ·边界网关协议 BGP4+ | 第23-24页 |
| ·IPv6 安全机制 IPsec | 第24-34页 |
| ·认证报头 AH 协议 | 第25-26页 |
| ·封装安全有效载荷 ESP 协议 | 第26页 |
| ·因特网密钥交换协议 IKE 协议 | 第26-34页 |
| ·本章小结 | 第34-35页 |
| 第三章 协议安全性形式化验证理论 | 第35-42页 |
| ·协议安全性验证的形式化方法 | 第35-38页 |
| ·模态逻辑 | 第35-36页 |
| ·定理证明 | 第36页 |
| ·模型检测 | 第36-38页 |
| ·模型检测技术 | 第38-41页 |
| ·模型检测工具 SPIN | 第38-39页 |
| ·建模语言 Promela | 第39-40页 |
| ·线性时态逻辑 LTL | 第40-41页 |
| ·模型检测技术的研究点 | 第41页 |
| ·本章小结 | 第41-42页 |
| 第四章 IPv6 协议的安全性分析 | 第42-54页 |
| ·IPv6 网络安全问题分析和对策 | 第42-43页 |
| ·网络安全威胁分类 | 第42-43页 |
| ·提高网络安全措施 | 第43页 |
| ·IPsec 的安全性分析 | 第43-48页 |
| ·DoS 攻击分析 | 第44-45页 |
| ·基于分片的 DoS 攻击分析 | 第45-46页 |
| ·中间人攻击分析 | 第46-47页 |
| ·反射攻击分析 | 第47-48页 |
| ·身份保护问题 | 第48页 |
| ·邻居发现协议的安全性分析 | 第48-51页 |
| ·IPv6 路由协议的安全性分析 | 第51-53页 |
| ·本章小结 | 第53-54页 |
| 第五章 IPsec 安全性的形式化验证 | 第54-79页 |
| ·对 SPIN 工具的改进 | 第54-60页 |
| ·SPIN 工作原理 | 第54页 |
| ·对 SPIN 内存管理算法的改进 | 第54-56页 |
| ·对 SPIN 内存管理算法改进的描述 | 第56-60页 |
| ·IPv6 数据报秘密性的形式化验证 | 第60-76页 |
| ·ESP 协议行为抽象 | 第60-61页 |
| ·建立 ESP 的 Promela 模型 | 第61-71页 |
| ·ESP 协议目标安全性质的 LTL 描述 | 第71-72页 |
| ·改进的 SPIN 验证结果与分析 | 第72-76页 |
| ·IPv6 数据报完整性安全功能的验证 | 第76-78页 |
| ·本章小结 | 第78-79页 |
| 第六章 总结与展望 | 第79-81页 |
| ·总结 | 第79-80页 |
| ·展望 | 第80-81页 |
| 致谢 | 第81-82页 |
| 参考文献 | 第82-86页 |
