SecGoal: A Benchmark for Security Goal Extraction and Formalization from Protocol Documents

• URL: http://arxiv.org/abs/2604.27601v1
• Date: Thu, 30 Apr 2026 08:50:03 GMT
• Title: SecGoal: A Benchmark for Security Goal Extraction and Formalization from Protocol Documents
• Abstract summary: SecGoal is the first expert-annotated benchmark covering 15 widely deployed protocol documents.<n>We introduce SecGoal and AIFG, an AI-assisted framework that decomposes the task into context-aware goal extraction.
• Score: 3.363429643522915
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Formal verification provides rigorous guarantees for cryptographic security, yet automating the extraction and formalization of security goals from natural language protocol documents remains a major bottleneck, compounded by the scarcity of expert-annotated resources and integrated frameworks bridging unstructured text and symbolic logic. We introduce SecGoal, the first expert-annotated benchmark covering 15 widely deployed protocol documents, including 5G-AKA and TLS 1.3, and AIFG, an AI-assisted framework that decomposes the task into context-aware goal extraction and retrieval-augmented formalization. We conduct a comprehensive evaluation to assess whether contemporary LLMs are ready to automate this pipeline. Our results reveal a pronounced precision-recall imbalance: frontier models, such as Gemini 2.5-Pro, achieve high recall but precision below 15%, frequently misclassifying operational text as security goals. In contrast, instruction tuning on SecGoal enables compact models with 7B/9B parameters to achieve F1-scores above 80%, substantially outperforming larger general-purpose models. Our work establishes a foundational dataset and reproducible baseline for automated formal protocol analysis.

Related papers

• A2ABreak: Systematic Security Analysis of the A2A Protocol [9.340181893879683]
  This paper presents A2ABreak, the first rigorous systematic security analysis of the A2A protocol.<n>We introduce a novel framework that utilizes an LLM-assisted extraction of a verified finite-state machine directly from the natural-language specification.<n>Our analysis uncovers 11 new vulnerabilities, each exploitable by a specification-compliant adversary without requiring any implementation flaw.
  arXiv  Detail & Related papers  (2026-09-09T22:18:36Z)
• A Hybrid LLM-Based Framework for Automated Security Annotation Generation in Business Process Models [1.527655765319308]
  This paper presents a hybrid framework that takes a BPMN process model and a security requirements document as input and automatically generates security annotations adhering to the SecBPMN2 specification.<n>The framework is evaluated comprehensively on a curated dataset of 27 process models from various domains.
  arXiv  Detail & Related papers  (2026-08-14T15:11:10Z)
• CrypFormBench: Benchmarking Formal Analysis Capability of Large Language Models for Cryptographic Schemes [16.171581449458582]
  Large language models (LLMs) are a promising alternative, but their effectiveness in this domain remains unexplored.<n>We introduce CrypFormBench (C.F.B), a benchmark jointly covering symbolic and computational security to evaluate five core LLM capabilities.<n>It comprises 700 instances spanning 677 schemes, 7 mainstream formal verifier languages, and 160 security properties.<n>Overall, their performance remains limited, with Claude-3.5 achieving the highest score at 48.7 out of 100.
  arXiv  Detail & Related papers  (2026-06-24T08:37:38Z)
• Auto-ART: Structured Literature Synthesis and Automated Adversarial Robustness Testing [0.0]
  We analyze nine peer-reviewed corpus sources through seven complementary protocols.<n>We introduce Auto-ART, an open-source framework that operationalizes identified gaps.<n> Empirical validation on RobustBench demonstrates that Auto-ART's pre-screening identifies gradient masking in 92% of flagged cases.
  arXiv  Detail & Related papers  (2026-04-22T15:46:11Z)
• Benchmarking Large Language Models for Safety Data Extraction [0.0]
  This study benchmarks state-of-the-art Large Language Models (LLMs) for automated SDS data extraction.<n>We evaluate four models: Gemini 1.5 Pro, GPT-4o, Claude 3.7 Sonnet, and Llama 3.1-70B, across three prompting strategies.<n>Results show that text-based extraction consistently outperforms multimodal processing across all metrics.
  arXiv  Detail & Related papers  (2026-04-22T12:12:25Z)
• SecPI: Secure Code Generation with Reasoning Models via Security Reasoning Internalization [50.71047638695205]
  Reasoning language models (RLMs) are increasingly used in programming.<n>Yet, even state-of-the-art RLMs frequently introduce critical security vulnerabilities in generated code.<n>We present SecPI, a fine-tuning pipeline that teaches RLMs to internalize structured security reasoning.
  arXiv  Detail & Related papers  (2026-04-04T04:29:11Z)
