論文の概要: FVQKD: A Formal Verification of Quantum Key Distribution Security in Rocq

• arxiv url: http://arxiv.org/abs/2610.30645v1
• Date: Thu, 22 Oct 2026 03:06:21 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-24 02:08:44.196792
• Title: FVQKD: A Formal Verification of Quantum Key Distribution Security in Rocq
• Title（参考訳）: FVQKD: Rocqにおける量子キー配布セキュリティの形式検証
• Abstract要約: 本稿では,量子鍵分布証明を機械学習で検証するFVQKDを提案する。 最初の原則から完全な証明基盤を再構築する。 これはQKDセキュリティ証明の最初のエンドツーエンドの形式検証である。
• 参考スコア（独自算出の注目度）: 7.812556323227458
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Quantum key distribution (QKD), whose security is derived from quantum mechanics rather than computational assumptions, is moving into standardization and commercial deployment. Yet its security guarantees rest on technically delicate proofs checked by hand. Formal verification closes this gap, establishing a two-factor assurance: unconditional security from physical principles, and machine-checked proofs against reasoning errors. We present FVQKD, a Rocq library for machine-checking QKD security proofs. Its first result is a complete, end-to-end machine-checked proof of composable, finite-key security for BB84. The mechanization reconstructs the complete proof infrastructure from first principles, including the smooth entropy framework, the entropic uncertainty relation, and the Quantum Leftover Hash Lemma. It uncovers necessary side conditions that the published argument leaves unstated, one of which reveals a missing proof branch, and it grounds the information-theoretic bound in a formal semantics of protocol execution, which the pen-and-paper analysis lacks. The proof is entirely admit-free, relying only on the Rocq kernel and standard foundational axioms. To our knowledge, this is the first end-to-end formal verification of a QKD security proof. Built on MathComp, MathComp-Analysis, and CoqQ, the development provides quantum-information infrastructure designed for reuse across broader QKD variants and quantum cryptography applications.
• Abstract（参考訳）: 量子鍵分布(Quantum Key Distribution, QKD)は、計算的な仮定ではなく、量子力学に由来するセキュリティであり、標準化と商用展開へと移行しつつある。 しかし、そのセキュリティは、技術的に繊細な証明を手作業でチェックすることを保証する。 形式的検証は、このギャップを埋め、物理的原則からの無条件のセキュリティと、推論エラーに対するマシンチェックされた証明という、2要素の保証を確立する。 本稿では,機械学習によるQKDセキュリティ証明を行うRocqライブラリであるFVQKDを紹介する。 最初の結果はBB84の完全なエンドツーエンドのマシンチェックによる有限鍵セキュリティの証明である。 機械化は、スムーズなエントロピーの枠組み、エントロピーの不確実性関係、量子残余Hash Lemmaを含む第一原理から完全な証明基盤を再構築する。 これは、公表された議論が公表されていない必要条件を明らかにし、そのうちの1つは、欠落した証明分岐を明らかにし、ペンとペーパーの分析が欠落しているプロトコル実行の形式的意味論において、情報理論のバウンダリを根拠にしている。 この証明は完全に無罪であり、Rocqカーネルと標準基底公理にのみ依存している。 我々の知る限り、これはQKDセキュリティ証明のエンドツーエンドの正式な検証としては初めてのものです。 MathComp、MathComp-Analysis、CoqQをベースとして開発されたこの開発は、より広範なQKD変種と量子暗号アプリケーションの再利用のために設計された量子情報基盤を提供する。

関連論文リスト

• Quantum Cryptography and Autoformalization in Lean [0.0]
  リーン証明アシスタントで形式化されたエンドツーエンドのセキュリティ定理を作成します。 量子情報科学における公式証明エンジンの発見をいかに加速するかを示す。
  論文  参考訳（メタデータ） (2026-10-12T18:41:50Z)
