The reviewed record of science sign in
Pith

arxiv: 2604.27601 · v2 · pith:OVCYLFVB · submitted 2026-04-30 · cs.CR

SecGoal: A Benchmark for Extracting Formalizable Security Goals from Protocol Documents

Dawei Huang , Hui Li , Bo Jia , Haonan Feng , Jingjing Guan , Yueshuang Jiao , Xiangdong Li This is my paper

Reviewed by Pith T0 review T1 audit T2 compute T3 formal T4 kernel 2026-07-01 08:16 UTCgrok-4.3pith:OVCYLFVBrecord.jsonopen to challenge →

classification cs.CR
keywords security goal extractionprotocol documentsformal verificationLLM fine-tuningbenchmark datasetcryptographic protocolsstructured property generation
0
0 comments X

The pith

Fine-tuning a 9B LLM on expert annotations raises precision of extracting formalizable security goals from 24% to 66.6% with 97.6% recall.

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

The paper presents SecGoal, an expert-annotated dataset spanning 15 deployed protocols, to measure how well models can pull formalizable security goal statements out of natural-language protocol documents. Frontier LLMs reach high recall of the underlying properties but low precision because they mix in non-goal material such as background or implementation details. Fine-tuning Gemma2-9B on the dataset lifts precision to 66.6% while keeping property recall at 97.6%, beating both larger prompted models and encoder baselines. The companion AIFG framework shows that concise extracted goals support high-recall structured property generation, leaving over-generation as the chief remaining limit. The work therefore supplies a dataset, benchmark, and generation method aimed at reducing the manual step that currently blocks formal verification of cryptographic protocols.

Core claim

Expert-annotated data in SecGoal lets smaller open-source LLMs become far more selective extractors of formalizable security goals than larger prompted models; on held-out protocols Gemma2-9B-FT reaches 66.6% extraction precision and 97.6% property recall while AIFG demonstrates that concise goal statements enable high-recall structured property generation, with expert-vetted inputs exposing over-generation as the dominant remaining bottleneck.

What carries the argument

SecGoal expert-annotated dataset of 15 protocols paired with AIFG, a schema- and flow-conditioned generator that turns extracted goal statements into structured formal security properties.

If this is right

  • Smaller open-source models fine-tuned on SecGoal outperform larger prompted LLMs on selective extraction.
  • Property recall near 98% is achievable alongside the precision lift.
  • Concise extracted goals fed to AIFG produce high-recall structured properties.
  • Over-generation appears only when inputs come from automatic extraction rather than expert vetting.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same annotation-plus-fine-tuning pattern could be applied to other specification documents such as API standards or hardware manuals.
  • If the precision gain holds, formal-verification teams could process many more protocols per year without increasing expert review time.
  • A follow-up experiment could test whether the same fine-tuned model maintains its precision on protocols released after the training cut-off.
  • The bottleneck of over-generation might be addressed by adding a second filtering stage that scores generated properties against the original document text.

Load-bearing premise

Expert annotations correctly and consistently mark which sentences in the protocol documents are formalizable security goals rather than background or implementation text.

What would settle it

Independent experts re-annotate the held-out test protocols; if the fine-tuned model then scores below 40% precision on the new labels, the reported selectivity gains would be falsified.

Figures

Figures reproduced from arXiv: 2604.27601 by Bo Jia, Dawei Huang, Haonan Feng, Hui Li, Jingjing Guan, Xiangdong Li, Yueshuang Jiao.

Figure 1
Figure 1. Figure 1: The Protocol Formal Verification Workflow. view at source ↗
Figure 2
Figure 2. Figure 2: Overview of the AIFG framework. 3 The SecGoal Dataset This section presents SecGoal, detailing our pro￾tocol selection criteria, data processing pipeline, human-in-the-loop annotation methodology, and final dataset statistics. 3.1 Data Selection and Scope The SecGoal dataset encompasses a diverse array of 15 widely deployed protocols spanning criti￾cal domains, including telecommunications (e.g., 5G-AKA), … view at source ↗
Figure 3
Figure 3. Figure 3: Performance comparison of security goal extraction across LLMs. view at source ↗
Figure 4
Figure 4. Figure 4: Evaluation results on the test set comparing off-the-shelf instruction-tuned models (Instruct) with those view at source ↗
read the original abstract

Formal verification provides rigorous guarantees for cryptographic security, yet extracting formalizable security goals from natural-language protocol documents remains largely manual. We introduce SecGoal, a dedicated expert-annotated dataset and benchmark for extracting formalizable security goal statements from protocol documents, covering 15 widely deployed protocols, together with AIFG, a schema- and flow-conditioned framework for structured formal security property generation. Our evaluation shows that frontier and large LLMs achieve high property recall but low extraction precision because they often fail to distinguish formalizable security goals from non-goal protocol content. In contrast, SecGoal fine-tuning makes smaller open-source LLMs substantially more selective extractors of formalizable security goals. On the held-out test protocols, Gemma2-9B-FT improves extraction precision from 24.0\% to 66.6\% and reaches 97.6\% property recall, outperforming larger prompted LLMs and encoder baselines. In a controlled setting, AIFG shows that concise goal inputs can support high-recall structured property generation, while expert-vetted extracted inputs reveal over-generation as the main remaining bottleneck. Together, SecGoal and AIFG provide a dataset, benchmark, and framework for specification-grounded security goal extraction and property generation.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper introduces SecGoal, an expert-annotated dataset covering 15 widely deployed protocols, as a benchmark for extracting formalizable security goal statements from natural-language protocol documents. It also presents AIFG, a schema- and flow-conditioned framework for structured formal security property generation. The central empirical result is that fine-tuning smaller open-source LLMs on SecGoal substantially improves extraction precision (Gemma2-9B-FT reaches 66.6% from a 24.0% baseline) while attaining 97.6% property recall on held-out test protocols, outperforming larger prompted LLMs and encoder baselines; AIFG further shows that concise goal inputs enable high-recall property generation.

