基于串空间理论的安全协议分析

论文摘要

安全协议提供安全服务，是保证网络安全的基础。近年来，安全协议越来越多地用于保护因特网上传输的各种交易，保护针对计算机系统的访问。由于验证安全协议自身的安全性是十分困难的。因此，必须借助形式化方法，对安全协议进行分析。在众所多的形式化分析方法中，串空间模型是一种结合定理证明和协议迹的混合方法，将安全协议的形式化分析技术推向一个新的高度，由于其高效、严谨、直观的特点而受到广泛推崇。本文在对串空间模型研究的基础上，首次以串空间理论中的“理想”和“诚实”为工具，对改进的NSSK协议从机密性和认证性两个方面进行了严格的证明。结果表明，改进的NSSK认证协议实现了协议设计的目标，是正确有效的。安全协议的正确性主要体现在一致性和机密性两个方面。虽然串空间模型在协议分析过程中比其它形式化方法更为简洁和直观，但在分析协议为什么不正确及如何改进方面，同其他形式化分析方法一样，显得分析能力较弱。针对这一问题，本文在认证测试的基础上，提出了参数一致性矩阵的概念。利用参数一致性矩阵对安全协议的一致性进行分析，与原有的分析过程相比更为直观、简单，有效地揭示协议失败的原因，并针对这些原因给出相应的改进思路。

论文目录

• 摘要
• Abstract
• 目录
• 第一章 绪论
• 1.1 安全协议验证的研究背景
• 1.2 安全协议验证的研究现状
• 1.3 本文工作
• 1.4 章节安排
• 第二章 安全协议形式化分析
• 2.1 密码学基础
• 2.1.1 密码学简介
• 2.1.2 基本概念
• 2.1.3 密码体制
• 2.2 安全协议
• 2.2.1 基本概念
• 2.2.2 系统模型
• 2.2.3 安全协议缺陷
• 2.3 形式化分析的基本假定
• 2.4 形式化分析方法
• 第三章 串空间模型
• 3.1 串空间模型简介
• 3.2 串空间基础知识
• 3.2.1 基本概念
• 3.2.2 丛和节点间的因果依赖关系
• 3.2.3 项与加密
• 3.2.4 自由假设
• 3.2.5 攻击者模型
• 3.2.6 正确性概念
• 3.3 串空间模型分析方法
• 3.3.1 NSL串空间
• 3.3.2 NSL协议安全性分析
• 第四章 NSSK协议分析
• 4.1 理想与诚实
• 4.1.1 理想
• 4.2.2 入口点与诚实
• 4.2 NSSK协议
• 4.3 协议的机密性分析
• 4.4 协议的一致性分析
• 4.4.1 发起者的保证
• 4.4.2 响应者的保证
• 4.5 本章小结
• 第五章 安全协议一致性分析
• 5.1 认证测试技术
• 5.1.1 基本概念
• 5.1.2 认证测试的性质
• 5.2 参数一致性矩阵
• 5.2.1 参数一致性矩阵的元素
• 5.2.2 参数一致性矩阵的运算规则
• 5.3 方法有效性验证
• 5.3.1 Otway-Rees协议
• 5.3.2 Otway-Rees协议的一致性分析
• 5.4 结果分析
• 5.5 本章小结
• 第六章 结束语
• 参考文献
• 致谢
• 附录1 攻读硕士学位期间发表的论文