AIエージェントによる暗号プロトコルの自動検証の革新

一般社団法人Nyx Foundationが、暗号プロトコルのLean形式検証を自動化するためのAIエージェントを開発し、その成功を報告しました。この技術は暗号理論における重要な進展をもたらし、今後の安全性証明の手法に大きな影響を与えることが期待されています。

暗号プロトコルの形式検証とは

暗号プロトコルの形式検証は、暗号仕様の正確性や安全性を数学的に保証するための方法です。これまでのところ、従来の手法では専門家が手動で行ってきたため、時間とリソースが必要でした。特に、暗号プロトコルが複雑化するにつれて、人的エラーのリスクも増大しています。そのため、形式検証の自動化は、高度な技術的な必要性がある領域となっています。

AIエージェントによる革新

この度、Nyx Foundationが開発したAIエージェントは、Lean言語を用いて暗号プロトコルの安全性を自動的に証明することを可能にしました。このエージェントは、独自のワークフローを構築し、それによってほとんどの工程を自動化します。具体的には、暗号に特化したチェックリストに基づく査読の役割を持つシステムを介し、採用された草案をLean形式に自動変換し、型検査と証明検証を行います。これにより、知られている限り、暗号プロトコル領域におけるAIエージェントの系統的適用が初めて実現されたと言えます。

具体的な成果

特に、耐量子暗号のXMSSと呼ばれるハッシュベースの署名スキームに関連する形式的安全性を証明することに成功しました。この実装は、公開リポジトリhttps://github.com/NyxFoundation/tsl-formal-verificationにて共有されています。

今後の展望

この技術は、2025年11月に開催される国際学会、24th International Conference on Cryptology and Network Security (CANS2025)でのポスター発表が決定しています。このイベントがさらなる発展の契機となることが期待されます。また、NYx Foundationはこのエージェントをオープンソース化し、さらなる精度向上に向けた取り組みを進めていく方針です。

Nyx Foundationについて

Nyx Foundationは東京都文京区に位置する、イーサリアム・ブロックチェーン専門の研究機関です。サポート資金は寄付や研究助成金から成り、イーサリアムの解決すべき課題に取り組んでいます。また、業界関係者と連携し、大学などで研究成果を発表するなど、活発な活動を行っています。

私たちはリーダーシップを発揮しながら、この新しいAIエージェント技術を活用して形式検証の自動化をさらに推進していく所存です。興味のある方は、ぜひNyx Foundationのウェブサイトを訪れてみてください。