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

安全协议的漏洞分析及自动验证工具

作　者: 周璐
导　师: 傅育熙
学　校: 上海交通大学
专　业: 计算机科学与技术
关键词: 安全协议漏洞一般安全协议模型自动验证工具
分类号: TP393.08
类　型: 硕士论文
年　份: 2007年
下　载: 298次
引　用: 1次
阅　读: 论文下载

内容摘要

网络时代的今天,多种服务于互联网应用的网络安全协议纷纷诞生;由安全协议设计上的漏洞引发的安全问题也越来越引起人们的重视。复杂的网络环境使攻击者可以利用通信协议自身的缺陷来实施各种各样的攻击,也给确保协议的安全性带来较大难度。安全协议形式化分析技术的提出,将协议的安全性问题转化为数学问题,采用数学证明的手段来代替直觉的判定,近年来已逐步被公认为解决安全问题的合理方案。国内外先后出现了多种模型和研究方法。本文主要从漏洞分析的角度,对安全协议形式化方法做了一些探索。首先通过对安全协议缺陷的观察和整理,从形式化角度将所有的安全问题归纳为六大漏洞,即身份认证漏洞、假冒攻击漏洞、保密数据泄漏漏洞、新鲜性漏洞、类型攻击漏洞和攻击者不当得利漏洞。能否完善解决这六大漏洞的检测与判定,可作为安全协议形式化模型是否完备的参考标准。接着,通过对“一般安全协议模型(GSPM)”的增强与完善,将新鲜性漏洞和类型攻击漏洞的验证引入该模型,并分别给予实例研究。一般安全协议模型本身已是较为成熟的一个安全协议形式化模型,但由于缺乏时间上的语义,并不能解决新鲜性漏洞问题。另一方面,由于类型

全文目录

摘要  2-4
ABSTRACT  4-9
第一章绪言  9-17
  1.1 引言  9-10
  1.2 安全协议的原理与分类  10-12
    1.2.1 安全协议  10-11
    1.2.2 安全协议的类型  11
    1.2.3 安全性质  11-12
  1.3 安全协议形式化分析  12-14
    1.3.1 形式化分析的意义  12-13
    1.3.2 形式化分析概述  13-14
  1.4 安全协议形式化分析的自动工具  14-15
  1.5 本文主要工作  15-17
第二章安全协议的六种漏洞  17-22
  2.1 身份认证漏洞  17-18
  2.2 假冒攻击漏洞  18
  2.3 保密数据泄漏漏洞  18
  2.4 新鲜性漏洞  18-19
  2.5 类型攻击漏洞  19
  2.6 攻击者不当得利漏洞  19-22
第三章一般安全协议模型的增强  22-37
  3.1 一般安全协议模型（GSPM）  22-27
    3.1.1 GSPM 的消息空间及消息推理原理  22-24
    3.1.2 GSPM 的语法和语义  24
    3.1.3 GSPM 中定义的安全性质  24-25
    3.1.4 利用GSPM 分析安全协议  25-26
    3.1.5 GSPM 的不足  26-27
  3.2 新鲜性漏洞的检测  27-32
    3.2.1 新鲜性问题的产生  27-28
    3.2.2 新鲜性的形式化定义  28-30
    3.2.3 实例研究  30-32
  3.3 类型攻击漏洞的检测  32-37
    3.3.1 类型攻击漏洞的产生  32-33
    3.3.2 针对类型缺陷问题对GSPM 进行的改进  33-35
    3.3.3 实例研究  35-37
第四章安全协议自动验证工具GSPMC 的实现  37-48
  4.1 系统概述  37-39
  4.2 基于XML 的GSPM 语法解析  39-40
  4.3 消息推理的算法设计  40-41
  4.4 状态空间搜索树的结构设计  41-43
  4.5 安全性质的自动分析  43-44
  4.6 工具应用实例  44-48
第五章总结与展望  48-50
  5.1 本文工作总结  48
  5.2 未来工作展望  48-50
参考文献  50-54
附录：GSPMC 的输入规范（XML SCHEMA）  54-61
致谢  61-62
攻读学位期间发表的学术论文  62-64

安全协议的漏洞分析及自动验证工具

内容摘要

全文目录

相似论文