基于SPIN的802.1X协议形式化验证和改进
| 摘要 | 第1-6页 |
| ABSTRACT | 第6-9页 |
| 第1章 绪论 | 第9-12页 |
| ·研究背景 | 第9页 |
| ·网络协议安全性分析的复杂性 | 第9页 |
| ·使用传统测试方式进行验证的缺点 | 第9-10页 |
| ·使用模型检测技术进行检验的优点 | 第10页 |
| l.5 本文的工作 | 第10页 |
| ·国内外研究现状 | 第10-11页 |
| ·论文结构 | 第11-12页 |
| 第2章 Promela语言 | 第12-17页 |
| ·Promela语言介绍 | 第12页 |
| ·Promela模型对象 | 第12-17页 |
| ·进程 | 第12-13页 |
| ·数据对象 | 第13页 |
| ·数据结构 | 第13-14页 |
| ·消息通道 | 第14页 |
| ·顺序发送和随机接收 | 第14页 |
| ·会聚通道 | 第14-15页 |
| ·控制流复合语句 | 第15-17页 |
| 第3章 SPIN | 第17-21页 |
| ·SPIN的介绍 | 第17-18页 |
| ·Cygwin环境下SPIN的安装 | 第18页 |
| ·定义正确性属性 | 第18-21页 |
| ·基本断言 | 第18页 |
| ·元标签 | 第18-19页 |
| ·never声明 | 第19-20页 |
| ·线性时态逻辑LTL | 第20-21页 |
| 第4章 IEEE 802.1X协议介绍 | 第21-32页 |
| ·802.1X的作用 | 第21页 |
| ·802.1X体系结构 | 第21页 |
| ·802.1X的认证方式 | 第21-22页 |
| ·802.1X的基本概念 | 第22-23页 |
| ·受控/非受控端口 | 第22页 |
| ·授权/非授权状态 | 第22-23页 |
| ·授权方向 | 第23页 |
| ·802.1X的认证触发方式 | 第23页 |
| ·客户端主动触发方式 | 第23页 |
| ·设备端主动触发方式 | 第23页 |
| ·802.1X的认证过程 | 第23-30页 |
| ·EAP中继方式 | 第23-25页 |
| ·EAP终结方式 | 第25-26页 |
| ·主体状态转移关系 | 第26-30页 |
| ·802.1X的接入方式 | 第30页 |
| ·802.1X的定时器 | 第30-32页 |
| 第5章 基于SPIN的802.1X协议形式化验证 | 第32-53页 |
| ·协议的形式化描述 | 第32-40页 |
| ·802.1X协议的具体内容 | 第32-33页 |
| ·802.1X协议的相关说明 | 第33-34页 |
| ·802.1X协议的Promela结构 | 第34-36页 |
| ·802.1X协议主体的Promela建模 | 第36-40页 |
| ·SPIN模拟802.1X协议的运行过程 | 第40-43页 |
| ·协议的时态行为分析 | 第43-46页 |
| ·协议的攻击者模型 | 第46-49页 |
| ·802.1X协议的改进 | 第49-52页 |
| ·基于公钥密钥的加密过程 | 第49-51页 |
| ·改进后的模型验证 | 第51-52页 |
| ·小结 | 第52-53页 |
| 第6章 结论与展望 | 第53-54页 |
| ·IEEE802.1X协议形式化分析的总结 | 第53页 |
| ·进一步的工作 | 第53-54页 |
| 参考文献 | 第54-57页 |
| 致谢 | 第57页 |
