パオロ・モデスティー (Paolo Modesti) 氏は2026年11月5日(現地時間)、グローバル監視システムにおけるネットワークトラフィックの分析精度向上を目指し、キャプチャされたデータからパッシブなドレフ-ヤオ侵入者 (Dolev-Yao intruder) の実行を再構築する自動化された手法に関する研究論文をarXivで発表した。本手法は、プロトコルレベルのセマンティクス理解の深化を目的としており、再構築された実行を形式的なプロトコル仕様と照合して検証する機能を持つ。
本研究論文は、従来のパケットキャプチャのみではプロトコルレベルのセマンティクスが十分に明らかにならないという課題に対処している。提案されたフレームワークは、PCAPキャプチャ、AnBx仕様、および関連するデプロイメントメタデータを取り込み、TCPストリームからJavaシリアライズされたオブジェクトを抽出する。その後、プロトコルセッションとチャネル-ステップ割り当てを再構築し、AnBxコンパイラによって生成されるDolev-Yao導出チェックを評価するパッシブ侵入者を生成する。
再構築における三つの主要な課題が解決された。一つ目はTCPストリーム内の複数のシリアライズされたオブジェクトおよびオブジェクト参照の処理、二つ目はインターリーブされた接続を並行プロトコルセッションにマッピングする際の曖昧さの解消、三つ目は候補再構築のセマンティック検証である。この手法はAnBxテストスイートの121のプロトコルで評価された。
シングルセッションキャプチャにおいては、標準的なJDK cryptographic providerが期待されるオブジェクトの97.8%を回復し、94.2%の再構築に成功した。成功の基準は、完全なオブジェクト回復とクリーンなパッシブ侵入者実行である。また、112の並行処理可能なプロトコルにおいては、二つおよび三つの並行セッションで89.3%の再構築成功率を達成し、約97.2%の期待されるオブジェクトを回復した。プロトコル-ロールマッピングの不一致や意図的に改変されたトレースを用いた実験では、生成されたDolev-Yaoチェックがセマンティックな不整合に対応することが示された。このソリューションは、再構築ステップを明示化することで、プロトコルの回復力評価や防御的対策の設計に活用可能なプロトコルレベルの観測結果を提供する。
参考: arXiv cs.CR (アーカイブ) — 2026年11月6日 14:00 (JST)
原文ハイライト"an automated, specification-guided methodology for reconstructing passive Dolev-Yao intruder executions"