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

点击翻译按钮获取中文摘要

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