基于ATL的公平电子商务协议形式化分析

针对传统时序逻辑LTL,CTL及CTL*等把协议看成封闭系统进行分析的缺点,Kremer博士(2003)提出用一种基于博弈的ATL(Alternating-time Temporal Logic)方法分析公平电子商务协议并对几个典型的协议进行了公平性等方面的形式化分析。本文讨论了ATL逻辑及其在电子商务协议形式化分析中的应用,进一步扩展了Kremer博士的方法,使之在考虑公平性等特性的同时能够分析协议的安全性。最后本文用新方法对Zhou等人(1999)提出的 ZDB协议进行了严格的形式化分析,结果发现该协议在非保密通道下存在两个可能的攻击：保密信息泄露和重放攻击。     

一种基于计算能力的无需可信第三方公平非抵赖信息交换协议

随着互联网电子商务等业务的发展,公平非抵赖的信息传送协议(fair non-repudiation protocol)逐渐成为网络安全研究的新热点.现有的一些协议大多建立在可信第三方(trusted third party——TTP)基础之上,协议能否顺利进行主要依赖于TTP,如果TTP受到攻击,那么协议将失效.因此,迫切需要一个无需TTP的公平非抵赖协议.由于已有此类协议在安全性上是不对称的,不能保证发送方的信息安全.本文在分析已有非抵赖协议机制及其安全性的基础上,设计了一种发送方优先的协议,并根据双方的计算能力提出了一种可协商的无需可信第三方的公平非抵赖信息交换协议,使非抵赖信息交换的安全性摆脱了对TTP的依赖,并解决了信息的发送方和接收方的计算能力不对等时而存在的安全问题.     

移动自组网中基于动态第三方的可信公平非抵赖协议

由于移动自组网Manet(Mobile Ad-hoc Networks)是一个无中心的网络且不存在值得信任的结点,传统的公平非抵赖协议因需要一个固定可信第三方TTP(Trusted Third Party)而不足以保证Manet的高效性和安全性.本文在可信平台模块TPM(Trusted Platform Module)的安全体系结构基础上提出了一种Manet中基于动态第三方的可信公平非抵赖协议,以取代固定TTP,提高协议效率,并运用TPM完整性度量技术和DAA(Direct Anonymous Attestation)远程认证技术,保证证据可信.最后利用Event B对该协议进行形式化建模,证明其有效性和公平性.     

基于并发签名的公平交易协议的分析与改进

针对一个基于完美并发签名的公平交易协议,分析指出此协议在假设参与双方都诚实可信的情况下不满足不可滥用性,即双方交换2个模糊签名及相关交易数据后,在秘密消息公布之前,任何人都能辨认出是谁签了哪一个签名.进而,提出了一个新的改进方案,改进的方案不仅弥补了原方案的缺陷,实现了不可滥用性,同时保持了原协议的公平性、不可否认性以及简洁高效的特性.     

电子支付协议的博弈逻辑模型与形式化分析

提出用一种新的基于博弈逻辑ATL（Ahernating-time Temporal Logic）的电子支付协议建模与分析方法。新方法克服了传统时序逻辑把协议看成封闭系统进行分析的缺点．可以成功地对电子商务中的对抗与合作行为进行描述．利用新方法对Bolignano协议进行了严格的形式化分析．发现该协议不能满足公平性要求．     

基于ATL的电子商务协议建模与形式化分析

LTL和CTL等由于把协议看成封闭式并发系统进行研究,不能有效描述协议与外部环境的联系,引入一种新的基于博弈逻辑的ATL分析方法,能够对日益复杂的多方电子商务协议进行建模与分析,利用新方法对Markowitch和Kremer提出的多方非否认协议进行建模与严格的形式化分析,发现该协议存在的不公平性问题并提出改进方法.     

基于身份的公平不可否认协议

利用基于身份的密码体制,提出了一种基于身份的一次性盲公钥签名方案,并以此为基础提出了一个新的公平不可否认协议,实现了协议中发送方的匿名性,解决了通信中因发方身份公开而带来的信息内容被猜到以至被故意延迟阅读或拒收的问题,保证了收发双方的公平性及不可否认性.分析表明,该一次性盲公钥签名方案及不可否认协议是安全的,且具有较高的效率.     

一个非否认协议ZG的形式化分析

非否认性是电子商务协议的一个重要性质,其形式化分析问题引起了人们的密切关注.本文运用SVO逻辑对一个非否认协议实例进行了有效的形式化分析,并对协议的缺陷进行了改进.     

移动环境公平支付协议的设计与分析研究

