乐观电子合同签订协议的一种有限状态机模型

乐观电子合同签订协议是一类典型的安全协议，用于在两个或多个主体之间公平高效地实现电子合同签订。与其它类型的安全协议相比，乐观电子合同签订协议更为复杂，从而为其形式化分析带来了一定困难。模型检验是一类有效的形式化分析方法，应用模型检测方法分析安全协议时，前提和关键是对协议及其执行环境进行准确和全面的建模。     

安全协议形式化分析方法

安全协议的形式化分析是检验协议安全性的必要手段。为了实现协议的规范描述和合理完备的安全性验证,各种数学理论和人工智能方法被引进安全协议形式化分析与自动化验证领域。主要从逻辑方法、模型检测方法和证明方法3个方面对符号化的安全协议形式化分析方法进行了综述,并指出了今后该领域的研究方向。     

基于项重写的安全电子交易形式化模型

构建一个安全电子交易的形式化模型,为实现对相关安全协议的自动化分析提供了理论基础和技术手段.该模型基于项重写理论进行构建,通过符号化和规则化的方式刻画电子交易的3个主要过程,不但体现交易双方能互相检验身份的安全机制,并且通过项重写系统终止性和会聚性的性质证明该模型具有完整性和一致性等特点,在安全性分析方面验证该模型满足认证性和发送非否认性.     

一种形式化分析安全协议的新模型

串空间是安全协议形式化分析的一种新模型．利用次序关系的理论证明了借助串空间模型进行安全协议形式化分析的一个重要结论．通过构造入侵者串的方法,针对Woo-Lam协议提出了一个入侵者串空间模型,同时利用此入侵者串空间模型分析了该协议存在的缺陷,说明了改进后的Woo-Lam协议可克服此缺陷．与现有安全协议形式化分析方法相比较,串空间模型不仅具有简洁直观的优点,而且还可避免状态空间爆炸的问题．     

安全协议及其形式化分析研究

安全协议是网络安全的重要基础,形式化分析是保证安全协议具备相应安全性质的有效途径.通过对安全协议进行分类,阐述了各类协议所应具备的安全性质;并基于安全协议进行形式化分析时所作的各种假设,综述和分析了三类典型的安全协议形式化方法,给出了安全协议形式化分析研究的发展趋势.     

基于串空间模型的SSL3.0协议认证性分析

形式化分析技术是揭示安全协议是否存在漏洞的重要途径，串空间模型是一种基于定理证明的、新兴的安全协议形式化模型。介绍了SSL3．0协议的握手过程和串空间模型的基本概念以及基于串空间模型的认证性测试方法，在此基础上建立了基于串空间的SSL协议握手过程的模型，并验证了SSL协议的认证性。     

安全协议及其形式化分析研究

安全协议是网络安全的重要基础，形式化分析是保证安全协议具备相应安全性质的有效途径。通过对安全协议进行分类，阐述了各类协议所应具备的安全性质；并基于安全协议进行形式化分析时所作的各种假设，综述和分析了三类典型的安全协议形式化方法，给出了安全协议形式化分析研究的发展趋势。     

基于概率模型检测的合同签订协议分析

概率合同签订协议的公平性具有典型的概率性质。概率模型检测是一种验证存在随机行为系 统的分析技术。基于概率模型检测技术,在原协议的基础上建立了离散马尔可夫链和有限状态机模型, 用概率模型检测工具——PRISM验证了它的公平性,发现其公平性不满足时,在此基础上对原协议从 双方交换信息的策略上进行了扩充改进,使协议更为公平,满足了合同签订的基本要求。     

一种描述协议的新模型:线索空间模型

线索空间模型是一种新的安全协议模型 ,它可利用线索空间图证明 Needham- Schroeder协议的某些安全特性。在描述和分析此过程协议存在的漏洞同时并对协议进行了改进。线索空间模型同其他模型相比 ,最大优点就是简洁直观 ,是形式化技术的一个重要的研究方向     

