認証プロトコルの完全性を自動検証するシステム

齋藤 孝道  Wu WEN  溝口 文雄  

誌名
電子情報通信学会論文誌 A   Vol.J85-A   No.2   pp.207-213
発行日: 2002/02/01
Online ISSN: 
DOI: 
Print ISSN: 0913-5707
論文種別: 論文
専門分野: 情報セキュリティ基礎
キーワード: 
情報セキュリティ,  認証プロトコル,  検証,  

本文: PDF(259.3KB)>>
論文を購入




あらまし: 
コンピュータネットワークにおいて認証プロトコルは重要な役割を担っており,その安全性が強く求められている.認証プロトコルが安全であるためにはまずそれが正しく動作すること,すなわち,プロトコルが完全であることが必要である.プロトコルの完全性をその仕様に基づいて手作業で確認することは一般に必ずしも容易ではない.そこで我々は認証プロトコルの完全性を自動的に検証できるシステムを構築した.検証は次の手順でなされる.与えられた認証プロトコルの仕様とそれに対する仮定をBAN論理の命題として記述し,これらをCafeOBJ言語で記述された推論システムに入力する.すると自動的に推論され,そのプロトコルが完全であるか否かが判定される.よく知られたいくつかの認証プロトコルの完全性を提案したシステムで正しく検証することができた.その中の二つのプロトコル,すなわち,Needham-Schroederの共有鍵及び公開鍵プロトコルの検証を例として示す.