論文の概要: ShannonProver: Towards Automating Formal Cryptographic Proofs

• arxiv url: http://arxiv.org/abs/2607.02847v2
• Date: Wed, 08 Jul 2026 21:06:54 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-07-10 14:45:27.244132
• Title: ShannonProver: Towards Automating Formal Cryptographic Proofs
• Title（参考訳）: ShannonProver: フォーマルな暗号証明の自動化を目指す
• Abstract要約: ShannonProverは暗号証明を自動化するエージェントフレームワークである。 暗号化者がセキュリティモデルを提供し、ターゲット定理をProvレベルの証明義務に分解する設定をターゲットにしている。 本稿では,ShannonProverがケーススタディの暗号証明工学のかなりの部分を自動化可能であることを示す。
• 参考スコア（独自算出の注目度）: 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.
• Abstract（参考訳）: 暗号証明は、手動で検証するコミュニティの能力を超えた規模で作成される。 マシンチェックされた証明は、スケーラブルな証明検証への道筋を提供するが、EasyCryptのような表現力のある証明アシスタントのための証明スクリプトを書くことは、依然として大きなボトルネックである。 本稿では,暗号証明を自動化するエージェントフレームワークであるShannonProverについて述べる。 ShannonProverは、暗号化者がセキュリティモデルと目標定理を補題レベルの証明義務に分解する設定を目標とし、システムはそれらの義務に対するEasyCrypt証明スクリプトを自動構築する。 我々はShannonProverをEasyCryptの正式な暗号証明のデータセットで評価した。 データセットは教科書のプリミティブ、デプロイプロトコル、NIST提案などの標準化作業にまたがっており、これまでオンラインで利用できなかったコーパスから抽出された専門ケーススタディを含んでいる。 本稿では,ChaChaPoly1305やMEE-CBCなどのケーススタディにおいて,ShannonProverが暗号証明技術のかなりの部分を自動化可能であることを示す。 この研究は、暗号研究を加速する道のりを示唆している。エージェントが証明・エンジニアリングの負担を自動化するにつれ、暗号学者は新たな構築をすばやく反復し、早期にマシンチェックされた保証を取得し、設計からデプロイまでの信頼できるプロトコルをより早く導入することができる。

関連論文リスト

• Scratchy: Visual-Scratchpad Multimodal Reasoning for Cryptographic Proof Generation in EasyCrypt [8.739112129971362]
  大規模言語モデル(LLM)は、最近、形式的証明生成において大きな進歩を遂げた。 計算セキュリティの議論は、有効な証明は確率、逆ゲーム、不変量、仮定および境界を調整しなければならないと仮定する。 本稿では、これらの依存関係をマルチモーダル生成に公開するビジュアルスクラッチパッドアプローチであるScratchyを提案する。
  論文  参考訳（メタデータ） (2026-09-05T18:49:38Z)
• Game Hopping in Lean [5.623680633781937]
  本稿では,ゲームベースの暗号証明を機械化するリーン4フレームワークであるHOPSCOTCHを紹介する。 セキュリティ定義は、ステートフルな確率的オラクル間の区別不可能性として表現され、証明は標準的なゲームホッピングパラダイムに従う。 本稿では, IND-CCAの暗号化-then-MACのセキュリティ, DDHからのElGamal暗号化のセキュリティ, ワンタイムシークレットからパブリックキーのIND-CPAセキュリティへの影響, GGM擬似ランダム機能構築の形式化された証明を行った。
  論文  参考訳（メタデータ） (2026-08-06T16:52:16Z)
• CryptanalysisBench: Can LLMs do Cryptanalysis? [76.79639292270497]
  CryptanalysisBenchは、暗号プリミティブの6つのファミリーにまたがる191のタスクである。 我々のベンチマークは3つの階層から構成されている: (i) 実用的ブレークを既知のプリミティブ; (ii) 実用的ブレークを知らないプリミティブ。 5つのフロンティアモデルではタイア1スキームの65%-86%、全力で6-12ティア2スキーム、全スケールダウンモデルの24-61が破られる。
  論文  参考訳（メタデータ） (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]
  バイブコーディングは高速で、低臨界のコンシューマソフトウェアには適しています。 DO-178C、IEC 61508、ISO 26262によって管理される安全クリティカルなシステムでは、認証への道は提供されない。 フォーマルな検証を通じてビブコーディングをガイドするクローズドループパイプラインであるForgeを紹介します。
  論文  参考訳（メタデータ） (2026-06-21T10:01:45Z)
• Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
  Chain-of-Thoughtプロンプトは、大規模言語モデル(LLM)から推論能力を引き出すデファクトメソッドとなっている。 検出が極めて難しいCoTの幻覚を緩和するために、現在の方法は不透明なボックスとして機能し、彼らの判断に対する確認可能な証拠を提供しておらず、おそらくその効果を制限する。 任意のスコアを割り当てるのではなく、各推論ステップで形式数学言語Lean 4で数学的主張を明確にし、幻覚を識別するための公式な証明を提供しようとしている。
  論文  参考訳（メタデータ） (2025-06-05T03:16:08Z)