基于概率模型检测的合同签订协议分析

概率合同签订协议的公平性具有典型的概率性质。概率模型检测是一种验证存在随机行为系统的分析技术。基于概率模型检测技术，在原协议的基础上建立了离散马尔可夫链和有限状态机模型，用概率模型检测工具——PRISM验证了它的公平性，发现其公平性不满足时，在此基础上对原协议从双方交换信息的策略上进行了扩充改进，使协议更为公平，满足了合同签订的基本要求。     

电子商务系统及其安全性研究

介绍了电子商务系统的基本内容;分析了目前电子交易中的主流协议SSL协议和SET协议;从网络和系统安全的角度介绍了一种信息安全系统的组合模型.     

盲签名及其在电子商务中的应用

电子商务正在成为一种重要的商务发展模式,它的安全性是通过以密码学为基础的技术和协议来保障的.盲签名技术由于其所具有的匿名性、不可伪造性等特性而应用于电子商务的诸多领域,起着越来越重要的作用.本文围绕盲签名的概念展开,首先给出了盲签名的一般模式,然后在此基础上分别阐述强盲签名、弱盲签名、代理盲签名和部分盲签名等主要的盲签名方案,并讨论它们在电子商务中的应用领域,最后给出了它在电子商务中的两个较成熟的应用--电子现金和电子投票.     

SET协议支付过程的符号模型检验

电子商务协议的安全性是电子商务健康发展的关键。随着SET协议应用的日益广泛,其安全性受到了业界的极大关注。分析、寻找SET协议安全隐患或证明其安全性,将有助于协议的进一步应用和发展。将模型检测应用于分析SET协议,给出SET协议支付过程的形式化模型和有限状态机模型,以及协议安全属性的CTL公式,并在网络环境被入侵者控制的假设下,基于SMV符号模型检测工具对协议进行了分析。结果表明,SET协议拥有保密性、完整性、认证性等电子商务安全需求属性。     

电子商务协议原子性的SPIN分析

电子商务协议的研究有利于促进电子商务的发展,电子商务协议的原子性是电子商务协议研究的重点.对NetBill协议及其原子性在开放性的环境中进行形式化描述的基础上,给出基于SPIN平台的NetBill协议模型,用LTL刻画协议需要满足的性质,用模型检测器SPIN对NetBill协议分析结果表明NetBill协议满足原子性.该方法对类似电子商务协议的其它性质分析具有一定的通用性.     

基于椭圆曲线的多银行电子现金支付协议的研究

椭圆曲线密码体制以其特有的优越性被广泛用于进行数据加密、数字签名，同样也可用来构建盲签名协议和电子现金协议。本文设计出了多银行电子现金支付协议。上述协议都是基于椭圆曲线离散对数表示问题的，其安全性是基于椭圆曲线离散对数的安全性。     

轻量级RFID双向认证协议设计与分析

针对现有的RFID认证协议存在的安全隐私保护弱点和性能不高问题,提出了一个基于Hash的RFID双向认证协议．采用可证明安全模型对其安全性进行了证明,分析了协议的隐私保护和安全特性．与现有几个结构类似的RFID认证协议相比,该协议有效地解决了RFID系统的隐私保护及安全问题,具有显著的性能优势,极大地降低了标签的存储量和计算量,尤其是提高了服务器数据库的检索效率．     

可转换认证加密的安全邮件协议

通过对电子商务中不可否认公平交换协议的运行流程进行了研究,论证了基于第三方的不可否认公平交换协议至少需要运行4步骤,进而指出现有一个协议实质上是需要运行4步骤的,而不仅仅是运行3步骤。依据安全协议与密码系统分开设计的原则,对比分析已有可转换认证加密方案,提出了一个可转换认证加密方案的系统模型。并基于该系统模型,设计了基于半可信第三方的不可否认的安全邮件协议。通过形式化方法分析表明,该协议具备邮件发送方和接收方均不可否认的特点。