Pith. sign in

REVIEW 4 major objections 5 minor 20 references

ModelForge: Using GenAI to Improve the Development of Security Protocols

T0 review · 4 major / 5 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Fine-tuned LLM turns plain English into CPSA protocol definitions

desk verdict A useful proof-of-concept for LLM-to-CPSA translation whose headline claim about syntactic accuracy is not actually checked against CPSA, and whose own limitations section admits it struggles on the real-world RFC inputs that motivate it. read the letter →

arxiv 2506.07010 v1 pith:VPTRQ2ZQ submitted 2025-06-08 cs.CR

Martin Duclos , Ivan A. Fernandez , Kaneesha Moore , Sudip Mittal , Edward Zieglar This is my paper
classification cs.CR
keywords formalmethodssecurityprotocolsCPSAlargelanguagemodelsfine-tuningsyntheticdataprotocolspecificationtranslationGPT-3.5
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper introduces ModelForge, a translator that takes natural-language security protocol specifications and produces definitions in the CPSA formal-analysis language. The authors claim that a GPT-3.5 model fine-tuned on synthetic question-answer pairs generates CPSA definitions that human experts rate as more syntactically correct and clearer than those from general-purpose LLMs, and competitive overall. The motivation is to lower the expertise barrier that keeps protocol developers from using formal verification during standards development. The paper's own evaluation shows strong syntax but unresolved weaknesses in protocol details such as public-key handling.

What carries the argument

The load-bearing mechanism is a synthetic training dataset: ten seed CPSA definitions generated by GPT-4 are paired with GPT-4-written natural-language specifications, then expanded by GPT-4-generated variance to 340 question-answer pairs, which fine-tune GPT-3.5-turbo with temperature set to zero for deterministic output. This dataset carries the argument because it substitutes for the scarce supply of real CPSA definitions and lets a general model be reshaped into a domain translator.

What would settle it

Run the full text of an existing standards document through ModelForge without manual preprocessing and count how many generated definitions parse in CPSA and produce non-empty shape sets; if most fail, the motivating use case of translating standards documents is not achieved.

Watch

Extended reading notes

Core claim

On the paper's own terms, ModelForge establishes that a domain-specific fine-tuned LLM can produce CPSA protocol definitions from natural-language queries well enough to be useful as a draft for a human expert. Across three test queries, ModelForge achieved the highest normalized correctness and clarity scores on two of them, and the authors' qualitative survey judged its CPSA syntax the best among the five systems compared. The authors also find that the model depends on the query supplying variable names and on the input being free of extraneous standards content, so the translation task is not yet solved for the motivating real-world documents.

Load-bearing premise

The load-bearing premise is that the synthetic GPT-4-generated training pairs capture the variety and detail of real protocol specifications; if the training distribution is too narrow, the high query scores will not transfer to actual standards-style input.

Editorial extensions

If this is right

  • If the syntactic edge holds on larger queries, a human-in-the-loop workflow can shift formal-methods work from writing CPSA definitions from scratch to checking and repairing machine-generated drafts.
  • Protocol developers without formal-methods expertise could obtain a first CPSA model early in the design cycle, aligning with the standards body's push for verification before proposal submission.
  • The same pipeline—small seed set, synthetic expansion, fine-tune—could be rerun for other formal tools whose input grammars are also structured, such as ProVerif or Tamarin.
  • The identified weaknesses delimit the claim: ModelForge is a draft generator, not an autonomous translator, and its outputs need expert review before analysis.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A stronger test than human ratings would be to run the generated definitions through CPSA itself and check whether they produce the expected skeletons and shapes; if most outputs fail to parse or yield empty shape sets, the syntactic praise would not translate to usable verification.
  • The variable-name dependency suggests a natural extension: coupling ModelForge with a lightweight information extractor that identifies role names, nonces, and keys from free text could close the gap to full standards-document translation without changing the core fine-tuning approach.
  • Because the dataset is generated by GPT-4 and then used to train GPT-3.5, the approach inherits any distribution bias of the generator; protocols with structures under-represented in the seed templates would be the first place to probe generalization.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 5 minor

