あなたは、自分の新しい金庫が絶対に破られないことを証明しようとしている熟練の鍵師だと想像してください。あなたは単に「これは強い！」と言うだけではありません。あなたは一連の手順を示す必要があります。「もしこの小さな鍵を壊せないなら、ドアも壊せない。ドアを壊せないなら、金庫も壊せない」というように。これが現代の暗号学の仕組みです。専門家は、セキュリティをテストするために「ゲーム」を用います。そこでは、ハッカーが秘密を推測しようとし、システムの安全性は、それを破ることが既知の「不可能なパズル」を解くことと同じくらい難しいことを示すことで証明されます。しかし、ここに落とし穴があります。これらの証明を手作業で行うことは、ハリケーンの中でトランプの家をバランスさせるようなものです。些細なミスをしたり、微妙な隙間を見逃したり、複雑さに迷い込んだりするのは容易なことです。そして、もし一歩でも踏み外せば、証明全体が崩壊してしまいます。だからこそ、科学者たちは、コンピュータにすべてのカードをチェックさせ、その家がしっかりと立っていることを保証する方法を探してきました。

ここで、この論文が登場します。著者たちは、強力なコンピュータプログラムである Lean 4 の中に、HOPSCOTCH（ホッピング・ゲームの「ホップ・スコッチ」にちなんだ遊び心のある名前）と呼ばれるデジタル作業場を構築しました。HOPSCOTCHを、単に数学をチェックするだけでなく、セキュリティ証明の「物語」をも理解する超スマートでロボットのような校閲者だと考えてください。HOPSCOTCHは、暗号学者が独自の、制限された言語で書くことを強いるのではなく、彼らが他のあらゆる数学で使用しているツールを使って証明を書けるようにします。それは、「ゲーム・ホッピング」のプロセス（一つのセキュリティ・シナリオから次のシナリオへと飛び移ること）を、コンピュータが検査、検証、さらには自動化の支援さえできる、明確でステップバイステップのオブジェクトへと変えるのです。著者たちは単にツールを作っただけではありません。彼らは、複雑な構成であるGGMを含むいくつかの有名な暗号化手法の安全性を証明することに成功し、この「ロボット校閲者」が混乱することなく、現実世界の暗号学的課題を処理できることを示しました。

大きな構図：なぜ校閲ロボットが必要なのか

デジタルセキュリティの世界では、私たちは「証明可能なセキュリティ」に依存しています。これは、コードが安全であることを単に願うのではなく、それを証明しようとすることを意味します。これを行う標準的な方法は、「ゲームベース」のアプローチです。セキュリティガード（システム）と泥棒（攻撃者）を想像してください。ガードには秘密があり、泥棒はその秘密を当てることを試みます。ガードが安全であることを証明するために、私たちは単に「彼は優秀だ」と言うだけではありません。私たちは一連の「ゲーム」またはシナリオを作成します。

1. 実際のゲーム： 泥棒は実際のシステムを破ろうとします。
2. ホップ： 実際とほぼ同じだが、分析がより容易な、少し異なるゲームを想定します。もし泥棒が「実際のゲーム」で勝てるなら、この新しい、わずかに異なるゲームでも勝てることを証明します。
3. 連鎖： 一つのゲームから別のゲームへと、ルールを毎回ほんの少しずつ変えながら、ホップし続けます。最終的には、明らかに勝つことが不可能なゲーム（例えば、コイン投げを100万回連続で正しく当てるなど）に到達します。

もし、すべての「ホップ」が安全であることを証明できれば、連鎖全体が安全であると言えます。これは「ゲーム・ホッピング証明」と呼ばれます。

問題は、人間がこれを完璧に行うのが非常に苦手であることです。これらの証明は長く、乱雑で、細部に満ちています。たった一つの見落とした詳細が、証明全体を誤らせ、システムを脆弱にする可能性があります。長年、研究者たちはこれらの証明をチェックするための特別なコンピュータツールを構築しようとしてきましたが、これらのツールはしばしば数学者とは異なる言語を話します。それらは、数学ではなく「セキュリティ」の言葉しか話さない翻訳者のようで、専門家にアイデアを何度も翻訳し直すことを強いるため、遅く、エラーが発生しやすくなります。

HOPSCOTCHの登場：ユニバーサル・トランスレーター

この論文の著者であるStefan Dziembowski、Grzegor Fabiański、Daniele Micciancio、およびRafał Stefańskiは、架け橋を作ることにしました。彼らは、数学的証明の検証に使用される一般的なプログラムである Lean 4 の中のフレームワーク、HOPSCOTCH を作成しました。

HOPSCOTCHの魔法はここにあります：

