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

arXiv: https://arxiv.org/abs/2606.25561 · HTML: https://mlsanity.com/paper/2606.25561/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 24 Jun 2026.

## Built on by (most cited first, 2 of 2)

- [Evaluating Large Language Models for Symbolic Security Protocol Analysis](https://mlsanity.com/paper/2607.20712/) (2026)
- [CESBench: Benchmarking Large Language Models on Cryptographic Engineering Security for IoT Devices](https://mlsanity.com/paper/2609.21344/) (2026)

## Abstract (arXiv)

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.