Summary. The paper introduces ModelForge, a proof-of-concept tool that uses a fine-tuned GPT-3.5 model to translate natural-language security protocol specifications into CPSA protocol definitions. The architecture consists of a query input, an instruction prompt, a fine-tuned LLM, and post-processing steps. The authors evaluate ModelForge against four other LLMs (Claude 3.5, Llama 3.1, GPT-4o, Codestral) by having four domain experts rate outputs on correctness, clarity, and completeness, and they report that ModelForge performs well in syntactic correctness, with qualitative feedback noting its strong CPSA syntax but also weaknesses such as public-key handling. The paper frames the work as supporting the IETF's usable formal methods goals.

Significance. If the claims are supported, ModelForge would be a useful step toward lowering the barrier to formal analysis of security protocols, and the architectural description plus fine-tuning recipe could be reused for other formal-method targets. The paper also contributes an honest discussion of limitations, including sensitivity to variable names and extraneous RFC content. However, the significance is weakened by the evaluation: it relies on subjective ratings from only four participants over three hand-crafted queries, with no check of whether the generated definitions are accepted by CPSA's actual parser or analyzer. The central claim of 'excelling in syntactic accuracy' is therefore not established beyond the small, self-similar benchmark.

major comments (4)
  1. [§4.2, Table 3] The central claim that ModelForge 'excels in syntactic accuracy' is not backed by an objective check. Table 1 defines correctness as 'Output uses proper CPSA syntax,' but the paper never reports running any generated definition through CPSA's parser, the CPSA tool, or any syntax validator. Subjective ratings can miss or tolerate syntactic defects, as the paper's own Table 4 shows: an expert-flagged 'public key issue' was not caught or penalized in the quantitative ratings. The authors should validate every generated output with the actual CPSA parser and report pass/fail rates, and if Table 3 is instead about human-perceived syntax, this should be stated explicitly without implying CPSA-level syntactic correctness.
  2. [§4.1, §4.2, Table 3] The empirical basis is very small: 4 participants, 3 queries, and no statistical tests, error bars, or inter-rater reliability measures. The table reports 'normalized average ratings' but neither the raw ratings nor the normalization formula are provided. With n=4 raters, the differences in Table 3 (e.g., Query 1 correctness 0.67 vs. 0.50) are not shown to be significant. The paper should report raw scores, per-rater variability, and, at minimum, descriptive statistics; ideally it should use a small-sample statistical test or clearly label the results as informal proof-of-concept observations.
  3. [§5, Limitations and Future Work] The limitations section concedes that ModelForge 'performs better when variable names are provided' and that RFCs contain 'a considerable amount of unnecessary content,' and that both are current challenges. These are precisely the conditions of the IETF/RFC use case that motivates the work in §1 and Figure 1. The three evaluation queries (e.g., Figure 4) are clean, hand-crafted, variable-annotated prompts. The paper therefore does not demonstrate performance on realistic protocol specifications; the motivating scenario remains unvalidated. The authors should either evaluate on actual RFC text or temper the claimed contribution to a proof of concept on curated inputs.
  4. [§3.4, §4.4] The fine-tuning dataset is entirely synthetic: 340 Q&A pairs generated by GPT-4, starting from ten seed templates, and the evaluation queries are also clean, hand-crafted texts. This creates a risk of self-similarity: the model may be optimized for the distribution of GPT-4-generated specifications rather than for real-world protocol prose. The paper should report the overlap or distance between the evaluation queries and the synthetic training distribution, and should test on at least a few genuine RFC excerpts or independently written protocol descriptions to assess generalization.
