Formal Analysis of Rational Exchange Protocols Based on the Improved Buttyan Model

A rational exchange protocol is a type of e-commerce protocol that aims to maximize the participants’ own interests. The Buttyan model is commonly used to analyze the security of such protocols. However, this model has limitations in dealing with uncertainties and false messages in rational exchanges. To address these shortcomings, this paper proposes a formal analysis method based on Bayesian games. By incorporating participants’ types and beliefs, the Buttyan model is extended to enhance its ability to express uncertainties. Additionally, attack messages are introduced to simulate the potential fraudulent behaviors that participants may exploit through the security vulnerabilities in the protocol. Finally, the improved model is applied to conduct a formal analysis of a rational electronic contract signing protocol, and it is found that the protocol meets the usability requirements. The results show that this method can be effectively applied to the security analysis of rational exchange protocols, thereby enhancing the security of the e-commerce transaction process.