安全协议的形式化方法及其应用的研究
| 摘要 | 第1-6页 |
| 英文摘要 | 第6-10页 |
| 目录 | 第10-16页 |
| 图目录 | 第16-18页 |
| 表目录 | 第18-20页 |
| 第一章 引言 | 第20-32页 |
| ·本文的研究背景 | 第20-29页 |
| ·安全协议的发展 | 第20-23页 |
| ·安全协议形式化研究的发展 | 第23-26页 |
| ·无线局域网安全 | 第26-28页 |
| ·可信计算的发展 | 第28-29页 |
| ·本文的贡献 | 第29-30页 |
| ·论文的组织 | 第30-32页 |
| 第二章 基本理论 | 第32-46页 |
| ·密码机制 | 第32-39页 |
| ·对称密钥密码系统 | 第32-34页 |
| ·公开密钥密码系统 | 第34-36页 |
| ·对称与公开密钥密码系统的比较 | 第36页 |
| ·重要公开密钥密码系统 | 第36-39页 |
| ·认知逻辑 | 第39-42页 |
| ·知识逻辑 | 第39-41页 |
| ·信念逻辑 | 第41-42页 |
| ·知识和信念的关系 | 第42页 |
| ·主体 | 第42-46页 |
| ·主体的定义 | 第42-43页 |
| ·多主体系统 | 第43页 |
| ·面向主体的软件工程 | 第43-46页 |
| 第三章 一种面向主体的安全协议形式描述语言 | 第46-62页 |
| ·安全协议描述的研究现状 | 第46-49页 |
| ·认证 | 第46-47页 |
| ·协议安全特性 | 第47页 |
| ·协议需求 | 第47页 |
| ·协议目的 | 第47-49页 |
| ·面向主体的形式语言 | 第49-54页 |
| ·语法 | 第49-51页 |
| ·语义 | 第51-54页 |
| ·主体 | 第54页 |
| ·角色 | 第54-55页 |
| ·消息 | 第55-56页 |
| ·信道 | 第56-57页 |
| ·密钥 | 第57-58页 |
| ·密码协议目的 | 第58页 |
| ·身份认证协议的目的 | 第58页 |
| ·密钥协商协议的目的 | 第58页 |
| ·NSSK 协议的形式化描述 | 第58-60页 |
| ·主体的特性和角色 | 第59页 |
| ·形式化描述 | 第59-60页 |
| ·与CKT5的比较 | 第60-61页 |
| ·结论 | 第61-62页 |
| 第四章 一种面向主体的安全协议设计逻辑 | 第62-88页 |
| ·安全协议设计的研究现状 | 第62-67页 |
| ·安全协议设计的形式化研究 | 第62-64页 |
| ·安全协议设计的非形式化研究 | 第64-66页 |
| ·安全协议的设计规则 | 第66-67页 |
| ·面向主体的逻辑 | 第67-72页 |
| ·面向主体的形式语言 | 第67-68页 |
| ·公理集 | 第68-72页 |
| ·推理规则 | 第72页 |
| ·安全协议的设计规则 | 第72-75页 |
| ·细化规则 | 第73页 |
| ·合成规则 | 第73页 |
| ·转发规则 | 第73页 |
| ·规范消息规则 | 第73-74页 |
| ·关联规则 | 第74页 |
| ·全信息规则 | 第74页 |
| ·优化消息规则 | 第74-75页 |
| ·安全协议的设计步骤 | 第75-76页 |
| ·目的的确定 | 第75页 |
| ·主体角色与特性的分析 | 第75页 |
| ·密码机制的确定 | 第75页 |
| ·目的的细化 | 第75页 |
| ·初始假设的分析 | 第75-76页 |
| ·消息的设计 | 第76页 |
| ·安全协议的优化 | 第76页 |
| ·一个新的基于对称密钥机制安全协议的设计 | 第76-81页 |
| ·目的的确定 | 第76页 |
| ·主体角色与特性的分析 | 第76页 |
| ·密码机制的确定 | 第76页 |
| ·目的的细化 | 第76-79页 |
| ·初始假设的分析 | 第79-80页 |
| ·消息的设计 | 第80-81页 |
| ·安全协议的优化 | 第81页 |
| ·一个新的基于公钥密码机制的安全协议的设计 | 第81-86页 |
| ·目的的确定 | 第81页 |
| ·主体角色与特性的分析 | 第81页 |
| ·密码机制的确定 | 第81页 |
| ·目的的细化 | 第81-84页 |
| ·初始假设的分析 | 第84-85页 |
| ·消息的设计 | 第85-86页 |
| ·安全协议的优化 | 第86页 |
| ·与BSW 逻辑的比较 | 第86-87页 |
| ·结论 | 第87-88页 |
| 第五章 一种面向主体的安全协议分析逻辑 | 第88-114页 |
| ·安全协议逻辑分析的研究现状 | 第88-92页 |
| ·BAN 逻辑 | 第88-91页 |
| ·GNY 逻辑 | 第91页 |
| ·VO 逻辑 | 第91-92页 |
| ·语法 | 第92-102页 |
| ·面向主体的形式语言 | 第92-95页 |
| ·分析安全协议的逻辑 | 第95-102页 |
| ·语义 | 第102-106页 |
| ·计算模型 | 第102-104页 |
| ·真值语义解释 | 第104-106页 |
| ·逻辑的可靠性 | 第106-107页 |
| ·安全协议的目的 | 第107-108页 |
| ·身份认证协议的目的 | 第107页 |
| ·密钥协商协议的目的 | 第107-108页 |
| ·安全协议的分析步骤 | 第108页 |
| ·NSSK 协议的形式化分析 | 第108-111页 |
| ·主体角色与特性 | 第108页 |
| ·形式化描述 | 第108-109页 |
| ·初始假设 | 第109-110页 |
| ·形式化分析 | 第110-111页 |
| ·与BAN 类型逻辑的比较 | 第111-112页 |
| ·结论 | 第112-114页 |
| 第六章 WAPI 中的认证和密钥协商协议 | 第114-136页 |
| ·WLAN 中安全协议的现状 | 第114-118页 |
| ·WAI的系统结构 | 第118-119页 |
| ·WAI的协议步骤 | 第119-120页 |
| ·WAPI 和802.11i 的比较 | 第120-124页 |
| ·WAI协议的形式化分析 | 第124-134页 |
| ·主体角色与特性 | 第124页 |
| ·形式化描述 | 第124-127页 |
| ·初始假设 | 第127-128页 |
| ·形式化分析 | 第128-133页 |
| ·改进分析 | 第133-134页 |
| ·结论 | 第134-136页 |
| 第七章 可信计算中的OIAP 协议 | 第136-150页 |
| ·可信计算的研究现状 | 第136-137页 |
| ·可信平台的基本特性 | 第137-139页 |
| ·保护能力 | 第137页 |
| ·完整性度量 | 第137页 |
| ·完整性报告 | 第137-138页 |
| ·可递信任 | 第138-139页 |
| ·TPM 的系统结构 | 第139-143页 |
| ·TPM 的授权协议 | 第143-144页 |
| ·OIAP 的会话过程 | 第144页 |
| ·OIAP 的形式化分析 | 第144-148页 |
| ·主体角色和特性 | 第144-145页 |
| ·形式化描述 | 第145-146页 |
| ·初始假设 | 第146页 |
| ·形式化分析 | 第146-148页 |
| ·改进分析 | 第148页 |
| ·结论 | 第148-150页 |
| 第八章 总结与展望 | 第150-154页 |
| 参考文献 | 第154-162页 |
| 致谢 | 第162-164页 |
| 作者简历 | 第164页 |
