CrypFormBench: Benchmarking Formal Analysis Capability of Large Language Models for Cryptographic Schemes

• URL: http://arxiv.org/abs/2606.25561v1
• Date: Wed, 24 Jun 2026 08:37:38 GMT
• Title: CrypFormBench: Benchmarking Formal Analysis Capability of Large Language Models for Cryptographic Schemes
• Abstract summary: 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.
• Score: 16.171581449458582
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Manual formal analysis of cryptographic schemes is labor-intensive and requires substantial expertise. While model-checking tools (e.g., Scyther and Tamarin) and computational-security tools (e.g., CryptoVerif and EasyCrypt) improve the automation of security proofs, they still rely on experts to abstract schemes and write tool-specific formal descriptions. Large language models (LLMs) are a promising alternative, but their effectiveness in this domain remains unexplored due to the absence of standardized evaluation methodologies. To fill this gap, we introduce CrypFormBench (C.F.B for short), a comprehensive benchmark jointly covering symbolic and computational security to evaluate five core LLM capabilities: interpretation, generation, completion, transformation, and correction. It comprises 700 instances spanning 677 schemes, 7 mainstream formal verifier languages, and 160 security properties. The evaluation of 9 state-of-the-art LLMs reveals that most of them perform well on interpretation and completion, given their code-awareness advantages, but struggle with generation, transformation, and correction. Overall, their performance remains limited, with Claude-3.5 achieving the highest score at 48.7 out of 100. We further provide practical guidance, e.g., few-shot prompting, Pass@K sampling, and lightweight fine-tuning, to mitigate the executability bottleneck and improve tool-usable outputs. Taken together, our benchmark and analyses offer a grounded view of current progress and concrete directions toward reliable LLM-assisted formal cryptographic analysis.

Related papers

