Ke Yang

Smart contracts, as a critical application of blockchain technology, significantly enhance its programmability and scalability, offering broad application prospects. However, frequent security incidents have resulted in substantial economic losses and diminished user trust, making security issues a key challenge for further development. Since smart contracts cannot be modified after deployment, flaws in their design or implementation may lead to severe consequences. Therefore, rigorous pre-deployment verification of their correctness is particularly crucial. This paper explores the symmetry in control flows and state transitions of Solidity smart contracts and leverages this inherent structural symmetry to develop a normalized state transition model based on a finite state machine. The FSM model is subsequently formalized into a Promela model with the Spin model checker. By integrating manually defined Linear Temporal Logic formulas with those generated by Smart Pulse, the Promela model is formally verified in Spin to ensure the correctness and security of smart contracts. This approach establishes a systematic verification framework, providing effective support to enhance the reliability and security of smart contracts.

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.

Ratchet protocols are a class of secure protocols based on ratcheting encryption mechanisms, widely employed in instant messaging. Against the backdrop of frequent incidents of communication privacy breaches, ratchet protocols have become a vital technology for ensuring secure end-to-end communication. This paper presents a formal analysis framework for ratchet protocols grounded in Logic of Events theory (LoET). We further extend LoET by introducing dedicated Diffie–Hellman (DH) and ratchet event classes, along with tailored axioms and inference rules, to support precise modeling of ratcheted encryption. Using the Signal protocol as a case study, we construct a bidirectional authentication model and rigorously prove that both its symmetric and asymmetric ratchet phases satisfy strong authentication properties. Compared with existing formal approaches, our method enables more expressive modeling of key update sequences and supports structured reasoning over causality and authentication flows. The proposed framework lays a theoretical foundation for analyzing the security of modern ratcheted protocols and holds potential for future automated verification.