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

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

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

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

网络支付协议的形式化安全需求及验证逻辑

从整个网络支付协议的安全角度出发，提出网络支付协议的多层安全需求模型，包括以认证和密钥分配为基础的基层需求、网络支付协议固有的中层需求(包括保密性、原子性、公平性、完整性、匿名性、不可否认性、可追究性等)、以及面向具体应用的高层需求。基于一阶逻辑和时序逻辑，提出一种适合描述网络支付协议的形式化安全需求的逻辑，描述了该逻辑的语法结构和推理规则，并用该安全需求逻辑对网络支付协议的多层安全需求进行了形式化描述。最后，以SET协议为例进行需求验证。     

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

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

公平的移动小额支付协议

为了实现具有完全公平性和非单元支付功能的小额支付协议,该文首先提出了双PayWord链(DPWC)的概念和非单元支付的实现机制。利用DPWC,并基于数据业务管理平台(DSMP)提出了一种新的公平的移动小额支付协议(FMMP)。该协议由注册、支付、仲裁、结算和注销5个子协议组成。分析结果表明,该协议能提供支付的完全公平性和非单元支付功能,并且具有安全、高效和不可否认的特点。     

ISI协议的符号模型检验分析

电子商务协议的非否认性与公平性问题已成为电子商务和信息安全领域研究的热点。本文建立了网络支付协议ISI的有限状态机模型,并用SMV检验工具对其两个重要特性———非否认性与公平性进行了分析检验,发现了ISI协议不满足公平性。结果表明利用符号模型检验方法分析检验电子商务协议的新特性是行之有效的。     

通用可组合的公平电子支付协议

公平性是电子支付协议的一个基本属性。该文基于通用可组合模型,定义了公平电子支付理想函数。在可转化签名理想函数、注册理想函数和安全会话理想函数辅助的混合模型下,构造了一个实现公平电子支付理想函数的公平电子支付协议。新的协议结构简单,通信量较低,并且在任意的和未知的多方环境中运行时仍然是安全的。     

基于博弈的电子商务协议分析

提出用一种新的基于博弈的逻辑方法分析电子商务协议,克服了传统时序逻辑把协议看成封闭系统进行分析的缺点。新方法可以成功地对电子商务中的对抗与合作行为进行描述,能够分析协议的保密性、安全性、非否认性及公平性等。最后用新方法对Zhou-Gollmann协议进行了严格的形式化分析。结果表明基于博弈的ATL逻辑比传统的基于计算树逻辑(CTL)更适合于描述和分析复杂电子商务协议。     

基于SSL安全协议电子支付终端的实现

通过网络进行交易和电子支付,安全问题越来越重要。SSL协议现已成为加密通讯的全球化标准。嵌入式的电子商务终端在SSL协议的保护下,安全问题得到了保证。本文在嵌入式LINUX系统平台的基础上,提出了一种嵌入式SSL安全协议的实现方案,并开发出基于INTERNET的安全电子支付终端。该终端的安全性在实验中得到了验证。     

对基于公钥密码体制的IBS协议的改进

分析了基于公钥密码体制的IBS协议,针对其中存在的一些不足和缺陷,提出改进方案。最后对改进后的协议进行形式化分析,证明改进后协议的不可否认性和公平性。     

A lightweight and secure NFC‐base mobile payment protocol ensuring fair exchange based on a hybrid encryption algorithm with formal verification

During the past few years, many near‐field communication (NFC) mobile payment protocols have been widely used and received more and more attentions. This could be an essential factor for the growth of the world economy and leads to the improvement of the quality of life for human beings. The NFC mobile payment is one prominent approach in allowing m‐commerce to conduct a sales transaction. However, fair exchange and information security are significant concerns in creating trust among the parties participating in the transaction. Many NFC mobile payment protocols have been introduced by researchers. But, most of them still lack some crucial properties of information security and fair exchange, and this can be an obstacle to their uses. In this article, we propose an NFC mobile payment protocol that possesses comprehensive properties of both information security and fair exchange for sales transaction processing. The protocol employs both symmetric and asymmetric encryptions, hash function, and the technique of offline session key generation, in order to improve the security while maintaining the lightweight property. The fairness analysis shows that the proposed protocol is more competent and effective than others. It can resolve any dispute in case one party misbehaves. Finally, the proposed protocol's security has been successfully verified using both Burrows, Abadi and Needham (BAN logic) and the Scyther tool.     

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

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

多方不可否认协议的增广CSP建模与分析

基于逆向工程的思想,使用前期工作中提出的面向两方不可否认协议分析的增广CSP方法,对典型的Kremer-Markowitch多方不可否认协议的安全性进行了探索性建模与分析。借助该分析成功发现此协议在满足不可否认性和公平性的同时却不具备时限性。这表明在适用于两方不可否认协议安全性验证的同时,增广CSP方法也可作为多方不可否认协议安全性验证的新方法。     

Symbolic Model Checking and Analysis for E-Commerce Protocol

The widely use of networks and e-commerce has brought great convenience to our daily life. The basis of normal e-commerce transaction between the seller and customers is the secure e-commerce protocols which must also include the two important properties, namely, non-repudiation and fairness, in addition to those basic properties such as secrecy, security, authentication and integrity[1]. So there are special and higher demands of the performance and function of the e-commerce protocol. To att…     

Discrete micropayment protocol based on master-slave payword chain

Using the idea of Payword, the new concept of master-slave payword chain (MSPC) is proposed in this article. MSPC consists of one master payword chain and one slave payword chain. On the basis of MSPC, a new micropayment protocol called discrete micropayment protocol (DMP), is presented in this article. DMP consists of three sub-protocols: registration, payment, and settlement. Both part fairness and non-unit-wise payment can be provided by DMP.     

移动计算网络环境中的认证与支付研究

该文针对移动计算网络的技术特点设计了一个用于移动用户与收费信息服务网络相互认证和用户进行电子支付的方案，该方案的新颖之处在于把小额支付方案融入认证协议当中，方案不仅在公共参数的存储空间需求和用户端计算负荷上是适当的，而且可以保护用户不被错误收费，同时提供服务者防止用户抵赖的合法证据。该方案基于一个全局的公钥基础设施，适合于未来的基于第三代移动通信系统的网络计算环境。