基于SVO逻辑的电子商务协议形式化分析与研究
发布时间：2023-01-06 09:38
电子商务协议形式化分析是电子商务研究的一个重要方面，电子商务协议是面向电子商务的密码协议，安全的电子商务协议是保证电子商务活动正常开展的基础。进行电子商务协议的形式化分析研究具有重大理论意义和现实的应用价值，是顺利开展电子商务应用的技术保障。 形式化的方法是分析安全协议的主要方法。目前已经有很多研究安全协议的理论和方法，其中比较著名的有可证明安全理论、BAN类逻辑以及模型检测和定理证明的方法等。 本文主要对基于逻辑的形式化方法与模型检测技术及其在电子商务协议形式化分析中的应用进行了系统研究，重点对SVO逻辑方法在电子商务协议时限性形式化分析中的应用进行了研究。总的来说，从理论到实践两个层面上研究了电子商务协议的形式化分析的相关技术。本文所做的工作、技术难点和创新之处如下： （1）首先从电子商务安全出发，对电子商务协议及其协议形式化分析的国内外研究现状进行了综述。 （2）研究了BAN逻辑和其相关形式化协议分析的方法、步骤，对BAN的公理规则进行了部分扩展。同时对SVO逻辑进行了部分扩展，使该逻辑可以分...
【文章页数】：70 页
【学位级别】：硕士
【文章目录】：
目录
摘要
Abstract
1 绪论
1.1 研究背景及意义
1.2 国内外研究现状
1.2.1 电子商务协议及其发展现状
1.2.2 安全协议形式化分析研究现状
1.3 主要研究内容
1.4 本文的组织结构
2 基于逻辑的电子商务协议分析方法
2.1 BAN逻辑
2.1.1 BAN逻辑概念
2.1.2 推理规则
2.1.3 BAN逻辑的优缺点
2.1.4 BAN逻辑的应用
2.1.5 BAN逻辑的扩展
2.2 SVO逻辑
2.2.1 SVO逻辑概念
2.2.2 推理规则
2.2.3 SVO逻辑分析步骤
2.2.4 SVO逻辑的语义
2.2.5 SVO逻辑优缺点
2.2.6 SVO逻辑的改进
3 模型检测及模型检测工具SPIN
3.1 模型检测
3.1.1 模型检测的过程
3.1.2 线性时态逻辑(LTL)
3.2 SPIN概述
3.2.1 SPIN的基本结构
3.2.2 SPIN的特征
3.3 SPIN建模语言Promela
3.3.1 简介
3.3.2 语句的可执行性
3.3.3 Promela变量和数据类型
3.3.4 进程
3.3.5 消息传递
3.3.6 控制流
3.3.7 语句类型
3.3.8 高级操作
3.4 SPIN的使用
3.4.1 SPIN的运行时参数
3.4.2 pan运行时参数和编译时参数
4 基于公钥的Kerberos协议改进和证明
4.1 Kerberos认证协议概述
4.1.1 工作原理
4.1.2 Kerberos协议的局限性
4.1.3 Kerberos协议的改进方案
4.2 用扩展BAN逻辑证明改进的Kerberos认证协议
4.2.1 协议理想化
4.2.2 证明目标
4.2.3 证明步骤
4.3 改进后的特性
5 基于NZG、ISI的电子货币支付协议证明
5.1 协议概述
5.1.1 NZG不可否认协议及其缺陷
5.1.2 ISI电子支付协议及其缺陷
5.1.3 改进后的电子货币支付协议
5.2 使用扩展后的SVO逻辑对新协议进行验证
5.2.1 协议初始化
5.2.2 协议目标
5.2.3 协议证明
5.3 使用SPIN对新协议进行模型检测
5.3.1 协议行为抽象
5.3.2 协议的Promela结构
5.3.3 协议主体的状态及行为描述
5.3.4 属性结果验证分析
6 结论与展望
致谢
主要参考文献
附录
【参考文献】：
期刊论文
[1]一个非否认协议ZG的形式化分析[J]. 范红,冯登国. 电子学报. 2005(01)
[2]安全协议20年研究进展[J]. 卿斯汉. 软件学报. 2003(10)
[3]Kerberos身份认证协议分析及改进[J]. 张红旗,车天伟,李娜. 计算机应用. 2002(12)
博士论文
[1]电子商务协议形式化方法及模型检测技术的研究与应用[D]. 文静华.贵州大学 2006
硕士论文
[1]SPIN模型检测的研究与应用[D]. 王巧丽.贵州大学 2006
[2]网络安全协议的形式化描述与验证[D]. 代新敏.重庆大学 2004
[3]安全协议形式化验证方法和安全协议设计研究[D]. 侯峻峰.清华大学 2004
[4]安全协议形式化分析及其应用[D]. 刘学锋.湘潭大学 2004
[5]形式化逻辑方法在分析认证协议以及电子商务协议中的应用[D]. 何加亮.吉林大学 2004
[6]基于逻辑的电子商务协议属性的分析与研究[D]. 边培泉.兰州理工大学 2004
本文编号：3728104
【文章页数】：70 页
【学位级别】：硕士
【文章目录】：
目录
摘要
Abstract
1 绪论
1.1 研究背景及意义
1.2 国内外研究现状
1.2.1 电子商务协议及其发展现状
1.2.2 安全协议形式化分析研究现状
1.3 主要研究内容
1.4 本文的组织结构
2 基于逻辑的电子商务协议分析方法
2.1 BAN逻辑
2.1.1 BAN逻辑概念
2.1.2 推理规则
2.1.3 BAN逻辑的优缺点
2.1.4 BAN逻辑的应用
2.1.5 BAN逻辑的扩展
2.2 SVO逻辑
2.2.1 SVO逻辑概念
2.2.2 推理规则
2.2.3 SVO逻辑分析步骤
2.2.4 SVO逻辑的语义
2.2.5 SVO逻辑优缺点
2.2.6 SVO逻辑的改进
3 模型检测及模型检测工具SPIN
3.1 模型检测
3.1.1 模型检测的过程
3.1.2 线性时态逻辑(LTL)
3.2 SPIN概述
3.2.1 SPIN的基本结构
3.2.2 SPIN的特征
3.3 SPIN建模语言Promela
3.3.1 简介
3.3.2 语句的可执行性
3.3.3 Promela变量和数据类型
3.3.4 进程
3.3.5 消息传递
3.3.6 控制流
3.3.7 语句类型
3.3.8 高级操作
3.4 SPIN的使用
3.4.1 SPIN的运行时参数
3.4.2 pan运行时参数和编译时参数
4 基于公钥的Kerberos协议改进和证明
4.1 Kerberos认证协议概述
4.1.1 工作原理
4.1.2 Kerberos协议的局限性
4.1.3 Kerberos协议的改进方案
4.2 用扩展BAN逻辑证明改进的Kerberos认证协议
4.2.1 协议理想化
4.2.2 证明目标
4.2.3 证明步骤
4.3 改进后的特性
5 基于NZG、ISI的电子货币支付协议证明
5.1 协议概述
5.1.1 NZG不可否认协议及其缺陷
5.1.2 ISI电子支付协议及其缺陷
5.1.3 改进后的电子货币支付协议
5.2 使用扩展后的SVO逻辑对新协议进行验证
5.2.1 协议初始化
5.2.2 协议目标
5.2.3 协议证明
5.3 使用SPIN对新协议进行模型检测
5.3.1 协议行为抽象
5.3.2 协议的Promela结构
5.3.3 协议主体的状态及行为描述
5.3.4 属性结果验证分析
6 结论与展望
致谢
主要参考文献
附录
【参考文献】：
期刊论文
[1]一个非否认协议ZG的形式化分析[J]. 范红,冯登国. 电子学报. 2005(01)
[2]安全协议20年研究进展[J]. 卿斯汉. 软件学报. 2003(10)
[3]Kerberos身份认证协议分析及改进[J]. 张红旗,车天伟,李娜. 计算机应用. 2002(12)
博士论文
[1]电子商务协议形式化方法及模型检测技术的研究与应用[D]. 文静华.贵州大学 2006
硕士论文
[1]SPIN模型检测的研究与应用[D]. 王巧丽.贵州大学 2006
[2]网络安全协议的形式化描述与验证[D]. 代新敏.重庆大学 2004
[3]安全协议形式化验证方法和安全协议设计研究[D]. 侯峻峰.清华大学 2004
[4]安全协议形式化分析及其应用[D]. 刘学锋.湘潭大学 2004
[5]形式化逻辑方法在分析认证协议以及电子商务协议中的应用[D]. 何加亮.吉林大学 2004
[6]基于逻辑的电子商务协议属性的分析与研究[D]. 边培泉.兰州理工大学 2004
本文编号：3728104
本文链接：https://www.wllwen.com/shekelunwen/ljx/3728104.html