世界初！セキュリティプロトコル形式解析器の並列化に成功 －解析時間を大幅に短縮し、より安全なインターネットに貢献－
世界初！セキュリティプロトコル形式解析器の並列化に成功
－解析時間を大幅に短縮し、より安全なインターネットに貢献－
【ポイント】
- 逆向き探索技術「バックワードナローウイング」の並列化に成功
- 膨大な解析時間を要する従来手法に対し、並列化による高速化と効率化を実現
- 多数のセキュリティプロトコルで実証済み
| 北陸先端科学技術大学院大学 コンピューティング科学研究領域の緒方 和博教授とDO, Minh Canh（ド ミン カン）助教らは、インターネットの安全を支える重要な技術であるTLS 注１）などのセキュリティプロトコルの形式解析器を世界で初めて並列化し、高速化に成功しました。セキュリティホールの有無を科学的に検証するためのセキュリティプロトコルの形式解析には、攻撃者の存在や行動パターンを考慮した詳細な解析が必要であり膨大な計算時間が必要でしたが、今回の並列化により解析速度が大幅に向上しました。また、多数のセキュリティプロトコルを用いた実験でその効果を実証しています。本研究はスペインのバレンシア工科大学Santiego Escobar教授及びマドリードコンプルテンセ大学Adrian Riesco准教授との国際共同研究の成果であり、ディペンダブル・セキュアコンピューティング分野トップ学術雑誌IEEE Transactions on Dependable and Secure Computingに2025年7月16日付で掲載されました。 |
【研究概要】
セキュリティプロトコルの設計ミスや脆弱性を事前に科学的に検証し、インターネット通信の安全性を確保することは極めて重要です。今回、並列化した形式解析器は「Maude-NPA」と呼ばれ、主開発者は国際共同研究者のSantiago Escobar教授です。このMaude-NPAに加え、「ProVerif」「Tamarin」「Scyther」などいくつもの形式解析器が開発されていますが、これまでセキュリティプロトコルの形式解析器の並列化に成功した例はありませんでした。
Maude-NPAは、攻撃を受けた状態から解析を開始し、プロトコルの動作を逆方向に探索する「バックワードナローウイング 注２）」という技術を用いています。攻撃を受けた状態から、初期状態に到達できれば、その攻撃手順を示すことができます。逆に、初期状態に到達できなければその攻撃を受けた状態に至る経路は存在しないため、その攻撃は現実には成立しないことが理論的に証明できます。ただし、本技術は解析対象の状態が急激に増加する（状態爆発）という課題を抱えています。そこで、バックワードナローウイングを行うたびに既に訪れた状態を再度調べないようにする「最適化処理」を加え、無駄な探索を省く工夫がされています。本研究では、この「バックワードナローウイング」と最適化処理の両方を並列化しました。具体的には、解析対象の状態空間を複数に分割し、それぞれを同時に探索する方法を採用しました（図1参照）。また、最適化の並列化では、状態間の依存関係を考慮しながら、木構造を逆向きに辿る手順を用いて効率的に実現しています（図2参照）。この並列版Maude-NPA（Parallel Maude-NPA）は、TLSなどの従来のセキュリティプロトコルだけではなく、量子コンピュータが実用化されたとしてもインターネットを安心安全に持続的に利用することを可能にする耐量子計算機暗号版TLSの形式解析も可能であることを事例研究で示しています。
図1：バックワードナローウイングの並列化
図2：最適化の並列化
本研究は、国立研究開発法人科学技術振興機構（JST）戦略的国際共同プログラム（SICORP）（JPMJSC20C2）による財政的支援を受けて実施されました。
【論文情報】
| 掲載誌 | IEEE Transactions on Dependable and Secure Computing |
| 論文タイトル | Parallel Maude-NPA for Cryptographic Protocol Analysis |
| 著者 | Canh Minh Do, Adrian Riesco, Santiago Escobar, Kazuhiro Ogata |
| 掲載日 | 2025年7月16日 |
| DOI | 10.1109/TDSC.2025.3589584 |
【用語説明】
Transport Layer Securityの略記です。ネットショッピングなどでクレジットカード番号等の個人情報が第三者に漏洩すること等を防ぐために使われる、インターネットを安心安全にするために不可欠な技術のひとつです。
ナローウイングとは、状態を表す式に変数（まだ具体的な値が決まっていない部分）を用いることで、無限も近い状態をまとめて表現できる技術です。プロトコルの動作を記述した規則を、変数を含む状態式に適用する際には、論理プログラミング言語Prologで採用されている単一化（ユニフィケーション）という手法を使います。単一化を用いて規則を状態式に適用し、状態の移り変わりを導くことを「ナローウイング」と呼びます。バックワードナローウイングは、このナローウイングを逆方向に適用する方法であり、攻撃を受けた状態から初期状態へと探索を行う技術です。この逆向きの探索により、攻撃経路の有無を効率的に検証できます。
令和7年8月1日
