2009 Fiscal Year Annual Research Report
論理推論を基にした暗号プロトコルの計算論的安全性検証法の構築
| Project/Area Number |
21700023
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
長谷部 浩二 University of Tsukuba, 大学院・システム情報工学研究科, 研究員 (80470045)
|
|---|
| Keywords | 暗号プロトコル / 数理的技法 / 論理推論 / 計算論的安全性証明 / 安全性検証 |
|---|
| Research Abstract |
本年度は,研究代表者によって提案された論理推論体系であるBasic Protocol Logicに対し,暗号プロトコルの安全性に関する種々の性質を扱うための拡張を行い,かつその拡張体系の公理が妥当となるような(すなわち推論体系に対して健全である)計算論的モデルを与えた.特に安全性に関する性質として,本年度は特にプロトコルのメッセージに含まれるデータの秘匿性(secrecy)を対象とした.以上の研究によって得られた本年度の具体的な成果は以下の通りである.
まず論理推論体系の言語として,プロトコルのメッセージの記号論的表現と計算論的表現の両方を,1階述語論理の項として統一的に与える言語を考案した.またこの言語を基に,秘匿性に関連するいくつかの概念を定式化した.さらに,この言語に対する公理系を与え,その中で秘匿性の証明が行えることを,Needham-Schroederプロトコルなどの具体的な暗号プロトコルを例に示すことができた.また,この秘匿性の証明を補題として利用することにより,合意性(agreement property)を示す方法も考案した.また一方で,以上のことが行いうる公理系に対し,健全な計算論的モデルを与えた.以上の結果は,特に秘匿性を基に合意性を証明しなければならない暗号プロトコルの証明に対しても有効であるという利点を持つ.また,この推論体系が,公開鍵暗号と対称鍵暗号のいずれを基にしたプロトコルに対しても適用可能であることが,先行研究に対する利点であると言える.
一方,本年度に得られた推論体系は,上記のような証明が行える一方で,言語の表現力の高さから証明が複雑になるという欠点を持っている.今後は,この欠点を改善するために,安全性証明を行う上で有用でかつ汎用性の高い補題を見出すことを課題としている.
|
