Open Access

ARTICLE

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

by Ke Yang¹, Meihua Xiao^2,*, Zehuan Li¹

1 School of Electrical Engineering and Automation, East China Jiaotong University, Nanchang, 330013, China
2 School of Software, East China Jiaotong University, Nanchang, 330013, China

* Corresponding Author: Meihua Xiao. Email:

(This article belongs to the Special Issue: Advances in Ambient Intelligence and Social Computing under uncertainty and indeterminacy: From Theory to Applications)

Computer Modeling in Engineering & Sciences 2024, 138(3), 2641-2663. https://doi.org/10.32604/cmes.2023.031458

Received 17 June 2023; Accepted 27 July 2023; Issue published 15 December 2023

Abstract

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 developed model enhances the ability to reason about and evaluate the security properties of fair exchange protocols, thereby contributing to the advancement of secure network transactions.

---

Keywords

---