2008 Fiscal Year Annual Research Report
形式手法に基づくセキュリティプロトコルの匿名性検証法に関する研究
| Project/Area Number |
19700018
|
|---|
| Research Institution | Aichi Institute of Technology |
|---|
Principal Investigator |
河辺 義信 Aichi Institute of Technology, 経営情報学部, 准教授 (80396184)
|
|---|
| Keywords | 匿名性 / フォーマルメソッド / セキュリティ検証 / 定理証明 / 形式検証 / I / 0-オートマトン |
|---|
| Research Abstract |
インターネット上の暗号プロトコル(セキュリティプロトコル)では, 全てのデータを暗号化する場合であっても, 通信パターンの特徴などから個人情報が漏れてしまう危険性がある. そのような個人情報漏えいを防ぐには, 通信パターンの特徴の正しさまで考慮した匿名性の検証手法が必要である. しかし, これまで, 大規模プロトコルに対する計算機を用いた匿名性検証技術については, 十分検討されているとは言えなかった.
本研究では, 実環境(インターネットなど)に適したプロトコルの匿名性を保証するための, 従来の匿名性(トレース匿名性)の拡張について検討した. とくに, 前年度の結果である「盗聴以外の攻撃に関する匿名性」の結果をもとに, 電子投票の重要な性質であるreceipt-freeness性を形式化した. また, 確率的振舞いをするプロトコルの匿名性検証に関連して, そのベースとなる匿名性検証法(バックワード型匿名性検証法)を道入した.
今後は, 他の電子投票の重要な性質(coercion-resistanceなど)と研究の結果の関係を明らかにしたい. また, 検証ツールによる実際のシステムの検証実験等を通じて, 本研究の手法の適用可能性を明らかにする予定である.
|
