A Formal Model for Analyzing Fair Exchange Protocols Based on Event Logic

Fair exchange protocols play a critical role in enabling two distrustful entities to conduct electronic data exchanges in a fair and secure manner.These protocols are widely used in electronic payment systems and electronic contract signing,ensuring the reliability and security of network transactions.In order to address the limitations of current research methods and enhance the analytical capabilities for fair exchange protocols,this paper proposes a formal model for analyzing such protocols.The proposed model begins with a thorough analysis of fair exchange protocols,followed by the formal definition of fairness.This definition accurately captures the inherent requirements of fair exchange protocols.Building upon event logic,the model incorporates the time factor into predicates and introduces knowledge set axioms.This enhancement empowers the improved logic to effectively describe the state and knowledge of protocol participants at different time points,facilitating reasoning about their acquired knowledge.To maximize the intruder’s capabilities,channel errors are translated into the behaviors of the intruder.The participants are further categorized into honest participants and malicious participants,enabling a comprehensive evaluation of the intruder’s potential impact.By employing a typical fair exchange protocol as an illustrative example,this paper demonstrates the detailed steps of utilizing the proposed model for protocol analysis.The entire process of protocol execution under attack scenarios is presented,shedding light on the underlying reasons for the attacks and proposing corresponding countermeasures.The developedmodel enhances the ability to reason about and evaluate the security properties of fair exchange protocols,thereby contributing to the advancement of secure network transactions.

A Protocol for Fair Electronic Purchase Based on Concurrent Signatures

E-commerce protocols for the electronic purchase of goods are difficult to design and implement due to their complexity and high security demands. Fairness of such protocols in literature highly depends on an additional TTP（trusted third party）. However, it is difficult to find such a TTP in some situations. In addition, fairness for customers has been neither fully considered nor well satisfied in existing electronic purchasing protocols. In this paper, a new protocol FEP （fair electronic purchase） without a special TTP but an online bank is presented based on a concurrent digital signature scheme. The FEP protocol guarantees fair electronic purchase of goods via electronic payment between consumers, merchants and their online banks. The protocol is practical and the analysis based on the game logics shows that it achieves the properties of viability, fairness, and timeliness.

ARROW-WTCP:A fast transport protocol based on explicit congestion notification over wired/wireless networks

An explicit congestion notification (ECN)-based distributed transport protocol,ARROW-WTCP (AcceleRate tRansmission towards Optimal Window size TCP for Wireless network),was proposed.The ARROW-WTCP enables feasible deployment of ARROW-TCP from wired to wireless networks by providing a joint design of source and router algorithms.The protocol obtains the actual capacity of the wireless channel by calculating the queue variation in base station (BS) and adjusts the congestion window by using the feedback from its bottleneck link.The simulation results show that the ARROW-WTCP achieves strong stability,max-min fairness in dynamic networks,fast convergence to efficiency without introducing much excess traffic,and almost full link utilization in the steady state.It outperforms the XCP-B (eXplicit Control Protocol Blind),the wireless version of XCP,in terms of stability,fairness,convergence and utilization in wireless networks.

MULTI-ITEM FAIR EXCHANGE SCHEME

As more business is conduced over the Internet, the fair exchange problem assumes increasing importance. However, the problem of multi-party fair exchange has not been studied as widely as the more fundamental problem of 2-party fair exchange. Recently, Franklin arid Tsudik proposed two protocols for n-party multi-item exchange on FC'98, SUCEX-1 and SUCES-2. This paper first gives an attack on the proposed protocol SUCEX-1, then presents two protocols for multi-item exchange, one is an improved protocol of SUCEX-1, another is the extension of protocol SUCEX-2.

Tree Based Energy and Congestion Aware Routing Protocol for Wireless Sensor Networks

Wireless Sensor Networks (WSNs) have inherent and unique characteristics rather than traditional networks. They have many different constraints, such as computational power, storage capacity, energy supply and etc;of course the most important issue is their energy constraint. Energy aware routing protocol is very important in WSN, but routing protocol which only considers energy has not efficient performance. Therefore considering other parameters beside energy efficiency is crucial for protocols efficiency. Depending on sensor network application, different parameters can be considered for its protocols. Congestion management can affect routing protocol performance. Congestion occurrence in network nodes leads to increasing packet loss and energy consumption. Another parameter which affects routing protocol efficiency is providing fairness in nodes energy consumption. When fairness is not considered in routing process, network will be partitioned very soon and then the network performance will be decreased. In this paper a Tree based Energy and Congestion Aware Routing Protocol (TECARP) is proposed. The proposed protocol is an energy efficient routing protocol which tries to manage congestion and to provide fairness in network. Simulation results shown in this paper imply that the TECARP has achieved its goals.

