2009 Fiscal Year Annual Research Report
セキュリティプロトコルの形式的検証の計算論的健全性に関する研究
Project/Area Number |
09J07885
|
Research Institution | The University of Tokyo |
Principal Investigator |
川本 裕輔 The University of Tokyo, 大学院・情報理工学系研究科, 特別研究員(DC2)
|
Keywords | 暗号プロトコル / 形式的手法 / 計算論的健全性 |
Research Abstract |
暗号プロトコルの検証には、形式的手法と計算論的手法がある。形式的手法では、メッセージが記号表現に抽象化され、攻撃者は記号表現に対する限られた操作しか実行できないため、プロトコル検証は単純で自動化しやすいが、暗号を解読するような攻撃は考慮されない。一方、計算論的手法では、計算量理論に基づいて暗号プリミティブの脆弱性を考慮するため、プロトコル検証は、いかなる攻撃も見逃さないが、複雑で間違いやすい。近年、形式的手法の計算論的健全性、すなわち「プロトコルで用いられる暗号プリミティブが一定の計算量的安全性を満たすならば、形式的手法によるプロトコル検証がいかなる攻撃も見逃さない」という性質の研究が盛んである。本研究では、計算論的健全性の新たな証明技法を考案することにより、先行研究よりも多くの暗号プリミティブに対して計算論的健全性の結果を得られるようになった。具体的には、先行研究では、計算論的健全性を証明するために、「ビット列を受け取って項を返すパーズ関数」を用いていたため、ハッシュ関数や排他的論理和などの暗号プリミティブに関しては計算論的健全性を証明することができなかった。そこで、本研究では、パーズ関数を用いずに計算木の書き換えを行う新たな証明技法を考案した。これにより、ハッシュ関数が原像計算困難性と衝突困難性のみを満たす場合であっても、様々な長さのメッセージのハッシュ値を扱えるようになった。また、メッセージの電子署名がそのメッセージを伴わずに送られるような場合も扱えるようになった。この新たな証明技法は排他的論理和に関しても計算論的健全性を得るのに有用と考えられる。
|
Research Products
(4 results)