2010 Fiscal Year Annual Research Report
暗号プロトコルに対する計算論的に健全な安全性検証技術と再設計支援技術の開発
| Project/Area Number |
21700015
|
|---|
| Research Institution | Osaka University |
|---|
Principal Investigator |
吉田 真紀 大阪大学, 大学院・情報科学研究科, 助教 (50335387)
|
|---|
| Keywords | 暗号プロトコル / 安全性 / 形式的検証 / UC安全性 / GUC安全性 / EUC安全性 / Generic model |
|---|
| Research Abstract |
本研究では,暗号プロトコルにとって望ましい強さの計算量的安全性を保証するUC安全性を形式的に検証するための基盤技術と,検証システムの開発を目的とする.本年度は具体的には以下の研究を行った.
1.記号論的モデルと計算論的に健全な検証法の拡張
UC安全性のモデルのうち,昨年度定式化したGUCモデルの等価な簡易版であるEUCモデルを対象とし,記号論的モデルを定義した.EUCモデルは,GUCモデルと同様にPKI環境下の強固な安全性を保証しつつ、各種概念が簡明となっている.それらの概念を記号論的に対応する形で定義した.さらに,インターネットにおいて必須となる鍵交換プロトコルと認証プロトコルの安全性判定問題が決定可能となるための十分条件を導出し,その十分条件下で計算論的に健全な検証法を設計した.
2.再設計支援に有用となる攻撃の検討と攻撃導出法の設計
暗号プロトコルの計算量的安全性の根拠として,様々な数学問題の困難性が仮定されている,安全性を保証するためには,基となる数学的構造を理想化したGeneric model(GM)において困難性仮定に対する攻撃の有無を判定する必要がある.そこで,GMにおける攻撃の有無判定・導出法を設計した.
3.検証技術の主要部分の試作
攻撃有無判定・導出法を数式処理システムMapleにより実装した,さらに,暗号分野における代表的な論文アーカイブであるCryptology ePrint Archive へ最近1年間に投稿された論文(713本)で言及された困難性仮定に適用し,攻撃の有無を確認した.これにより,査読による検証が行われていない ePrint上の困難性仮定の信頼性向上に寄与した.
|
Research Products
(5 results)
