学位论文 > 优秀研究生学位论文题录展示

网络安全协议的模型检测分析及验证系统

作　者: 程莹
导　师: 肖美华
学　校: 南昌大学
专　业: 计算机软件与理论
关键词: 模型检测 SPIN 静态分析技术 LTL Promela
分类号: TP393.08
类　型: 硕士论文
年　份: 2010年
下　载: 116次
引　用: 0次
阅　读: 论文下载

内容摘要

随着计算机时代的迅猛发展,分析网络的安全性相当重要。保证安全协议的安全性及秘密性已是网络安全领域的最热门话题之一。安全协议自身的缺陷给网络安全造成了巨大的威胁,为了确保网络中传输的信息及数据不被篡改或丢失,必须对协议进行分析,且可以采用形式化及非形式化方法对协议进行验证；为解决状态空间爆炸问题,必须利用搜索优化算法对协议模型进行改进。由此可知,形式化分析验证方法是在网络安全中最关键的技术。其中,对密码协议性质进行规范极为重要,可以利用LTL性质对协议进行描述。本文主要采用模型检测技术对协议进行形式化分析,旨在发现网络安全协议中隐藏的漏洞,并对协议加以改进。论文的主要工作和贡献有：1.通过使用强大的验证密钥协议的模型检测工具—SPIN,运用静态分析技术及自动约简方法,简化输入方式以达到改善SPIN运行环境的目的,从而使模型更简单易懂。2.通过将SPIN工具内嵌入安全协议验证系统,并使用状态搜索方法满足协议的设计规范,检测协议的构造模型(如协议单步建模及完整建模),收集数据流信息,从而对网络安全协议进行分析与验证,通过减少建模空间的迁移数,有效降低了状态空间爆炸问题。3.设计并实现了网络安全协议验证系统,并对具有可信第三方的对称密钥协议及电子商务协议SSL3.0握手协议的Promela建模,并使用LTL对协议性质进行描述,提高搜索效率,证明协议本身的安全性与可靠性,并通过协议的实例分析来验证系统的可用性。

全文目录

摘要  3-4
ABSTRACT  4-9
第1章引言  9-12
  1.1 研究背景  9
  1.2 安全协议的发展及国内外研究现状  9-10
  1.3 本人主要工作  10-11
  1.4 论文组织结构  11-12
第2章安全协议  12-18
  2.1 密码协议  12-13
    2.1.1 密码协议的安全属性  12
    2.1.2 密码协议分类  12-13
    2.1.3 密码协议的安全性分析  13
  2.2 安全协议的形式化方法  13-16
    2.2.1 逻辑推理  14-15
    2.2.2 定理证明  15
    2.2.3 模型检测  15-16
  2.3 安全协议的非形式化分析  16-18
第3章模型检测技术  18-23
  3.1 模型检测基本原理  18
  3.2 模型检测工具SPIN  18-21
    3.2.1 SPIN工作原理及特征  18-19
    3.2.2 基于SPIN的协议分析  19-21
  3.3 Promela建模  21-23
第4章基于SPIN的SSL 3.0握手协议模型检测  23-30
  4.1 SSL3.0握手协议简介  23
  4.2 建立SSL3.0握手协议的Promela模型  23-30
    4.2.1 诚信主体建模  26-27
    4.2.2 攻击者建模  27-28
    4.2.3 LTL描述协议性质  28-29
    4.2.4 分析及验证  29-30
第5章网络安全协议验证系统  30-42
  5.1 系统平台搭建  30-33
    5.1.1 系统功能介绍  30-31
    5.1.2 系统PDL语言描述及数据输入规则  31-33
  5.2 平台设计与实现  33-37
    5.2.1 设计类图描述  33
    5.2.2 SSL3.0握手协议的PDL描述  33-35
    5.2.3 系统流程图及实现  35-37
  5.3 搜索优化算法  37-42
    5.3.1 协议主体建模算法步骤  38-40
    5.3.2 改进的攻击者建模算法步骤  40-42
第6章静态分析技术在安全协议中的应用  42-51
  6.1 静态分析技术基本原理  42
  6.2 NS公钥认证协议分析  42-46
    6.2.1 NS协议简介  42-43
    6.2.2 协议实例模型  43
    6.2.3 静态分析结果  43-46
  6.3 TMN协议分析  46-51
    6.3.1 TMN协议简介  46-47
    6.3.2 TMN协议实例模型  47
    6.3.3 静态分析结果  47-51
第7章结论与展望  51-53
  7.1 结论  51
  7.2 进一步工作的方向  51-53
致谢  53-54
参考文献  54-57
攻读学位期间的研究成果  57

网络安全协议的模型检测分析及验证系统

内容摘要

全文目录

相似论文