論文の概要: Quantum Cryptography and Autoformalization in Lean

• arxiv url: http://arxiv.org/abs/2610.17286v1
• Date: Mon, 12 Oct 2026 18:41:50 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-18 02:23:09.651114
• Title: Quantum Cryptography and Autoformalization in Lean
• Title（参考訳）: リーンにおける量子暗号とオートフォーマル化
• Abstract要約: リーン証明アシスタントで形式化されたエンドツーエンドのセキュリティ定理を作成します。 量子情報科学における公式証明エンジンの発見をいかに加速するかを示す。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Quantum key distribution provides secure communication by relying on physics principles and mathematical reasoning. Security proofs across the field can contain gaps, often between individually valid theorems integrated under mismatched assumptions. We produce an end-to-end security theorem formalized in the Lean proof assistant, eliminating hidden hypotheses by building only on Lean's standard axioms. Our proof covers composable security of the entanglement-based qubit BB84 protocol against coherent attacks by the postselection technique, accounting for finite block size, and is written in a language that enforces local operations and classical communication to help ensure a faithful representation of the protocol. The proof itself was enabled by LLM-based autoformalization, and with the proof complete, we used the same pipeline as a discovery machine, reducing the finite-size penalty on the key rate. Our work sets a reproducible standard for security arguments in quantum cryptography and shows how formal proof engines can accelerate discovery across quantum information science.
• Abstract（参考訳）: 量子鍵分布は、物理学の原理と数学的推論に頼ってセキュアな通信を提供する。 フィールド上のセキュリティ証明は、しばしば不一致な仮定の下で統合された個々に有効な定理の間のギャップを含むことができる。 私たちはLeanの証明アシスタントで形式化されたエンドツーエンドのセキュリティ定理を作成し、Leanの標準公理のみに基づいて構築することで隠れた仮説を排除します。 提案手法は, 有限ブロックサイズを考慮に入れたポストセレクション手法によるコヒーレント攻撃に対して, 絡み合いベースの BB84 プロトコルの構成可能なセキュリティをカバーし, プロトコルの忠実な表現を保証するために, ローカル操作と古典的通信を強制する言語で記述されている。 証明そのものはLLMによる自己形式化によって実現され、証明が完了すると、我々は発見機と同じパイプラインを使用してキーレートの有限サイズのペナルティを減らした。 我々の研究は、量子暗号におけるセキュリティ引数の再現可能な標準を設定し、正式な証明エンジンが量子情報科学における発見をいかに加速するかを示す。

関連論文リスト

• Succinct Arguments for QMA in the Quantum Random Oracle Model [50.20559283775139]
  量子乱数オラクルモデル(QROM)におけるQMAの最初の簡潔な議論を、暗号的仮定や証明されていない予想に頼ることなく構築する。 我々の結果は、量子インタラクティブなオラクル証明(QIOP)を同じ言語の量子引数にコンパイルする効率保存変換である。
  論文  参考訳（メタデータ） (2026-09-29T12:54:55Z)
• Game Hopping in Lean [5.623680633781937]
  本稿では,ゲームベースの暗号証明を機械化するリーン4フレームワークであるHOPSCOTCHを紹介する。 セキュリティ定義は、ステートフルな確率的オラクル間の区別不可能性として表現され、証明は標準的なゲームホッピングパラダイムに従う。 本稿では, IND-CCAの暗号化-then-MACのセキュリティ, DDHからのElGamal暗号化のセキュリティ, ワンタイムシークレットからパブリックキーのIND-CPAセキュリティへの影響, GGM擬似ランダム機能構築の形式化された証明を行った。
  論文  参考訳（メタデータ） (2026-08-06T16:52:16Z)
• Semantic Security with Infinite Dimensional Quantum Eavesdropping Channel [1.5070870469725095]
  本稿では,ワイヤタップチャネルの直接符号化定理の証明法を提案する。 この方法はブロック長の増加とともに指数関数的に減衰する誤差を生じる。 セマンティックセキュリティの量子バージョンを保証する。
  論文  参考訳（メタデータ） (2022-05-16T13:25:56Z)
• Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
  完全同型暗号方式として, 完全同型暗号方式を初めて構築する。 我々の主要な技術要素は、量子証明器が古典的検証器に量子状態の形でのLearning with Errors分布からのサンプルが削除されたことを納得させる対話的プロトコルである。
  論文  参考訳（メタデータ） (2022-03-03T10:07:32Z)
• Experimental quantum key distribution certified by Bell's theorem [0.0]
  暗号鍵交換プロトコルは、伝統的に、盗聴攻撃に対するセキュリティを提供するために、計算予想に依存しています。 量子鍵分布プロトコルは、そのような攻撃に対して情報理論のセキュリティを提供する。 しかし、量子プロトコルは、関連する物理デバイスの実装欠陥を悪用する新たなタイプの攻撃の対象となっている。 ここでは、これらの脆弱性に免疫する完全量子鍵分布プロトコルの実験的実現について述べる。
  論文  参考訳（メタデータ） (2021-09-29T17:52:48Z)
• Secure Two-Party Quantum Computation Over Classical Channels [63.97763079214294]
  古典的アリス(Alice)と量子的ボブ(Quantum Bob)が古典的なチャネルを通してのみ通信できるような設定を考える。 悪質な量子逆数の場合,ブラックボックスシミュレーションを用いた2次元量子関数を実現することは,一般に不可能であることを示す。 我々は、QMA関係Rの古典的量子知識(PoQK)プロトコルを入力として、古典的当事者によって検証可能なRのゼロ知識PoQKを出力するコンパイラを提供する。
  論文  参考訳（メタデータ） (2020-10-15T17:55:31Z)
• Semantic Security for Quantum Wiretap Channels [68.24747267214373]
  本稿では,古典的量子および量子的通信路によるセマンティックセキュリティの課題について考察する。 非セキュアなコードをセマンティックにセキュアなコードに変換するために、明示的な構造を使い、二正規の既約関数によってキャパシティを達成します。
  論文  参考訳（メタデータ） (2020-01-16T09:55:49Z)
• Quantum-secure message authentication via blind-unforgeability [74.7729810207187]
  我々は、ブラインド・アンフォージェビリティ(英語版)と呼ばれる量子敵に対する非フォージェビリティ(英語版)の自然な定義を提案する。 この概念は、予測値に「部分的に盲目」アクセスを使用できる敵が存在する場合、関数を予測可能と定義する。 標準構造と減量支援のためのブラインド・アンフォージェビリティの適合性を示す。
  論文  参考訳（メタデータ） (2018-03-10T05:31:38Z)

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

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