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

Area of Science:

• Computer Science
• Cybersecurity
• Formal Methods

Background:

• Automated formal analysis is crucial for cryptographic protocol security, comprising formal modeling and analysis stages.
• Existing research heavily focuses on formal analysis, neglecting formal modeling, which impedes the progress of automated formal analysis.
• The synthesis of formal languages is key to constructing formal models for security protocol analysis.

Purpose of the Study:

• To address the challenge of insufficient formal modeling methodologies in automated formal analysis.
• To introduce P2FGPT (Protocol specification to Formal model Generative Pre-trained Transformer), an LLM-based framework for generating and refining formal declarations of cryptographic protocols.
• To enable efficient and accurate construction of formal models for security protocol design and verification.

Main Methods:

• Developed P2FGPT, an LLM-based framework that takes Alice&Bob style specifications as input.
• Utilized semantic analysis and LLM for generative synthesis of formal languages via Generator, Checker, and Modifier components.
• Evaluated the framework using a specialized dataset from ProVerif's documentation and three state-of-the-art LLMs (GLM4.0, Llama3-8b, Qwen2.5-7b).

Main Results:

• P2FGPT demonstrates efficient and accurate generation of formal descriptions for cryptographic protocols.
• The framework's effectiveness was validated across different LLM architectures, confirming its versatility.
• Experimental results confirm the framework's capability to rapidly construct formal models.

Conclusions:

• P2FGPT significantly advances the application of LLMs in cryptographic protocol analysis by automating formal model construction.
• The framework overcomes the long-standing challenge in formal modeling, paving the way for future research in automated formal analysis.
• P2FGPT enhances the efficiency and scalability of security protocol design and verification for researchers and practitioners.