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

特殊环境下的协议安全研究

作　者: 高长喆
导　师: 陈克非
学　校: 上海交通大学
专　业: 计算机系统结构
关键词: 安全协议形式化方法自动工具挑战-应答协议
分类号: TP393.08
类　型: 硕士论文
年　份: 2007年
下　载: 47次
引　用: 1次
阅　读: 论文下载

内容摘要

随着Internet技术的发展,安全协议在电子商务和电子政务中的应用越来越多。与此相应的就是人们对协议的安全性更加关注,尤其是在特殊环境下如何建模和分析安全协议显得尤为重要。本文首先研究和分析了现有的安全协议的建模和分析方法,找出其中的优势和不足。考虑环境的特殊性,选用符合标准的基于事件的GSPML语言对广义的挑战-应答协议和TLS握手协议的简化版本建立了可视化的模型。在此基础上,本文对广义的挑战-应答协议的安全条件进行了分析,列出了在对称密码体制和非对称密码体制下挑战-应答协议需要满足的安全条件,以及不满足这些条件将会导致的攻击和与之相应的协议认证性的缺失。值得注意的是,在两种密码体制下挑战-应答协议在最小形式上是有所区别的。然后,作者对传统认为的三轮认证协议进行了分析,认为在有主动攻击者存在的情况下,单纯的认证协议无法完全保证认证的目的。此外,本文对四种形式化方法的自动工具进行了分析,这些工具涵盖了形式化分析方法的三大流派。作者主要从用户界面和易用性,运行状态数和时间,数据独立性和离散时间支持,协议错误的发现能力这四个方面进行比较,并给出了综合能力的结论。

全文目录

摘要  2-3
ABSTRACT  3-10
1 绪论  10-14
  1.1 背景介绍  10-11
  1.2 研究内容及主要工作  11-12
  1.3 论文的内容  12-14
2 安全协议的建模和分析方法概述  14-27
  2.1 安全协议的建模方法  14-16
  2.2 安全协议的分析方法  16-23
  2.3 安全协议的自动化分析工具  23-26
  2.4 本章小结  26-27
3 特殊环境下的安全协议建模  27-34
  3.1 特殊环境的定义  27-28
  3.2 针对广义的挑战-应答协议等的模型建立  28-31
  3.3 模型分析  31-33
  3.4 本章小结  33-34
4 协议分析与模型检测  34-55
  4.1 无第三方参与的认证协议的分析  34-41
  4.2 有第三方参与的认证协议的分析  41-44
  4.3 对于密码学中认证性的一些讨论  44-46
  4.4 形式化方法自动工具的深入研究  46-53
  4.5 本章小结  53-55
5 总结与展望  55-57
  5.1 本文的工作总结  55
  5.2 今后的工作  55-57
参考文献  57-61
附录  61-65
致谢  65-66
攻读学位期间发表的学术论文  66-69

特殊环境下的协议安全研究

内容摘要

全文目录

相似论文