minor comments (5)
  1. [§4.1] The sentence 'three distinct queries and a total of nine corresponding CPSA protocol definitions' is inconsistent with Table 3, which lists ratings for five models across three queries, implying fifteen outputs. Please clarify how many outputs were actually rated.
  2. [Table 2] The model list has inconsistent naming: 'LLama 3' in the table caption and 'LLama 3.1' in Table 3. These should be unified, and the parameter counts for GPT-4o and Codestral should be cited or stated as approximate.
  3. [§4.4] The fine-tuning section reports training and validation loss but does not state the number of training steps or the learning rate, nor how the 70/30 split was stratified (e.g., whether all ten seed templates appear in the training set). Adding these details would aid reproducibility.
  4. [§2.3] There is a stray quotation mark after 'LISP (LISt Processing)-like syntax.' and the sentence is grammatically incomplete. Please correct.
  5. [§4.5] The statement that 'ModelForge remains competitive, consistently ranking among the top-performers overall' is not directly supported by Table 3 for Query 3, where GPT-4o scores 0.80 on all dimensions and ModelForge scores 0.75, 0.50, and 0.50. The prose should more precisely characterize the per-query results.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the central claim is an empirical result grounded in human expert ratings external to the model, and no derivation step reduces to its own input.

full rationale

ModelForge is an empirical ML paper; there is no mathematical derivation chain whose conclusion equals an assumption by construction. The fine-tuning data is synthetically generated by GPT-4 (Sections 3.4 and 4.4), but the evaluation is not a re-description of that data: three hand-crafted queries are rated by four human experts on correctness, clarity, and completeness (Sections 4.1-4.2, Tables 1 and 3). The correctness criterion is defined as 'Output uses proper CPSA syntax,' and while the paper does not report running outputs through CPSA's parser, that is a limitation of measurement validity, not circularity: the expert ratings are external to the model's training objective. Section 5 concedes that ModelForge performs better when variable names are provided and that RFCs contain extraneous content; this is an honest scope limitation, not a circular step. No self-citation is load-bearing, no uniqueness theorem is imported, and no ansatz is smuggled in via citation. The reader's intuition about distribution similarity between GPT-4-generated training data and the clean evaluation queries is a benchmark representativeness concern, not an exhibitable reduction of the claimed capability to the training input.

Assumptions & free parameters 3 free parameters · 2 assumptions · 0 invented entities

The central claim rests on the synthetic data generation process and the subjective evaluation. The model weights and hyperparameters are fitted or hand-chosen, and the axioms capture assumptions about data representativeness and evaluation validity.

free parameters (3)
  • Fine-tuning dataset composition (340 synthetic Q&A pairs) = 340 pairs, 70/30 train/test split
    The dataset is generated solely by GPT-4 with no ground-truth validation against existing CPSA protocol models. The model's capabilities are entirely determined by this dataset, so the choice of dataset is a hand-chosen parameter on which the central claim rests.
  • Fine-tuning epochs = 3
    The number of epochs was selected without reported hyperparameter search; 3 epochs produced training loss 0.2976 and validation loss 0.3902, but there is no evidence this is optimal or that overfitting is avoided.
  • Sampling temperature = 0
    Set to 0 for deterministic generation of the fine-tuning dataset and protocol definitions. This choice reduces output diversity and may make the model brittle to variations in input phrasing.
assumptions (2)
  • domain assumption GPT-4 generated synthetic protocol specifications are representative of natural language descriptions in real standards documents (e.g., RFCs).
    The fine-tuning dataset is built entirely by GPT-4 starting from ten seed templates (Section 3.4). No validation against real CPSA inputs is reported.
  • domain assumption Human expert ratings of correctness, clarity, and completeness are a valid proxy for whether a generated protocol definition is correct for CPSA analysis.
    Section 4.1 defines correctness as 'Output uses proper CPSA syntax,' but the generated definitions are never run through CPSA to confirm parseability. The ratings are subjective.

how reviews work

0 comments
Cite this review

Pith. "Pith review of ModelForge: Using GenAI to Improve the Development of Security Protocols." pith.science (2026). https://pith.science/paper/VPTRQ2ZQ

