Constructing formal models of cryptographic protocols from Alice&Bob style specifications via LLM
Abstract 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 exp...
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Nature Portfolio
2025-04-01
|
| Series: | Scientific Reports |
| Subjects: | |
| Online Access: | https://doi.org/10.1038/s41598-025-93373-y |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1850201442944548864 |
|---|---|
| author | Qiang Li Jihong Han Lin Yuan Xiangcheng Li Xiaoyu Wang |
| author_facet | Qiang Li Jihong Han Lin Yuan Xiangcheng Li Xiaoyu Wang |
| author_sort | Qiang Li |
| collection | DOAJ |
| description | Abstract 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. |
| format | Article |
| id | doaj-art-d9fdd366b5944305bf5e5c2f9efee72b |
| institution | OA Journals |
| issn | 2045-2322 |
| language | English |
| publishDate | 2025-04-01 |
| publisher | Nature Portfolio |
| record_format | Article |
| series | Scientific Reports |
| spelling | doaj-art-d9fdd366b5944305bf5e5c2f9efee72b2025-08-20T02:12:01ZengNature PortfolioScientific Reports2045-23222025-04-0115111710.1038/s41598-025-93373-yConstructing formal models of cryptographic protocols from Alice&Bob style specifications via LLMQiang Li0Jihong Han1Lin Yuan2Xiangcheng Li3Xiaoyu Wang4Information Engineering University, The Third InstituteInformation Engineering University, The Third InstituteInformation Engineering University, The Third InstituteInformation Engineering University, The Third InstituteInformation Engineering University, The Third InstituteAbstract 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.https://doi.org/10.1038/s41598-025-93373-yCryptographic protocolAlice& Bob style specificationsFormal model constructionPrompt engineering |
| spellingShingle | Qiang Li Jihong Han Lin Yuan Xiangcheng Li Xiaoyu Wang Constructing formal models of cryptographic protocols from Alice&Bob style specifications via LLM Scientific Reports Cryptographic protocol Alice& Bob style specifications Formal model construction Prompt engineering |
| title | Constructing formal models of cryptographic protocols from Alice&Bob style specifications via LLM |
| title_full | Constructing formal models of cryptographic protocols from Alice&Bob style specifications via LLM |
| title_fullStr | Constructing formal models of cryptographic protocols from Alice&Bob style specifications via LLM |
| title_full_unstemmed | Constructing formal models of cryptographic protocols from Alice&Bob style specifications via LLM |
| title_short | Constructing formal models of cryptographic protocols from Alice&Bob style specifications via LLM |
| title_sort | constructing formal models of cryptographic protocols from alice bob style specifications via llm |
| topic | Cryptographic protocol Alice& Bob style specifications Formal model construction Prompt engineering |
| url | https://doi.org/10.1038/s41598-025-93373-y |
| work_keys_str_mv | AT qiangli constructingformalmodelsofcryptographicprotocolsfromalicebobstylespecificationsviallm AT jihonghan constructingformalmodelsofcryptographicprotocolsfromalicebobstylespecificationsviallm AT linyuan constructingformalmodelsofcryptographicprotocolsfromalicebobstylespecificationsviallm AT xiangchengli constructingformalmodelsofcryptographicprotocolsfromalicebobstylespecificationsviallm AT xiaoyuwang constructingformalmodelsofcryptographicprotocolsfromalicebobstylespecificationsviallm |