Quantum Cryptography and Autoformalization in Lean

安全な通信の世界において、最も信頼されている鍵は鋼鉄で作られるのではなく、物理学の基本法則によって作られます。これが量子鍵配送（QKD）の領域であり、アリスとボブと呼ばれる二人が、メッセージを保護するための共有された秘密のコードを生成する手法です。複雑な数学的問題を解くことの難しさに依存する従来の暗号とは異なり、このアプローチは、光の微粒子であるフォトンの測定が必然的にその状態を変化させるという事実に依拠しています。もし、イブと呼ばれる第三者の盗聴者が聞き耳を立てようとすれば、彼女は自身の干渉による検知可能な痕跡を残すことになります。数十年にわたり、科学者たちはこれらの鍵を作成するためのプロトコルを開発してきましたが、これらのシステムが真に安全であることを証明するプロセスは脆弱なものでした。証明はしばしば、異なる論文から繋ぎ合わされた数学的議論の連鎖に依存しており、それぞれの論文には独自の仮定が存在していました。もしその連鎖のどこか一つのリンクが他のものとわずかに不一致であったり、あるいは隠れた仮定が見落とされていたりすれば、誰にも気づかれることなく、セキュリティの保証全体が損なわれる可能性がありました。

マサチューセッツ工科大学の研究チームは、数学的論理をチェックするように設計されたコンピュータプログラムを用いて、基礎からセキュリティ証明を構築することにより、この脆弱性に対処しました。彼らは、鍵を生成するためにもつれ状態にある粒子のペアを使用する、BB84プロトコルと呼ばれる特定の広く用いられている手法に焦点を当てました。すべての論理ステップが整合していることを検証するために人間に頼る代わりに、彼らはセキュリティの議論全体を、コンピュータが読み取り、絶対的な精度で検証できる形式言語へと翻訳しました。その結果、隠れた隙間や不一致の仮定を一切許さない、マシンチェックされた証明が得られました。これにより、交換される粒子の数が限られている場合でも、プロトコルが安全であり続けることが確認されました。これは、現実世界の制約として一般的であり、しばしばセキュリティの推定値を弱めてしまう要因です。さらに、この証明を検証したのと同じコンピュータシステムを使用して、新しい、よりタイトな数学的境界を見つけ出し、有限サイズによる鍵レートへのペナルティを減少させることに成功しました。

研究者たちは、局所操作および古典通信（LOCC）のルールを厳格に強制するデジタル言語をコンピュータシステム内に作成することから始めました。量子暗号の文脈において、これは、アリスとボブが自身の粒子に対してのみ操作を行うことができ、公開チャネルを通じてのみ情報を共有でき、決して魔法のように互いのプライベートなデータにアクセスすることはできないことを意味します。この言語はガードレールとして機能し、人間の査読者が見逃してしまうような論理的エラーを防ぎます。例えば、これらの証明を形式化しようとする以前の試みでは、人工知能エージェントが、両者が実際には所有していない文字列を組み合わせることで最終的な鍵を作成するという手法を提案したことがありました。コンピュータの厳格なルールは、これを即座に不可能であるとフラグ立てし、チームにアプローチの洗練を強いました。この制約された環境内でプロトコルをステップ・バイ・ステップで構築することで、チームは最終的なセキュリティ定理が、彼らが保護しようとしている物理的プロセスを正確に記述することを保証しました。

プロトコルの構築後、チームは、盗聴者が粒子を一つずつではなく、すべての粒子に対して同時に干渉する「コヒーレント攻撃」と呼ばれる強力な攻撃に対するセキュリティを、コンピュータに検証させました。コンピュータは、粒子の初期測定から、エラー訂正およびプライバシー増幅の最終ステップに至るまで、あらゆる論理的ステップをチェックしました。そして、プロトコルが安全であることを確認しました。つまり、システムが中断されない限り、得られる鍵は、無限の計算能力を持つ盗聴者にとっても、完全でランダムな秘密鍵と区別がつかないものであることを意味します。決定的なのは、この証明が、現実世界のシステムは無限のストリームではなく、有限の数の粒子で動作するという事実を考慮に入れている点です。この有限サイズ効果は、通常、科学者に過度に保守的であることを強いて、安全性を確保するために、より多くの潜在的な鍵材料を破棄させる原因となります。しかし、この新しい証明は、どれだけの鍵材料を安全に保持できるかの精密な計算を提供し、これらの有限の制限によって課されるペナルティを軽減しました。

驚くべき展開として、研究者たちは同じコンピュータ・パイプラインを、単に自分たちの仕事を検証するためだけでなく、それを改善するためにも使用しました。システムが論理をチェックしている間に、それは、システムのセキュリティを推定するために使用される条件付きエントロピーの分散に関する、よりタイトな境界を特定する助けとなりました。既存の公式は緩すぎたため、秘密鍵の長さを不必要に短縮させていました。チームは、異なる数学的境界をテストし比較するコンピュータの能力に導かれ、より鋭い不等式を導き出しました。この新しい境界はよりタイトであり、セキュリティを犠牲にすることなく、古い公式が許容していたものよりも減少した有限サイズ・ペナルティで鍵を生成することを可能にします。この発見は推測ではなく、コンピュータによって真実であると検証された厳密な数学的結果であり、形式証明エンジンが単に仕事をチェックするだけでなく、古い問題に対するより良い解決策を見つけ出すことで、科学的発見を積極的に加速できることを示しました。

この研究はまた、将来の暗号システムがどのように検証されるべきかというテンプレートとしての役割も果たします。研究者たちは、基礎となる定義と定理のライブラリをオープンソースとして公開することで、コミュニティに再利用可能なツールキットを提供しました。このライブラリには、量子状態、チャネルの形式的な定義、およびプロトコルを記述するための特定の言語が含まれており、他の科学者がこの基盤の上に構築できるように設計されています。これは、将来の異なる量子プロトコル、あるいは量子情報科学の他の領域に対する証明が、同様の厳密さを持って構築できることを意味します。チームは、人間の洞察力と、マシンチェックされた論理の絶え間ない精密さを組み合わせることで、長年この分野を悩ませてきた隠れた不確実性を排除できることを示しました。その結果、量子鍵の信頼性は、単に研究者が主張するものではなく、機械によって検証された事実となる、セキュリティ論証の新しい標準が誕生しました。