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

2000 Fiscal Year Annual Research Report

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

Research Abstract

本研究ではまず,これまで提案されている種々の暗号プロトコル,およびセキュリティが必要とされるネットワークシステムのニーズを調査した.その結果,クライアント・サーバ間で認証を行い,かつ両者がその後の通信のための情報を共有するようなプロトコル(「認証・情報共有プロトコル」と呼ぶ)の必要性が非常に高く,かつしばしば他の応用的な暗号プロトコルの前提となっていることがわかった.この種の暗号プロトコルについての形式的検証法は従来よく議論されており,その成果を活用することも十分期待できる.そこで本研究では認証・情報共有のプロトコルを対象とした形式的設計法に集中してとりかかることとした.次に,この方針のもとで,2種類のネットワークシステム(3次元画像の共同制作システムおよび電子モールシステム)に対して,それぞれの目的に合った認証・情報共有プロトコルを設計し組み込んだ.これらのシステムは,1台のサーバ計算機にインターネットを介して多数の利用者が接続するという点では共通であるが,想定するクライアント計算機の安全性に大きな違いがあり,そのため設計した認証・情報共有プロトコルもそれぞれ大きく異なったものとなっている.いずれのプロトコルも,実証実験を行ったところ,セキュリティの欠陥,運用上の不具合ともに検出されなかった.今後は,この成果を基に,認証・情報共有プロトコルの形式的設計モデルを構築すること,およびそれを利用して安全かつ実用的なプロトコルを設計することを目指す.

Research Products

• [Publications] Takehiko Tanaka: "Support System for Distributed Collaborative 3-D Graphics Design"Knowledge-Based Software Engineering. 31-34 (2000)
• [Publications] 野上暁功: "かき電子モールの構築"第七回社会情報学シンポジウム学術講演論文集. 29-34 (2001)