• 新しい言語を必要としない： 他のツールのように、制限された新しい書き方を学ぶことを強いるのではなく、HOPSCOTCHは標準的なLeanを使用して証明を書くことを可能にします。それは、シェフに自分のお気に入りのナイフを使う代わりに、プラスチック製のナイフを使うよう強いるようなものです。
• オブジェクトとしての証明： HOPSCOTCHにおいて、証明は単なるテキストの塊ではありません。それはレゴモデルのような、構造化されたオブジェクトです。ゲームにおける各「ホップ」は、特定のレゴブロックです。それらを組み合わせることができ、コンピュータはそれらが完璧に適合するかどうかをチェックします。もし一致しない二つのブロックを繋ごうとすれば、コンピュータは「ダメです、それは機能しません」と告げます。
• 「抽象化」のトリック： これらの証明で最も難しい部分の一つは、二つの異なる見た目のシステムが、全く同じように振る舞うことを示すことです。HOPSCOTCHは「状態抽象化」と呼ばれる巧妙なトリックを使用します。二つのロボットを想像してください。一つは内部配線図が乱雑で、もう一つは整然としています。HOPSCOTCHは、乱雑な配線が整然としたものとどのように対応しているかを示す「マップ（抽象化関数）」を描くことを可能にします。もしそのマップが正しければ、たとえ内部の見た目が異なっていても、コンピュータはそのロボットたちが挙動において同一であることを理解します。

彼らが実際に行ったことと発見したこと

著者たちは単にツールを構築しただけではありません。彼らはそれをテストしました。彼らは、4つの主要な暗号学的概念の安全性を形式的に検証するためにHOPSCOTCHを使用しました。

1. Encrypt-then-MAC： メッセージを秘密かつ改ざん不能にする手法です。基礎となる暗号化と「タグ付け（MAC）」が安全であれば、全体がスマートなハッカーに対しても安全であることを証明しました。
2. ElGamal暗号： 公開鍵を使用して秘密のメッセージを送信する有名な方法です。決定性ディフィー・ヘルマン（DDH）仮定と呼ばれる困難な数学的問題に基づいた、その安全性の証明方法を示しました。
3. One-Time Secrecy から IND-CPAへ： システムが単一のメッセージに対して安全であれば、それが多くのメッセージに対して安全にできることを証明しました。これは、堅牢な暗号を構築するための極めて重要なステップです。
4. GGM構成： これは最大級の成果です。GGM法は、単純な乱数生成器を、複雑な「擬似乱数関数」（本物の乱数生成器のように見える偽の乱数生成器）へと変えます。以前のコンピュータによる証明は、非常に浅いバージョン（例えば3ステップのツリー）しか扱うことができませんでした。著者たちは、GGMの非定数深さ（non-constant depth）、つまり任意のサイズのツリーに対して機能する安全性を証明するためにHOPSCOTCHを使用しました。彼らの知る限り、これは汎用的なコンピュータ証明支援システムが、この特定の複雑な構成を正常に検証した初めての事例です。

その仕組み（「ゲーム」のメカニクス）

論文では、HOPSCOTCHが証明を特定のステップ、すなわち「コンストラクタ」に分解することで機能すると説明しています。

• 観測的等価性（Observational Equivalence）： 二つのゲームが外部からは同じように見えることを証明すること。
• リダクション（Reductions）： ゲームAを破れるなら、ゲームBも破れることを示すこと。
• ハイブリッド・シーケンス（Hybrid Sequences）： 多くの小さなステップを連鎖させること。

フレームワークには、これらのステップを解決するために自動化されたヘルパーである「タクティクス」が含まれています。例えば、二つのオーラクル（ゲームシステム）が同一であることを証明する必要がある場合、コンピュータは自動的に「状態抽象化」マップを見つけようとします。もし見つけられなければ、そのステップを人間が解決できるように残しておきますが、構造自体は維持されるため、人間は自分がどこにいるのかを正確に把握できます。

著者たちはまた、「計算論的健全性定理（computational soundness theorem）」も証明しました。これは、もっと専門的な言い方をすれば、「コンピュータがこの証明を有効であると言えば、それは現実世界においても実際に有効である」ということです。彼らは、HOPSCOTHが作成するすべての証明オブジェクトに対して、証明で使用されている仮定に基づいて、ハッカーが得られる「アドバンテージ」を数学的に正確に計算できることを示しました。これにより、コンピュータが単に自分自身の中でゲームをしているのではなく、現実的で具体的なセキュリティ保証を与えていることが保証されます。

結論

この論文は、HOPSCOTCHが、特化したセキュリティツールによる利便性と、汎用的な数学支援プログラムの強力な力の間の溝をうまく埋めることに成功したと結論付けています。これにより、暗号学者は、より読みやすく、チェックしやすく、人間のミスが起こりにくい証明を書くことができます。著者たちは、コンピュータがまだ「ハッカー」が十分に高速に動作しているかどうか（これは多項式時間と呼ばれる技術的な詳細です）まではチェックできていないことを認めていますが、完全に自動化された信頼できるセキュリティ証明への基礎を築きました。

彼らはまた、将来についても示唆しています。これらの構造化された証明オブジェクトがあれば、AIを使用してこれらの証明を自動的に書くのを支援したり、あるいは「悪いイベント」や確率を含むさらに複雑なシナリオを扱うようにシステムを拡張したりすることが、間もなく可能になるかもしれません。しかし、現時点での主な成果は明白です。彼らは、私たちのデジタルの秘密が安全であることを証明するために、コンピュータが私たちを助けてくれる、信頼性が高く、柔軟で強力な方法を構築したのです。