| 致谢 | 第1-6页 |
| 中文摘要 | 第6-7页 |
| ABSTRACT | 第7-9页 |
| 縮略语 | 第9-12页 |
| 1 引言 | 第12-20页 |
| ·研究背景 | 第12-13页 |
| ·研究现状 | 第13-18页 |
| ·EN50159标准 | 第13-15页 |
| ·铁路信号安全通信协议发展现状 | 第15-16页 |
| ·协议的形式化分析方法 | 第16-17页 |
| ·目前研究的不足 | 第17-18页 |
| ·论文结构 | 第18-20页 |
| 2 基于UPPAAL的RSSP-Ⅱ安全通信协议的建模 | 第20-38页 |
| ·时间自动机理论 | 第20-22页 |
| ·时间自动机的语法和语义 | 第20-21页 |
| ·时钟约束和时钟解释 | 第21页 |
| ·时间自动机网络 | 第21-22页 |
| ·模型检测工具UPPAAL | 第22-24页 |
| ·UPPAAL的结构和特征 | 第22-23页 |
| ·UPPAAL的系统描述语言 | 第23-24页 |
| ·RSSP-Ⅱ安全通信协议 | 第24-31页 |
| ·安全应用中间子层 | 第25-30页 |
| ·消息鉴定安全层 | 第30-31页 |
| ·RSSP-Ⅱ安全通信协议的建模 | 第31-36页 |
| ·SAI连接管理流程的建模 | 第31-35页 |
| ·时间戳初始化流程的建模 | 第35-36页 |
| ·RSSP-Ⅱ安全通信协议模型与协议的一致性 | 第36页 |
| ·本章小结 | 第36-38页 |
| 3 基于UPPAAL的RSSP-Ⅱ安全通信协议的模拟与验证 | 第38-48页 |
| ·在UPPAAL中构造时间自动机网络 | 第38-40页 |
| ·RSSP-Ⅱ安全通信协议的模拟 | 第40-43页 |
| ·SAI连接管理流程的模拟 | 第40-42页 |
| ·时间戳初始化流程的模拟 | 第42-43页 |
| ·RSSP-Ⅱ安全通信协议的验证 | 第43-47页 |
| ·SAI连接管理流程的验证 | 第44-45页 |
| ·时间戳初始化流程的验证 | 第45-47页 |
| ·本章小结 | 第47-48页 |
| 4 RSSP-Ⅱ安全通信协议消息鉴定安全码的安全性分析 | 第48-58页 |
| ·对等实体认证过程 | 第48-49页 |
| ·消息鉴定安全码的生成原理 | 第49-55页 |
| ·消息鉴定安全码的安全性分析 | 第55-57页 |
| ·消息鉴定安全码加密算法的安全性分析 | 第55-56页 |
| ·消息鉴定安全码的残余错误 | 第56-57页 |
| ·本章小结 | 第57-58页 |
| 5 RSSP-Ⅱ安全通信仿真平台的设计与实现 | 第58-78页 |
| ·RSSP-Ⅱ安全通信仿真平台的需求 | 第58-59页 |
| ·RSSP-Ⅱ安全通信仿真平台的总体设计 | 第59-60页 |
| ·RSSP-Ⅱ安全通信仿真平台的软件设计 | 第60-68页 |
| ·基于TCP/IP协议的通信模块 | 第60-61页 |
| ·RSSP-Ⅱ安全通信软件 | 第61-68页 |
| ·RSSP-Ⅱ安全通信仿真平台的测试验证 | 第68-76页 |
| ·SAI连接管理功能测试验证 | 第69-71页 |
| ·应用数据交互功能测试验证 | 第71-73页 |
| ·故障管理功能测试验证 | 第73-76页 |
| ·本章小结 | 第76-78页 |
| 6 结论与展望 | 第78-80页 |
| ·结论 | 第78页 |
| ·展望 | 第78-80页 |
| 参考文献 | 第80-84页 |
| 附录A | 第84-86页 |
| 图索引 | 第86-88页 |
| 表索引 | 第88-90页 |
| 作者简历 | 第90-94页 |
| 学位论文数据集 | 第94页 |
