ShannonProver: Towards Automating Formal Cryptographic Proofs

• URL: http://arxiv.org/abs/2607.02847v2
• Date: Wed, 08 Jul 2026 21:06:54 GMT
• Title: ShannonProver: Towards Automating Formal Cryptographic Proofs
• Abstract summary: ShannonProver is an agentic framework for automating cryptographic proofs.<n>It targets the setting in which a cryptographer provides the security model and a decomposition of the target theorem into Prov-level proof obligations.<n>We show that ShannonProver can automate substantial portions of cryptographic proof engineering for case studies.
• Score: 14.266077895853288
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Cryptographic proofs are produced at a scale that increasingly exceeds the community's ability to verify them manually. Machine-checked proofs offer a path toward scalable proof verification, but writing proof scripts for expressive proof assistants such as EasyCrypt remains a major bottleneck: even when the high-level proof plan is known, converting it into proof tactics requires substantial reasoning effort. This paper presents ShannonProver, an agentic framework for automating cryptographic proofs. ShannonProver targets the setting in which a cryptographer provides the security model and a decomposition of the target theorem into lemma-level proof obligations, while the system automatically constructs EasyCrypt proof scripts for those obligations. We evaluate ShannonProver on a dataset of formal cryptographic proofs in EasyCrypt. The dataset spans textbook primitives, deployed protocols, and standardization efforts such as NIST proposals, and includes expert case studies drawn from a corpus that has not previously been available online. We show that ShannonProver can automate substantial portions of cryptographic proof engineering for case studies such as ChaChaPoly1305 and MEE-CBC. More broadly, this work suggests a path toward accelerating cryptographic research: as agents automate the proof-engineering burden, cryptographers can iterate more quickly on new constructions, obtain machine-checked assurance earlier, and bring trustworthy protocols from design to deployment faster.

Related papers

• Scratchy: Visual-Scratchpad Multimodal Reasoning for Cryptographic Proof Generation in EasyCrypt [8.739112129971362]
  Large language models (LLMs) have recently made substantial progress in formal proof generation.<n> Computational security arguments posit that a valid proof must coordinate probability, adversarial games, invariants, assumptions and bounds.<n>This paper presents Scratchy, a visual-scratchpad approach that exposes these dependencies for multimodal generation.
  arXiv  Detail & Related papers  (2026-09-05T18:49:38Z)
• Game Hopping in Lean [5.623680633781937]
  We present HOPSCOTCH, a Lean 4 framework for mechanizing sound, game-based cryptographic proofs.<n>Security definitions are expressed as indistinguishability between stateful probabilistic oracles, and proofs follow the standard game-hopping paradigm.<n>We illustrate the framework with formalized proofs of the IND-CCA security of encrypt-then-MAC, the security of ElGamal encryption from DDH, the implication from one-time secrecy to public-key IND-CPA security, and the GGM pseudorandom-function construction.
  arXiv  Detail & Related papers  (2026-08-06T16:52:16Z)
• CryptanalysisBench: Can LLMs do Cryptanalysis? [76.79639292270497]
  We introduce CryptanalysisBench, 191 tasks across six families of cryptographic primitives.<n>Our benchmark consists of three tiers: (i) primitives with known practical breaks; (ii) primitives with no known practical break, evaluated both at full strength and as scaled-down variants.<n>Five frontier models break 65%-86% of Tier 1 schemes, 6-12 Tier-2 schemes at full strength, and 24-61 across all scaled-down variants.
  arXiv  Detail & Related papers  (2026-07-20T22:09:40Z)
• Formal-Method-Guided Vibe Coding: Closing the Verification Loop on AI-Generated Safety-Critical Software Through Model-Driven Engineering [40.048798975817924]
  Vibe coding is fast and may be adequate for low-criticality consumer software.<n>For safety-critical systems governed by DO-178C, IEC 61508, or ISO 26262, it offers no path to certification.<n>We present Forge, a closed-loop pipeline that guides vibe coding through formal verification.
  arXiv  Detail & Related papers  (2026-06-21T10:01:45Z)
• Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
  Chain-of-Thought prompting has become the de facto method to elicit reasoning capabilities from large language models (LLMs)<n>To mitigate hallucinations in CoT that are notoriously difficult to detect, current methods operate as opaque boxes and do not provide checkable evidence for their judgments, possibly limiting their effectiveness.<n>We propose a retrospective, step-aware formal verification framework $Safe$. Rather than assigning arbitrary scores, we strive to articulate mathematical claims in formal mathematical language Lean 4 at each reasoning step and provide formal proofs to identify hallucinations.
  arXiv  Detail & Related papers  (2025-06-05T03:16:08Z)
