基于SAT的安全协议自动化检测技术研究

摘要

安全协议是以密码学为基础,在通信网络和分布式系统中提供各种安全服务的一种协议,在信息系统安全中占据重要的位置。然而对安全协议进行分析和验证是一项非常有挑战的工作,成为安全协议发展与应用的瓶颈。由于安全协议的发展已经超出了人们进行严格分析和验证的能力,因此有必要对安全协议自动化检测技术进行研究。
　　 本文研究了基于SAT(Satisfaction)的安全协议自动化检测的关键技术,并指出现有检测工具在检测协议类型上的局限性,然后针对该问题,对检测协议类型进行扩展,提出了无类型消息和多协议中的候选辅助协议的概念,设计并实现了基于SAT的安全协议自动化检测系统SAT-ADS(Automatic Detection System ofSecurity Protocols Based SAT),使SAT-ADS可以检测类型缺陷攻击和多协议攻击,并经过实例验证检测的可行性。
　　 最后,应用SAT-ADS检测系统对BAN modified Andrew Secure RPC协议进行检测,发现了一个尚未公开的中间人攻击。本文对此协议提出了一种改进方法,即在协议交互消息中加入一个身份标识,经验证,改进后的协议避免了中间人攻击的漏洞。

目录

文摘

英文文摘

第一章 绪论

1.1 研究背景及意义

1.2 相关内容研究现状

1.3 论文主要工作及章节安排

第二章 安全协议与模型检测基础

2.1 安全协议基础与符号表示

2.1.1 安全协议密码学基础

2.1.2 安全协议的安全属性

2.1.3 安全协议符号表示

2.2 攻击者能力与协议攻击

2.2.1 攻击者的攻击能力

2.2.2 安全协议攻击

2.3 模型检测

2.3.1 模型检测技术

2.3.2 有界模型检测

2.3.3 安全协议模型检测

2.4 本章小结

第三章 基于SAT的安全协议自动化检测

3.1 协议不安全模型PIP

3.1.1 协议不安全模型的构成元素

3.1.2 安全协议形式化

3.1.3 攻击者能力形式化

3.2 规划问题

3.2.1 规划问题概述

3.2.2 k-规划图

3.3 编码为命题公式并求解

3.3.1 线性编码(Linear Encoding)

3.3.2 图形编码(Graphplan-based Encoding)

3.4 布尔可满足性问题(SAT)

3.4.1 命题公式

3.4.2 SAT求解

3.5 本章小结

第四章 基于SAT的安全协议自动化检测改进

4.1 类型缺陷攻击检测系统

4.1.1 SAT-ADS模型针对类型缺陷的改进

4.1.2 SAT-ADS检测Otway-Rees类型缺陷协议

4.1.3 SAT-ADS检测Otway-Rees类型缺陷协议结果

4.2 多协议攻击检测系统

4.2.1 候选辅助协议

4.2.2 多协议攻击搜索子系统

4.2.3 多协议攻击确认子系统

4.3 BAN Modified Andrew Secure RPC协议分析

4.3.1 BAN Modified Andrew Secure RPC协议

4.3.2 BAN Modified Andrew Secure RPC协议形式化

4.3.3 BAN Modified Andrew Secure RPC协议检测结果

4.3.4 BAN Modified Andrew Secure RPC协议改进与分析

4.4 本章小结

第五章 总结与展望

5.1 工作总结

5.2 研究展望

致谢

参考文献

硕士期间参与项目与研究成果