暗号を用いたプロトコルにおけるデータの偽造不可能性検証システムの開発

1998 Fiscal Year Annual Research Report

• Project/Area Number: 10650361
• Research Institution: Osaka University
• Principal Investigator: 藤原 融 大阪大学, 基礎工学研究科, 教授 (70190098)
• Keywords: 情報セキュリティ / 暗号 / 暗号を用いたプロトコル / 形式的検証 / 安全性 / 偽造不可能性 / アルゴリズム

Research Abstract

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