@misc{pith2026250607010,
  author       = {Pith},
  title        = {Pith review of: ModelForge: Using GenAI to Improve the Development of Security Protocols},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/VPTRQ2ZQ}},
  note         = {Machine review of arXiv:2506.07010}
}
read the original 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.

Figures

Figures reproduced from arXiv: 2506.07010 by the authors.

Figure 1
Figure 1. Overview of the IETF standards process for security protocols, highlighting the lack of formal verification at key stages. ModelForge aims to automate aspects of formal methods analysis to address these gaps. (1) Developers design a new protocol, (2) compile protocol specifications into a proposal, (3) often submitting it without formal proofs, (4) leaving the IETF to establish formal proofs during review. Building … view at source ↗
Figure 2
Figure 2. Blanchet’s Protocol, defined in CPSA syntax, consists of two steps. First, the initiator (init) sends a symmetric key s to the responder (resp), signed with init’s private key (a) and encrypted with resp’s public key (b). Then, resp sends data d back to init, encrypted with s. 2.6 StrucBench Extending LLMs beyond simple text generation can be challenging. Tang et al. [19] note that LLMs, such as GPT-4, struggle with… view at source ↗
Figure 3
Figure 3. ModelForge architecture: (1) A user submits protocol specifications as a query. (2) The controller combines the query with an instruction prompt and sends it to the fine-tuned LLM. (3) The LLM generates a CPSA protocol definition. (4) The output is then delivered to the user for validation. 3.1 Query A user-provided query serves as both the input and the starting point for Mod￾elForge. The query consists of a natura… view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: Example of a user-submitted query for a secure protocol using public-key en￾cryption. This query serves as input for ModelForge. 3.4 Fine-Tuning Dataset One of the initial challenges we faced was the scarcity of CPSA protocol defini￾tions available to us for our fine-t…
Figure 5
Figure 5. Figure 5: Example of a generated CPSA protocol definition by ModelForge, illustrating the output format using s-expressions for protocol roles and trace sequences. 3.10 Controller The controller’s role is to orchestrate the sequence of execution between the ar￾chitectural compon…

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

20 extracted references · 16 canonical work pages

  1. [1]

    Duclos et al

    Bommasani, R., Hudson, D.A., Adeli, E., Altman, R., Arora, S., von Arx, S., Bernstein, M.S., Bohg, J., Bosselut, A., Brunskill, E., et al.: On the opportunities and risks of foundation models (2021) 14 M. Duclos et al

    work page 2021

  2. [2]

    Braunschweiler, N., Doddipatla, R., Keizer, S., Stoyanchev, S.: Evaluating large language models for document-grounded response generation in information- seeking dialogues (2023), https://arxiv.org/abs/2309.11838

    work page Pith review arXiv 2023

  3. [3]

    Advances in neural information processing systems33, 1877–1901 (2020)

    Brown, T., Mann, B., Ryder, N., Subbiah, M., Kaplan, J.D., Dhariwal, P., Nee- lakantan, A., Shyam, P., Sastry, G., Askell, A., et al.: Language models are few-shot learners. Advances in neural information processing systems33, 1877–1901 (2020)

    2020

  4. [4]

    22nd Annual Symposium on Foundations of Computer Science (sfcs 1981) pp

    Dolev, D., Yao, A.C.C.: On the security of public key protocols. 22nd Annual Symposium on Foundations of Computer Science (sfcs 1981) pp. 350–357 (1981)

    work page 1981

  5. [5]

    Computer Communications22(8), 697–709 (1999)

    Gritzalis, S., Spinellis, D., Georgiadis, P.: Security protocols over open networks and distributed systems: Formal methods for their analysis, design, and verifica- tion. Computer Communications22(8), 697–709 (1999)

    work page 1999

  6. [6]

    https://datatracker.ietf.org/doc/charter-irtf-ufmrg/01/ (January 2023), accessed: 1/08/2024

    Internet Engineering Task Force (IETF): Usable Formal Methods Proposed Re- search Group (UFMRG). https://datatracker.ietf.org/doc/charter-irtf-ufmrg/01/ (January 2023), accessed: 1/08/2024

    work page 2023

  7. [7]

    RFC 7296 (Oct 2014)

    Kaufman, C., Hoffman, P.E., Nir, Y., Eronen, P., Kivinen, T.: Inter- net Key Exchange Protocol Version 2 (IKEv2). RFC 7296 (Oct 2014). https://doi.org/10.17487/RFC7296, https://www.rfc-editor.org/info/rfc7296

    doi:10.17487/rfc7296 2014

  8. [8]

    Kemmerer, R.: Using formal methods to analyze encryption protocols. IEEE J. Select. Areas Commun.7(4), 448–457 (1989)

    work page 1989