A Kind of Multi-party Non-repudiation Protocol with Consistent Evidence

With development of electronic com- merce, non-repudiation protocol as the basal component of non-repudiation service has done more and more important functions. Comparing with lots of work on two-party non-repudiation, there are less work on multi-party non-repudiation protocol. Multi-party protocol is more complex and facing more challenge of collusion attack. In this paper we give a kind of multi-party non-repudiation protocol based on off-line TTP with consistent evidence. Consistent evidence is a property that can not only simplify the process of disputation resolving, but also make the service more friendly to users, which means that whether or not TTP involves, evidences participants obtained are consistent. In the meanwhile we analyze the collusion attack that multi-party protocol facing, our protocol can prevent collusion attack.

Collision Detection and the Design of Fair and Stable MAC Scheme for Wireless Ad Hoc Networks

Fairness and stability guarantee among TCP flows is very stubborn in wireless ad hoc networks. There is not a MAC protocol that can fulfill this acquirement until now. In this paper, we firstly reveal the in-depth causes of the severe TCP unfairness and instability problems in IEEE 802.11-based multihop networks. Then we utilize the collision detection mechanism of the IEEE 802.11 protocol which is often ignored by most of the people to design a novel collision detection mechanism-based MAC (CDMB-MAC) scheme to solve the short-term and long-term fairness and stability issues while providing a good aggregate throughput in many topologies.

Dynamic Characteristics of Explicit Control Protocol

The dynamic characteristics of eplicit control protocol (XCP) were investigated with single bottleneck on the microscopic time-scale. Analysis and simulation results show that the bandwidth utilization of an XCP bottleneck link converges to 1 at exponential rate, persistent congestion cannot occur at the bottleneck link, and throughput of an arbitrary subset of XCP flows at the bottleneck link converges to its fair share in exponential rate. The XCP has high bandwidth utilization and good fairness properties.

Symbolic Model Checking and Analysis for E-Commerce Protocol

A new approach is proposed for analyzing non-repudiation and fairness of e-commerce protocols. The authentication e-mail protocol CMP1 is modeled as finite state machine and analyzed in two vital aspects- non-repudiation and fairness using SME. As a result, the CMP1 protocol is not fair and we have improved it. This result shows that it is effective to analyze and check the new features of e-commerce protocols using SMV model checker.

太赫兹无线个域网公平高效的MAC层优化机制

针对太赫兹无线个域网双信道媒体访问控制(Medium Access Control,MAC)协议中存在的信道资源分配公平性差、数据帧重传效率低和控制开销较高的问题,提出了一种公平高效的MAC层优化机制。新机制采用基于历史时隙申请信息的信道资源分配策略优化时隙分配公平性,根据信道质量自适应选择数据帧重传机制,控制节点从申请时隙的节点发送的控制帧中的“duration”字段提取时隙申请信息,省略时隙申请帧的发送,从而降低数据帧排队时延和控制开销,提高吞吐量。仿真结果表明,与TAB-MAC和MDP-MAC协议的机制相比,所提机制的数据帧平均排队时延降低了15%,吞吐量提高了5%。

基于非线性能量收集的认知WPCN性能优化

考虑了一个基于点对点主通信链路的认知无线供电通信网络(Wireless Powered Communication Network,WPCN),该认知WPCN由一个多天线混合接入点组成,该接入点将无线能量传输给一组低功耗无线设备,并接收来自这些无线设备的传感数据。为了解决认知WPCN中固有的用户不公平问题,同时考虑到同相/正交不平衡、非线性放大幅度和相位噪声对低成本传感器节点物理收发器的影响,提出了一个基于非线性能量收集的簇协作协议,从而平衡不同无线设备的能量消耗,提高了认知WPCN系统的吞吐量性能。为了保证主系统的性能,考虑了主系统的温度干扰约束,在三种实际网络环境下进行了仿真,结果表明,该方法能有效提高认知WPCN的吞吐量公平性,同时保证了主网络的通信质量。

