Constructing formal models of cryptographic protocols from Alice&Bob style specifications via LLM

Automated formal analysis is a fundamental method for ensuring the security of cryptographic protocol design. This approach entails two stages: formal modeling and formal analysis. While significant research has been conducted on formal analysis methodologies, there remains insufficient exploration into formal modeling, which has hindered the broader dissemination and development of automated formal analysis. In this paper, we address this challenge by delving into methodologies for the synthesis of formal languages, which are instrumental in constructing formal models for security protocol analysis. Our main contribution is the development of P2FGPT (Protocol specification to Formal model Generative Pre-trained Transformer), an innovative LLM-based framework designed for generating and refining cryptographic protocol formal declarations. Unlike existing methods, P2FGPT uniquely processes Alice&Bob style specifications as input. By leveraging semantic analysis, it employs LLM to perform generative synthesis of formal languages. The framework incorporates three core components: Generator, Checker, and Modifier, each serving distinct yet complementary roles in the modeling process. To rigorously evaluate our framework, we constructed a specialized dataset derived from the ProVerif's official demonstration documentation, ensuring the authority and reliability of the data. We conducted extensive experiments using three state-of-the-art LLMs (GLM4.0, Llama3-8b, Qwen2.5-7b) to validate the framework's effectiveness across different model architectures. The experimental results show that the framework can generate formal description efficiently and accurately, enabling protocol designers or analyzers to rapidly construct formal models. This work represents a significant advancement in applying LLM to cryptographic protocol analysis. By automating the construction of formal models, P2FGPT not only addresses the long-standing challenge of formal modeling but also lays a foundation for future research in automated formal analysis. Our framework provides researchers and practitioners a way to improve the efficiency and scalability of security protocol design and verification.