• Rigorous Security Proofs for Practical Quantum Key Distribution [0.0]
  この論文は量子鍵分配(QKD)プロトコルの厳密なセキュリティ解析に関係している。 IID集団攻撃に対する可変長QKDプロトコルのセキュリティ証明を確立し、この結果をポストセレクション手法を用いてコヒーレント攻撃に拡張する。 第2に,このプロトコルの観測統計値のみを用いて,エントロピー不確実性関係に基づく位相誤差率と位相誤差率に基づく証明の有界化手法を開発した。 第3に、限界制約付きエントロピー累積定理に基づく、非常に一般的なセキュリティ解析を示す。
  論文  参考訳（メタデータ） (2026-04-23T15:48:02Z)
• Send the Key in Cleartext: Halving Key Consumption while Preserving Unconditional Security in QKD Authentication [59.664950447941386]
  量子鍵分配(QKD)プロトコルは、蒸留された鍵の無条件のセキュリティを維持するために、古典的なチャネルの情報理論セキュア(ITS)認証を必要とする。 QKDは相互認証を必要とするため、2つの独立したワンタイム鍵は通常ラウンド毎に消費される。 我々は$varepsilon$-Almost Strongly Universal$(varepsilon$-ASU$)に基づく新しいITS認証方式を提案する。
  論文  参考訳（メタデータ） (2026-03-26T14:36:05Z)
• Quantum Key Distribution with Imperfections: Recent Advances in Security Proofs [0.0]
  量子鍵分配(QKD)は、2つの空間的に分離されたパーティが情報理論的に安全な暗号化を確立することを可能にする。 広範囲の盗聴戦略に対して堅牢なセキュリティ証明は、いくつかのQKDプロトコルの理論的健全性を確立している。 ほとんどの証明は、そのようなプロトコルに関わる物理系の理想化されたモデルに基づいており、実際的な実装では満たされない仮定を含むことが多い。
  論文  参考訳（メタデータ） (2026-02-04T21:16:33Z)
• Device-Independent Quantum Key Distribution: Protocols, Quantum Games, and Security [0.0]
  量子鍵分布(Quantum Key Distribution, QKD)は、量子力学の法則に基づいて、確実にセキュアな通信を可能にする。 理論上のセキュリティ保証にもかかわらず、実用的なQKDシステムは、サイドチャネル攻撃や検出器の抜け穴を含む深刻な攻撃に対して脆弱である。 デバイス独立量子鍵分布(DIQKD)は、観測された非局所相関のみに依存することにより、これらの制限を克服する。
  論文  参考訳（メタデータ） (2025-05-20T11:52:21Z)
• A consolidated and accessible security proof for finite-size decoy-state quantum key distribution [0.0]
  我々は,コヒーレント攻撃に対する有限サイズ1-デコイおよび2-デコイBB84プロトコルに対する厳密で包括的なセキュリティ証明を提供する。 我々は、多くの作品から概念を広く統合し、統一し、基礎となる前提を徹底的に議論し、技術的な矛盾を解消する。
  論文  参考訳（メタデータ） (2024-05-26T14:13:33Z)
• Existential Unforgeability in Quantum Authentication From Quantum Physical Unclonable Functions Based on Random von Neumann Measurement [45.386403865847235]
  物理的非閉包関数(PUF)は、固有の非閉包不可能な物理的ランダム性を利用して、ユニークな入出力ペアを生成する。 量子PUF(Quantum PUFs)は、量子状態を入出力ペアとして使用することによって、この概念を拡張している。 ランダムなユニタリQPUFは、量子多項式時間に対する実存的非偽造性を達成できないことを示す。 本稿では,QPUFが非単体量子チャネルとして機能する2番目のモデルを提案する。
  論文  参考訳（メタデータ） (2024-04-17T12:16:41Z)
• Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
  完全同型暗号方式として, 完全同型暗号方式を初めて構築する。 我々の主要な技術要素は、量子証明器が古典的検証器に量子状態の形でのLearning with Errors分布からのサンプルが削除されたことを納得させる対話的プロトコルである。
  論文  参考訳（メタデータ） (2022-03-03T10:07:32Z)
• Backflash Light as a Security Vulnerability in Quantum Key Distribution Systems [77.34726150561087]
  量子鍵分布(QKD)システムのセキュリティ脆弱性について概説する。 我々は主に、盗聴攻撃の源となるバックフラッシュ光(backflash light)と呼ばれる特定の効果に焦点を当てる。
  論文  参考訳（メタデータ） (2020-03-23T18:23:12Z)

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

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