セキュリティプロトコルの簡易検証 I ～具体的意味論～

モデル検査の応用として、セキュリティプロトコルの検証が盛んに行われている。しかし、代表的なモデル検査機の反例出力は、与えられたプロトコルを機械的に展開して得られた状態遷移図と時相論理式から生成された状態遷移図との積に対する非空テストから得られる機械的な表現である。この方法は、yes/noの結果が求められる、プロトコルの最終判定段階で用いる場合に有効であるが、試行錯誤を繰り返す段階にある、プロトコルデザイナーにはおよそ直感的な情報を与えない。筆者はあるクラスのセキュリティプロトコルに対して直感的な意味を与えるとともに、効率的なモデル検査を行うための方法を示した。

千葉商大論叢

第44巻第4号 (27)