一种分析电子商务协议的新工具

提出了一种新的形式化分析方法 ,可用于分析电子商务协议 .与 Kailar逻辑相比 ,它有 3个优点 :(1)能够有效地分析协议的公平性 ,在进行公平性分析时充分考虑了通信信道的可靠性 ;(2 )初始化拥有集合只依赖于环境 ,不需要人为地引入初始化假设 ;(3)增加了密文理解规则 ,能够有效地分析包含有签过名的加密公式的消息 .

基于签密的多方认证邮件协议

签密方案可以在一个逻辑步骤内同时实现签名和加密,可以有效地减少运算.本文在已有的两方签密方案的基础上结合组可验证的签密方案,提出了一种新的、可用于多方认证邮件协议的签密方案,进而设计出了异步的一对多的认证邮件协议,并证明了该协议的公平性与非否认性.文中还通过与已有协议进行比较,阐述了新协议的优点.

基于RSA签名的优化公平交换协议

公平性是电子商务协议的基本安全要求.RSA是应用最为广泛的公钥密码体制之一.公平交换协议可以使得参与交换的双方以公平的方式交换信息,这样,要么任何一方都可以得到对方的信息,要么双方都得不到对方的信息.分析了现有的公平交换协议构造方法、体系结构及其在实用性和效率方面存在的问题.在此基础上,利用精心构造的扩环中可公开验证的、加密的RSA签名,提出了一种完全基于RSA签名方案的优化公平交换协议,并对其安全性和效率进行了证明和分析.分析表明,提出的方案是简洁、高效、安全的.

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

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

电子商务协议的公平性

本文指出在分析电子商务协议公平性的过程中 ,不仅要考虑参与协议的主体被动攻击的情况 ,同时还要考虑参与协议的主体进行主动攻击的情况 .在此基础上 ,本文对Kailar逻辑进行了改进 ,使之能够分析协议的可追究性和公平性 .

基于半可信离线第三方的公平交易协议

电子商务是 Internet应用的发展趋势 ,它的基础之一是公平的交易协议 .提出一种新的解决方案 ,它所依赖的第三方不必完全可信 ,且只需离线工作 .协议还是高效的 ,表现为在一般情况下 ,一次交易只需交互 4条信息 .同时 ,交互的信息都自然地被加密 ,因而特别适合 Internet这种几乎没有物理安全性的公共网络 .

无线mesh网中一种基于博弈论的公平性路由协议

提出一种基于博弈论的以树为拓扑结构的公平性路由协议。新的协议综合了先验式路由和按需路由,并且将路由计算和信道资源分配控制分布到树中的每个枝节点上,降低了根节点的负担,使其更适合于无线mesh网的通信需求。仿真结果表明,新的路由协议改进了AODV、HWMP路由协议的端到端平均延迟和网络吞吐量,并且网络中各个无线节点占有的信道资源基本相近,满足公平性原则。

新颖的基于并发签名的公平交易协议

基于完美的并发签名,提出了一个新颖的公平交易协议,在双方起初交换2个模糊签名及相关交易数据的时候,任何人都无法辨认是谁签了哪一个签名,直到发起方公布一个秘密信息,2个签名才同时绑定到各自的签署方,之后另一方发送解密商品的密钥,从而让双方都能公平的得到对方的物品,而且本协议无需可信第三方(TTP)的参与即可让交易双方公平地交易数据条目,避免了两方勾结的可能性以及可信第三方参与协议的瓶颈。通过分析,协议很好地保证了公平性、不可否认性以及不可滥用性等性质,而且协议只需两方发送4条消息,简洁高效。

基于ProVerif的电子商务协议分析

采用应用pi演算来建模自动解决争端的公平电子商务协议,基于一致性给出了公平性的形式描述方法,利用应用pi演算的自动化分析工具——ProVerif分析了该协议,结果表明,利用一致性描述协议公平性是可行的,同时指出了基于ProVerif验证电子商务协议的优缺点:适用于分析"A事件发生以前,B事件是否曾经发生",但不适用于分析"A事件发生之后,B事件将来是否会必然(或可能)发生"。