書換えモデルを用いた暗号プロトコルの形成的設計法

2001 Fiscal Year Annual Research Report

• Project/Area Number: 12780227
• Research Institution: Wakayama University
• Principal Investigator: 田中 猛彦 和歌山大学, システム工学部, 助手 (90304154)
• Keywords: 情報セキュリティ / 暗号プロトコル / 認証 / 情報共有 / 安全性検証 / 形式的手法

Research Abstract

昨年度の研究に引続き,クライアント・サーバ間で認証を行い,かつ両者がその後の通信のために情報を共有するプロトコル(認証・情報共有プロトコル)を対象とした形式的設計モデルの構築に取り組んだ.この形式的設計モデルにおいて中心となるのが、そのモデルに基づいて記述した認証・情報共有プロトコルに対する安全性判定アルゴリズムである.報告者は,本研究を実施する以前に,暗号プロトコルの安全性判定アルゴリズムについて考察しており,その成果を用いることで容易に解決できると考えていた.しかし,その実現において,考察したアルゴリズムが半決定アルゴリズムである(安全でない場合,原理的には常に安全でないような攻撃方法を指摘できるが,安全である場合にこのアルゴリズムを適用すると無限ループに陥るケースが存在する)ことが判明した.そのため,この判定アルゴリズムと別の着想による判定法を検討した.形式的記述には条件付き項書換え系を採用しているが,項書換え系の諸性質の判定に木オートマトンが有用なことが知られている.そこで,木オートマトンを用いた判定アルゴリズムの構築を試みたが,線型性条件を回避することができず徒労に終わった.今後は,これまでの安全性判定アルゴリズムに立ち返って,このアルゴリズムの適用範囲を明らかにしたのちに,この判定法を含む形式的設計モデルを用いて,安全かつ実用的な認証・情報共有プロトコルの設計を目指す.

Research Products

• [Publications] Masaru Nakagawa: "Building an Electronic Shopping Mall for Oysters"Information Systems Modeling. (2001)
• [Publications] 平野 貴弘: "同業者を集めた電子モールシステムの構築"情報知識学会第9回研究報告会講演論文集. 55-58 (2001)
• [Publications] 松本 然: "介護保険サービス利用者を支援するデータベースシステムの構築"2002年情報学シンポジウム講演論文集. 63-70 (2002)
• [Publications] 川崎 淳子: "ツリー型質問掲示板を対象とした記事検索システム"第八回社会情報システム学シンポジウム学術講演論文集. 25-30 (2002)
• [Publications] 今井 直基: "電子掲示板におけるキーワード提案型記事検索システム"第八回社会情報システム学シンポジウム学術講演論文集. 31-36 (2002)