网络安全协议的高效分析系统

论文摘要

网络安全协议的安全性是网络安全的重要基础,安全协议的安全性分析与验证是当今计算机安全领域中研究的热点和重大课题。形式化方法是安全协议分析的主要方法和可靠途径。目前常用的形式化分析方法有逻辑推证、模型检测及定理证明等,其中模型检测作为一种提高软硬件系统,特别是Safety-Critical系统的安全性与可靠性的自动分析与验证技术,以其简洁明了和自动化程度高而倍受注目。本文围绕安全协议形式化分析这一前沿领域,研究基于模型检测技术的安全协议的自动分析与验证技术,主要工作及成果有:1.为了能够便于计算机自动实现对安全协议的分析,本文作者通过对大量的安全协议实例进行分析与验证,归纳出协议的通用建模算法和协议存储的数据结构;2.扩展文献提出的协议描述语言PDL（Protocol Description Language）的语义描述能力,使其具有更强的语义描述能力,更具通用性:3.在对协议建模时采用了原子序列atomic和d step、偏序规约、语法重定序及类型检查等优化策略以提高验证效率,有效地缓解了模型检测过程中的状态爆炸问题;4.设计并实现了一个网络安全协议自动分析系统“安全协议自动分析系统”,该系统能够对认证协议及有可信第三方的电子商务协议进行自动分析,检测协议是否存在漏洞,如果存在漏洞,系统能够以图形化的方式显示攻击路径。该系统具有较强的实用性,可作为网络系统安全性评测以及安全协议设计的有效辅助工具。

论文目录

• 摘要
• ABSTRACT
• 第一章 引言
• 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 安全协议形式化分析
• 第三章 模型检测技术
• 3.1 模型检测的基本概念
• 3.1.1 基本术语
• 3.1.2 基本原理
• 3.2 模型检测工具SPIN
• 3.2.1 SPIN工作机理
• 3.2.2 Promela语言
• 3.2.3 线性时态逻辑（LTL）
• 3.3 利用SPIN对NS协议进行形式化分析
• 3.3.1 建立NS协议的Promela模型
• 3.3.2 利用LTL对NS协议性质的描述
• 3.3.3 利用SPIN对NS协议进行验证
• 3.3.4 验证效率分析
• 第四章 安全协议自动分析系统的设计与实现
• 4.1 系统概述
• 4.1.1 系统简介
• 4.1.2 系统功能
• 4.1.3 系统的特点
• 4.2 系统实现
• 4.2.1 消息数据结构和通道定义
• 4.2.2 扩展后的PDL语法
• 4.2.3 验证模型自动生成算法
• 4.3 安全协议实例分析
• 第五章 系统优化策略
• step'>5.1 atomic和d_step
• 5.2 偏序规约
• 5.3 语法重定序
• 5.4 类型检查
• 5.5 验证效率
• 第六章 总结与展望
• 6.1 总结
• 6.2 进一步工作方向
• 致谢
• 参考文献
• 攻读学位期间发表的论文