| 研究概要 |
本研究では,暗号を用いたプロトコルにおけるデータの偽造不可能性の問題を形式的に記述し,偽造不可能性の判定が可能となるプロトコルのクラスを抽出し,そのクラスについて偽造不可能性を形式的に検証するシステムの開発を目的としている.
1.偽造不可能性判定問題の形式的記述について検討を行った.システムで提供されている操作,すなわち,敵対者の行い得る操作,敵対者が盗聴で知り得る情報はそれぞれ関数,項で表し,関数間の関係は公理として記述することとした.これらは従来の秘密漏洩判定問題と同一である.偽造対象は項で表し,偽造とはならない正規の操作を項で表現することとした.
2.偽造不可能性判定問題が決定可能となり,かつ,多項式時間で決定可能となるための十分条件を抽出した.
3.秘密漏洩判定問題での知見を用いて,実際のプロトコルに対して,効率よく働く判定アルゴリズムを考案した.最終的にはオートマトンの受理言語の空問題に帰着されるが,実際のプロトコルではオートマトンの一つの状態から出る枝数がそれほど多くはならないので,その特性を利用して,アルゴリズムの効率化を行った.実用的なプロトコルに対して効率よく判定が行えるような工夫について詳細に検討し,安全性を判定するシステムの試作を行った.
4.偽造不可能性判定問題の考え方は,暗号を用いたプロトコルだけでなく,データベースのセキュリティにも利用できる.データベース不正なデータ読み出しについても,その安全生判定問題を定式化し,アルゴリズムを開発した.
|
