【世界初*】AIエージェントで暗号プロトコルのLean形式検証を自動化

イーサリアムの研究組織であるNyx Foundationは、AIエージェントで暗号プロトコルのLean形式検証を自動化し、一部耐量子暗号の安全性証明に成功しました。

一般社団法人 Nyx Foundation (所在地: 東京都文京区) は、暗号プロトコルのLean形式検証をAIエージェントで自動化することに成功したことをお知らせいたします。

このAIエージェントは独自のワークフローを活用してLean言語を生成することで、暗号プロトコルの仕様正当性や安全性の形式的証明自動化を実現します。

暗号プロトコルの形式検証がなぜ重要なのか？

暗号プロトコルの形式検証とは、仕様の正当性や暗号の安全性を数学的に証明する枠組みです。Leanという定理証明支援系であるプログラミング言語を用いて、形式検証することが可能です。

従来の暗号理論における暗号プロトコルの安全性は、数学的な証明を人の手で行うことによって保証されます。しかし、暗号プロトコルの高機能化や安全性要件の複雑化に伴い、安全性証明の誤りがしばしば起きるという問題があります。実際に、安全性が証明されたはずのプロトコルに何年も後になってから不備が指摘されるという事例も起きています。

また安全性証明そのものも複雑化し、専門家であっても証明を記述・理解するのが困難になってきているという背景もあります。形式手法を取り入れることによって、より厳密に証明を記述・検証することが可能になります。

Lean形式検証AIエージェントによる自動化に成功

この度、本エージェントを用いて耐量子暗号の一部形式的安全性証明に成功しました。具体的には、XMSSと呼ばれるハッシュベース署名スキームの一部エンコーディングスキームの命題を、Lean言語にて形式的に証明しました。

こちらのリポジトリで実装も公開しています。

https://github.com/NyxFoundation/tsl-formal-verification

一般的に形式検証を行うことは非常に高度な人材と多大な時間を要します。我々は既存のAIモデルを活用し、独自のワークフローを実装することで大部分の工程を自動化しました。

本研究では、暗号プロトコルのLean形式検証をAIエージェントで自動化するパイプラインを提案します。

1. 自然言語による非形式証明の生成

2. 暗号特化のチェックリストに基づく査読者ロールによる採否判定

3. 採択された草案のみをLeanに自動形式化して型検査・証明検証

このような二段ゲート設計を採用しています。評価では、2〜3種の代表的命題に対し、Lean検証成功率などの効率・品質指標を測定します。

マルチラウンドによる段階的形式証明のワークフローの概要図

AIエージェントで数学のLean形式的証明を自動化する論文は多く発表されていますが、暗号学に適用した例は非常に少ないです。公開文献の範囲で、暗号プロトコル領域へのLean×AIエージェントの系統的適用報告は未確認です。

今後の展望

2025年11月、国際学会 24th International Conference on Cryptology and Network Security (CANS2025) にPostersとして採択されました。ご興味ある方はぜひお越しください。

本エージェントはオープンソース化を予定しております。今後も更なる精度向上を目指して開発を進め、段階的に情報を発信してまいります。

Nyx Foundationは、高度な暗号学・形式検証の知見とソフトウェア開発エンジニアリングの経験を活かし、AIエージェントを活用した形式検証の自動化を推進してまいります。

* 公開文献の範囲で、暗号プロトコル領域へのLean形式検証×AIエージェントの系統的適用報告は未確認です。

Nyx Foundationについて

一般社団法人 Nyx Foundation（所在地：東京都文京区）は、イーサリアム・ブロックチェーンに特化した私設の研究機関です。

すべての活動資金は寄付・研究助成金・スポンサーシップによって支えられています。そのような資金を原資にイーサリアムの重要課題を解決するための活動を継続してきました。

既にイーサリアム財団やブロックチェーン企業・大学との連携を進め、コロンビア・ビジネススクール等で成果を発表しています。

■ 関連サイト・連絡先

ホームページ: https://nyx.foundation

寄付ページ: https://nyx.foundation/donate

メールアドレス: [e-mail]