Utilizing Large Language Models to Translate RFC Protocol Specifications to CPSA Definitions

TL;DR

This paper introduces a novel method using Large Language Models to automatically translate RFC protocol specifications into CPSA-compatible definitions, simplifying protocol analysis and enhancing security assessments.

Contribution

It presents an innovative LLM-based translation approach that automates converting RFCs into formal models for CPSA, reducing manual effort and complexity.

Findings

Successful implementation of RFC Protocol Translator

Improved accessibility of formal methods analysis

Potential for enhanced internet protocol security

Abstract

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. In this paper we discuss the implementation of an RFC Protocol Translator, its impact on enhancing the accessibility of formal methods analysis, and its potential for improving the security of internet protocols.