• Provably Secure Public-Key Steganography Based on Admissible Encoding [66.38591467056939]
  The technique of hiding secret messages within seemingly harmless covertext is known as provably secure steganography (PSS)<n>PSS evolves from symmetric key steganography to public-key steganography, functioning without the requirement of a pre-shared key.<n>This paper proposes a more general elliptic curve public key steganography method based on admissible encoding.
  arXiv  Detail & Related papers  (2025-04-28T03:42:25Z)
• From Scientific Texts to Verifiable Code: Automating the Process with Transformers [2.536225150399618]
  transformers can read research papers that propose algorithms with formal proofs and translate these proofs into verifiable code.<n>We argue that this approach can significantly reduce the barrier to formal verification.
  arXiv  Detail & Related papers  (2025-01-09T14:03:35Z)
• CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection [41.94295877935867]
  We introduce a benchmark to assess the ability of Large Language Models to autonomously identify vulnerabilities in new cryptographic protocols. We created a dataset of novel, flawed, communication protocols and designed a method to automatically verify the vulnerabilities found by the AI agents.
  arXiv  Detail & Related papers  (2024-11-20T14:16:55Z)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  We introduce SAFE, a framework that overcomes the lack of human-written snippets to enable automated proof generation of Rust code.<n> SAFE re-purposes the large number of synthesized incorrect proofs to train the self-ging capability of the fine-tuned models.<n>We achieve a 52.52% accuracy rate in a benchmark crafted by human experts, a significant leap over GPT-4o's performance of 14.39%.
  arXiv  Detail & Related papers  (2024-10-21T08:15:45Z)
• ImProver: Agent-Based Automated Proof Optimization [18.315243539816464]
  We present ImProver, a large-language-model agent that rewrites proofs to optimize arbitrary user-defined metrics in Lean. We test ImProver on rewriting real-world undergraduate, competition, and research-level mathematics theorems.
  arXiv  Detail & Related papers  (2024-10-07T05:14:18Z)
• miniCodeProps: a Minimal Benchmark for Proving Code Properties [22.548472305010005]
  We present miniCodeProps, a benchmark of 201 program specifications in the Lean proof assistant. Despite its simplicity, miniCodeProps is sufficient to break current LLM-based provers.
  arXiv  Detail & Related papers  (2024-06-16T21:11:23Z)
• CodeChameleon: Personalized Encryption Framework for Jailbreaking Large Language Models [49.60006012946767]
  We propose CodeChameleon, a novel jailbreak framework based on personalized encryption tactics. We conduct extensive experiments on 7 Large Language Models, achieving state-of-the-art average Attack Success Rate (ASR) Remarkably, our method achieves an 86.6% ASR on GPT-4-1106.
  arXiv  Detail & Related papers  (2024-02-26T16:35:59Z)
• CryptoVerif: a Computationally-Sound Security Protocol Verifier (Initial Version with Communications on Channels) [2.06682776181122]
  This document presents the security protocol verifier CryptoVerif. It does not rely on the symbolic, Dolev-Yao model, but on the computational model. It can work automatically, or the user can guide it with manual proof indications.
  arXiv  Detail & Related papers  (2023-10-23T07:53:38Z)
• CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model [8.838422697156195]
  We introduce the CryptoVampire cryptographic protocol verifier, which for the first time fully automates proofs of trace properties in the BC Logic. Key technical contribution is a first-order (FO) formalization of protocol properties with tailored handling of subterm relations. On the theoretical side, we restrict full FO logic with cryptographic axioms to ensure that, by losing the expressivity of the HO BC Logic, we do not lose soundness.
  arXiv  Detail & Related papers  (2023-05-20T11:26:51Z)
• Proof-of-Learning is Currently More Broken Than You Think [41.3211535926634]
  We introduce the first spoofing strategies that can be reproduced across different configurations of the Proof-of-Learning (PoL) verification. We identify key vulnerabilities of PoL and systematically analyze the underlying assumptions needed for robust verification of a proof. We conclude that one cannot develop a provably robust PoL verification mechanism without further understanding of optimization in deep learning.
  arXiv  Detail & Related papers  (2022-08-06T19:07:07Z)
• Cross-Thought for Sentence Encoder Pre-training [89.32270059777025]
  Cross-Thought is a novel approach to pre-training sequence encoder. We train a Transformer-based sequence encoder over a large set of short sequences. Experiments on question answering and textual entailment tasks demonstrate that our pre-trained encoder can outperform state-of-the-art encoders.
  arXiv  Detail & Related papers  (2020-10-07T21:02:41Z)

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.