| 摘要 | 第1-7页 |
| Abstract | 第7-9页 |
| 第一章 绪论 | 第9-19页 |
| ·模型检测概述 | 第9-13页 |
| ·形式化方法 | 第9-11页 |
| ·模型检测及原理 | 第11-13页 |
| ·课题研究的背景 | 第13-16页 |
| ·研究工具的选用 | 第13-14页 |
| ·基于TLA的系统与性质 | 第14-16页 |
| ·论文的主要研究工作 | 第16-18页 |
| ·论文内容的结构安排 | 第18-19页 |
| 第二章 行为时序逻辑TLA | 第19-36页 |
| ·概述 | 第19页 |
| ·TLA的语法与语义 | 第19-21页 |
| ·符号与语法 | 第19-20页 |
| ·行为、基本定义与语义 | 第20-21页 |
| ·线性时态逻辑LTL | 第21-23页 |
| ·线性时态逻辑LTL的语法 | 第21页 |
| ·线性时态逻辑LTL的语义 | 第21-22页 |
| ·◇、□、◇□与□◇ | 第22页 |
| ·描述系统性质的一些LTL公式 | 第22-23页 |
| ·TLA中的时态逻辑、公平性与活性 | 第23-24页 |
| ·TLA中的时态逻辑 | 第23页 |
| ·公平性 | 第23-24页 |
| ·活性 | 第24页 |
| ·TLA中的逻辑规则 | 第24-26页 |
| ·基于TLA的描述语言TLA+ | 第26-29页 |
| ·TLA+的语法 | 第26-29页 |
| ·TLA+的描述形式 | 第29-35页 |
| ·TLA+描述的标准形式 | 第29-30页 |
| ·一个时钟系统的TLA+描述与检测 | 第30-35页 |
| ·TLC检测工具 | 第35页 |
| ·TLC检测形式 | 第35页 |
| ·本章小结 | 第35-36页 |
| 第三章 基于TLA的可控属性的转移系统 | 第36-42页 |
| ·引言与活性 | 第36-37页 |
| ·引言 | 第36页 |
| ·活性 | 第36-37页 |
| ·可控属性的转移系统 | 第37-38页 |
| ·基于可控属性的转移系统在网络协议中的应用 | 第38-41页 |
| ·Needham-Schroeder协议 | 第38页 |
| ·基于可控系统的Needham-Schroeder协议的TLA+的描述与检测 | 第38-41页 |
| ·检测结果分析 | 第41页 |
| ·本章小结 | 第41-42页 |
| 第四章 基于TLA的安全转移系统 | 第42-51页 |
| ·引言与安全性 | 第42页 |
| ·言 | 第42页 |
| ·安全性 | 第42页 |
| ·安全转移系统 | 第42-44页 |
| ·基于安全转移的网络银行系统的分析与检测 | 第44-49页 |
| ·基于安全转移的网络银行的建模分析 | 第44-46页 |
| ·检测内容设计与系统的TLA+的描述 | 第46-49页 |
| ·检测结果 | 第49页 |
| ·本章小结 | 第49-51页 |
| 第五章 强、弱公平性下多行为活性规则的研究 | 第51-68页 |
| ·引言与公平性 | 第51页 |
| ·引言 | 第51页 |
| ·公平性 | 第51页 |
| ·基于TLA的系统活性规则 | 第51-57页 |
| ·验证过程的演绎规则 | 第51-52页 |
| ·强、弱公平性下活性规则 | 第52-54页 |
| ·强、弱公平性下多行为的活性规则 | 第54-57页 |
| ·网络银行多用户取款行为并发互斥系统的分析与检测 | 第57-62页 |
| ·并发互斥与PV原语 | 第57-58页 |
| ·活性与多行为者活性检测设计 | 第58-62页 |
| ·检测结果 | 第62页 |
| ·多行为在安全系统中的活性规则 | 第62-67页 |
| ·安全系统中强、弱公平性下的多行为的活性规则 | 第62-65页 |
| ·基于安全系统的网络银行多用户取款行为的活性的分析与检测 | 第65-66页 |
| ·检测结果 | 第66-67页 |
| ·本章小结 | 第67-68页 |
| 第六章 基于TLA的协议形式化分析与检测 | 第68-102页 |
| ·信息安全 | 第68-75页 |
| ·概述 | 第68-69页 |
| ·安全机制 | 第69-71页 |
| ·网络安全威胁 | 第71页 |
| ·网络安全的模型 | 第71-72页 |
| ·身份认证 | 第72-75页 |
| ·协议的形式化分析方法 | 第75-78页 |
| ·基于逻辑的安全协议形式化分析方法 | 第76-77页 |
| ·基于模型检测的安全协议分析方法 | 第77-78页 |
| ·基于证明的安全协议分析方法 | 第78页 |
| ·基于TLA的AVISPA及其描述语言HLPSL | 第78-86页 |
| ·AVISPA介绍 | 第78-79页 |
| ·HLPSL语言规范 | 第79-86页 |
| ·基于AVISPA的Kerberos协议的形式化与检测 | 第86-96页 |
| ·Kerberos协议 | 第86-87页 |
| ·Kerberos协议的模型、形式化与检测 | 第87-96页 |
| ·四步模型与检测 | 第87-92页 |
| ·六步模型与检测 | 第92-96页 |
| ·基于TLA+的Needham-Schroeder协议的形式化与检测 | 第96-101页 |
| ·Needham-Schroeder协议 | 第96页 |
| ·Needham-Schroeder协议的形式化与检测 | 第96-101页 |
| ·Needham-Schroeder协议的形式化 | 第96-98页 |
| ·Needham-Schroeder协议的检测 | 第98-101页 |
| ·本章小结 | 第101-102页 |
| 第七章 结束语 | 第102-103页 |
| ·主要工作总结 | 第102页 |
| ·下一步研究工作 | 第102-103页 |
| 致谢 | 第103-104页 |
| 参考文献 | 第104-109页 |
| 附录A:攻读博士学位期间发表的学术论文和科研情况 | 第109-110页 |
