2011 Fiscal Year Annual Research Report
論理推論を基にした暗号プロトコルの計算論的安全性検証法の構築
| Project/Area Number |
21700023
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
長谷部 浩二 筑波大学, システム情報系, 助教 (80470045)
|
|---|
| Keywords | 形式手法 / 暗号プロトコル / 安全性検証 / 論理推論 / 計算論的安全性 |
|---|
| Research Abstract |
昨年度までに,暗号プロトコルの計算論的安全性に関する論理推論体系と,その拡張体系の公理が妥当となるような(すなわちその論理体系に対して健全であるような)計算論的モデルが得られていたが,国際会議論文で不採録となっていた.今年度は,この論理体系の簡略化を目指して研究を行った。そのための方針として,昨年度までに得られた論理体系において使われていた原子述語の改良と,それによる公理と計算論的モデルの構築を進めた.また一方で,改良された体系を定理証明支援ツールのひとつであるIsabelleを用いた証明の半自動化を試みた.以上の成果は,主にGergely Bana氏らの協力の下で進められ,再度国際会議への論文投稿を行ったものの,不採録となった.その理由としては,改良された論理体系は,計算論的安全性証明の手法としては意義のあるものであるが,実際の安全性証明への適用のためには,さらに簡略化が必要であるというものであった.今年度の後半では,簡略化のために,これまで採用してきた一階述語論理を基にするアプローチの他に,新たに動的論理(Dynamic Logic)などの枠組みを用いた公理化なども試みてみたが,十分な簡略化された体系を得ることができなかった.そのため,一階述語論理の枠組みを維持しながら,安全性証明の対象として,プロトコルの認証に関する性質のみに焦点を絞り,プロトコルで扱われる情報の秘匿性については,論理体系の仮定として扱うという方針で研究を進めており,その成果を論文としてまとめる作業を行った.
|
