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

基于SVO逻辑的多方不可否认协议的形式化分析与研究

作　者: 王远敏
导　师: 汪学明
学　校: 贵州大学
专　业: 计算机应用技术
关键词: 多方不可否认协议 SVO逻辑 CMOCHA 模型检测
分类号: TP393.08
类　型: 硕士论文
年　份: 2009年
下　载: 7次
引　用: 0次
阅　读: 论文下载
 

内容摘要


近年来,随着网络的普及及应用的推广,电子商务的使用得到了极大的发展,其可实现的功能也越来越全面,包括网络购物、网络支付、网络银行、电子订货等等。网络密码协议是保证电子商务公平性、安全性的有效技术,其中多方不可否认协议适用于当参与方多于两人时的网络交易,这也是电子商务不断发展的趋势和要求。多方不可否认协议分为含在线可信第三方、离线可信第三方及无可信·第三方三类,目前均出现了一些具有代表性的各类协议。本文选取了一个含离线可信第三方协议与一个无可信第三方协议,从公平性、协议消息交换方法及抵御攻击方面对协议进行改进并使用SVO逻辑和MOCHA模型检测工具对改进后的协议进行验证。多数多方不可否认协议都是通过SVO逻辑来进行形式化的分析,SVO逻辑是BAN类逻辑中用于形式化分析网络安全协议的可靠工具之一,它拥有推理协议属性的所有公理和规则,与GNY、AT、VO逻辑相比更为简单,表达的含义更为准确,成为继BAN逻辑之后,分析协议安全性的一个比较完善的形式化验证方法。原始SVO逻辑在论证消息的发送时间点上存在不足,因此本文引用了针对相关时间论证的扩展SVO逻辑对协议进行验证和改进。同时,本文研究了模型检测工具的CMOCHA版本,从安装方法、常用参数及模型建立方法等方面论述了MOCHA工具在协议验证中的应用,最后使用CMOCHA对改进后的协议进行模型验证。本文具体的工作如下：(1)分析多方不可否认协议及其发展现状,并对多方不可否认协议涉及的各种加密技术进行研究。(2)分析多方不可否认协议在公平性、安全性、保密性及抵御重放攻击性方面的要求。选取了一个含离线可信第三方的多方不可否认协议和一个无可信第三方的多方不可否认协议,对其进行改进,以满足多方不可否认协议的各方面要求。(3)研究形式化分析工具SVO逻辑的语义、语法规则及推导方法,SVO逻辑在时间点论证方面的扩展语法规则,并使用SVO逻辑对改进后的两个协议进行形式化分析论证。(4)研究模型检测工具MOCHA的安装配置、常用参数命令及使用方法。在MOCHA的两个版本中,CMOCHA版本可以使用ATL时序逻辑语言建立协议模型对协议进行检测。本文研究了CMOCHA工具的安装和使用,并对改进后的两个协议进行建模和验证。

全文目录


摘要  5-7
Abstract  7-9
第一章 绪论  9-16
  1.1 研究背景及意义  9-10
  1.2 国内外研究现状  10-13
    1.2.1 多方不可否认协议及其发展现状  10-12
    1.2.2 安全协议分析方法的研究现状  12-13
  1.3 主要研究内容  13-14
  1.4 本文的组织结构  14-16
第二章 协议加密的相关技术  16-26
  2.1 对称密码体制  16-18
    2.1.1 Feistel密码结构  16-17
    2.1.2 Feistel依赖的参数  17-18
  2.2 公钥密码体制  18-21
    2.2.1 公钥密码体制的算法  18-20
    2.2.2 RSA密码  20-21
  2.3 数字签名  21-23
    2.3.1 数字签名的基本概念  21-22
    2.3.2 DSS签名标准  22-23
    2.3.3 数字签名的应用  23
  2.4 组加密方案  23
  2.5 组播的原理  23-25
  2.6 签密技术  25-26
第三章 多方不可否认协议形式化分析方法  26-44
  3.1 SVO逻辑  26-33
    3.1.1 SVO逻辑概念  26-28
    3.1.2 SVO逻辑的公理及推理规则  28-30
    3.1.3 基于SVO逻辑的协议分析步骤  30-31
    3.1.4 SVO逻辑语义的计算模型  31-32
    3.1.5 SVO逻辑优缺点  32
    3.1.6 SVO逻辑的改进  32-33
  3.2 ATS与ATL  33-38
    3.2.1 交替转换系统ATS  33-34
    3.2.2 时间交替时序逻辑ATL  34-38
  3.3 验证工具MOCHA  38-44
    3.3.1 MOCHA的特点  38-39
    3.3.2 MOCHA模型检测原理  39-41
    3.3.3 MOCHA运行参数  41-44
第四章 含可信第三方的多方不可否认协议形式化分析研究  44-58
  4.1 协议改进  44-45
  4.2 协议目标分析  45-46
  4.3 基于SVO逻辑的形式化分析  46-48
    4.3.1 协议前提  46-47
    4.3.2 协议目标  47
    4.3.3 证明过程  47-48
  4.4 协议的MOCHA模型验证  48-58
第五章 无可信第三方的多方不可否认协议形式化分析研究  58-71
  5.1 协议改进  58-60
  5.2 协议目标分析  60
  5.3 基于SVO逻辑的形式化分析  60-62
    5.3.1 协议前提  60-61
    5.3.2 协议目标  61
    5.3.3 证明过程  61-62
  5.4 协议的MOCHA模型验证  62-71
第六章 工作总结与展望  71-73
  6.1 工作总结  71-72
  6.2 下一步工作展望  72-73
致谢  73-74
主要参考文献  74-77
附录  77-78

相似论文

  1. 基于BMC的Web服务失配检测方法研究,TP311.52
  2. 端到端的信息安全传输系统关键技术研究,TP393.08
  3. 内部网络威胁模型与检测技术,TP393.08
  4. 防御DDoS攻击的新型密钥交换协议研究,TP393.08
  5. 二元判断图BDD及其JAVA实现的应用与研究,TP311.52
  6. 硬件系统SystemC～（FL）设计模型的SPIN验证,TP368.1
  7. 基于无穷模型命题投影时序逻辑的模型检查,TP311.11
  8. 保密以太网卡密钥协商协议的研究,TP393.11
  9. 印刷品质量在线检测机器视觉系统的设计与实现,TS803
  10. 计算机辅助检测规划系统的研究,F270.7
  11. 可拓检测技术研究,TP274
  12. 框架时序逻辑程序设计解释器及模型检测工具,TP311.52
  13. 基于SPIN的命题投影时序逻辑模型检查,TP311.52
  14. 基于SPIN的UML活动图验证,TP311.52
  15. 鉴别协议的分析研究,TP393.08
  16. 基于免疫原理的网络入侵检测器生成算法及其模型研究,TP393.08
  17. SOC异步互联技术研究,TN47
  18. 基于Petri网的on-the-fly模型检测,TP301.1
  19. 电子商务协议的形式化分析,F713.36
  20. 一种Web服务组合的自动化模型检测方法,TP393.09

中图分类: > 工业技术 > 自动化技术、计算机技术 > 计算技术、计算机技术 > 计算机的应用 > 计算机网络 > 一般性问题 > 计算机网络安全
© 2012 www.xueweilunwen.com