• Beyond the Syntax: Do Security Experts Trust LLMs for NIDS Rule Engineering? [70.17374586573033]
  This paper presents a human-centered investigation into Large Language Models (LLMs)-based NIDS rule engineering.<n>Our evaluation reveals a syntax-semantics paradox: although LLMs generate syntactically correct rules, experts find them only partially deployable.<n>While large-scale models consistently produce syntactically valid rules, small models are largely ineffective for IDS rule generation.
  arXiv  Detail & Related papers  (2026-07-07T07:09:56Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  Large language models (LLMs) and agents have shown promising progress, but their true capabilities and failure modes remain unclear.<n>We present the first systematic and contamination-aware study of LLM- and agent-based formal specification generation for C programs.
  arXiv  Detail & Related papers  (2026-05-02T11:31:33Z)
• From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification [0.30915521808748864]
  Large Language Models show promise in automated software engineering, yet their guarantee of correctness is frequently undermined by erroneous or hallucinated code.<n>We provide the NaturalLanguage2VerifiedCode dataset: a collection of 60 complex algorithmic problems.<n>We evaluate 11 randomly selected problem sets across seven open-weight LLMs using a tiered prompting strategy.<n>Our results show that while contextless prompting leads to near-universal failure, structural anchors and iterative self-healing facilitate a dramatic performance turnaround.
  arXiv  Detail & Related papers  (2026-04-24T14:28:10Z)
• Compiled AI: Deterministic Code Generation for LLM-Based Workflow Automation [3.225273674498579]
  We study compiled AI, a paradigm in which large language models generate executable code artifacts during a compilation phase, after which execute deterministically without further model invocation.<n>Our contribution is a systems-oriented study of its application to high-stakes runtime enterprise.
  arXiv  Detail & Related papers  (2026-04-06T20:25:20Z)
• RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
  Large Language Models (LLMs) have demonstrated remarkable capabilities in code generation, but their proficiency in producing secure code remains a critical, under-explored area.<n>We introduce RealSec-bench, a new benchmark for secure code generation meticulously constructed from real-world, high-risk Java repositories.
  arXiv  Detail & Related papers  (2026-01-30T08:29:01Z)
• LLMxCPG: Context-Aware Vulnerability Detection Through Code Property Graph-Guided Large Language Models [2.891351178680099]
  This paper presents a novel framework integrating Code Property Graphs (CPG) with Large Language Models (LLM) for robust vulnerability detection.<n>Our approach's ability to provide a more concise and accurate representation of code snippets enables the analysis of larger code segments.<n> Empirical evaluation demonstrates LLMxCPG's effectiveness across verified datasets, achieving 15-40% improvements in F1-score over state-of-the-art baselines.
  arXiv  Detail & Related papers  (2025-07-22T13:36:33Z)
• VerifyThisBench: Generating Code, Specifications, and Proofs All at Once [9.383313869205628]
  We introduce a new benchmark that evaluates end-to-end program verification from natural language descriptions.<n>Our evaluation reveals that even state-of-the-art (SOTA) models, such as o3-mini, achieve a pass rate of less than 4%.
  arXiv  Detail & Related papers  (2025-05-25T19:00:52Z)
• BinMetric: A Comprehensive Binary Analysis Benchmark for Large Language Models [50.17907898478795]
  We introduce BinMetric, a benchmark designed to evaluate the performance of large language models on binary analysis tasks.<n>BinMetric comprises 1,000 questions derived from 20 real-world open-source projects across 6 practical binary analysis tasks.<n>Our empirical study on this benchmark investigates the binary analysis capabilities of various state-of-the-art LLMs, revealing their strengths and limitations in this field.
  arXiv  Detail & Related papers  (2025-05-12T08:54:07Z)
• CASTLE: Benchmarking Dataset for Static Code Analyzers and LLMs towards CWE Detection [2.5228276786940182]
  This paper introduces CASTLE, a benchmarking framework for evaluating the vulnerability detection capabilities of different methods.<n>We assess 13 static analysis tools, 10 LLMs, and 2 formal verification tools using a hand-crafted dataset of 250 micro-benchmark programs covering 25 common CWEs.
  arXiv  Detail & Related papers  (2025-03-12T14:30:05Z)
• EquiBench: Benchmarking Large Language Models' Reasoning about Program Semantics via Equivalence Checking [58.15568681219339]
  We introduce EquiBench, a new benchmark for evaluating large language models (LLMs)<n>This task directly tests a model's ability to reason about program semantics.<n>We evaluate 19 state-of-the-art LLMs and find that in the most challenging categories, the best accuracies are 63.8% and 76.2%, only modestly above the 50% random baseline.
  arXiv  Detail & Related papers  (2025-02-18T02:54:25Z)
• BigCodeBench: Benchmarking Code Generation with Diverse Function Calls and Complex Instructions [72.56339136017759]
  We introduce BigCodeBench, a benchmark that challenges Large Language Models (LLMs) to invoke multiple function calls as tools from 139 libraries and 7 domains for 1,140 fine-grained tasks.<n>Our evaluation shows that LLMs are not yet capable of following complex instructions to use function calls precisely, with scores up to 60%, significantly lower than the human performance of 97%.<n>We propose a natural-language-oriented variant of BigCodeBench, BigCodeBench-Instruct, that automatically transforms the original docstrings into short instructions only with essential information.
  arXiv  Detail & Related papers  (2024-06-22T15:52:04Z)
• SORRY-Bench: Systematically Evaluating Large Language Model Safety Refusal [64.9938658716425]
  SORRY-Bench is a proposed benchmark for evaluating large language models' (LLMs) ability to recognize and reject unsafe user requests.<n>First, existing methods often use coarse-grained taxonomy of unsafe topics, and are over-representing some fine-grained topics.<n>Second, linguistic characteristics and formatting of prompts are often overlooked, like different languages, dialects, and more -- which are only implicitly considered in many evaluations.
  arXiv  Detail & Related papers  (2024-06-20T17:56:07Z)

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.