Significance. If the ground-truth annotations are shown to be reliable, SecGoal and AIFG would constitute a useful, reproducible resource for reducing the manual effort in formal verification pipelines by automating the identification of security goals from protocol specifications. The fine-tuning results provide concrete evidence that domain-specific adaptation can address the precision bottleneck observed in zero-shot LLM extraction, which is a practically relevant finding for the security community.

major comments (2)
  1. [Dataset construction section] Dataset construction section: the manuscript provides no inter-annotator agreement statistic, no annotation guidelines, and no adjudication procedure for labeling sentences as formalizable security goals versus background or implementation content. Because all reported precision and recall figures (including the 24.0% o 66.6% improvement and 97.6% recall) are computed against these labels as fixed ground truth, the absence of IAA directly undermines the interpretability of the benchmark and the fine-tuning gains.
  2. [Evaluation section] Evaluation on held-out protocols: the paper does not report statistical significance tests or confidence intervals on the precision/recall differences between fine-tuned and prompted models. Given that the headline claim rests on these specific numeric improvements, the lack of statistical grounding makes it difficult to assess whether the observed gains are robust.
minor comments (1)
  1. [Abstract and Introduction] The abstract and §1 could more clearly state the train/test split sizes and the exact definition of 'formalizable' used by annotators.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback on dataset reliability and evaluation robustness. We respond to each major comment below.

read point-by-point responses

  1. Referee: [Dataset construction section] Dataset construction section: the manuscript provides no inter-annotator agreement statistic, no annotation guidelines, and no adjudication procedure for labeling sentences as formalizable security goals versus background or implementation content. Because all reported precision and recall figures (including the 24.0% o 66.6% improvement and 97.6% recall) are computed against these labels as fixed ground truth, the absence of IAA directly undermines the interpretability of the benchmark and the fine-tuning gains.

    Authors: We agree that explicit documentation of the annotation process is necessary for benchmark interpretability. The SecGoal annotations were produced by domain experts using a written protocol that defines formalizable security goals versus background/implementation content; this protocol and the adjudication steps (initial labeling followed by expert review for disagreements) were omitted from the initial submission for brevity. In revision we will add a dedicated subsection (and appendix) reproducing the annotation guidelines verbatim, describing the annotator pool, and reporting any available inter-annotator agreement on a sampled subset. If the primary annotations were performed by a single lead expert with secondary review, we will state this limitation explicitly rather than claim multi-annotator IAA. revision: yes

  2. Referee: [Evaluation section] Evaluation on held-out protocols: the paper does not report statistical significance tests or confidence intervals on the precision/recall differences between fine-tuned and prompted models. Given that the headline claim rests on these specific numeric improvements, the lack of statistical grounding makes it difficult to assess whether the observed gains are robust.

    Authors: We accept that the current manuscript lacks statistical grounding for the reported deltas. Although the absolute improvements are large, we will recompute the held-out metrics with bootstrap confidence intervals and paired significance tests (McNemar’s test for precision/recall at the sentence level) and include these results in the revised evaluation section and tables. revision: yes

Circularity Check

0 steps flagged

No circularity: empirical benchmark on held-out protocols with no self-referential derivations

full rationale

The paper presents an empirical benchmark introducing the SecGoal dataset of expert-annotated protocol documents and evaluates fine-tuned models on held-out test protocols. Reported metrics (precision/recall improvements) are computed via standard train/test splits on distinct protocols. No equations, fitted parameters, or derivations are present that reduce any claimed result to the input data by construction. No self-citation chains, uniqueness theorems, or ansatzes are invoked as load-bearing elements. The evaluation is self-contained against external held-out data and does not rely on renaming or self-definitional steps.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the domain assumption that expert human annotations provide reliable ground truth for formalizable security goals and that the 15 protocols plus held-out split are representative of real protocol documents. No free parameters or invented entities are introduced beyond standard supervised fine-tuning.

axioms (1)
  • domain assumption Expert annotations reliably identify formalizable security goals
    The benchmark and all reported metrics depend on the quality and consistency of the human labels used as ground truth.

pith-pipeline@v0.9.1-grok · 5762 in / 1188 out tokens · 49325 ms · 2026-07-01T08:16:38.379679+00:00 · methodology

Review history (2 revisions) →

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

2 extracted references · 2 canonical work pages

  1. [1]

    online" 'onlinestring :=

    ENTRY address archivePrefix author booktitle chapter edition editor eid eprint eprinttype howpublished institution journal key month note number organization pages publisher school series title type volume year doi pubmed url lastchecked label extra.label sort.label short.list INTEGERS output.state before.all mid.sentence after.sentence after.block STRING...

    work page

  2. [2]

    write newline

    " write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION word.in bbl.in capitalize " " * FUNCT...

    work page