| Research Abstract |
1,安全性自動検証手法の1つT-PTOAにおける事例研究の拡張を行った.まず,新たに鍵交換プロトコルと電子署名プロトコルに対してT-PIOAを適用し,解析が可能であることを示した.また,適応的攻撃者モデル,能動的攻撃者モデルなどの複雑な攻撃モデルに対する解析法を提案し,実際にT-PTOAに適用可能であることを示した.これらの拡張により,T-PIOAの解析能力を評価し,UCSAやAPSGと比較することが可能となった.以下,比較を行った結果を示す.
(1),UCSAとT-PIOAはどちらも鍵交換プロトコルの解析能力を持っているが,T-PIOAの方がより高度な攻撃モデルで証明可能.
(2),APSGとT-PIOAはどちらも電子署名プロトコルの解析能力を持ち,かつ,もっとも高いレベルの安全性を証明可能.
このように,3つのアプローチの適用領域の解明に繋がる成果が得られたと言える.
2,低資源向き認証プロトコルの1つGPS方式の厳密な解析と拡張方式の提案をそれぞれ行い,以下のような成果を得た.
(1),GPS方式の各種パラメータの厳密な解析により,実用的な安全性を確保するには,メモリ領域を大きく取る必要があることを証明.
(2),認証成功確率を実用的に影響無い程度犠牲にすることにより,GPS方式よりも必要なメモリ領域が少なくて済む改良方式GPS^+を提案.
このように,従来の低資源向け認証プロトコルの(非)実用性を明らかにし,また,実用的には問題無いレベルの安全性を持った効率的なプロトコルが得られた.
|
