ModelForge: Using GenAI to Improve the Development of Security Protocols

• URL: http://arxiv.org/abs/2506.07010v1
• Date: Sun, 08 Jun 2025 06:27:09 GMT
• Title: ModelForge: Using GenAI to Improve the Development of Security Protocols
• Authors: Martin Duclos, Ivan A. Fernandez, Kaneesha Moore, Sudip Mittal, Edward Zieglar,
• Abstract summary: We introduce ModelForge, a novel tool that automates the translation of protocol specifications.<n>By leveraging advances in Natural Language Processing (NLP) and Generative AI (GenAI), ModelForge processes protocol specifications and generates a CPSA protocol definition.
• Score: 1.9241821314180376
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: Formal methods can be used for verifying security protocols, but their adoption can be hindered by the complexity of translating natural language protocol specifications into formal representations. In this paper, we introduce ModelForge, a novel tool that automates the translation of protocol specifications for the Cryptographic Protocol Shapes Analyzer (CPSA). By leveraging advances in Natural Language Processing (NLP) and Generative AI (GenAI), ModelForge processes protocol specifications and generates a CPSA protocol definition. This approach reduces the manual effort required, making formal analysis more accessible. We evaluate ModelForge by fine-tuning a large language model (LLM) to generate protocol definitions for CPSA, comparing its performance with other popular LLMs. The results from our evaluation show that ModelForge consistently produces quality outputs, excelling in syntactic accuracy, though some refinement is needed to handle certain protocol details. The contributions of this work include the architecture and proof of concept for a translating tool designed to simplify the adoption of formal methods in the development of security protocols.

Related papers

• LLM-Assisted Model-Based Fuzzing of Protocol Implementations [9.512044399020514]
  Faults in protocol behavior can lead to vulnerabilities and system failures.<n>A common approach to protocol testing involves constructing Markovian models that capture the state transitions and expected behaviors of the protocol.<n>We propose a novel method that leverages large language models (LLMs) to automatically generate sequences for testing network protocol implementations.
  arXiv  Detail & Related papers  (2025-08-03T13:16:18Z)
• ProtocolLLM: RTL Benchmark for SystemVerilog Generation of Communication Protocols [45.66401695351214]
  Large Language Models (LLMs) have shown promising capabilities in generating code for general-purpose programming languages.<n>SystemVerilogs are logic-oriented and demand strict adherence to timing, semantics, and synthesizability constraints.<n>This paper introduces the first benchmark suite targeting four widely used protocols: I2C, This, IC, and AXI.
  arXiv  Detail & Related papers  (2025-06-09T17:10:47Z)
• Type-Constrained Code Generation with Language Models [51.03439021895432]
  We introduce a type-constrained decoding approach that leverages type systems to guide code generation.<n>For this purpose, we develop novel prefix automata and a search over inhabitable types, forming a sound approach to enforce well-typedness on LLM-generated code.<n>Our approach reduces compilation errors by more than half and significantly increases functional correctness in code synthesis, translation, and repair tasks.
  arXiv  Detail & Related papers  (2025-04-12T15:03:00Z)
• Games for AI Control: Models of Safety Evaluations of AI Deployment Protocols [52.40622903199512]
  This paper introduces AI-Control Games, a formal decision-making model of the red-teaming exercise as a multi-objective, partially observable game. We apply our formalism to model, evaluate and synthesise protocols for deploying untrusted language models as programming assistants.
  arXiv  Detail & Related papers  (2024-09-12T12:30:07Z)
• CodeIP: A Grammar-Guided Multi-Bit Watermark for Large Language Models of Code [56.019447113206006]
  Large Language Models (LLMs) have achieved remarkable progress in code generation.<n>CodeIP is a novel multi-bit watermarking technique that inserts additional information to preserve provenance details.<n>Experiments conducted on a real-world dataset across five programming languages demonstrate the effectiveness of CodeIP.
  arXiv  Detail & Related papers  (2024-04-24T04:25:04Z)
• Utilizing Large Language Models to Translate RFC Protocol Specifications to CPSA Definitions [2.038893829552158]
  This paper proposes the use of Large Language Models (LLMs) for translating Request for Comments (RFC) protocol specifications into a format compatible with the Cryptographic Protocol Shapes Analyzer (CPSA) This novel approach aims to reduce the complexities and efforts involved in protocol analysis, by offering an automated method for translating protocol specifications into structured models suitable for CPSA.
  arXiv  Detail & Related papers  (2024-01-30T16:50:14Z)
• Towards Auto-Modeling of Formal Verification for NextG Protocols: A Multimodal cross- and self-attention Large Language Model Approach [3.9155346446573502]
  This paper introduces Auto-modeling of Formal Verification with Real-world Prompting for 5G and NextG protocols (AVRE) AVRE is a novel system designed for the formal verification of Next Generation (NextG) communication protocols.
  arXiv  Detail & Related papers  (2023-12-28T20:41:24Z)
• From Ambiguity to Explicitness: NLP-Assisted 5G Specification Abstraction for Formal Analysis [5.526122280732959]
  We introduce a two-step pipeline that uses NLP tools to construct data and then uses constructed data to extract identifiers and formal properties. Our results of the optimal model reach valid accuracy of 39% for extraction and 42% for formal properties identifier predictions.
  arXiv  Detail & Related papers  (2023-08-07T03:37:31Z)
• PIP: Parse-Instructed Prefix for Syntactically Controlled Paraphrase Generation [61.05254852400895]
  Parse-Instructed Prefix (PIP) is a novel adaptation of prefix-tuning to tune large pre-trained language models. In contrast to traditional fine-tuning methods for this task, PIP is a compute-efficient alternative with 10 times less learnable parameters.
  arXiv  Detail & Related papers  (2023-05-26T07:42:38Z)
• Bayesian Prompt Learning for Image-Language Model Generalization [64.50204877434878]
  We use the regularization ability of Bayesian methods to frame prompt learning as a variational inference problem. Our approach regularizes the prompt space, reduces overfitting to the seen prompts and improves the prompt generalization on unseen prompts. We demonstrate empirically on 15 benchmarks that Bayesian prompt learning provides an appropriate coverage of the prompt space.
  arXiv  Detail & Related papers  (2022-10-05T17:05:56Z)
• Exploring Software Naturalness through Neural Language Models [56.1315223210742]
  The Software Naturalness hypothesis argues that programming languages can be understood through the same techniques used in natural language processing. We explore this hypothesis through the use of a pre-trained transformer-based language model to perform code analysis tasks.
  arXiv  Detail & Related papers  (2020-06-22T21:56:14Z)
• PEL-BERT: A Joint Model for Protocol Entity Linking [6.5191667029024805]
  In this paper, we propose a model that joints a fine-tuned language model with an RFC Domain Model. Firstly, we design a Protocol Knowledge Base as the guideline for protocol EL. Secondly, we propose a novel model, PEL-BERT, to link named entities in protocols to categories in Protocol Knowledge Base. Experimental results demonstrate that our model achieves state-of-the-art performance in EL on our annotated dataset, outperforming all the baselines.
  arXiv  Detail & Related papers  (2020-01-28T16:42:40Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.