-
ModelForge: Using GenAI to Improve the Development of Security Protocols
Authors:
Martin Duclos,
Ivan A. Fernandez,
Kaneesha Moore,
Sudip Mittal,
Edward Zieglar
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 L…
▽ More
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.
△ Less
Submitted 8 June, 2025;
originally announced June 2025.
-
Utilizing Large Language Models to Translate RFC Protocol Specifications to CPSA Definitions
Authors:
Martin Duclos,
Ivan A. Fernandez,
Kaneesha Moore,
Sudip Mittal,
Edward Zieglar
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 su…
▽ More
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.
△ Less
Submitted 30 January, 2024;
originally announced February 2024.
-
Effect of MTU length on child-adult difference in neuromuscular fatigue
Authors:
Enzo Piponnier,
Vincent Martin,
Emeric Chalchat,
Bastien Bontemps,
Valérie Julian,
Olivia Bocock,
Martine Duclos,
Sébastien Ratel
Abstract:
Purpose The purpose of this study was to compare the development and etiology of neuromuscular fatigue of the knee extensor muscles (KE) at different muscle-tendon unit (MTU) lengths during repeated maximal voluntary isometric contractions (MVIC) between boys and men.Methods Twenty-two pre-pubertal boys (9-11 years) and 22 men (18-30 years) performed three KE fatigue protocols at short (SHORT), op…
▽ More
Purpose The purpose of this study was to compare the development and etiology of neuromuscular fatigue of the knee extensor muscles (KE) at different muscle-tendon unit (MTU) lengths during repeated maximal voluntary isometric contractions (MVIC) between boys and men.Methods Twenty-two pre-pubertal boys (9-11 years) and 22 men (18-30 years) performed three KE fatigue protocols at short (SHORT), optimal (OPT) and long (LONG) MTU lengths, consisting of repeating 5-s MVIC interspersed with 5-s passive recovery periods until torque reached 60% of the initial MVIC torque. The etiology of neuromuscular fatigue was identified using non-invasive methods such as surface electromyography, near-infrared spectroscopy, magnetic nerve stimulation and twitch interpolation technique.Results The number of repetitions was significantly lower in men at OPT (14.8$\pm$3.2) and LONG (15.8$\pm$5.8) than boys (39.7$\pm$18.4 and 29.5 $\pm$10.2, respectively; p<0.001), while no difference was found at SHORT between both age groups (boys: 33.7$\pm$15.4, men: 40.9$\pm$14.2). At OPT and LONG boys showed a lower reduction in the single potentiated twitch (Qtwpot) and a greater decrease in the voluntary activation level (VA) than men. At SHORT, both populations displayed a moderate Qtwpot decrement and a significant VA reduction (p<0.001). The differences in maximal torque between boys and men were almost twice greater at OPT (223.9 N.m) than at SHORT (123.3 N.m) and LONG (136.5 N.m).Conclusion The differences in neuromuscular fatigue between children and adults are dependent on MTU length. Differences in maximal torque could underpin differences in neuromuscular fatigue between children and adults at OPT and SHORT. However, at LONG these differences do not seem to be explained by differences in maximal torque. The origins of this specific effect of MTU length remain to be determined.
△ Less
Submitted 27 March, 2019;
originally announced March 2019.
