暗号を用いたプロトコルの安全性検証法に関する研究

本研究では暗号を用いたプロトコルに関し、以下のような結果を得た。これまでに提案してきたアルゴリズムでは、現実に提案されているシステムの安全性を判定できないものも少なからず存在していた。そこで本研究では、プロトコルのある通信において、その送信データと受信データの意味的な関係を考慮に入れながら、安全か否かの判定を行なうようにアルゴリズムを改良を行なった。具体的にはデータに型という属性を持たせ、実際に送信データが制限される場合をアルゴリズムに組み込むことにより、考えるべき情報集合を制限する。そして、既存のアルゴリズムではこれまで判定できなかったクラスの問題について、安全であることを検証できるアルゴリズムを提案した。同時にこの手法で検証できる問題のクラスが、安全であるようなシステムについてはもとのアルゴリズムのクラスを真に含んでおり、安全でないようなシステムについてはもとのものと等しいことを示した。その上で、上記の検証法について、その実用性を確認するためにアルゴリズムを計算機上で実現した。適用例として、MITが提案したKerberosシステムの安全性を検証し、その安全性を示した。また、ディジタルデータの不正コピーを防ぐという、著作権保護を目的としたプロトコルを提案し、その安全性を示した。

本研究では暗号を用いたプロトコルに関し、以下のような結果を得た。これまでに提案してきたアルゴリズムでは、現実に提案されているシステムの安全性を判定できないものも少なからず存在していた。そこで本研究では、プロトコルのある通信において、その送信データと受信データの意味的な関係を考慮に入れながら、安全か否かの判定を行なうようにアルゴリズムを改良を行なった。具体的にはデータに型という属性を持たせ、実際に送信データが制限される場合をアルゴリズムに組み込むことにより、考えるべき情報集合を制限する。そして、既存のアルゴリズムではこれまで判定できなかったクラスの問題について、安全であることを検証できるアルゴリズムを提案した。同時にこの手法で検証できる問題のクラスが、安全であるようなシステムについてはもとのアルゴリズムのクラスを真に含んでおり、安全でないようなシステムについてはもとのものと等しいことを示した。その上で、上記の検証法について、その実用性を確認するためにアルゴリズムを計算機上で実現した。適用例として、MITが提案したKerberosシステムの安全性を検証し、その安全性を示した。また、ディジタルデータの不正コピーを防ぐという、著作権保護を目的としたプロトコルを提案し、その安全性を示した。