结合固定网络中的支付协议并充分考虑移动装置和无线网络的特点,提出了一种移动环境公平支付协议。利用模型检验工具对协议进行分析并将该协议与其他支付协议进行比较,分析和比较结果表明,该协议具有公平、保密、高效等特点,适用于移动环境。     

基于PPV的公平移动支付协议

结合CEMBS的设计思想,在尽量满足移动网络特性的情况下,设计了一个能在移动终端观看视频服务的即看即付的公平协议.该协议在服务请求阶段通过利用CEMBS,在乐观情况下,可信第三方移动网络运营商不需参与,就可使互不信任的User与VASP完美地实现双方的认证与会话密钥协商,同时完成了服务请求的建立,双方均是不可否认的,且整个过程只需三条消息;在支付阶段,也可以保证双方公平地进行交易.通过分析,该协议满足公平性、不可否认、原子性、认证性以及保密性等一些必备性质,且协议比较简单,应用范围比较广泛.     

带脱线半可信第三方的公平非否认交换协议

不可否认性和公平性是电子商务交换协议中的两个重要性质.本文以带盲密文的可验证加密方案为基础,提出了一种新的带有脱线半可信第三方公平的非否认协议,使协议中的任何一方可以单方面终止协议的执行但又不破坏公平性.     

对一种电子支付协议的改进

随着电子商务在全球的迅猛发展，电子商务的安全问题日益受到人们的关注。安全的电子商务协议是确保电子商务活动可靠开展的基础，其中不可否认性和公平性则是电子商务协议的两个重要安全需求。介绍了Bolignano电子支付协议，对其不可否认性和公平性进行了分析，发现了协议在公平性方面存在不足，并通过引入ftp传送的思想，对协议进行了改进。最后本文通过严格的协议形式化分析，证明了改进后的协议满足不可否认性和公平性。     

基于CPN模型的不可否认协议分析

通过对不可否认协议的语义进行分析,建立有色Petri网（Coloured Petri Net,CPN）中基本元素与安全协议中元素的对应关系,对CPN Tools提供的建模语言（CPN ML）在规范协议描述、简化协议建模及自动检测方面进行扩展,提出了一种基于CPN模型的不可否认协议分析方法,该方法利用CPN tools的状态空间查询功能和自建的查询函数库来对不可否认协议进行分析和验证,该工具具有通用性强、时效性强和交互性好等诸多优点,并通过实例说明了这种方法的有效性。     

一种基于非否认协议的电子邮件传输方案

在电子邮件传输中,发信人和收信人的不可否认性是一个重要的安全问题。该问题可以通过采用数据传输中的非否认协议来解决。目前多数非否认协议基于可信第三方,并且对可信第三方的安全性、通信能力要求很高,因而难以在实际中应用。提出了一种基于安全第三方的非否认协议,该协议适合于电子邮件传输的特定应用;同时该协议减少了通信流量,降低了对可信第三方的安全性要求。随后结合安全多用途邮件扩展技术,得出了基于该协议的电子邮件传输实现方案。     

A PTD‐based transaction protocol for public transportation

Advances in wireless network technology and the increasing number of users of the personal trusted device (PTD) make the PTD an ideal channel for offering personalized services to mobile users. In this paper, we propose using a PTD as a payment tool in a mobile transaction system for public transportation. To overcome the inherent weakness of computing resources in a PTD, we use a trusted observer to coordinate the mobile transaction and to integrate cryptology (such as a digital signature and a one‐way hash function). The proposed scheme satisfies the requirements for mobile transactions. These requirements include fairness, non‐repudiation, anonymity, off‐line capability, no forgery, efficient verification, simplicity, and practicability. Because a PTD is more portable and personal than a personal computer and because the public transportation can be a necessity in our daily lives, our scheme proposes a novel use of PTDs in mobile commerce. Copyright © 2008 John Wiley & Sons, Ltd.     

改进新密钥交换协议及其形式化分析

Diffie-Hellman协议不具有认证功能且不能抵抗中间人攻击。Seo等人提了一种简单的算法（SAKA）协议可以抵抗中间人攻击且运算简单,但是SAKA协议也存在不足。另有人提出了Lin协议、E-SAKA协议等。分析上述协议可看出存在不足。于是提出改进的新密钥交换协议。它具有SAKA及其改进协议优点的同时可以避免SAKA及其改进协议的缺陷。并给出该协议的BAN逻辑形式分析。     

多方不可否认协议时限性分析与改进

 时限性是实用的不可否认协议必须具备的一个基本性质.形式化分析典型的多方不可否认协议时发现其存在未公布的时限性缺陷.本文通过向协议消息中添加额外时间控制信息和改变协议交互步骤的办法对该缺陷进行了改进.