基于串空间的网络安全协议形式化分析模型与工具研究

摘要

网络安全协议从功能上主要可分为数字签名协议、密钥交换协议、密钥分配协议、身份认证协议等。随着计算机网络的普及以及电子商务和电子政务的蓬勃兴起，网络安全协议的应用越来越广泛，确保网络安全协议的安全性己经成为一项重要的研究课题。20年来，业界投入大量精力对网络安全协议的分析进行了深入的研究，取得了较多成果。在现有的理论和方法中，形式化分析方法研究最为突出。
　　 本文对网络安全协议的形式化分析作了较为全面的综述。在前人研究基础上，F'abrega，Herzog和Gunman三人提出了串空间(STRANDSPACE)模型，使用一种节点间存在因果关系的有向图来表示协议的运行，是分析网络安全协议的一种实用、直观和严格的形式化方法。在深入研究串空间理论的基础上，本文对攻击者模型进行了扩展，增加了攻击者签名、签名验证和HMAC功能以及相应的初始化假设，并基于扩展模型进行了实例协议分析，找到了协议的漏洞。最后，本文分析了目前串空间分析工具的研究现状，并深入研究了基于软约束的串空间工具，借助分析工具Csolver实现了对NSPK和NSPK-L等协议的实例分析，找到了NSPK和NSPK-L协议所受的中间人攻击和消息重放攻击。

目录

文摘

英文文摘

第一章 绪论

1.1 基本概念

1.2 形式化方法在安全协议分析方面的研究现状

1.3 论文的章节安排

第二章 协议安全性和攻击方法

2.1 安全协议的功能与安全目标

2.2 安全协议的缺陷和攻击类型

2.3 安全协议的攻击模型

第三章 形式化分析方法及串空间理论基础

3.1 安全协议的形式化分析过程

3.2 安全协议的三种分析方法

3.3 基本串空间理论

第四章 串空间理论中的攻击模型及其扩展

4.1 代数理论基础

4.2 攻击者模型

4.2.1 入侵者串

4.2.2 攻击知识集

4.2.3 攻击能力

4.3 攻击者串类型扩展

4.4 基于扩展类型的攻击实例分析

第五章 基于软约束的串空间分析工具研究

5.1 串空间工具研究现状

5.2 基于软约束的形式化分析模型

5.2.1 软约束方法

5.2.2 串空间应用分析

5.3 软约束串空间分析工具的分析流程

5.4 软约束串空间工具分析实例

5.4.1 NSPK协议分析

5.4.2 NSPK-L协议分析

第六章 总结

6.1 工作总结

6.2 研究展望

参考文献

致谢

攻读学位期间发表的学术论文目录