ModelForge: Using GenAI to Improve the Development of Security Protocols

TL;DR

ModelForge leverages GenAI and NLP to automate translating natural language security protocol specifications into formal representations, simplifying formal analysis adoption.

Contribution

Introduces a novel tool that automates protocol specification translation for CPSA using GenAI, enhancing accessibility of formal methods.

Findings

ModelForge produces syntactically accurate protocol definitions.

The tool outperforms other LLMs in quality of generated outputs.

Some protocol details require further refinement.

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.