論文の概要: Game Hopping in Lean

• arxiv url: http://arxiv.org/abs/2608.06261v1
• Date: Thu, 06 Aug 2026 16:52:16 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-08-07 17:43:06.808038
• Title: Game Hopping in Lean
• Title（参考訳）: リーンにおけるゲームホッピング
• Authors: Stefan Dziembowski, Grzegorz Fabiański, Daniele Micciancio, Rafał Stefański,
• Abstract要約: 本稿では,ゲームベースの暗号証明を機械化するリーン4フレームワークであるHOPSCOTCHを紹介する。 セキュリティ定義は、ステートフルな確率的オラクル間の区別不可能性として表現され、証明は標準的なゲームホッピングパラダイムに従う。 本稿では, IND-CCAの暗号化-then-MACのセキュリティ, DDHからのElGamal暗号化のセキュリティ, ワンタイムシークレットからパブリックキーのIND-CPAセキュリティへの影響, GGM擬似ランダム機能構築の形式化された証明を行った。
• 参考スコア（独自算出の注目度）: 5.623680633781937
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We present HOPSCOTCH, a Lean 4 framework for mechanizing computationally sound, game-based cryptographic proofs. Security definitions are expressed as indistinguishability between stateful probabilistic oracles, and proofs follow the standard game-hopping paradigm. HOPSCOTCH uses a shallow embedding: oracles and reductions are ordinary Lean definitions, enabling direct integration with the full Lean ecosystem, including general mathematical theories from Mathlib, such as finite-group theory. A game-hopping proof in HOPSCOTCH is represented as an explicit formal object whose constructors correspond to the standard steps of a game-hopping argument, making proofs easier to construct, automate, and inspect. We prove a general computational soundness theorem that interprets these proof objects by constructing reductions against the assumptions they use and deriving a concrete bound on the advantage of any distinguisher. Observational equivalence between oracles is established using a state-abstraction methodology: a simple yet powerful approach that supports transformations such as adding or forgetting state and replacing eager sampling with lazy sampling. 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. To the best of our knowledge, the last is the first mechanized proof of GGM for non-constant depth.
• Abstract（参考訳）: HOPSCOTCHは,ゲームベースの暗号証明を機械化するための,Lean 4フレームワークである。 セキュリティ定義は、ステートフルな確率的オラクル間の区別不可能性として表現され、証明は標準的なゲームホッピングパラダイムに従う。 オラクルと還元は通常のリーン定義であり、有限群理論のようなMathlibの一般的な数学的理論を含む完全なリーンエコシステムと直接統合できる。 HOPSCOTCHのゲームホッピング証明は、コンストラクタがゲームホッピング引数の標準ステップに対応する明示的な形式オブジェクトとして表現され、証明の構築、自動化、検査が容易になる。 我々は、これらの証明対象を、それらが使用する仮定に対する還元を構築し、いかなる微分器の利点にもとづく具体的な境界を導出することによって解釈する一般的な計算音響性定理を証明した。 オーラクル間の観測的等価性は、状態抽出手法を用いて確立される: 状態の追加や忘れ、熱心なサンプリングを遅延サンプリングに置き換えるといった変換をサポートする、単純で強力なアプローチである。 本稿では, IND-CCAの暗号化-then-MACのセキュリティ, DDHからのElGamal暗号化のセキュリティ, ワンタイムシークレットからパブリックキーのIND-CPAセキュリティへの影響, GGM擬似ランダム機能構築の形式化された証明を行った。 我々の知る限りでは、GGMの非定常深度に関する最初の機械化証明である。

関連論文リスト

• BioZKFHE: Scalable Encrypted Biometric Identification via Verifiable Homomorphic Similarity Evaluation [20.524348401618735]
  BioZKFHEは、検証可能な同型類似性評価によるスケーラブルな暗号化生体認証のためのフレームワークである。 BGV準同型計算と委員会による証明/復号化とオープンな証明バッチのスマートコントラクト検証を組み合わせる。 FaceNetとMobileFaceNetの実験では、ほぼ無数のバイオメトリックなユーティリティ、最大67%の暗号化ストレージの削減、22～44秒のエンドツーエンドの証明検証ランタイムが示されている。
  論文  参考訳（メタデータ） (2026-07-24T08:08:54Z)
• ShannonProver: Towards Automating Formal Cryptographic Proofs [14.266077895853288]
  ShannonProverは暗号証明を自動化するエージェントフレームワークである。 暗号化者がセキュリティモデルを提供し、ターゲット定理をProvレベルの証明義務に分解する設定をターゲットにしている。 本稿では,ShannonProverがケーススタディの暗号証明工学のかなりの部分を自動化可能であることを示す。
  論文  参考訳（メタデータ） (2026-07-03T00:50:51Z)
• Anamorphic Encryption with CCA Security: A Standard Model Construction [32.95661036494699]
  アナモルフィック暗号化は秘密通信にとって重要なツールであり、コンパイル後のシナリオにおいても機密性を維持する。 我々は、PKAKEM(Public-Key)とSKAKEM(Symmetric-Key)の両方を包含するAnamorphic Key Encapsulation Mechanism(AKEM)を定式化する。 本稿では, 標準モデルにおける厳密な形式的証明を提供し, カプセル化キーを制御する「独裁者」に対してレジリエンスを示す。
  論文  参考訳（メタデータ） (2026-04-09T03:49:41Z)
• Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
  大規模言語モデル(LLM)は、現実のパーソナライズされたアプリケーションにますます統合されている。 RAGで使用される知識基盤の貴重かつしばしばプロプライエタリな性質は、敵による不正使用のリスクをもたらす。 これらの知識基盤を保護するための透かし技術として一般化できる既存の方法は、一般的に毒やバックドア攻撃を含む。 我々は、無害な」知識基盤の著作権保護の名称を提案する。
  論文  参考訳（メタデータ） (2025-02-10T09:15:56Z)
• Prototype-based Aleatoric Uncertainty Quantification for Cross-modal Retrieval [139.21955930418815]
  クロスモーダル検索手法は、共通表現空間を共同学習することにより、視覚と言語モダリティの類似性関係を構築する。 しかし、この予測は、低品質なデータ、例えば、腐敗した画像、速いペースの動画、詳細でないテキストによって引き起こされるアレタリック不確実性のために、しばしば信頼性が低い。 本稿では, 原型に基づくAleatoric Uncertainity Quantification (PAU) フレームワークを提案する。
  論文  参考訳（メタデータ） (2023-09-29T09:41:19Z)
• CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model [8.838422697156195]
  我々はCryptoVampire暗号プロトコル検証を初めて導入し、BC論理におけるトレース特性の証明を完全に自動化した。 主要な技術的貢献は、プロトコルプロパティの1次(FO)形式化と、サブターム関係の調整されたハンドリングである。 理論面では、全FO論理を暗号公理で制限し、HO BC論理の表現性を失うことにより、音質を損なわないことを保証する。
  論文  参考訳（メタデータ） (2023-05-20T11:26:51Z)
• Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
  完全同型暗号方式として, 完全同型暗号方式を初めて構築する。 我々の主要な技術要素は、量子証明器が古典的検証器に量子状態の形でのLearning with Errors分布からのサンプルが削除されたことを納得させる対話的プロトコルである。
  論文  参考訳（メタデータ） (2022-03-03T10:07:32Z)

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

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