一、Netbill协议原子性的符号模型检验分析（论文文献综述）
崔凯[1]（2020）在《嵌入式软件形式化建模与测试方法研究》文中指出航天软件评测中心统计数据表明航天领域大型实时嵌入式软件故障80%是由中断嵌套引起的,而中断嵌套产生的原子性违背（Atomic Violation）问题至今没得到有效解决;基于多核CPU的嵌入式软件由于多线程交织导致数据竞争（Data Race）问题以及运行结果随机而难以保证其可信性,不得不采用多个单核CPU通过网络通信避免数据竞争问题,这势必影响多核CPU在航天领域的应用;针对这类实时嵌入式软件测试,存在测试用例数量庞大问题,难以评估其可信性。本文从以下几方面开展研究,解决上面提出的几个亟待解决的问题:针对中断嵌套引起的原子性违背问题,本文提出瘦中断处理（Re-Engineering Interrupt Processing）的状态变迁矩阵（State Transition Matrix,STM）模型用于解决中断嵌套引发的原子性违背问题,即把中断处理程序中访问共享变量的程序块移植到主程序STM中,而中断处理程序仅负责将外部中断请求数据存到缓冲区当中,由主程序STM完成中断处理及中断嵌套功能,从而有效解决了原子性违背问题。针对多线程交织引发原子性侵犯和数据竞争问题,提出基于STM的多线程访问控制与访问分离方法:首先建立多线程的STM模型,为了验证多线程模型,通常采用集成的方法进行验证,但容易造成状态空间爆炸,因此,提出控制-访问分离方法,即将各个STM中访问共享变量的控制逻辑集成到一个独立的STM中,最终实现共享变量的控制与访问分离,只需要对控制STM进行验证,这样可以解决多线程验证的状态空间爆炸问题。针对嵌入式软件实时性集成测试用例生成问题,提出层次模型的时间约束和循环约束的集成测试方法。本方法通过对待测系统进行层次化模型的设计,并建立针对规模大结构复杂的软件系统实时性的测试方法,通过增加测试用例的结构复杂度,最终生成比待测模型更为复杂的正则测试用例串,从而找出隐藏较深的软件功能问题。针对复杂软件集成测试的模型划分和用例化简问题,提出模型结构分解方法与测试优化方法。通过对待测软件整体功能的有限状态自动机（FSM）对应的有向图进行结构分解,对分解后的子模型先进行功能测试,根据模型有向图的连通特征以及语义网络的语义特征进行状态聚类,并生成相应的测试用例,然后对系统进行组合测试,进而发现更深层次的错误。最后,利用上述研究方法在航天控制系统中得到实际应用,有效解决数据竞争和原子性违背等问题。在智能电视,电机控制等实际应用中对实时的结构复杂的大型软件进行集成测试,找出隐藏较深的缺陷。经过验证后,发现多状态机模型的验证问题以及对于同类型系统普适性测试问题,将在以后解决。
肖茵茵,苏开乐[2]（2014）在《电子商务支付协议认证性的SVO逻辑验证》文中指出与证伪法（如模型检测）相比,采用证真法（如定理证明和逻辑推理）能验证协议在任意会话中的正确性,但分析难度较高,验证过程较为复杂。使用SVO逻辑方法,以Netbill微支付协议为例,对电子商务支付协议的认证性进行形式化分析。扩展了SVO逻辑的公理集;在不影响Netbill协议安全性的前提下,为其建立了简化模型;针对协议特点,修正和补充了其验证目标;给出了比之前更合理的协议假设,展示了具体的推理过程,分析了验证结果。结果表明,Netbill协议基本满足认证性。最后对相关研究工作进行了比较。
常寅龙[3]（2013）在《电子商务协议的形式化分析与漏洞检测》文中研究说明电子商务安全协议,为电子商务活动提供一系列的安全保护工作,是整个系统安全体系的核心。电子商务安全协议除需要提供保密性、认证性等一般安全性质外,通常还需要满足原子性、匿名性以及不可否认性等多种特性。因此,电子商务安全协议的设计与安全检测是目前的研究热点与难点。研究某种方法能准确高效的发现协议中的安全问题,并对检测出的漏洞进行有效的分析和修复,对于电子商务协议的安全运行至关重要。本文围绕电子商务安全协议的形式化分析与协议漏洞检测开展研究工作,主要工作与创新点为：1.在介绍基于CSP的模型检测工具FDR以及建模工具Casper的基础上,对Caper/FDR中攻击者的能力以及系统中产生的攻击者模型进行了描述和分析；2.将Casper/FDR2模型检测方法运用到电子商务领域的研究分析中,找到了多个电子商务协议的漏洞,并提出了具体的改进方案；3.在给出电子商务协议原子性的两个扩展特性的基础上,提出了运用CSP建模方式对交易协议的扩展原子性进行形式化分析方法,建立了非常规状态的系统模型,并运用FDR对建立的CSP模型进行检测,对于实验中发现的协议漏洞,提出了改进方案；4.在基于CSP的安全协议匿名性理论基础上,提出了一套对于电子商务协议匿名性的形式化分析方法,给出了适用于CSP/FDR模型检测技术的建模框架,并通过对一个电子商务协议进行实验描述了具体的建模分析过程。本文研究成果表明：以CSP理论框架为基础,运用相应的模型检测工具Casper和FDR2,通过有限自动机结构对电子商务协议中的所有状态集合进行检测,可有效测试与发现电子商务协议中保密性、认证性和匿名性等重要特性的满足情况,对保障电子商务系统的安全高效运行具有重要意义。
肖仕成,李开,甘早斌[4]（2012）在《基于四方的安全电子商务支付协议分析与验证》文中研究说明以基于四方的安全电子商务支付协议为研究对象,建立了协议的有限状态模型以及安全计算树逻辑CTL公式,利用符号模型检测工具SMV对协议的原子性进行检测验证。验证结果证明,基于四方的安全电子商务支付协议满足电子支付的金钱原子性、商品原子性以及确认发送原子性,协议符合电子支付的原子性安全要求。
肖仕成[5]（2011）在《基于四方的安全电子商务支付协议研究》文中提出随着Internet的发展和电子商务的迅速普及,电子商务支付的安全越来越受到人们的重视,尤其是电子支付的原子性,已成为了电子商务领域的研究热点之一。关于电子支付的原子性,从目前的研究成果来看,大多数的电子商务支付协议仅局限于满足电子支付的金钱原子性,对于商品原子性和确认发送原子性,专家学者的研究重点也只仅仅在于如何解决数字商品的商品原子性和确认发送原子性,而对于满足传统商品的电子支付商品原子性和确认发送原子性的支付协议方面的研究成果,尚未见有关文献报道。在分析国内外电子支付的支付模式和支付协议现状基础上,重点研究国际电子商务支付协议标准安全电子交易SET（Secure Electronic Transaction）协议及其存在的缺陷,比较分析了国内外学者对SET的改进方案。以SET协议为范型,针对其不能满足商品原子性和确认发送原子性的缺陷,进行了一些改进,建立了一个基于四方的能够自动存取关键电子证据、确保商品原子性和确认发送原子性、仲裁处理交易纠纷的安全电子商务支付协议,并给出了协议的形式化描述,然后对基于四方的电子商务支付协议的安全性进行了分析比较。根据基于四方的安全电子商务支付协议,建立了协议的有限状态模型和安全计算树逻辑CTL （Computation Tree Logic）公式,利用国际上流行的协议检测工具符号模型检测SMV（symbolic model checking）对协议的安全原子性进行了仿真实验检测验证,实验验证了协议满足电子交易的安全原子性要求。基于四方的安全电子商务支付协议跟SET协议一样,仅适用于信用卡的电子商务支付。针对协议仅适用于信用卡支付的缺陷,扩展其数据结构,设计适用于借记卡支付的功能,并用ASN.1抽象语法标记（Abstract Syntax Notation One）对其数据结构进行描述,最后对电子商务支付系统软件模块进行简要设计。
王兵[6]（2007）在《电子商务协议的形式化分析》文中认为电子商务协议的安全性、原子性、不可否认性等性质的验证的方法一直制约着电子商务的发展。形式化分析技术可使协议设计者通过系统分析将注意力集中于接口、系统环境的假设、在不同条件下系统的状态、条件不满足时出现的情况以及系统不变的属性,并通过系统验证,提供协议必要的安全保证。目前,国内外形式化研究安全协议主要有基于知识与信念推理的模态逻辑方法,基于定理证明的方法和基于攻击的结构性方法三种。电子商务协议作为安全协议的一部分,这些方法在电子商务协议中同样有效。本论文应用形式化方法对电子商务协议进行分析,工作如下;1.概述了电子商务协议的发展过程以及在此发展过程中运用的加密方式和形式化方法。2.分析了电子商务协议的安全性质,如匿名性、原子性、不可否认性等,并给出了实例分析。3.在对电子商务协议安全性质全面分析的基础上,设计了一个安全的电子商务协议。该协议满足钱原子性、商品原子性以及不可否认性,最后对协议进行了详细分析。
孙守卿[7]（2006）在《基于模型检测工具SPIN的安全协议分析和验证》文中研究说明随着Internet和分布式系统的广泛应用,安全协议逐渐发挥着越来越重要的作用。形式化的方法是分析安全协议的主要方法。目前已经有很多研究安全协议的理论和方法,其中比较着名的有可证明安全理论、BAN逻辑、串空间模型理论以及模型检测和定理证明的方法等。 模型检测作为形式化分析安全理论方法的一种,有着自动化和提供反例等诸多优点。并且近年在硬件验证中得到了广泛应用。模型检测器SPIN是由贝尔实验室开发的一种专门用于软件和协议验证的工具。 本文基于模型检测工具SPIN,对电子商务协议Netbill协议做形式化地分析和验证。 首先对此协议从行为属性和安全性两方面进行抽象。包括对协议主体建立状态和状态转移描述;然后对协议采用PROMELA语言建立模型。协议的安全属性描述采用LTL逻辑公式。最后运用SPIN对协议的模型进行行为模拟,对LTL描述的协议属性进行正确性及安全性验证。在验证和模拟的过程中,随时根据模型的状态数目和系统的消耗调整抽象模型的结构和行为。对协议中不满足属性的验证结果进行分析和改进。最后,将分析和验证结果和其他安全协议的验证方法比较,总结现有工作和尚需完善的工作。
刘霞[8]（2006）在《移动电子商务协议的模型检验分析与设计研究》文中认为目前,全球移动电子商务呈现异常强劲的势头,我国移动电子商务也在迅速发展。用户使用移动电子商务时最关心的是安全问题,而移动电子商务协议的安全是保证移动电子商务安全的一个重要方面。移动电子商务协议是一类特殊的电子商务协议,与传统电子商务协议相比,由于移动装置和无线网络的特点,移动电子商务协议的执行环境更为复杂,从而使其更容易存在安全缺陷,同时也为其形式化分析与设计带来了新的挑战。本文主要研究了移动电子商务协议（包括无线认证协议,因为无线认证协议是移动电子商务协议的基础）的模型检验分析与设计,所取得的主要研究成果有:（1）应用模型检验方法对无线认证协议Server-specific MAKEP进行分析,借助模型检验工具SMV,成功地找到了协议存在的认证性缺陷,并对该缺陷所产生的影响进行了讨论;（2）针对Server-specific MAKEP协议存在的认证性缺陷,给出了协议的一种改进,并对改进后的协议再次进行模型检验分析,分析结果表明协议达到了安全要求;（3）针对移动电子商务协议,提出了一种基于有限状态机的建模方法;应用该方法,以一个典型的移动支付协议KSL为例进行模型检验分析;在检测出协议存在的公平性缺陷之后,给出了协议的一种改进;（4）针对移动装置和无线网络的特点,设计了一种移动环境公平支付协议,并对协议的公平性、保密性、时间性等性质进行模型检验分析,验证了其可行性。
刘宏有[9]（2006）在《加入有效期的无可信第三方的多银行电子现金协议研究》文中进行了进一步梳理电子商务正在以爆炸性的速度发展,其最终目标是实现商务活动各环节的电子化。但是真正进行电子支付、开展电子交易的仍然比较少,电子商务的一个核心问题是支付问题,如何安全、公平并且保护用户隐私的电子交易是决定电子商务发展的关键问题。解决这些问题的关键技术就是电子现金技术,本文的目标是在椭圆曲线密码体制的基础之上,研究如何表示支付中的电子现金表示问题,并根据现存的多银行现象,研究如何实现一个适用于多银行的满足原子性和公平匿名性的电子交易协议。本文的主要内容包括:（1）综述了密码技术的相关知识,分析了电子交易中的核心技术,介绍了公钥基础设施的结构模型和功能。（2）综述了电子现金系统匿名性控制的发展历史、研究现状,分析了电子交易协议中银行数据库的效率问题,提出在电子现金中加入有效期可大大提高银行效率,采用无可信第三方的方式可以在降低系统负担的同时实现电子现金的可撤销匿名性。（3）给出了基于限制性群盲签名技术的加入有效期的无可信第三方电子现金方案。并据此提出了一个多银行的电子交易协议,这个协议同时实现了很好的原子性和公平匿名性,然后详细描述了整个协议的过程。（4）对提出的电子交易协议进行了分析,非形式化的证明了协议的原子性、可撤销匿名性、安全性,然后分析了协议的效率。本文分析了椭圆曲线密码体制,给出了如何用椭圆曲线密码体制表示数字签名,并给出了相应的电子现金系统,基于限制性群盲签名的电子现金系统保证了多银行的电子交易协议的有效实现。
董荣胜,郭云川,古天龙[10]（2005）在《一种电子商务协议原子性的模型检验分析方法》文中研究指明提出了一个分析电子商务协议的形式化模型,介绍了基于该模型的电子商务协议原子性的描述方法。同其他模型相比,该模型能较好地分析具有多个实例并发运行时电子商务协议的原子性。最后基于该模型,用符号模型检验工具（SMV）分析了Digicash协议和Netbill协议。
二、Netbill协议原子性的符号模型检验分析（论文开题报告）
（1）论文研究背景及目的
此处内容要求：
首先简单简介论文所研究问题的基本概念和背景，再而简单明了地指出论文所要研究解决的具体问题，并提出你的论文准备的观点或解决方法。
写法范例：
本文主要提出一款精简64位RISC处理器存储管理单元结构并详细分析其设计过程。在该MMU结构中,TLB采用叁个分离的TLB,TLB采用基于内容查找的相联存储器并行查找,支持粗粒度为64KB和细粒度为4KB两种页面大小,采用多级分层页表结构映射地址空间,并详细论述了四级页表转换过程,TLB结构组织等。该MMU结构将作为该处理器存储系统实现的一个重要组成部分。
（2）本文研究方法
调查法：该方法是有目的、有系统的搜集有关研究对象的具体信息。
观察法：用自己的感官和辅助工具直接观察研究对象从而得到有关信息。
实验法：通过主支变革、控制研究对象来发现与确认事物间的因果关系。
文献研究法：通过调查文献来获得资料，从而全面的、正确的了解掌握研究方法。
实证研究法：依据现有的科学理论和实践的需要提出设计。
定性分析法：对研究对象进行“质”的方面的研究，这个方法需要计算的数据较少。
定量分析法：通过具体的数字，使人们对研究对象的认识进一步精确化。
跨学科研究法：运用多学科的理论、方法和成果从整体上对某一课题进行研究。
功能分析法：这是社会科学用来分析社会现象的一种方法，从某一功能出发研究多个方面的影响。
模拟法：通过创设一个与原型相似的模型来间接研究原型某种特性的一种形容方法。
三、Netbill协议原子性的符号模型检验分析（论文提纲范文）
（1）嵌入式软件形式化建模与测试方法研究（论文提纲范文）
| 摘要 |
| ABSTRACT |
| 主要符号表 |
| 1 绪论 |
| 1.1 研究背景与意义 |
| 1.2 国内外相关工作研究进展 |
| 1.3 本文主要工作与章节安排 |
| 1.4 本文创新点 |
| 2 有限状态自动机与STM形式化定义 |
| 2.1 状态变迁矩阵定义 |
| 2.2 有限状态自动机概念 |
| 2.3 本章小结 |
| 3 基于STM并发程序建模研究 |
| 3.1 并发程序的缺陷问题分析 |
| 3.2 中断嵌套引发原子性违背的解决方法 |
| 3.2.1 基于STM的嵌入式软件中断建模 |
| 3.2.2 多级中断嵌套建模方法 |
| 3.3 线程交织引发数据竞争的解决方法 |
| 3.3.1 多线程全局变量读/写规则 |
| 3.3.2 全局变量无关程序语句剪枝规则 |
| 3.3.3 解决原子性违背的信号量通信与访问控制分离方法 |
| 3.4 瘦中断处理模型仿真实验分析 |
| 3.5 解决原子性违背的形式化模型建立 |
| 3.5.1 信号量法与控制-访问分离法对比分析 |
| 3.5.2 建模方法对比分析 |
| 3.6 本章小结 |
| 4 复杂嵌入式软件多属性一体化测试方法 |
| 4.1 问题描述 |
| 4.2 正则表达式扩充定义 |
| 4.3 带有闭包循环正则式用例生成策略 |
| 4.3.1 记忆性正则表达式转化方法 |
| 4.3.2 基于圈复杂度的循环边界方法 |
| 4.3.3 状态机网络节点介数的测试入口选择 |
| 4.4 带有时间属性的正则表达式用例生成策略 |
| 4.4.1 基于时间复杂度的函数执行时间估算方法 |
| 4.4.2 测试用例最坏执行时间估算 |
| 4.5 正则表达式用例测试用例优化方法 |
| 4.5.1 函数路径的组合测试方法 |
| 4.5.2 用例文本选取优化方法 |
| 4.6 实例分析 |
| 4.7 本章小结 |
| 5 基于结构分解的嵌入式软件测试方法 |
| 5.1 问题描述 |
| 5.2 模型的组合测试方法 |
| 5.3 结构模型分解 |
| 5.3.1 非强连通模型分解方法 |
| 5.3.2 强连通模型分解方法 |
| 5.4 最小正则表达式测试用例生成方法 |
| 5.5 实例分析 |
| 5.6 本章小结 |
| 6 结论与展望 |
| 6.1 结论 |
| 6.2 展望 |
| 参考文献 |
| 附录A |
| 附录B |
| 附录C |
| 附录D |
| 攻读博士学位期间科研项目及科研成果 |
| 致谢 |
| 作者简介 |
（3）电子商务协议的形式化分析与漏洞检测（论文提纲范文）
| 中文摘要 |
| Abstract |
| 第一章 绪论 |
| 1.1 研究背景与意义 |
| 1.1.1 电子商务发展现状 |
| 1.1.2 对电子商务协议分析的意义 |
| 1.1.3 国内外研究现状 |
| 1.2 主要工作 |
| 1.3 本文章节安排 |
| 1.4 小结 |
| 第二章 电子商务协议简介 |
| 2.1 安全电子商务协议概述 |
| 2.1.1 电子商务协议运行环境中的主要角色 |
| 2.1.2 安全电子商务协议的主要特性 |
| 2.1.3 Digicash电子商务协议 |
| 2.2 安全电子商务协议的缺陷 |
| 2.2.1 常见攻击手段 |
| 2.2.2 利用协议设计漏洞的攻击 |
| 2.3 新的潜在安全威胁 |
| 2.4 小结 |
| 第三章 基于CSP方法的模型检测技术 |
| 3.1 安全协议的形式化分析基础 |
| 3.1.1 模态逻辑技术 |
| 3.1.2 模型检测技术 |
| 3.1.3 定理证明技术 |
| 3.2 CSP简介 |
| 3.2.1 CSP中常用操作符 |
| 3.2.2 进程 |
| 3.2.3 CSP中的迹模型 |
| 3.2.4 一个简单的CSP系统模型 |
| 3.3 基于CSP的模型检测工具 |
| 3.3.1 FDR |
| 3.3.2 Casper |
| 3.4 Casper/FDR中的攻击者模型 |
| 3.4.1 攻击者能力分析 |
| 3.4.2 具有攻击者的系统模型 |
| 3.4.3 入侵者建模 |
| 3.5 小结 |
| 第四章 基于CASPER/FDR2的电子商务协议形式化分析研究 |
| 4.1 协议背景 |
| 4.2 注册协议建模和分析 |
| 4.2.1 注册协议 |
| 4.2.2 注册协议的Casper建模 |
| 4.2.3 检测结果及分析 |
| 4.3 对注册协议的改进 |
| 4.4 小结 |
| 第五章 电子商务协议扩展原子性的分析验证 |
| 5.1 电子商务协议原子性的扩展 |
| 5.1.1 接收验证原子性 |
| 5.1.2 撤销交易原子性 |
| 5.2 建立协议的CSP模型 |
| 5.2.1 交易协议 |
| 5.2.2 定义协议的运行环境 |
| 5.2.3 定义协议数据、通信信道和进程 |
| 5.2.4 对交易实体及系统整体进行建模 |
| 5.2.5 建立协议目标声明 |
| 5.2.6 协议的非常规状态模型 |
| 5.3 FDR模型检测 |
| 5.3.1 FDR检测 |
| 5.3.2 检测结果调试 |
| 5.4 协议原子性目标分析 |
| 5.4.1 接收验证原子性分析 |
| 5.4.2 撤销交易原子性分析 |
| 5.5 协议改进 |
| 5.6 小结 |
| 第六章 电子商务协议强匿名性分析验证 |
| 6.1 基于CSP模型的协议匿名性分析理论基础 |
| 6.1.1 匿名性定义 |
| 6.1.2 观察者模型 |
| 6.2 改进的电子商务协议匿名性形式化分析框架 |
| 6.2.1 电子商务协议匿名性要求 |
| 6.2.2 电子商务协议匿名性模型框架 |
| 6.3 电子商务协议的匿名性模型建立 |
| 6.3.1 协议环境建模 |
| 6.3.2 参与实体建模 |
| 6.3.3 匿名性目标建模 |
| 6.4 结果验证和分析 |
| 6.4.1 协议观察者 |
| 6.4.2 模型检测结果和分析 |
| 6.4.3 内部观察者模型检测和分析 |
| 6.5 小结 |
| 第七章 总结和展望 |
| 7.1 总结 |
| 7.2 展望 |
| 参考文献 |
| 致谢 |
| 个人简历、在读期间研究成果以及发表的学术论文 |
（4）基于四方的安全电子商务支付协议分析与验证（论文提纲范文）
| 1 引言 |
| 2 SMV符号模型检测 |
| 3 基于四方的安全电子商务支付协议SMV分析建模 |
| 3.1 基于四方的安全电子商务支付协议形式化模型描述 |
| 3.1.1 基于四方的安全电子商务支付协议的主协议消息描述 |
| 3.1.2 基于四方的安全电子商务支付协议的换货协议消息描述 |
| 3.1.3 基于四方的安全电子商务支付协议的退货协议消息描述 |
| 3.1.4 基于四方的安全电子商务支付协议的纠纷处理协议消息描述 |
| 3.2 基于四方的安全电子商务支付协议的有限状态模型 |
| 3.2.1 客户C的有限状态模型 |
| 3.2.2 商家M的有限状态模型 |
| 3.2.3 支付机构P的有限状态模型 |
| 3.2.4 第四方W的有限状态模型 |
| 4 基于四方的安全电子商务支付协议的CTL原子性属性描述 |
| 4.1 金钱原子性 (Money Atomicity) |
| 4.2 商品原子性 (Goods Atomicity) |
| 4.3 确认发送原子性 (Certified Delivery Atomicity) |
| 5 基于四方的安全电子商务支付协议模型检测验证结论 |
（5）基于四方的安全电子商务支付协议研究（论文提纲范文）
| 摘要 |
| ABSTRACT |
| 1 绪论 |
| 1.1 课题的研究背景及目的 |
| 1.2 国内外研究概况 |
| 1.3 论文的研究内容 |
| 1.4 论文的组织结构 |
| 2 安全电子交易SET 协议分析 |
| 2.1 安全电子交易SET 协议 |
| 2.2 SET 协议形式化分析描述 |
| 2.3 SET 协议安全性分析及改进 |
| 2.4 本章小结 |
| 3 基于四方的安全电子商务支付协议设计 |
| 3.1 设计目标 |
| 3.2 协议的设计及形式化描述 |
| 3.3 协议的安全性分析及比较 |
| 3.4 本章小结 |
| 4 协议模型检测仿真实验验证 |
| 4.1 模型检测技术分析 |
| 4.2 协议SMV 建模 |
| 4.3 协议的CTL 原子性属性设计 |
| 4.4 协议的原子性仿真实验验证 |
| 4.5 本章小结 |
| 5 基于四方的安全电子商务支付系统应用设计 |
| 5.1 系统结构设计 |
| 5.2 数据结构设计描述 |
| 5.3 系统软件模块设计 |
| 5.4 本章小结 |
| 6 总结与展望 |
| 6.1 研究工作总结 |
| 6.2 下一步研究工作展望 |
| 致谢 |
| 参考文献 |
| 附录Ⅰ 攻读硕士学位期间发表论文目录 |
| 附录Ⅱ 攻读硕士期间参与的科研工作 |
（6）电子商务协议的形式化分析（论文提纲范文）
| 摘要 |
| ABSTRACT |
| 第1章 引言 |
| 1.1 研究背景 |
| 1.2 研究现状 |
| 1.3 研究内容 |
| 1.4 本文结构 |
| 第2章 概述电子商务协议 |
| 2.1 电子商务协议的背景 |
| 2.2 电子商务协议分类 |
| 第3章 电子商务协议安全基础 |
| 3.1 逻辑分析方法 |
| 3.1.1 KAILAR逻辑 |
| 3.1.2 实例分析 |
| 3.2 模型检测技术 |
| 3.2.1 线性时序逻辑LTL语法 |
| 3.2.2 线性时序逻辑LTL的语义 |
| 3.2.3 模型检测器SPIN |
| 3.3 加密技术 |
| 3.3.1 对称密钥加密方式 |
| 3.3.2 非对称密钥加密方式 |
| 3.3.3 消息摘要 |
| 3.3.4 数字签名 |
| 3.3.5 公钥证书 |
| 第4章 电子商务协议安全性质分析 |
| 4.1 匿名性 |
| 4.2 原子性 |
| 4.2.1 原子性的来源 |
| 4.2.2 实例分析 |
| 4.3 不可否认性、公平性 |
| 4.3.1 不可否认性 |
| 4.3.2 公平性 |
| 第5章 一个新的电子商务协议 |
| 5.1 设计电子商务协议的规则 |
| 5.2 协议的提出 |
| 5.3 协议的描述 |
| 5.4 安全性分析 |
| 5.4.1 秘密性分析 |
| 5.4.2 可追究性分析 |
| 5.4.3 原子性分析 |
| 5.4.4 公平性分析 |
| 5.4.5 其他性质 |
| 第6章 结论与展望 |
| 6.1 总结 |
| 6.2 展望 |
| 致谢 |
| 参考文献 |
| 攻读学位期间的研究成果 |
（7）基于模型检测工具SPIN的安全协议分析和验证（论文提纲范文）
| 原创性声明 |
| 关于学位论文使用授权的声明 |
| 摘要 |
| ABSTRACT |
| 目录 |
| 第一章 绪论 |
| §1.1 背景 |
| 1.1.1 分析和验证安全协议的困难性 |
| 1.1.2 国内外研究现状 |
| §1.2 本文工作 |
| §1.3 论文结构 |
| 第二章 理论背景 |
| §2.1 模型检测理论基础 |
| 2.1.1 概念及相关技术 |
| 2.1.2 应用 |
| §2.2 模型检测工具SPIN |
| 2.2.1 SPIN的基本结构 |
| 2.2.2 Promela语言 |
| 2.2.3 线性时态逻辑(LTL) |
| 2.2.4 基本算法 |
| §2.3 安全协议形式化分析方法理论基础 |
| 2.3.1 形式化方法分析安全协议概述 |
| 2.3.2 常见的形式化分析安全协议的方法 |
| BAN逻辑及BAN类逻辑 |
| 串空间(strand space)模型 |
| CSP模型与分析方法 |
| 定理证明的方法及模型检测方法 |
| §2.4 小结 |
| 第三章 基于SPIN的安全协议形式化分析和验证 |
| §3.1 协议描述 |
| 3.1.1 Netbill协议的内容 |
| 3.1.2 Netbill协议的说明 |
| §3.2 协议的行为抽象 |
| 3.2.1 模型的PROMELA结构 |
| 3.2.2 主体的状态及行为描述 |
| §3.3 协议的属性说明 |
| 3.3.1 SPIN可验证的正确性属性 |
| 3.3.2 协议的时态行为分析 |
| §3.4 协议行为模拟分析 |
| §3.5 属性验证结果分析 |
| 3.5.1 LTL属性P1的验证 |
| 3.5.2 关于其它属性的验证 |
| §3.6 和SMV方法比较 |
| §3.7 小结 |
| 第四章 结论及展望 |
| §4.1 论文的主要工作 |
| §4.2 与其他方法的比较 |
| §4.3 进一步的工作 |
| 参考文献 |
| 致谢 |
| 附录1 |
| 附录2 |
（8）移动电子商务协议的模型检验分析与设计研究（论文提纲范文）
| 摘要 |
| ABSTRACT |
| 第一章 概述 |
| 1.1 研究背景及意义 |
| 1.2 国内外研究现状 |
| 1.3 研究内容 |
| 1.4 结构安排 |
| 第二章 移动电子商务及移动电子商务协议 |
| 2.1 移动电子商务的概念及其优势 |
| 2.2 推动移动电子商务发展的技术 |
| 2.3 移动电子商务协议执行环境的特点 |
| 2.4 移动电子商务协议的性质要求 |
| 2.5 小结 |
| 第三章 无线认证协议的模型检验分析 |
| 3.1 模型检验与SMV 系统 |
| 3.2 无线认证协议的分析思路 |
| 3.3 SERVER-SPECIFIC MAKEP 协议简介 |
| 3.4 SERVER-SPECIFIC MAKEP 协议的模型检验分析 |
| 3.5 SERVER-SPECIFIC MAKEP 协议的改进及其模型检验分析 |
| 3.6 小结 |
| 第四章 移动电子商务协议的模型检验分析 |
| 4.1 移动电子商务协议的有限状态机建模方法 |
| 4.2 KSL 移动支付协议简介 |
| 4.3 KSL 移动支付协议的模型检验分析 |
| 4.4 KSL 移动支付协议的改进 |
| 4.5 小结 |
| 第五章 一种移动环境公平支付协议的设计与分析 |
| 5.1 引言 |
| 5.2 FMPP 协议 |
| 5.3 FMPP 协议的模型检验分析 |
| 5.4 结论 |
| 5.5 小结 |
| 第六章 结论 |
| 参考文献 |
| 致谢 |
| 附：在读期间发表的论文 |
（9）加入有效期的无可信第三方的多银行电子现金协议研究（论文提纲范文）
| 摘要 |
| Abstract |
| 第1章 绪论 |
| 1.1 引言 |
| 1.2 现有电子商务交易协议 |
| 1.2.1 安全电子交易协议 |
| 1.2.2 微支付协议 |
| 1.2.3 安全套接层协议 |
| 1.3 论文的研究意义及背景 |
| 1.4 本文的研究内容和结构安排 |
| 第2章 数学基础及相关知识 |
| 2.1 有限域 |
| 2.2 单向散列函数 |
| 2.3 交互式证明和零知识证明 |
| 2.4 椭圆曲线有关概念 |
| 2.4.1 任意域上的椭圆曲线 |
| 2.4.2 有限域上的椭圆曲线 |
| 2.4.3 椭圆曲线上的离散对数问题 |
| 2.4.4 椭圆曲线加密体制 |
| 2.4.5 椭圆曲线数字签名体制 |
| 2.5 公开密钥密码系统 |
| 2.5.1 密钥产生 |
| 2.5.2 加密体制 |
| 2.5.3 数字签名体制 |
| 2.5.4 同时达到秘密通信与数字签名 |
| 2.6 公开密钥基础设施 |
| 2.6.1 结构模型 |
| 2.6.2 功能 |
| 2.7 本章小结 |
| 第3章 电子现金系统的匿名性控制问题分析 |
| 3.1 引言 |
| 3.2 匿名性定义 |
| 3.3 发展历史 |
| 3.4 匿名性撤销的方式 |
| 3.5 匿名性控制问题分析 |
| 3.5.1 已有方法分析 |
| 3.5.2 匿名性的控制 |
| 3.6 本章小结 |
| 第4章 加入有效期的无可信方电子现金方案 |
| 4.1 引言 |
| 4.2 银行数据库分析 |
| 4.3 方案描述 |
| 4.3.1 方案建立 |
| 4.3.2 取款协议 |
| 4.3.3 支付协议 |
| 4.3.4 存款协议 |
| 4.4 方案分析 |
| 4.4.1 方案的正确性 |
| 4.4.2 公平匿名性 |
| 4.4.3 防止重复花费 |
| 4.4.4 效率分析 |
| 4.5 本章小结 |
| 第5章 多银行的电子交易协议 |
| 5.1 引言 |
| 5.2 多银行电子现金模型 |
| 5.3 基本假定 |
| 5.4 基本模块 |
| 5.4.1 电子收银台 |
| 5.4.2 电子钱包 |
| 5.4.3 支付网关 |
| 5.4.4 送货系统 |
| 5.4.5 商务系统 |
| 5.5 协议描述 |
| 5.5.1 标记 |
| 5.5.2 群的管理者(中央银行)的初始设置 |
| 5.5.3 发币银行证书的领取 |
| 5.5.4 开户协议 |
| 5.5.5 提取协议 |
| 5.5.6 支付协议 |
| 5.5.7 追踪协议 |
| 5.6 协议分析 |
| 5.6.1 匿名性 |
| 5.6.2 原子性 |
| 5.6.3 安全性 |
| 5.6.4 效率分析 |
| 5.7 本章小结 |
| 结论 |
| 参考文献 |
| 攻读硕士学位期间承担的科研任务与主要成果 |
| 致谢 |
| 作者简介 |
四、Netbill协议原子性的符号模型检验分析（论文参考文献）
- [1]嵌入式软件形式化建模与测试方法研究[D]. 崔凯. 大连理工大学, 2020
- [2]电子商务支付协议认证性的SVO逻辑验证[J]. 肖茵茵,苏开乐. 计算机工程与应用, 2014(08)
- [3]电子商务协议的形式化分析与漏洞检测[D]. 常寅龙. 福州大学, 2013(09)
- [4]基于四方的安全电子商务支付协议分析与验证[J]. 肖仕成,李开,甘早斌. 计算机科学, 2012(03)
- [5]基于四方的安全电子商务支付协议研究[D]. 肖仕成. 华中科技大学, 2011(06)
- [6]电子商务协议的形式化分析[D]. 王兵. 南昌大学, 2007(06)
- [7]基于模型检测工具SPIN的安全协议分析和验证[D]. 孙守卿. 兰州大学, 2006(09)
- [8]移动电子商务协议的模型检验分析与设计研究[D]. 刘霞. 桂林电子科技大学, 2006(04)
- [9]加入有效期的无可信第三方的多银行电子现金协议研究[D]. 刘宏有. 燕山大学, 2006(08)
- [10]一种电子商务协议原子性的模型检验分析方法[J]. 董荣胜,郭云川,古天龙. 计算机科学, 2005(04)