鍵交換プロトコルに対する受動的攻撃安全の検証ポイント

摘要

認証·鍵交換プロトコルはセキュリティ要件に従って，自動的かつ高速に検証されることが望ましい．著者らはBellareらのモデルにもとづく認証·鍵交換プロトコルに対する安全性検証手法を提案し，これらのプロトコルの安全性を自動的かつ高速に検証可能であるように，各安全性の検証ポイントを示した．検証ポイントとは，これらのプロトコルがある安全性の少なくとも1つの検証ポイントを満足するならば，その安全性を満足すると判定されるというものである．本稿では，各安全性の検証ポイントに対する導出プロセスに主眼を置き，特に鍵交換プロトコルに対する受動的攻撃安全の検証ポイントに関し，導出プロセスの詳細を述べる．具体的には，鍵交換プロトコルをモデル化し，Bellareらのモデルにもとづいて受動的攻撃の攻撃者もモデル化した上で，受動的攻撃に対する鍵交換プロトコルの安全性の証明手順を示す．更に，セッション鍵の4種類の形状に対して場合分けを行い，検証ポイントを導出する．