Symbolic protocol analysis serves as a pivotal technique for protocol design, security analysis, and the safeguarding of information assets. Several modern tools such as Tamarin and ProVerif have been proven successful in modeling and verifying real-world protocols, including complex protocols like TLS 1.3 and 5G AKA. However, developing formal models for protocol verification is a non-trivial task, which hinders the wide adoption of these powerful tools in practical protocol analysis. In this work, we aim to bridge the gap by developing an automatic method for generating symbolic protocol models using Large Language Models (LLMs) from protocol descriptions in natural language document. Although LLMs are powerful in various code generation tasks, it is shown to be ineffective in generating symbolic models (according to our empirical study). Therefore, rather than applying LLMs naively, we carefully decompose the symbolic protocol modeling task into several stages so that a series of formal models are incrementally developed towards generating the final correct symbolic model. Specifically, we apply LLMs for semantic parsing, enable lightweight manual interaction for disambiguation, and develop algorithms to transform the intermediate models for final symbolic model generation. To ensure the correctness of the generated symbolic model, each stage is designed based on a formal execution model and the model transformations are proven sound. To the best of our knowledge, this is the first work aiming to generate symbolic models for protocol verification from natural language documents. We also introduce a benchmark for symbolic protocol model generation, with 18 real-world security protocol's text description and their corresponding symbolic models. We then demonstrate the potential of our tool, which successfully generated correct models of moderate scale in 10 out of 18 cases. Our tool is released at [1].

Decentralized Identity (DID) enhances authentication and privacy by empowering individuals to control their own digital identities, which has gained traction globally. To our knowledge, this paper presents the first end-to-end verification effort (from design to implementation) of a real-world Decentralized Identity (DID) protocol following the IIFAA DID standard, which has been deployed within the widely used super app Alipay and issued millions of DIDs in practice. We integrate formal verification into the development lifecycle of such industrial security protocol to systematically enhance its reliability from two levels: (1) At the design level, we utilized state-of-the-art protocol design verifier Tamarin to formally model the IIFAA DID standard under a realistic threat model tailored for super apps. We then formulated and performed automated verification of desired security properties using Tamarin. We identified several design flaws that could lead to a security breach. These issues were reported to the design team and have been addressed in the updated design. (2) At the implementation level, we first extract the desired specification derived from the verified symbolic model of protocol design in the form of a set of intermediate I/O specifications. Subsequently, we translate the I/O specifications into a set of functional specifications at the implementation level, which can then be verified by the automated tool VeriFast. We identified several inconsistencies between the implementation and the verified design which are fixed by the development team and led to verified implementation faithfully obeying the verified design, together offering an end-to-end verified secure DID protocol in Alipay super app. Our work showcases how an industrial security protocol development team can design and implement a practical verified secure Decentralized Identity (DID) protocol with the help of end-to-end formal verification.

The rapid growth of decentralized applications, while revolutionizing financial transactions, has created an attractive target for malicious attacks.Existing approaches to detecting attacks often rely on predefined rules or simplistic and overly-specialized models, which lack the flexibility to handle the wide spectrum of diverse and dynamically changing attack types.To address this challenge, we present a general and extensible framework, MoE (Monitoring Ethereum), that leverages runtime verification to detect a wide range of attacks on Ethereum.MoE features an expressive attack modeling language, based on Metric First-order Temporal Logic (MFOTL), that can formalize a wide range of attacks.We integrate a novel semantic lifting approach that extracts system behaviors relevant for various attacks, which can be analyzed using the monitoring tool MonPoly.Furthermore, we also equip MoE with quantitative capabilities to evaluate the similarity between a transaction and an attack formula to enhance its performance in identifying attacks, including near-miss attacks.We carry out extensive experiments with MoE on a labeled benchmark and a large-scale dataset containing over one million transactions.On the labeled benchmark, MoE successfully detects 92.0% attacks and achieves a 45.0% higher recall rate than competing state-of-the-art tool.MoE finds 3,319 attacks with 95.4% precision on the large dataset.Furthermore, MoE uses quantitative analysis to uncover 8% additional attacks.Finally, the average time for * Xinyao Xu and Ziyu Mao contributed equally.