| 摘要 | 第9-11页 |
| ABSTRACT | 第11-12页 |
| 第1章 绪论 | 第17-31页 |
| 1.1 研究背景及意义 | 第17-20页 |
| 1.2 国内外研究现状 | 第20-27页 |
| 1.2.1 工业以太网协议安全的研究现状 | 第20-26页 |
| 1.2.1.1 协议漏洞挖掘的研究现状 | 第21-23页 |
| 1.2.1.2 协议安全改进的研究现状 | 第23-24页 |
| 1.2.1.3 协议安全评估的研究现状 | 第24-25页 |
| 1.2.1.4 协议入侵检测的研究现状 | 第25-26页 |
| 1.2.2 基于模型检测的安全协议形式化研究现状 | 第26-27页 |
| 1.3 论文的贡献 | 第27-28页 |
| 1.4 论文的组织 | 第28-31页 |
| 第2章 相关研究概述 | 第31-52页 |
| 2.1 ICS系统与协议 | 第31-36页 |
| 2.1.1 工业控制系统的体系结构 | 第31-32页 |
| 2.1.2 工业控制网络与传统IT网络的区别 | 第32-33页 |
| 2.1.3 工业以太网协议的体系结构 | 第33-34页 |
| 2.1.4 工业以太网协议安全防护模型与发展趋势 | 第34-36页 |
| 2.2 DNP3与DNP3-SA协议 | 第36-39页 |
| 2.2.1 DNP3协议的层次划分 | 第36-37页 |
| 2.2.2 DNP3协议的通信模式 | 第37页 |
| 2.2.3 DNP3协议应用层关键数据单元 | 第37-38页 |
| 2.2.4 DNP3-SA协议的安全机制与工作模式 | 第38-39页 |
| 2.3 有色PETRI网 | 第39-47页 |
| 2.3.1 Petri网的数学定义 | 第40-41页 |
| 2.3.2 有色Petri网的数学定义 | 第41-43页 |
| 2.3.3 有色Petri网的动态特性与分析工具 | 第43-44页 |
| 2.3.3.1 SSA工具 | 第43-44页 |
| 2.3.3.2 CTL工具 | 第44页 |
| 2.3.4 CPNTools建模工具与实例分析 | 第44-47页 |
| 2.3.4.1 CPNTools建模工具 | 第44-45页 |
| 2.3.4.2 CPNTools建模实例 | 第45-47页 |
| 2.4 AVISPA自动化模型检测工具 | 第47-50页 |
| 2.4.1 AVISPA的架构与协议自动化分析过程 | 第47-48页 |
| 2.4.2 SPAN安全性验证工具 | 第48-49页 |
| 2.4.3 基于HLPSL形式化语言的Yahalom协议描述 | 第49-50页 |
| 2.5 本文研究的问题 | 第50-51页 |
| 2.6 本章小结 | 第51-52页 |
| 第3章 DNP3-SA协议的HCPN建模 | 第52-66页 |
| 3.1 CPN的分层建模方法 | 第52-53页 |
| 3.1.1 分层原则 | 第52-53页 |
| 3.1.2 变迁触发规则 | 第53页 |
| 3.1.3 建模步骤 | 第53页 |
| 3.2 DNP3-SA协议的消息流模型 | 第53-56页 |
| 3.3 DNP3-SA协议的建模假设与颜色集 | 第56-57页 |
| 3.3.1 建模假设 | 第56页 |
| 3.3.2 关键消息与颜色集定义 | 第56-57页 |
| 3.4 DNP3-SA协议的HCPN模型建立 | 第57-64页 |
| 3.4.1 DNP3-SA协议的顶层模型 | 第57-58页 |
| 3.4.2 DNP3-SA协议的中层模型 | 第58-59页 |
| 3.4.3 DNP3-SA协议的底层模型 | 第59-64页 |
| 3.4.3.1 DNP3-SA协议的第3层模型 | 第59-63页 |
| 3.4.3.2 DNP3-SA协议的第4层模型 | 第63-64页 |
| 3.5 原始模型的功能一致性验证 | 第64-65页 |
| 3.5.1 预期结果分析 | 第64页 |
| 3.5.2 状态空间结果分析 | 第64-65页 |
| 3.6 本章小结 | 第65-66页 |
| 第4章 基于攻击者模型的协议安全评估 | 第66-87页 |
| 4.1 DELOV-YAO攻击者模型 | 第66-67页 |
| 4.2 改进的DELOV-YAO攻击者模型 | 第67-72页 |
| 4.2.1 基于消息拆分组合的攻击者模型 | 第67-68页 |
| 4.2.2 参数化的攻击者模型 | 第68-69页 |
| 4.2.3 应用改进Delov-Yao攻击者模型的NS协议 | 第69-71页 |
| 4.2.4 改进Delov-Yao攻击者模型的优势分析 | 第71-72页 |
| 4.3 协议的安全评估模型建立 | 第72-74页 |
| 4.4 CPN模型分析与验证方法 | 第74-78页 |
| 4.4.1 ASK-CTL形式化方法 | 第74-76页 |
| 4.4.2 State-Space工具验证方法 | 第76-78页 |
| 4.5 安全评估模型的状态空间分析 | 第78-79页 |
| 4.5.1 DNP3-SA协议安全评估模型的状态空间报告 | 第78页 |
| 4.5.2 功能一致性分析 | 第78-79页 |
| 4.6 基于状态空间的协议安全评估 | 第79-85页 |
| 4.6.1 协议认证属性的形式化定义 | 第79-80页 |
| 4.6.2 协议安全性验证 | 第80-81页 |
| 4.6.3 全攻击状态下的协议安全评估 | 第81-83页 |
| 4.6.4 协议漏洞分析 | 第83-85页 |
| 4.7 HCPN模型评估方法的优越性分析 | 第85页 |
| 4.8 本章小结 | 第85-87页 |
| 第5章 DNP3-SA协议的安全改进 | 第87-108页 |
| 5.1 可信计算与可信平台 | 第87-88页 |
| 5.1.1 可信平台TPM的架构 | 第87-88页 |
| 5.1.2 TPM的密钥管理 | 第88页 |
| 5.2 SCADA环境下协议面临的攻击向量及安全需求 | 第88-90页 |
| 5.3 协议单播模式的改进方案 | 第90-97页 |
| 5.3.1 改进协议单播模式的MSC模型 | 第90-93页 |
| 5.3.1.1 身份认证与密钥协商子协议的MSC模型 | 第90-91页 |
| 5.3.1.2 密钥更新与通信子协议的MSC模型 | 第91-93页 |
| 5.3.2 改进协议单播模式的CPN安全评估模型 | 第93-95页 |
| 5.3.3 改进协议单播模式安全评估与性能分析 | 第95-97页 |
| 5.3.3.1 改进协议单播模式的安全评估 | 第95-96页 |
| 5.3.3.2 改进协议单播模式的性能分析 | 第96-97页 |
| 5.4 协议广播模式的改进方案DNP3-BAE | 第97-105页 |
| 5.4.1 基于Hash链方法的TESLA认证算法 | 第98-99页 |
| 5.4.2 DNP3-BAE的MSC模型 | 第99-100页 |
| 5.4.3 DNP3-BAE协议的CPN安全评估模型 | 第100-103页 |
| 5.4.4 DNP3-BAE协议安全评估与性能分析 | 第103-105页 |
| 5.4.4.1 DNP3-BAE协议的安全评估 | 第103-104页 |
| 5.4.4.2 DNP3-BAE协议的性能分析 | 第104-105页 |
| 5.5 基于SPAN的广播协议安全性验证 | 第105-107页 |
| 5.6 本章小结 | 第107-108页 |
| 第6章 总结与展望 | 第108-110页 |
| 6.1 全文总结 | 第108-109页 |
| 6.2 工作展望 | 第109-110页 |
| 参考文献 | 第110-122页 |
| 致谢 | 第122-123页 |
| 附录A 攻读博士学位期间发表的学术论文 | 第123-124页 |
| 附录B 攻读博士学位期间参加的科研项目 | 第124-125页 |
| 附录C HCPN模型的颜色集 | 第125-126页 |