• GLM-OCR Technical Report [65.42028025507491]
  GLM-OCR is an efficient compact model designed for real-world document understanding.<n>It combines a CogViT visual encoder with a GLM language decoder, achieving a strong balance between computational efficiency and recognition performance.<n>Extensive evaluations on public benchmarks and industrial scenarios show that GLM-OCR achieves competitive or state-of-the-art performance.
  arXiv  Detail & Related papers  (2026-03-11T15:55:47Z)
• LDP: An Identity-Aware Protocol for Multi-Agent LLM Systems [0.0]
  Current protocols do not expose model-level properties as first-class primitives, ignoring properties fundamental to effective delegation.<n>We present the LLM Delegate Protocol (LDP), an AI-native communication protocol introducing five mechanisms.<n>Identity-aware routing achieves 12x lower latency on easy tasks through delegate specialization, though it does not improve aggregate quality in our small delegate pool.
  arXiv  Detail & Related papers  (2026-03-09T19:13:17Z)
• SPM-Bench: Benchmarking Large Language Models for Scanning Probe Microscopy [12.070587084660096]
  We present an original, PhD-level multimodal benchmark specifically designed for scanning probe microscopy (SPM)<n>By employing Anchor-Gated Sieve (AGS) technology, we efficiently extract high-value image-text pairs from arXiv and journal papers published between 2023 and 2025.<n>Our pipeline achieves extreme token savings while maintaining high dataset purity.
  arXiv  Detail & Related papers  (2026-02-26T13:08:56Z)
• AutoMalDesc: Large-Scale Script Analysis for Cyber Threat Research [81.04845910798387]
  Generating natural language explanations for threat detections remains an open problem in cybersecurity research.<n>We present AutoMalDesc, an automated static analysis summarization framework that operates independently at scale.<n>We publish our complete dataset of more than 100K script samples, including annotated seed (0.9K) datasets, along with our methodology and evaluation framework.
  arXiv  Detail & Related papers  (2025-11-17T13:05:25Z)
• Automated Skill Decomposition Meets Expert Ontologies: Bridging the Granularity Gap with LLMs [1.2891210250935148]
  This paper investigates automated skill decomposition using Large Language Models (LLMs)<n>Our framework standardizes the pipeline from prompting and generation to normalization and alignment with ontology nodes.<n>To evaluate outputs, we introduce two metrics: a F1-score that uses optimal embedding-based matching to assess content accuracy, and a hierarchy-aware F1-score that credits structurally correct placements to assess granularity.
  arXiv  Detail & Related papers  (2025-10-13T12:03:06Z)
• Bridging LLM Planning Agents and Formal Methods: A Case Study in Plan Verification [5.177308274872149]
  We introduce a novel framework for evaluating the alignment between natural language plans and their expected behavior by converting them into Kripke structures and Linear Temporal Logic (LTL)<n>We systematically evaluate this framework on a simplified version of the PlanBench plan verification dataset and report on metrics like Accuracy, Precision, Recall and F1 scores.
  arXiv  Detail & Related papers  (2025-10-03T19:46:55Z)
• ReliabilityRAG: Effective and Provably Robust Defense for RAG-based Web-Search [69.60882125603133]
  We present ReliabilityRAG, a framework for adversarial robustness that explicitly leverages reliability information of retrieved documents.<n>Our work is a significant step towards more effective, provably robust defenses against retrieved corpus corruption in RAG.
  arXiv  Detail & Related papers  (2025-09-27T22:36:42Z)
• CoVeR: Conformal Calibration for Versatile and Reliable Autoregressive Next-Token Prediction [49.09876340754804]
  conformsctextCoVeR is a model-free decoding strategy that balances search efficiency with the need for versatile trajectories.<n>We show that conformsctextCoVeR simultaneously maintains a compact search space and ensures high coverage probability over desirable trajectories.
  arXiv  Detail & Related papers  (2025-09-05T01:07:12Z)
• Hybrid-Segmentor: A Hybrid Approach to Automated Fine-Grained Crack Segmentation in Civil Infrastructure [52.2025114590481]
  We introduce Hybrid-Segmentor, an encoder-decoder based approach that is capable of extracting both fine-grained local and global crack features. This allows the model to improve its generalization capabilities in distinguish various type of shapes, surfaces and sizes of cracks. The proposed model outperforms existing benchmark models across 5 quantitative metrics (accuracy 0.971, precision 0.804, recall 0.744, F1-score 0.770, and IoU score 0.630), achieving state-of-the-art status.
  arXiv  Detail & Related papers  (2024-09-04T16:47:16Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.