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

论文摘要

近年来,随着网络的普及及应用的推广,电子商务的使用得到了极大的发展,其可实现的功能也越来越全面,包括网络购物、网络支付、网络银行、电子订货等等。网络密码协议是保证电子商务公平性、安全性的有效技术,其中多方不可否认协议适用于当参与方多于两人时的网络交易,这也是电子商务不断发展的趋势和要求。多方不可否认协议分为含在线可信第三方、离线可信第三方及无可信·第三方三类,目前均出现了一些具有代表性的各类协议。本文选取了一个含离线可信第三方协议与一个无可信第三方协议,从公平性、协议消息交换方法及抵御攻击方面对协议进行改进并使用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工具的安装和使用,并对改进后的两个协议进行建模和验证。

论文目录

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