2009 Fiscal Year Annual Research Report
形式手法に基づくセキュリティプロトコルの匿名性検証法に関する研究
| Project/Area Number |
19700018
|
|---|
| Research Institution | Aichi Institute of Technology |
|---|
Principal Investigator |
河辺 義信 Aichi Institute of Technology, 情報科学部, 准教授 (80396184)
|
|---|
| Keywords | 匿名性 / フォーマルメソッド / セキュリティ検証 / 定理証明 / 形式検証 / I / O-オートマトン |
|---|
| Research Abstract |
インターネット上の暗号プロトコル(セキュリティプロトコル)では,全てのデータを暗号化する場合であっても,通信パターンの特徴などから個人情報が漏れてしまう危険性がある.そのような個人情報漏えいを防ぐには,通信パターンの特徴の正しさまで考慮した匿名性の検証手法が必要である.しかし,これまで,大規模プロトコルに対する計算機を用いた匿名性検証技術については,十分検討されているとは言えなかった.
本年度は,まずLeeらの電子投票プロトコルを題材に,盗聴者よりも強い攻撃者が存在する状況を扱って,無証拠性の自動検証実験を行った.ここでは,Larch定理証明器を無証拠性の検証に適用するための具体的な手順が示された.
さらに,確率的振る舞いをするプロトコルの匿名性検証法を扱い,定理証明ソフトウェアを想定したシミュレーション検証技法が示された.ここでは,strong anonymityと呼ばれる匿名性のほか,probable innocenceと呼ばれる確率匿名性の検証手法まで示された.また,事例として,Crowdsシステムを対象に,確率的な条件のもとでの匿名性検証の適用例が示された.
|