• Provably Secure Public-Key Steganography Based on Admissible Encoding [66.38591467056939]
  一見無害な秘密文の中に秘密メッセージを隠蔽する技術は、Proprovably secure steganography (PSS)として知られている。 PSSは対称鍵ステガノグラフィーから公開鍵ステガノグラフィーへと進化し、事前共有鍵の必要なしに機能する。 本稿では,許容エンコーディングに基づくより一般的な楕円曲線公開鍵ステガノグラフィ法を提案する。
  論文  参考訳（メタデータ） (2025-04-28T03:42:25Z)
• From Scientific Texts to Verifiable Code: Automating the Process with Transformers [2.536225150399618]
  トランスフォーマーは 研究論文を読めます 正式な証明を持つアルゴリズムを 提案し これらの証明を 検証可能なコードに翻訳します このアプローチは形式的検証の障壁を大幅に減らすことができると我々は主張する。
  論文  参考訳（メタデータ） (2025-01-09T14:03:35Z)
• CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection [41.94295877935867]
  我々は,新たな暗号プロトコルの脆弱性を自律的に識別する大規模言語モデルの能力を評価するためのベンチマークを導入する。 私たちは、新しい、欠陥のある通信プロトコルのデータセットを作成し、AIエージェントが発見した脆弱性を自動的に検証する方法を設計しました。
  論文  参考訳（メタデータ） (2024-11-20T14:16:55Z)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  私たちは、Rustコードの自動証明生成を可能にする、人書きスニペットの欠如を克服するフレームワークであるSAFEを紹介します。 SAFEは、細調整されたモデルの自己老化能力を訓練するために、多数の合成不正確な証明を再利用する。 我々は、人間の専門家によるベンチマークで52.52%の精度で達成し、GPT-4oのパフォーマンス14.39%を大きく上回った。
  論文  参考訳（メタデータ） (2024-10-21T08:15:45Z)
• ImProver: Agent-Based Automated Proof Optimization [18.315243539816464]
  リーンの任意のユーザ定義メトリクスを最適化するために、証明を書き換える大規模な言語モデルエージェントであるImProverを紹介します。 我々は、現実世界の学部生、競争、研究レベルの数学定理の書き換えについてImProverをテストする。
  論文  参考訳（メタデータ） (2024-10-07T05:14:18Z)
• miniCodeProps: a Minimal Benchmark for Proving Code Properties [22.548472305010005]
  私たちはLeanの証明アシスタントで201のプログラム仕様のベンチマークであるminiCodePropsを紹介します。 その単純さにもかかわらず、MiniCodePropsは現在のLLMベースのプローバーを壊すのに十分である。
  論文  参考訳（メタデータ） (2024-06-16T21:11:23Z)
• CodeChameleon: Personalized Encryption Framework for Jailbreaking Large Language Models [49.60006012946767]
  パーソナライズされた暗号化手法に基づく新しいジェイルブレイクフレームワークであるCodeChameleonを提案する。 我々は、7つの大規模言語モデルに関する広範な実験を行い、最先端の平均アタック成功率(ASR)を達成する。 GPT-4-1106上で86.6%のASRを実現する。
  論文  参考訳（メタデータ） (2024-02-26T16:35:59Z)
• CryptoVerif: a Computationally-Sound Security Protocol Verifier (Initial Version with Communications on Channels) [2.06682776181122]
  この文書はセキュリティプロトコル検証器CryptoVerifを示す。 これはシンボリックなドレフ・ヤオモデルではなく、計算モデルに依存している。 自動で動作させることもできるし、手動による証明表示でガイドすることもできる。
  論文  参考訳（メタデータ） (2023-10-23T07:53:38Z)
• CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model [8.838422697156195]
  我々はCryptoVampire暗号プロトコル検証を初めて導入し、BC論理におけるトレース特性の証明を完全に自動化した。 主要な技術的貢献は、プロトコルプロパティの1次(FO)形式化と、サブターム関係の調整されたハンドリングである。 理論面では、全FO論理を暗号公理で制限し、HO BC論理の表現性を失うことにより、音質を損なわないことを保証する。
  論文  参考訳（メタデータ） (2023-05-20T11:26:51Z)
• Proof-of-Learning is Currently More Broken Than You Think [41.3211535926634]
  本稿では,Proof-of-Learning(PoL)検証の異なる構成で再現できる最初のスプーフィング戦略を紹介する。 我々はPoLの重要な脆弱性を特定し、証明の堅牢な検証に必要な前提条件を体系的に分析する。 我々は,ディープラーニングにおける最適化のさらなる理解なしに,実証可能な堅牢なPoL検証機構を開発することはできないと結論づける。
  論文  参考訳（メタデータ） (2022-08-06T19:07:07Z)
• Cross-Thought for Sentence Encoder Pre-training [89.32270059777025]
  Cross-Thoughtは、事前トレーニングシーケンスエンコーダに対する新しいアプローチである。 我々は、Transformerベースのシーケンスエンコーダを、多数の短いシーケンスに対してトレーニングする。 質問応答とテキストのエンコーダタスクの実験は、事前学習したエンコーダが最先端のエンコーダより優れていることを示す。
  論文  参考訳（メタデータ） (2020-10-07T21:02:41Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。