Show all 20 references
  1. [9]

    Lal, S., Jain, M., Chaplot, V.: Approaches to formal verification of security proto- cols (2011), https://api.semanticscholar.org/CorpusID:18414398

    2011

  2. [10]

    The MITRE Corporation (October 2023), version 4.3

    Liskov, M.D., Ramsdell, J.D., Guttman, J.D., Rowe, P.D.: The Cryptographic Protocol Shapes Analyzer: A Manual for CPSA 4.1. The MITRE Corporation (October 2023), version 4.3

    2023

  3. [11]

    Liskov, M.D., Rowe, P.D., Thayer, F.J.: Completeness of cpsa. Tech. rep., Citeseer (2011)

    2011

  4. [12]

    https://doi.org/10.5281/zenodo.1234, https://github.com/jerryjliu/llama_index, release date: 2022-11-01

    Liu, J.: Llamaindex (November 2022). https://doi.org/10.5281/zenodo.1234, https://github.com/jerryjliu/llama_index, release date: 2022-11-01

    2022 doi

  5. [13]

    Journal of Computer security1(1), 5–35 (1992)

    Meadows, C.: Applying formal methods to the analysis of a key management pro- tocol. Journal of Computer security1(1), 5–35 (1992)

    1992

  6. [14]

    Ramsdell, J.D.: Cpsa and formal security goals (2015)

    2015

  7. [15]

    Radiology 308(1), e230970 (2023)

    Rau, A., Rau, S., Zoeller, D., Fink, A., Tran, H., Wilpert, C., Nattenmueller, J., Neubauer, J., Bamberg, F., Reisert, M., et al.: A context-based chatbot surpasses radiologists and generic chatgpt in following the acr appropriateness guidelines. Radiology 308(1), e230970 (2023)

    2023

  8. [16]

    European radiology experimental 8(1), 60 (2024)

    Rau, S., Rau, A., Nattenmüller, J., Fink, A., Bamberg, F., Reisert, M., Russe, M.F.: A retrieval-augmented chatbot based on gpt-4 provides appropriate differ- ential diagnosis in gastrointestinal radiology: a proof of concept study. European radiology experimental 8(1), 60 (2024)

    2024

  9. [17]

    RFC 8446 (Aug 2018)

    Rescorla, E.: The Transport Layer Security (TLS) Protocol Version 1.3. RFC 8446 (Aug 2018). https://doi.org/10.17487/RFC8446, https://www.rfc- editor.org/info/rfc8446

    2018 doi

  10. [18]

    RFC 1334 (Oct 1992)

    Simpson, W.A.: PPP Authentication Protocols. RFC 1334 (Oct 1992). https://doi.org/10.17487/RFC1334, https://www.rfc-editor.org/info/rfc1334

    1992 doi

  11. [19]

    Tang, X., Zong, Y., Zhao, Y., Cohan, A., Gerstein, M.: Struc-bench: Are large language models really good at generating complex structured data? (2023)

    2023

  12. [20]

    Zhang, D., Liu, W., Tan, Q., Chen, J., Yan, H., Yan, Y., Li, J., Huang, W., Yue, X., Zhou, D., et al.: Chemllm: A chemical large language model (2024)

    2024

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.