暗号プロトコル安全性検証装置、方法およびプログラム
【課題】理想機能の種類や個数を限定することなく、種々の理想機能を部品として暗号化プロトコルの安全性検証を正確に行うこと。
【解決手段】暗号プロトコル安全性検証装置１００において、検証対象の暗号プロトコルの部品であって汎用結合可能安全性で定義される理想機能の記述である理想機能記述データの入力を受け付ける入力受付部１０１と、入力された理想機能記述データに含まれる処理の記述が、処理の要求元のパーティ以外のパーティおよび攻撃者以外のパーティとのメッセージの授受の処理を行わない局所的処理の記述を含むか否かを判断する局所判定部１０２と、理想機能記述データから、局所的処理の記述のみからなる攻撃者規則データ１１０を生成する攻撃者規則生成部１０３と、攻撃者規則データ１１０に基づいて検証対象の暗号プロトコルの安全性を検証する検証部１０６とを備えた。
【解決手段】暗号プロトコル安全性検証装置１００において、検証対象の暗号プロトコルの部品であって汎用結合可能安全性で定義される理想機能の記述である理想機能記述データの入力を受け付ける入力受付部１０１と、入力された理想機能記述データに含まれる処理の記述が、処理の要求元のパーティ以外のパーティおよび攻撃者以外のパーティとのメッセージの授受の処理を行わない局所的処理の記述を含むか否かを判断する局所判定部１０２と、理想機能記述データから、局所的処理の記述のみからなる攻撃者規則データ１１０を生成する攻撃者規則生成部１０３と、攻撃者規則データ１１０に基づいて検証対象の暗号プロトコルの安全性を検証する検証部１０６とを備えた。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、暗号プロトコルに欠陥があるか否かの安全性を検証する暗号プロトコル安全性検証装置、方法およびプログラムに関する。
【背景技術】
【０００２】
暗号プロトコルに欠陥があるか否かの安全性を検証する暗号プロトコル安全性検証の手法として、複雑な暗号プロトコルに対して直接に安全性証明を与えることは困難であるが、その暗号プロトコルが単純なプロトコルを部品として呼び出す場合には、その部品の安全性証明と、その部品の安全性を仮定した上での全体の安全性証明という比較的容易な二つの証明を与えることにより、全体の安全性証明を与えるモジューラアプローチという手法が提案されている。
【０００３】
しかし、暗号プロトコルは、そのプロトコルを一回だけ実行する場合（スタンドアロン実行）は安全であると証明されている場合でも、そのプロトコルを複数回実行した場合や、他の暗号プロトコルと混在させて実行した場合においても安全である保証はない。これは、ある暗号プロトコル実行を破ろうとする場合、攻撃者は、その暗号プロトコルの実行だけでなく他の暗号プロトコル実行から得た情報も使用して攻撃を行うことができるためである。
【０００４】
このような問題を解決するため、ユニバーサリィ・コンポーザブル安全性（UC 安全性）という暗号プロトコルの安全性の定式化の概念が提案されている（非特許文献１参照）。このＵＣ安全性の手法では、暗号プロトコルがスタンドアロン実行でＵＣ 安全であるならば、プロトコルを複数回実行した場合や、他の暗号プロトコルと混在させて実行した場合においてもＵＣ 安全であることを保証しているため、安全な部品を組み合わることで複雑な暗号プロトコルを安全に構築することが可能となる。
【０００５】
ここで、Canetti-Herzog は、汎用結合可能安全な、認証された公開鍵暗号の理想機能ＦCPKEを定義し、ＦCPKE−ハイブリッドモデルでの相互認証と鍵交換のプロトコルがＵＣ安全であるための記号的安全性基準を与えて、Blanchetが定義したstrong secrecyの概念（非特許文献２参照）を流用して鍵交換の記号的安全性基準を記述し、Blanchet が開発した定理証明ツールProVerif を用いて安全性証明を行っている（非特許文献３参照）。この手法の特徴は、もとの計算量的な安全性を持つ暗号プロトコルの安全性を証明するために、暗号プロトコルを記号的なプロトコルに変換し、その変換されたプロトコルが記号的な安全性基準を満たすことを確認すれば、その暗号プロトコルの安全性は証明される点にある。
【０００６】
このCanetti-Herzog による理想機能を用いた暗号プロトコルの安全性検証の手法は、１種類の理想機能ＦCPKEのハイブリッドモデルが対象であって、２種類以上の理想機能を対象とはしていない。このため、複数の異なる理想機能Ｆ1，・ ・ ・ ,Ｆnを用いる（Ｆ1，・ ・ ・ ,Ｆn）−ハイブリッドモデル（以下、「マルチハイブリッドモデル」といい、マルチハイブリッドモデルで構成された暗号プロトコルを「マルチハイブリッド暗号プロトコル」という。）で記述されている暗号プロトコルに対して記号的安全性記述を与えることができない。
【０００７】
Canetti-Herzogは、ＦCPKE−ハイブリッドモデルにおける２−パーティ相互認証と２−パーティ鍵交換のＵＣ安全性のために必要十分である記号的安全性基準を与えているが、ＦCPKE-ハイブリッドモデル以外のハイブリッドモデルについては類似の定式化は行っていない。
【０００８】
一方、Patil は, 公開鍵暗号理想機能ＦCPKEだけでなく, 署名理想機能ＦSIGも用いるマルチハイブリッドモデルへの拡張の手法を提案している（非特許文献４参照）。この手法では、Canetti-Herzog の手法を署名理想機能と公開鍵暗号理想機能のハイブリッドモデルへ拡張するものである。しかしながら、この手法は、署名の理想機能が公開鍵暗号の理想機能と近似する構造を有しているため実現可能となっているが、これら以外の理想機能を用いた暗号プロトコルの安全性検証について適用することはできない。
【０００９】
このように、複数の理想機能を用いた暗号プロトコルの安全性検証の実現が望まれている。
【００１０】
【非特許文献１】R. Canetti. Universally Composable Security: A New Paradigm for Cryptographic Protocols. In FOCS’01, pp.136-145. IEEE, 2001. Full version: http://eprint.iacr.org/2000/067.
【非特許文献２】B. Blanchet. Automatic Proof of Strong Secrecy for Security Protocols. In S&P’04, pp. 86-102. IEEE, 2004.
【非特許文献３】R. Canetti and J. Herzog. Universally Composable Symbolic Analysis of Cryptographic Protocols. Cryptology ePrint Archive Report 2004/334 http://eprint.iacr.org, 2004.
【非特許文献４】A. Patil. On symbolic analysis of cryptographic protocols. Mater’s thesis, 2005
【発明の開示】
【発明が解決しようとする課題】
【００１１】
ここで、公開鍵暗号理想機能が提供するインタフェースは、暗号化の要求命令（Ｅｎｃｒｙｐｔ，ＳＩＤ，ｍ）と復号化の要求命令（Ｄｅｃｒｙｐｔ，ＳＩＤ，ｃ）のフェーズにおいて、その要求命令を行ったパーティにそれぞれ暗号文ｃと平文ｍが返送され、当該パーティ以外のパーティとのメッセージ授受はない。このような、要求元のパーティ以外のパーティとメッセージの授受がないインタフェースを局所的なインタフェースという。署名理想機能は、公開鍵暗号理想機能と同様、局所的なインタフェースのみを有している。Canetti−Herzogの手法やPatilによる拡張は，理想機能が局所的インタフェースのみを持つことに依存している。
【００１２】
しかしながら、零知識証明の理想機能は、あるパーティが理想機能に証明を要求すると、理想機能は、要求元のパーティ以外の別のパーティにメッセージを送信するようになっている。このような要求元のパーティ以外のパーティとメッセージの授受を行うインタフェースを非局所的なインタフェースと呼ぶことにする。
【００１３】
攻撃者は、局所的インタフェースを利用して自分の知りうる情報を増やすことができるのに対して、非局所的インタフェースを利用しても、そのようなことはできない。
【００１４】
このため、非局所的インタフェースを含む理想機能を部品として暗号化プロトコルの安全性検証をＵＣ安全性に基づいて行う場合には、Canetti-Herzogの手法やPatilの拡張を用いても，正確な安全性検証を行うことができないという問題がある。
【００１５】
一方、局所的インタフェースのみを有する理想機能は、公開鍵暗号理想機能と署名理想機能等に限られており、種々の理想機能を部品として暗号化プロトコルの正確な安全性検証を行うことはできないという問題がある。
【００１６】
本発明は、上記に鑑みてなされたものであって、暗号プロトコルの部品としての理想機能の種類や個数を限定することなく、種々の理想機能を部品として暗号化プロトコルの安全性検証を正確に行うことができる暗号プロトコル安全性検証装置、方法およびプログラムを提供することを目的とする。
【課題を解決するための手段】
【００１７】
上述した課題を解決し、目的を達成するために、本発明にかかる暗号プロトコル安全性検証装置は、検証対象の暗号プロトコルの部品であって汎用結合可能安全性で定義される理想機能の記述である理想機能記述データの入力を受け付ける入力受付手段と、入力された前記理想機能記述データに含まれる処理の記述が、処理の要求元のパーティ以外のパーティおよび攻撃者以外のパーティとのメッセージの授受の処理を行わない局所的処理の記述を含むか否かを判断する局所判定手段と、前記理想機能記述データから、前記局所的処理の記述のみからなる攻撃者規則データを生成する攻撃者規則生成手段と、前記攻撃者規則データに基づいて前記検証対象の暗号プロトコルの安全性を検証する検証手段と、を備えたことを特徴とする。
【００１８】
また、本発明は、上記暗号プロトコル安全性検証装置で実行される暗号プロトコル安全性検証方法およびプログラムである。
【発明の効果】
【００１９】
本発明によれば、暗号プロトコルの部品としての理想機能の種類や個数を限定することなく、種々の理想機能を部品として暗号化プロトコルの安全性検証を正確に行うことができるという効果を奏する。
【発明を実施するための最良の形態】
【００２０】
以下に添付図面を参照して、この発明にかかる暗号プロトコル安全性検証装置、方法およびプログラムの最良な実施の形態を詳細に説明する。
【００２１】
（実施の形態１）
図１は、実施の形態１にかかる暗号プロトコル安全性検証装置の機能的構成を示すブロック図である。本実施の形態にかかる暗号プロトコル安全性検証装置１００は、図１に示すように、入力受付部１０１と、局所判定部１０２と、攻撃者規則生成部１０３と、プロトコル変換部１０４と、導出部１０５と、検証部１０６とを主に備えている。
【００２２】
入力受付部１０１は、検証対象の暗号プロトコルのプロトコル記述データと、検証対象の暗号プロトコルの部品として使用される理想機能Ｆ1〜ＦNの記述である理想機能Ｆ1記述データ〜理想機能ＦN記述データの入力を受け付ける処理部である。
【００２３】
理想機能とは、検証対象の暗号プロトコルの部品として使用され、汎用結合可能安全性で定義されるもので、理想機能におけるＵＣ安全性が証明された場合には、検証対象の暗号プロトコルの安全性が証明される。理想機能Ｆ記述データは、この理想機能における処理を記述したデータである。
【００２４】
図２は、理想機能Ｆ記述データのデータ構造図である。図２に示すように、理想機能Ｆ記述データは、複数のインタフェース記述から構成され、各インタフェース記述は、一または複数のコンストラクタ／デストラクタによる処理記述から構成される。
【００２５】
インタフェース記述は、例えば、暗号化の処理記述や復号化の処理記述が該当する。各インタフェース記述は、処理の関数であるコンストラクタやデストラクタによる処理記述から構成される。
【００２６】
図３は、理想機能Ｆ記述データの具体例を示す説明図である。図３の理想機能Ｆ記述データは、公開鍵暗号の理想機能ＦCPKEの理想機能記述データの例を示している。図３に示すように、３０１が初期化処理記述である。
【００２７】
また、公開鍵暗号理想機能が提供するインタフェースは暗号化の要求（Ｅｎｃｒｙｐｔ，ＳＩＤ，ｍ）と復号化の要求（Ｄｅｃｒｙｐｔ，ＳＩＤ，ｃ）であり、初期化処理のインタフェース記述３０１、「Ｅｎｃｒｙｐｔｉｏｎ」のインタフェース記述３０２と、「Ｄｅｃｒｙｐｔｉｏｎ」のインタフェース記述３０３とから構成される。図３の各インタフェース記述において、例えば、暗号化を行う関数ＥK（ｒ）がコンストラクタ、復号化を行う関数Ｄ（ｃ）がデストラクタである。
【００２８】
局所判定部１０２は、入力された理想機能Ｆ1記述データ〜理想機能ＦN記述データの局所性判定処理を行う処理部である。すなわち、局所判定部１０２は、入力された理想機能Ｆ1記述データ〜理想機能ＦN記述データのインタフェース記述のコンストラクタとデストラクタによる処理記述を解析して、各インタフェース記述が、局所的インタフェースであるか非局所的インタフェースであるかを判断し、インタフェース記述に局所的処理であるか否かを示す付加情報を付加する処理を行う。
【００２９】
ここで、局所的インタフェースとは、要求元のパーティ以外のパーティおよび攻撃者以外のパーティとのメッセージの授受の処理を行わない記述である。図４は、公開鍵暗号理想機能における局所的インタフェースを説明するための模式図である。
【００３０】
図４に示すように、公開鍵暗号理想機能が提供するインタフェースは暗号化の要求（Ｅｎｃｒｙｐｔ，ＳＩＤ，ｍ）と復号化の要求（Ｄｅｃｒｙｐｔ，ＳＩＤ，ｃ）であり、ぞれぞれ各命令を発したパーティに暗号文ｃと平文ｍが返され、それ以外のパーティとのメッセージ授受はない。従って、公開鍵暗号理想機能は、局所的インタフェースのみを有していることがわかる。この他、署名理想機能も局所的インタフェースのみを有している。
【００３１】
これに対し、非局所的インタフェースとは、要求元のパーティ以外のパーティまたは攻撃者以外のパーティとのメッセージの授受の処理を行う記述である。図５は、零知識証明理想機能における非局所的インタフェースを説明するための模式図である。
【００３２】
零知識証明理想機能では、図５に示すように、あるパーティＰPIDが理想機能ＦCPKEに証明を要求すると、理想機能ＦCPKEは、要求元のパーティＰPID以外の他のパーティＰPIDッセージを伝達している。従って、零知識証明理想機能は、非局所的インタフェースを有していることがわかる。
【００３３】
本実施の形態にかかる暗号プロトコル安全性検証装置１００では、局所判定部１０２によって、入力された理想機能Ｆ記述データを解析して、理想機能Ｆ記述データを各インタフェース記述に分割し、分割されたインタフェース記述に記述されているコンストラクタ／デストラクタによる処理記述からインタフェース記述が局所的か非局所的かを判断する。
【００３４】
具体的には、コンストラクタ／デストラクタによる処理記述において、理想機能と他のパーティとの間のメッセージ授受を解析し、そのインタフェースを呼び出した要求元のパーティとメッセージ授受の相手先のパーティと一致するか否かを調べることによって局所的インタフェースか非局所的インタフェースかを判断する。
【００３５】
そして、理想機能が、そのインタフェースを呼び出したパーティでも攻撃者でもないパーティとの間でメッセージを授受しており場合には、そのインタフェース記述は非局所的であると判断する。
【００３６】
例えば、図３に示す公開鍵暗号の理想機能ＦCPKEの理想機能記述データの場合には、初期化処理のインタフェース記述３０１、Ｅｎｃｒｙｐｔｉｏｎのインタフェース記述３０２、Ｄｅｃｒｙｐｔｉｏｎのインタフェース記述に分割する。そして、各インタフェース記述のインタフェースを解析すると、Ｅｎｃｒｙｐｔｉｏｎのインタフェース記述３０２の２．（ａ）において、平文ｍを攻撃者に渡しており、暗号化要求の要求元のパーティＰと攻撃者以外のパーティに対するメッセージの授受はない。このため、局所判定部１０２は、Ｅｎｃｒｙｐｔｉｏｎのインタフェース記述３０２は局所的インタフェースであると判断する。
【００３７】
また、Ｄｅｃｒｙｐｔｉｏｎのインタフェース記述３０３では、１．において対（ｍ，ｃ）を暗号化要求の要求元のパーティＰに返し、他のパーティとのメッセージ授受の記述は存在しない。このため、局所判定部１０２は、Ｄｅｃｒｙｐｔｉｏｎのインタフェース記述３０３は、局所インタフェースであると判断する。
【００３８】
そして、局所判定部１０２は、Ｅｎｃｒｙｐｔｉｏｎのインタフェース記述３０２およびＤｅｃｒｙｐｔｉｏｎのインタフェース記述３０３に局所的インタフェースを示す付加情報を付与する。
【００３９】
図６は、付加情報が付与された理想機能記述データのデータ構造図である。図６に示し召すように、各インタフェース記述に対して付加情報が付加されている。
【００４０】
ここで、付加情報は、局所的インタフェースであるか非局所的インタフェースであるかを示す情報であればよく例えば、数値や文字などで局所的インタフェースであるか非局所的インタフェースであるかを識別するように構成すればよい。
【００４１】
攻撃者規則生成部１０３は、理想機能Ｆ1記述データ〜理想機能ＦN記述データに付加された付加情報を参照して、理想機能Ｆ1記述データ〜理想機能ＦN記述データから局所的インタフェースの処理の記述のみを抽出して（あるいは非局所的インタフェースの処理の記述を削除して）、攻撃者規則データ１１０を生成し、ハードディスクドライブ装置（ＨＤＤ）やメモリ等の記憶媒体である記憶部に保存する処理部である。
【００４２】
図７は、攻撃者規則データの一例を示す説明図である。攻撃者規則データには、（Ｒｆ）、（Ｒｇ）、（Ｒｔ）におけるコンストラクタやデストラクタとして、非局所的インタフェースと判定されたインタフェース記述のコンストラクタ、デストラクタを含めないで生成される。
【００４３】
これは以下の理由による。すなわち、攻撃者が非局所的なインタフェースを利用しようとすると、第３者とのメッセージの授受により、コンストラクタおよびデストラクタを適用した結果が第３者に渡ってしまい、攻撃者の手に入らないからである。これに対して、局所的インタフェースの場合は、コンストラクタおよびデストラクタを適用した結果が、第３者に渡らずに、そのまま攻撃者に返されるので攻撃者規則に加えるのが妥当であるからである。また、インタフェース記述が複数のコンストラクタおよびデストラクタの組み合わせの場合には、個々のコンストラクタおよびデストラクタではなく、これらの組み合せをひとまとめにした処理を攻撃者が利用できるようにするためである。
【００４４】
プロトコル変換部１０４は、入力受付部１０１によって入力された検証対象の暗号プロトコル記述データをプロトコル規則１１１に変換して、ＨＤＤやメモリ等の記憶媒体である記憶部に保存する処理部である。図８は、プロトコル規則の一例を示す説明図である。
【００４５】
導出部１０５は、記憶部に保存されているプロトコル規則データ１１１と攻撃者規則データ１１０とを読み出して、両データを合併した規則データ１１３を生成し、ＨＤＤやメモリ等の記憶媒体である記憶部に規則集合として保存し、この規則データ１１３から安全性検証のための判断情報を導出する処理部である。
【００４６】
導出部１０５によって合併されたプロトコルＰ0に対する規則データ１１３の規則集合ＲP0は、（１）式で示される。
【００４７】
【数１】
【００４８】
ここで、（ＲP0）・ρは、（２）式で示される。また、σ0は、プロセスＰ0のすべての自由変数をＳｅｃｒの相異なる元へ写像する代入とする。
【００４９】
また、導出部１０５は、具体的には、この規則データ１１３の規則集合ＲP0の中から判断情報として「ｂａｄ」を導出する。導出部１０５は、規則集合ＲP0の中から判断情報として「ｂａｄ」を導出するため、B.Blanchet and A.Podelski. Verification of Cryptographic Protocols: Tagging Enforces Termination. In FoDDaCS'03, Vol.2620 of LNCS, pp.136-152. Springer-Verlag, 2003に記載された手法を拡張した自由選択による導出に基づく解決アルゴリズムを用いている。
【００５０】
解決アルゴリズムでは、２つの節Ｒ＝Ｈ→ＣとＲ’＝Ｆ∧Ｈ’→Ａから、（３）式によってＲｏＦＲ’＝σＨ∧σＨ’→σＣ’を導出する。
【００５１】
【数２】
【００５２】
（３）式において、ＣとＦは単一化可能で、σは最汎単一化である。複数の項に対して、その単一化が存在する場合に、それらの項を単一化可能という。単一化とは、複数の項に対して、変数に適当な項を代入することで、それらを同一の項にすることをいう。また、最汎単一化とは、複数の項の単一化の中で、最も一般的なものをいう。
【００５３】
導出部１０５では、規則集合を構成するプロトコル規則データ１１１と攻撃者規則データ１１０の各集合を二つの節（項）として、（３）式により、σＣ’としての「bad」を導出している。
【００５４】
ここで、導出は、（４）式に定義される選択関数ｓｅｌとして誘導される。 かかる導出は、ｓｅｌ（Ｒ）＝０かつＦ∈ｓｅｌ（Ｒ’）の場合にのみ実行される。
【００５５】
【数３】
【００５６】
検証部１０６は、解決部１０５によって導出した判断情報「ｂａｄ」から検証対象の暗号プロトコルの安全性を検証する処理部である。具体的には、検証部１０６は、導出部１０５によって規則データ１１３の規則集合から「ｂａｄ」が導出された場合には、暗号プロトコルの安全性が証明されたと判断し、導出部１０５によって規則データ１１３の規則集合から「ｂａｄ」が導出されなかった場合には、暗号プロトコルの安全性が証明されなかったと判断する。
【００５７】
次に、以上のように構成された実施の形態１にかかる暗号プロトコル安全性検証装置１００による暗号プロトコルの安全性検証処理について説明する。図９は、暗号プロトコルの安全性検証処理の手順を示すフローチャートである。
【００５８】
まず、入力受付部１０１によって、プロトコル記述データの入力を受付け（ステップＳ１１）、入力されたプロトコル記述データをプロトコル規則に変換してプロトコル規則データ１１１を記憶部にプロトコル規則集合として保存する（ステップＳ１２）。
【００５９】
かかる処理と並行して、入力受付部１０１によって、理想機能Ｆ記述データの入力を受付け（ステップＳ１３）、局所判定部１０２によって、入力した理想機能Ｆ記述データを解析して局所性判定処理を行う（ステップＳ１４）。
【００６０】
ここで、局所性判定処理について詳述する。図１０は、実施の形態１の局所性判定処理の手順を示すフローチャートである。
【００６１】
局所判定部１０２は、入力された理想機能Ｆ記述データを解析して、理想機能Ｆ記述データを各インタフェース記述に分割する（ステップＳ２１）。そして、分割されたインタフェース記述の中のコンストラクタ／デストラクタによる処理記述の解析を行う（ステップＳ２２）。
【００６２】
そして、インタフェース記述の中のコンストラクタ／デストラクタによる処理記述のすべてにおいて、そのインタフェースを呼び出したパーティ以外のパーティおよび攻撃者以外のパーティとのメッセージ授受の処理記述があるかどうか調べる（ステップＳ２３）。そして、呼び出したパーティ以外のパーティおよび攻撃者以外のパーティとのメッセージ授受の処理記述がない場合には（ステップＳ２３：Ｎｏ）、そのインタフェース記述は局所的インタフェースであると判定し（ステップＳ２４）、局所的の付加情報をインタフェース記述に付加する（ステップS２５）。
【００６３】
一方、ステップS２３において、インタフェース記述の中のコンストラクタ／デストラクタによる処理記述のいずれかにおいて、呼び出したパーティ以外のパーティまたは攻撃者以外のパーティとのメッセージ授受の処理記述がある場合には（ステップＳ２３：Ｙｅｓ）、そのインタフェース記述は、非局所的インタフェースであると判定し（ステップS２６）、非局所的の付加情報をインタフェース記述に付加する（ステップS２７）。
【００６４】
そして、ステップＳ２２からＳ２７までの処理を、全てのインタフェース記述に対して繰り返し行う（ステップＳ２８）。
【００６５】
図９に戻り、以上のように理想機能記述データの局所性判定処理が終了したら、攻撃者規則生成部１０３によって、付加情報が付加された理想機能記述データから局所的インタフェースのインタフェース記述のみを抽出した攻撃者規則データ１１０を生成して記憶部に保存する（ステップＳ１５）。
【００６６】
そして、導出部１０５によって、記憶部に保存されているプロトコル規則データ１１１と攻撃者規則データ１１０とを合併して規則データ１１３の規則集合を生成し（ステップＳ１６）、この規則集合から判断情報「ｂａｄ」を導出する判断情報の導出処理を行う（ステップＳ１７）。
【００６７】
次に、検証部１０６によって、検証処理を行う（ステップＳ１８）。すなわち、規則集合から判断情報「ｂａｄ」を導出できた場合には、検証部１０６は、プロトコル記述データの暗号プロトコルは安全性が証明されたと判断し、規則集合から判断情報「ｂａｄ」を導出できなかった場合には、プロトコル記述データの暗号プロトコルは安全性が証明されなかったと判断する。そして、最後に、検証部１０６は、この検証結果を表示装置や印刷装置などに出力する（ステップＳ１９）。
【００６８】
このように実施の形態１にかかる暗号プロトコル安全性検証装置１００では、理想機能記述データのインタフェース記述が局所的インタフェースか非局所的インタフェースかを判定し、局所的インタフェースのみからなる攻撃者規則データを生成して、暗号プロトコルの安全性検証を行っているので、理想機能が局所的インタフェースを含むか否かという種別や、理想機能の個数に限定されることなく、種々の理想機能を部品として暗号化プロトコルの安全性検証を正確に行うことができる。
【００６９】
（実施の形態２）
実施の形態１にかかる暗号プロトコル安全性検証装置１００は、入力した理想機能記述データの中のメッセージ授受の処理記述を解析して局所インタフェースであるか否かを判定していたが、この実施の形態２にかかる暗号プロトコル安全性検証装置１００は、予め局所インタフェースか否かの付加情報が含まれた理想理想機能記述データを入力して局所インタフェースがあるか否かを判定している。
【００７０】
実施の形態２にかかる暗号プロトコル安全性検証装置１００の機能的構成は実施の形態１と同様である。本実施の形態では、局所判定部１０２が、予め局所インタフェースか否かの付加情報が含まれた理想機能記述データの付加情報からインタフェース記述が局所インタフェースであるか否かを判定しており、理想機能記述データに付加情報を付加する処理は行わない。
【００７１】
実施の形態２にかかる暗号プロトコル安全性検証装置１００に入力される理想機能記述データのデータ構造は、図６で示したデータ構造と同様のものである。
【００７２】
次に、以上のように構成された実施の形態２にかかる暗号プロトコル安全性検証装置１００による暗号プロトコルの安全性検証処理について説明する。本実施の形態の暗号プロトコルの安全性検証の全体処理については実施の形態１の図９の処理手順と同様に行われる。実施の形態２では、ステップＳ１４における局所判定部１０２による局所性判定処理が実施の形態１と異なっている。
【００７３】
図１１は、実施の形態２の局所性判定処理の手順を示すフローチャートである。まず、局所判定部１０２は、入力された理想機能Ｆ記述データを解析して、理想機能Ｆ記述データを各インタフェース記述に分割する（ステップＳ３１）。そして、分割されたインタフェース記述に付加されている付加情報を抽出する（ステップＳ３２）。
【００７４】
次に、抽出した付加情報が局所的を示すか否かを調べる（ステップＳ３３）。そして、付加情報が局所的を示す場合には（ステップＳ３３：Ｙｅｓ）、当該インタフェース記述は局所インタフェースであると判定する（ステップＳ３４）。
【００７５】
一方、ステップＳ３３において、付加情報が局所的を示さない場合、すなわち非局所的である旨を示す場合には（ステップＳ３３：Ｎｏ）、、当該インタフェース記述は非局所インタフェースであると判定する（ステップＳ３５）。
【００７６】
そして、ステップＳ３２からＳ３５までの処理を、全てのインタフェース記述に対して繰り返し行う（ステップＳ３６）。
【００７７】
このようにして理想機能記述データの局所性判定が終了したら、実施の形態１と同様に、攻撃者規則情報の生成から暗号プロトコルの安全性の検証までの処理が行われる。
【００７８】
図１２は、実施の形態１および２の暗号プロトコル安全性検証装置１００のハードウェア構成を示すブロック図である。実施の形態１および２の暗号プロトコル安全性検証装置１００は、ＣＰＵ５１などの制御装置と、ＲＯＭ（Read Only Memory）５２やＲＡＭ（Random Access Memory）５３などの記憶装置と、ＨＤＤ、ＣＤドライブ装置などの外部記憶装置と、ディスプレイ装置などの表示装置と、キーボードやマウスなどの入力装置、通信インタフェース５７とを備えており、通常のコンピュータを利用したハードウェア構成となっている。
【００７９】
実施の形態１および２にかかる暗号プロトコル安全性検証装置１００で実行される暗号プロトコル安全性検証プログラムは、インストール可能な形式又は実行可能な形式のファイルでＣＤ−ＲＯＭ、フレキシブルディスク（ＦＤ）、ＣＤ−Ｒ、ＤＶＤ（Ｄｉｇｉｔａｌ Ｖｅｒｓａｔｉｌｅ Ｄｉｓｋ）等のコンピュータで読み取り可能な記録媒体に記録されて提供される。
【００８０】
また、実施の形態１および２にかかる暗号プロトコル安全性検証装置１００で実行される暗号プロトコル安全性検証プログラムを、インターネット等のネットワークに接続されたコンピュータ上に格納し、ネットワーク経由でダウンロードさせることにより提供するように構成しても良い。また、実施の形態１および２にかかる暗号プロトコル安全性検証装置１００で実行される暗号プロトコル安全性検証プログラムをインターネット等のネットワーク経由で提供または配布するように構成しても良い。
【００８１】
また、実施の形態１および２にかかる暗号プロトコル安全性検証装置１００で実行される暗号プロトコル安全性検証プログラムを、ＲＯＭ等に予め組み込んで提供するように構成してもよい。
【００８２】
実施の形態１および２にかかる暗号プロトコル安全性検証装置１００で実行される暗号プロトコル安全性検証プログラムは、上述した各部（入力受付部１０１、局所判定部１０２、攻撃者規則生成部１０３、プロトコル変換部１０４、導出部１０５、検証部１０６）を含むモジュール構成となっており、実際のハードウェアとしてはＣＰＵ５１（プロセッサ）が上記記憶媒体から暗号プロトコル安全性検証プログラムを読み出して実行することにより上記各部が主記憶装置上にロードされ、入力受付部１０１、局所判定部１０２、攻撃者規則生成部１０３、プロトコル変換部１０４、導出部１０５、検証部１０６が主記憶装置上に生成されるようになっている。
【００８３】
このように実施の形態２にかかる暗号プロトコル安全性検証装置１００では、理想機能記述データのインタフェース記述が局所的インタフェースか非局所的インタフェースかを判定し、局所的インタフェースのみからなる攻撃者規則データを生成して、暗号プロトコルの安全性検証を行っているので、理想機能が局所的インタフェースを含むか否かという種別や、理想機能の個数に限定されることなく、種々の理想機能を部品として暗号化プロトコルの安全性検証を正確に行うことができる。
【００８４】
また、実施の形態２にかかる暗号プロトコル安全性検証装置１００では、予め局所インタフェースか否かの付加情報が含まれた理想機能記述データの付加情報からインタフェース記述が局所インタフェースであるか否かを判定しているので、局所性の判定処理を正確かつ迅速に行うことが可能となる。
【００８５】
なお、本発明は、上記実施の形態そのままに限定されるものではなく、実施段階ではその要旨を逸脱しない範囲で構成要素を変形して具体化することができる。また、上記実施の形態に開示されている複数の構成要素の適宜な組み合わせにより、種々の発明を形成することができる。例えば、実施の形態に示される全構成要素からいくつかの構成要素を削除してもよい。
【図面の簡単な説明】
【００８６】
【図１】実施の形態１にかかる暗号プロトコル安全性検証装置の機能的構成を示すブロック図である。
【図２】理想機能記述データのデータ構造図である。
【図３】理想機能Ｆ記述データの具体例を示す説明図である。
【図４】公開鍵暗号理想機能における局所的インタフェースを説明するための模式図である。
【図５】零知識証明理想機能における非局所的インタフェースを説明するための模式図である。
【図６】付加情報が付与された理想機能記述データのデータ構造図である。
【図７】攻撃者規則データの一例を示す説明図である。
【図８】プロトコル規則の一例を示す説明図である。
【図９】暗号プロトコルの安全性検証処理の手順を示すフローチャートである。
【図１０】実施の形態１の局所性判定処理の手順を示すフローチャートである。
【図１１】実施の形態２の局所性判定処理の手順を示すフローチャートである。
【図１２】実施の形態１および２の暗号プロトコル安全性検証装置１００のハードウェア構成を示すブロック図である。
【符号の説明】
【００８７】
１０１ 入力受付部
１０２ 局所判定部
１０３ 攻撃者規則生成部
１０４ プロトコル変換部
１０５ 導出部
１０６ 検証部
１１０ 攻撃者規則データ
１１１ プロトコル規則データ
１１３ 規則データ
３０１〜３０２ インタフェース記述
【技術分野】
【０００１】
本発明は、暗号プロトコルに欠陥があるか否かの安全性を検証する暗号プロトコル安全性検証装置、方法およびプログラムに関する。
【背景技術】
【０００２】
暗号プロトコルに欠陥があるか否かの安全性を検証する暗号プロトコル安全性検証の手法として、複雑な暗号プロトコルに対して直接に安全性証明を与えることは困難であるが、その暗号プロトコルが単純なプロトコルを部品として呼び出す場合には、その部品の安全性証明と、その部品の安全性を仮定した上での全体の安全性証明という比較的容易な二つの証明を与えることにより、全体の安全性証明を与えるモジューラアプローチという手法が提案されている。
【０００３】
しかし、暗号プロトコルは、そのプロトコルを一回だけ実行する場合（スタンドアロン実行）は安全であると証明されている場合でも、そのプロトコルを複数回実行した場合や、他の暗号プロトコルと混在させて実行した場合においても安全である保証はない。これは、ある暗号プロトコル実行を破ろうとする場合、攻撃者は、その暗号プロトコルの実行だけでなく他の暗号プロトコル実行から得た情報も使用して攻撃を行うことができるためである。
【０００４】
このような問題を解決するため、ユニバーサリィ・コンポーザブル安全性（UC 安全性）という暗号プロトコルの安全性の定式化の概念が提案されている（非特許文献１参照）。このＵＣ安全性の手法では、暗号プロトコルがスタンドアロン実行でＵＣ 安全であるならば、プロトコルを複数回実行した場合や、他の暗号プロトコルと混在させて実行した場合においてもＵＣ 安全であることを保証しているため、安全な部品を組み合わることで複雑な暗号プロトコルを安全に構築することが可能となる。
【０００５】
ここで、Canetti-Herzog は、汎用結合可能安全な、認証された公開鍵暗号の理想機能ＦCPKEを定義し、ＦCPKE−ハイブリッドモデルでの相互認証と鍵交換のプロトコルがＵＣ安全であるための記号的安全性基準を与えて、Blanchetが定義したstrong secrecyの概念（非特許文献２参照）を流用して鍵交換の記号的安全性基準を記述し、Blanchet が開発した定理証明ツールProVerif を用いて安全性証明を行っている（非特許文献３参照）。この手法の特徴は、もとの計算量的な安全性を持つ暗号プロトコルの安全性を証明するために、暗号プロトコルを記号的なプロトコルに変換し、その変換されたプロトコルが記号的な安全性基準を満たすことを確認すれば、その暗号プロトコルの安全性は証明される点にある。
【０００６】
このCanetti-Herzog による理想機能を用いた暗号プロトコルの安全性検証の手法は、１種類の理想機能ＦCPKEのハイブリッドモデルが対象であって、２種類以上の理想機能を対象とはしていない。このため、複数の異なる理想機能Ｆ1，・ ・ ・ ,Ｆnを用いる（Ｆ1，・ ・ ・ ,Ｆn）−ハイブリッドモデル（以下、「マルチハイブリッドモデル」といい、マルチハイブリッドモデルで構成された暗号プロトコルを「マルチハイブリッド暗号プロトコル」という。）で記述されている暗号プロトコルに対して記号的安全性記述を与えることができない。
【０００７】
Canetti-Herzogは、ＦCPKE−ハイブリッドモデルにおける２−パーティ相互認証と２−パーティ鍵交換のＵＣ安全性のために必要十分である記号的安全性基準を与えているが、ＦCPKE-ハイブリッドモデル以外のハイブリッドモデルについては類似の定式化は行っていない。
【０００８】
一方、Patil は, 公開鍵暗号理想機能ＦCPKEだけでなく, 署名理想機能ＦSIGも用いるマルチハイブリッドモデルへの拡張の手法を提案している（非特許文献４参照）。この手法では、Canetti-Herzog の手法を署名理想機能と公開鍵暗号理想機能のハイブリッドモデルへ拡張するものである。しかしながら、この手法は、署名の理想機能が公開鍵暗号の理想機能と近似する構造を有しているため実現可能となっているが、これら以外の理想機能を用いた暗号プロトコルの安全性検証について適用することはできない。
【０００９】
このように、複数の理想機能を用いた暗号プロトコルの安全性検証の実現が望まれている。
【００１０】
【非特許文献１】R. Canetti. Universally Composable Security: A New Paradigm for Cryptographic Protocols. In FOCS’01, pp.136-145. IEEE, 2001. Full version: http://eprint.iacr.org/2000/067.
【非特許文献２】B. Blanchet. Automatic Proof of Strong Secrecy for Security Protocols. In S&P’04, pp. 86-102. IEEE, 2004.
【非特許文献３】R. Canetti and J. Herzog. Universally Composable Symbolic Analysis of Cryptographic Protocols. Cryptology ePrint Archive Report 2004/334 http://eprint.iacr.org, 2004.
【非特許文献４】A. Patil. On symbolic analysis of cryptographic protocols. Mater’s thesis, 2005
【発明の開示】
【発明が解決しようとする課題】
【００１１】
ここで、公開鍵暗号理想機能が提供するインタフェースは、暗号化の要求命令（Ｅｎｃｒｙｐｔ，ＳＩＤ，ｍ）と復号化の要求命令（Ｄｅｃｒｙｐｔ，ＳＩＤ，ｃ）のフェーズにおいて、その要求命令を行ったパーティにそれぞれ暗号文ｃと平文ｍが返送され、当該パーティ以外のパーティとのメッセージ授受はない。このような、要求元のパーティ以外のパーティとメッセージの授受がないインタフェースを局所的なインタフェースという。署名理想機能は、公開鍵暗号理想機能と同様、局所的なインタフェースのみを有している。Canetti−Herzogの手法やPatilによる拡張は，理想機能が局所的インタフェースのみを持つことに依存している。
【００１２】
しかしながら、零知識証明の理想機能は、あるパーティが理想機能に証明を要求すると、理想機能は、要求元のパーティ以外の別のパーティにメッセージを送信するようになっている。このような要求元のパーティ以外のパーティとメッセージの授受を行うインタフェースを非局所的なインタフェースと呼ぶことにする。
【００１３】
攻撃者は、局所的インタフェースを利用して自分の知りうる情報を増やすことができるのに対して、非局所的インタフェースを利用しても、そのようなことはできない。
【００１４】
このため、非局所的インタフェースを含む理想機能を部品として暗号化プロトコルの安全性検証をＵＣ安全性に基づいて行う場合には、Canetti-Herzogの手法やPatilの拡張を用いても，正確な安全性検証を行うことができないという問題がある。
【００１５】
一方、局所的インタフェースのみを有する理想機能は、公開鍵暗号理想機能と署名理想機能等に限られており、種々の理想機能を部品として暗号化プロトコルの正確な安全性検証を行うことはできないという問題がある。
【００１６】
本発明は、上記に鑑みてなされたものであって、暗号プロトコルの部品としての理想機能の種類や個数を限定することなく、種々の理想機能を部品として暗号化プロトコルの安全性検証を正確に行うことができる暗号プロトコル安全性検証装置、方法およびプログラムを提供することを目的とする。
【課題を解決するための手段】
【００１７】
上述した課題を解決し、目的を達成するために、本発明にかかる暗号プロトコル安全性検証装置は、検証対象の暗号プロトコルの部品であって汎用結合可能安全性で定義される理想機能の記述である理想機能記述データの入力を受け付ける入力受付手段と、入力された前記理想機能記述データに含まれる処理の記述が、処理の要求元のパーティ以外のパーティおよび攻撃者以外のパーティとのメッセージの授受の処理を行わない局所的処理の記述を含むか否かを判断する局所判定手段と、前記理想機能記述データから、前記局所的処理の記述のみからなる攻撃者規則データを生成する攻撃者規則生成手段と、前記攻撃者規則データに基づいて前記検証対象の暗号プロトコルの安全性を検証する検証手段と、を備えたことを特徴とする。
【００１８】
また、本発明は、上記暗号プロトコル安全性検証装置で実行される暗号プロトコル安全性検証方法およびプログラムである。
【発明の効果】
【００１９】
本発明によれば、暗号プロトコルの部品としての理想機能の種類や個数を限定することなく、種々の理想機能を部品として暗号化プロトコルの安全性検証を正確に行うことができるという効果を奏する。
【発明を実施するための最良の形態】
【００２０】
以下に添付図面を参照して、この発明にかかる暗号プロトコル安全性検証装置、方法およびプログラムの最良な実施の形態を詳細に説明する。
【００２１】
（実施の形態１）
図１は、実施の形態１にかかる暗号プロトコル安全性検証装置の機能的構成を示すブロック図である。本実施の形態にかかる暗号プロトコル安全性検証装置１００は、図１に示すように、入力受付部１０１と、局所判定部１０２と、攻撃者規則生成部１０３と、プロトコル変換部１０４と、導出部１０５と、検証部１０６とを主に備えている。
【００２２】
入力受付部１０１は、検証対象の暗号プロトコルのプロトコル記述データと、検証対象の暗号プロトコルの部品として使用される理想機能Ｆ1〜ＦNの記述である理想機能Ｆ1記述データ〜理想機能ＦN記述データの入力を受け付ける処理部である。
【００２３】
理想機能とは、検証対象の暗号プロトコルの部品として使用され、汎用結合可能安全性で定義されるもので、理想機能におけるＵＣ安全性が証明された場合には、検証対象の暗号プロトコルの安全性が証明される。理想機能Ｆ記述データは、この理想機能における処理を記述したデータである。
【００２４】
図２は、理想機能Ｆ記述データのデータ構造図である。図２に示すように、理想機能Ｆ記述データは、複数のインタフェース記述から構成され、各インタフェース記述は、一または複数のコンストラクタ／デストラクタによる処理記述から構成される。
【００２５】
インタフェース記述は、例えば、暗号化の処理記述や復号化の処理記述が該当する。各インタフェース記述は、処理の関数であるコンストラクタやデストラクタによる処理記述から構成される。
【００２６】
図３は、理想機能Ｆ記述データの具体例を示す説明図である。図３の理想機能Ｆ記述データは、公開鍵暗号の理想機能ＦCPKEの理想機能記述データの例を示している。図３に示すように、３０１が初期化処理記述である。
【００２７】
また、公開鍵暗号理想機能が提供するインタフェースは暗号化の要求（Ｅｎｃｒｙｐｔ，ＳＩＤ，ｍ）と復号化の要求（Ｄｅｃｒｙｐｔ，ＳＩＤ，ｃ）であり、初期化処理のインタフェース記述３０１、「Ｅｎｃｒｙｐｔｉｏｎ」のインタフェース記述３０２と、「Ｄｅｃｒｙｐｔｉｏｎ」のインタフェース記述３０３とから構成される。図３の各インタフェース記述において、例えば、暗号化を行う関数ＥK（ｒ）がコンストラクタ、復号化を行う関数Ｄ（ｃ）がデストラクタである。
【００２８】
局所判定部１０２は、入力された理想機能Ｆ1記述データ〜理想機能ＦN記述データの局所性判定処理を行う処理部である。すなわち、局所判定部１０２は、入力された理想機能Ｆ1記述データ〜理想機能ＦN記述データのインタフェース記述のコンストラクタとデストラクタによる処理記述を解析して、各インタフェース記述が、局所的インタフェースであるか非局所的インタフェースであるかを判断し、インタフェース記述に局所的処理であるか否かを示す付加情報を付加する処理を行う。
【００２９】
ここで、局所的インタフェースとは、要求元のパーティ以外のパーティおよび攻撃者以外のパーティとのメッセージの授受の処理を行わない記述である。図４は、公開鍵暗号理想機能における局所的インタフェースを説明するための模式図である。
【００３０】
図４に示すように、公開鍵暗号理想機能が提供するインタフェースは暗号化の要求（Ｅｎｃｒｙｐｔ，ＳＩＤ，ｍ）と復号化の要求（Ｄｅｃｒｙｐｔ，ＳＩＤ，ｃ）であり、ぞれぞれ各命令を発したパーティに暗号文ｃと平文ｍが返され、それ以外のパーティとのメッセージ授受はない。従って、公開鍵暗号理想機能は、局所的インタフェースのみを有していることがわかる。この他、署名理想機能も局所的インタフェースのみを有している。
【００３１】
これに対し、非局所的インタフェースとは、要求元のパーティ以外のパーティまたは攻撃者以外のパーティとのメッセージの授受の処理を行う記述である。図５は、零知識証明理想機能における非局所的インタフェースを説明するための模式図である。
【００３２】
零知識証明理想機能では、図５に示すように、あるパーティＰPIDが理想機能ＦCPKEに証明を要求すると、理想機能ＦCPKEは、要求元のパーティＰPID以外の他のパーティＰPIDッセージを伝達している。従って、零知識証明理想機能は、非局所的インタフェースを有していることがわかる。
【００３３】
本実施の形態にかかる暗号プロトコル安全性検証装置１００では、局所判定部１０２によって、入力された理想機能Ｆ記述データを解析して、理想機能Ｆ記述データを各インタフェース記述に分割し、分割されたインタフェース記述に記述されているコンストラクタ／デストラクタによる処理記述からインタフェース記述が局所的か非局所的かを判断する。
【００３４】
具体的には、コンストラクタ／デストラクタによる処理記述において、理想機能と他のパーティとの間のメッセージ授受を解析し、そのインタフェースを呼び出した要求元のパーティとメッセージ授受の相手先のパーティと一致するか否かを調べることによって局所的インタフェースか非局所的インタフェースかを判断する。
【００３５】
そして、理想機能が、そのインタフェースを呼び出したパーティでも攻撃者でもないパーティとの間でメッセージを授受しており場合には、そのインタフェース記述は非局所的であると判断する。
【００３６】
例えば、図３に示す公開鍵暗号の理想機能ＦCPKEの理想機能記述データの場合には、初期化処理のインタフェース記述３０１、Ｅｎｃｒｙｐｔｉｏｎのインタフェース記述３０２、Ｄｅｃｒｙｐｔｉｏｎのインタフェース記述に分割する。そして、各インタフェース記述のインタフェースを解析すると、Ｅｎｃｒｙｐｔｉｏｎのインタフェース記述３０２の２．（ａ）において、平文ｍを攻撃者に渡しており、暗号化要求の要求元のパーティＰと攻撃者以外のパーティに対するメッセージの授受はない。このため、局所判定部１０２は、Ｅｎｃｒｙｐｔｉｏｎのインタフェース記述３０２は局所的インタフェースであると判断する。
【００３７】
また、Ｄｅｃｒｙｐｔｉｏｎのインタフェース記述３０３では、１．において対（ｍ，ｃ）を暗号化要求の要求元のパーティＰに返し、他のパーティとのメッセージ授受の記述は存在しない。このため、局所判定部１０２は、Ｄｅｃｒｙｐｔｉｏｎのインタフェース記述３０３は、局所インタフェースであると判断する。
【００３８】
そして、局所判定部１０２は、Ｅｎｃｒｙｐｔｉｏｎのインタフェース記述３０２およびＤｅｃｒｙｐｔｉｏｎのインタフェース記述３０３に局所的インタフェースを示す付加情報を付与する。
【００３９】
図６は、付加情報が付与された理想機能記述データのデータ構造図である。図６に示し召すように、各インタフェース記述に対して付加情報が付加されている。
【００４０】
ここで、付加情報は、局所的インタフェースであるか非局所的インタフェースであるかを示す情報であればよく例えば、数値や文字などで局所的インタフェースであるか非局所的インタフェースであるかを識別するように構成すればよい。
【００４１】
攻撃者規則生成部１０３は、理想機能Ｆ1記述データ〜理想機能ＦN記述データに付加された付加情報を参照して、理想機能Ｆ1記述データ〜理想機能ＦN記述データから局所的インタフェースの処理の記述のみを抽出して（あるいは非局所的インタフェースの処理の記述を削除して）、攻撃者規則データ１１０を生成し、ハードディスクドライブ装置（ＨＤＤ）やメモリ等の記憶媒体である記憶部に保存する処理部である。
【００４２】
図７は、攻撃者規則データの一例を示す説明図である。攻撃者規則データには、（Ｒｆ）、（Ｒｇ）、（Ｒｔ）におけるコンストラクタやデストラクタとして、非局所的インタフェースと判定されたインタフェース記述のコンストラクタ、デストラクタを含めないで生成される。
【００４３】
これは以下の理由による。すなわち、攻撃者が非局所的なインタフェースを利用しようとすると、第３者とのメッセージの授受により、コンストラクタおよびデストラクタを適用した結果が第３者に渡ってしまい、攻撃者の手に入らないからである。これに対して、局所的インタフェースの場合は、コンストラクタおよびデストラクタを適用した結果が、第３者に渡らずに、そのまま攻撃者に返されるので攻撃者規則に加えるのが妥当であるからである。また、インタフェース記述が複数のコンストラクタおよびデストラクタの組み合わせの場合には、個々のコンストラクタおよびデストラクタではなく、これらの組み合せをひとまとめにした処理を攻撃者が利用できるようにするためである。
【００４４】
プロトコル変換部１０４は、入力受付部１０１によって入力された検証対象の暗号プロトコル記述データをプロトコル規則１１１に変換して、ＨＤＤやメモリ等の記憶媒体である記憶部に保存する処理部である。図８は、プロトコル規則の一例を示す説明図である。
【００４５】
導出部１０５は、記憶部に保存されているプロトコル規則データ１１１と攻撃者規則データ１１０とを読み出して、両データを合併した規則データ１１３を生成し、ＨＤＤやメモリ等の記憶媒体である記憶部に規則集合として保存し、この規則データ１１３から安全性検証のための判断情報を導出する処理部である。
【００４６】
導出部１０５によって合併されたプロトコルＰ0に対する規則データ１１３の規則集合ＲP0は、（１）式で示される。
【００４７】
【数１】
【００４８】
ここで、（ＲP0）・ρは、（２）式で示される。また、σ0は、プロセスＰ0のすべての自由変数をＳｅｃｒの相異なる元へ写像する代入とする。
【００４９】
また、導出部１０５は、具体的には、この規則データ１１３の規則集合ＲP0の中から判断情報として「ｂａｄ」を導出する。導出部１０５は、規則集合ＲP0の中から判断情報として「ｂａｄ」を導出するため、B.Blanchet and A.Podelski. Verification of Cryptographic Protocols: Tagging Enforces Termination. In FoDDaCS'03, Vol.2620 of LNCS, pp.136-152. Springer-Verlag, 2003に記載された手法を拡張した自由選択による導出に基づく解決アルゴリズムを用いている。
【００５０】
解決アルゴリズムでは、２つの節Ｒ＝Ｈ→ＣとＲ’＝Ｆ∧Ｈ’→Ａから、（３）式によってＲｏＦＲ’＝σＨ∧σＨ’→σＣ’を導出する。
【００５１】
【数２】
【００５２】
（３）式において、ＣとＦは単一化可能で、σは最汎単一化である。複数の項に対して、その単一化が存在する場合に、それらの項を単一化可能という。単一化とは、複数の項に対して、変数に適当な項を代入することで、それらを同一の項にすることをいう。また、最汎単一化とは、複数の項の単一化の中で、最も一般的なものをいう。
【００５３】
導出部１０５では、規則集合を構成するプロトコル規則データ１１１と攻撃者規則データ１１０の各集合を二つの節（項）として、（３）式により、σＣ’としての「bad」を導出している。
【００５４】
ここで、導出は、（４）式に定義される選択関数ｓｅｌとして誘導される。 かかる導出は、ｓｅｌ（Ｒ）＝０かつＦ∈ｓｅｌ（Ｒ’）の場合にのみ実行される。
【００５５】
【数３】
【００５６】
検証部１０６は、解決部１０５によって導出した判断情報「ｂａｄ」から検証対象の暗号プロトコルの安全性を検証する処理部である。具体的には、検証部１０６は、導出部１０５によって規則データ１１３の規則集合から「ｂａｄ」が導出された場合には、暗号プロトコルの安全性が証明されたと判断し、導出部１０５によって規則データ１１３の規則集合から「ｂａｄ」が導出されなかった場合には、暗号プロトコルの安全性が証明されなかったと判断する。
【００５７】
次に、以上のように構成された実施の形態１にかかる暗号プロトコル安全性検証装置１００による暗号プロトコルの安全性検証処理について説明する。図９は、暗号プロトコルの安全性検証処理の手順を示すフローチャートである。
【００５８】
まず、入力受付部１０１によって、プロトコル記述データの入力を受付け（ステップＳ１１）、入力されたプロトコル記述データをプロトコル規則に変換してプロトコル規則データ１１１を記憶部にプロトコル規則集合として保存する（ステップＳ１２）。
【００５９】
かかる処理と並行して、入力受付部１０１によって、理想機能Ｆ記述データの入力を受付け（ステップＳ１３）、局所判定部１０２によって、入力した理想機能Ｆ記述データを解析して局所性判定処理を行う（ステップＳ１４）。
【００６０】
ここで、局所性判定処理について詳述する。図１０は、実施の形態１の局所性判定処理の手順を示すフローチャートである。
【００６１】
局所判定部１０２は、入力された理想機能Ｆ記述データを解析して、理想機能Ｆ記述データを各インタフェース記述に分割する（ステップＳ２１）。そして、分割されたインタフェース記述の中のコンストラクタ／デストラクタによる処理記述の解析を行う（ステップＳ２２）。
【００６２】
そして、インタフェース記述の中のコンストラクタ／デストラクタによる処理記述のすべてにおいて、そのインタフェースを呼び出したパーティ以外のパーティおよび攻撃者以外のパーティとのメッセージ授受の処理記述があるかどうか調べる（ステップＳ２３）。そして、呼び出したパーティ以外のパーティおよび攻撃者以外のパーティとのメッセージ授受の処理記述がない場合には（ステップＳ２３：Ｎｏ）、そのインタフェース記述は局所的インタフェースであると判定し（ステップＳ２４）、局所的の付加情報をインタフェース記述に付加する（ステップS２５）。
【００６３】
一方、ステップS２３において、インタフェース記述の中のコンストラクタ／デストラクタによる処理記述のいずれかにおいて、呼び出したパーティ以外のパーティまたは攻撃者以外のパーティとのメッセージ授受の処理記述がある場合には（ステップＳ２３：Ｙｅｓ）、そのインタフェース記述は、非局所的インタフェースであると判定し（ステップS２６）、非局所的の付加情報をインタフェース記述に付加する（ステップS２７）。
【００６４】
そして、ステップＳ２２からＳ２７までの処理を、全てのインタフェース記述に対して繰り返し行う（ステップＳ２８）。
【００６５】
図９に戻り、以上のように理想機能記述データの局所性判定処理が終了したら、攻撃者規則生成部１０３によって、付加情報が付加された理想機能記述データから局所的インタフェースのインタフェース記述のみを抽出した攻撃者規則データ１１０を生成して記憶部に保存する（ステップＳ１５）。
【００６６】
そして、導出部１０５によって、記憶部に保存されているプロトコル規則データ１１１と攻撃者規則データ１１０とを合併して規則データ１１３の規則集合を生成し（ステップＳ１６）、この規則集合から判断情報「ｂａｄ」を導出する判断情報の導出処理を行う（ステップＳ１７）。
【００６７】
次に、検証部１０６によって、検証処理を行う（ステップＳ１８）。すなわち、規則集合から判断情報「ｂａｄ」を導出できた場合には、検証部１０６は、プロトコル記述データの暗号プロトコルは安全性が証明されたと判断し、規則集合から判断情報「ｂａｄ」を導出できなかった場合には、プロトコル記述データの暗号プロトコルは安全性が証明されなかったと判断する。そして、最後に、検証部１０６は、この検証結果を表示装置や印刷装置などに出力する（ステップＳ１９）。
【００６８】
このように実施の形態１にかかる暗号プロトコル安全性検証装置１００では、理想機能記述データのインタフェース記述が局所的インタフェースか非局所的インタフェースかを判定し、局所的インタフェースのみからなる攻撃者規則データを生成して、暗号プロトコルの安全性検証を行っているので、理想機能が局所的インタフェースを含むか否かという種別や、理想機能の個数に限定されることなく、種々の理想機能を部品として暗号化プロトコルの安全性検証を正確に行うことができる。
【００６９】
（実施の形態２）
実施の形態１にかかる暗号プロトコル安全性検証装置１００は、入力した理想機能記述データの中のメッセージ授受の処理記述を解析して局所インタフェースであるか否かを判定していたが、この実施の形態２にかかる暗号プロトコル安全性検証装置１００は、予め局所インタフェースか否かの付加情報が含まれた理想理想機能記述データを入力して局所インタフェースがあるか否かを判定している。
【００７０】
実施の形態２にかかる暗号プロトコル安全性検証装置１００の機能的構成は実施の形態１と同様である。本実施の形態では、局所判定部１０２が、予め局所インタフェースか否かの付加情報が含まれた理想機能記述データの付加情報からインタフェース記述が局所インタフェースであるか否かを判定しており、理想機能記述データに付加情報を付加する処理は行わない。
【００７１】
実施の形態２にかかる暗号プロトコル安全性検証装置１００に入力される理想機能記述データのデータ構造は、図６で示したデータ構造と同様のものである。
【００７２】
次に、以上のように構成された実施の形態２にかかる暗号プロトコル安全性検証装置１００による暗号プロトコルの安全性検証処理について説明する。本実施の形態の暗号プロトコルの安全性検証の全体処理については実施の形態１の図９の処理手順と同様に行われる。実施の形態２では、ステップＳ１４における局所判定部１０２による局所性判定処理が実施の形態１と異なっている。
【００７３】
図１１は、実施の形態２の局所性判定処理の手順を示すフローチャートである。まず、局所判定部１０２は、入力された理想機能Ｆ記述データを解析して、理想機能Ｆ記述データを各インタフェース記述に分割する（ステップＳ３１）。そして、分割されたインタフェース記述に付加されている付加情報を抽出する（ステップＳ３２）。
【００７４】
次に、抽出した付加情報が局所的を示すか否かを調べる（ステップＳ３３）。そして、付加情報が局所的を示す場合には（ステップＳ３３：Ｙｅｓ）、当該インタフェース記述は局所インタフェースであると判定する（ステップＳ３４）。
【００７５】
一方、ステップＳ３３において、付加情報が局所的を示さない場合、すなわち非局所的である旨を示す場合には（ステップＳ３３：Ｎｏ）、、当該インタフェース記述は非局所インタフェースであると判定する（ステップＳ３５）。
【００７６】
そして、ステップＳ３２からＳ３５までの処理を、全てのインタフェース記述に対して繰り返し行う（ステップＳ３６）。
【００７７】
このようにして理想機能記述データの局所性判定が終了したら、実施の形態１と同様に、攻撃者規則情報の生成から暗号プロトコルの安全性の検証までの処理が行われる。
【００７８】
図１２は、実施の形態１および２の暗号プロトコル安全性検証装置１００のハードウェア構成を示すブロック図である。実施の形態１および２の暗号プロトコル安全性検証装置１００は、ＣＰＵ５１などの制御装置と、ＲＯＭ（Read Only Memory）５２やＲＡＭ（Random Access Memory）５３などの記憶装置と、ＨＤＤ、ＣＤドライブ装置などの外部記憶装置と、ディスプレイ装置などの表示装置と、キーボードやマウスなどの入力装置、通信インタフェース５７とを備えており、通常のコンピュータを利用したハードウェア構成となっている。
【００７９】
実施の形態１および２にかかる暗号プロトコル安全性検証装置１００で実行される暗号プロトコル安全性検証プログラムは、インストール可能な形式又は実行可能な形式のファイルでＣＤ−ＲＯＭ、フレキシブルディスク（ＦＤ）、ＣＤ−Ｒ、ＤＶＤ（Ｄｉｇｉｔａｌ Ｖｅｒｓａｔｉｌｅ Ｄｉｓｋ）等のコンピュータで読み取り可能な記録媒体に記録されて提供される。
【００８０】
また、実施の形態１および２にかかる暗号プロトコル安全性検証装置１００で実行される暗号プロトコル安全性検証プログラムを、インターネット等のネットワークに接続されたコンピュータ上に格納し、ネットワーク経由でダウンロードさせることにより提供するように構成しても良い。また、実施の形態１および２にかかる暗号プロトコル安全性検証装置１００で実行される暗号プロトコル安全性検証プログラムをインターネット等のネットワーク経由で提供または配布するように構成しても良い。
【００８１】
また、実施の形態１および２にかかる暗号プロトコル安全性検証装置１００で実行される暗号プロトコル安全性検証プログラムを、ＲＯＭ等に予め組み込んで提供するように構成してもよい。
【００８２】
実施の形態１および２にかかる暗号プロトコル安全性検証装置１００で実行される暗号プロトコル安全性検証プログラムは、上述した各部（入力受付部１０１、局所判定部１０２、攻撃者規則生成部１０３、プロトコル変換部１０４、導出部１０５、検証部１０６）を含むモジュール構成となっており、実際のハードウェアとしてはＣＰＵ５１（プロセッサ）が上記記憶媒体から暗号プロトコル安全性検証プログラムを読み出して実行することにより上記各部が主記憶装置上にロードされ、入力受付部１０１、局所判定部１０２、攻撃者規則生成部１０３、プロトコル変換部１０４、導出部１０５、検証部１０６が主記憶装置上に生成されるようになっている。
【００８３】
このように実施の形態２にかかる暗号プロトコル安全性検証装置１００では、理想機能記述データのインタフェース記述が局所的インタフェースか非局所的インタフェースかを判定し、局所的インタフェースのみからなる攻撃者規則データを生成して、暗号プロトコルの安全性検証を行っているので、理想機能が局所的インタフェースを含むか否かという種別や、理想機能の個数に限定されることなく、種々の理想機能を部品として暗号化プロトコルの安全性検証を正確に行うことができる。
【００８４】
また、実施の形態２にかかる暗号プロトコル安全性検証装置１００では、予め局所インタフェースか否かの付加情報が含まれた理想機能記述データの付加情報からインタフェース記述が局所インタフェースであるか否かを判定しているので、局所性の判定処理を正確かつ迅速に行うことが可能となる。
【００８５】
なお、本発明は、上記実施の形態そのままに限定されるものではなく、実施段階ではその要旨を逸脱しない範囲で構成要素を変形して具体化することができる。また、上記実施の形態に開示されている複数の構成要素の適宜な組み合わせにより、種々の発明を形成することができる。例えば、実施の形態に示される全構成要素からいくつかの構成要素を削除してもよい。
【図面の簡単な説明】
【００８６】
【図１】実施の形態１にかかる暗号プロトコル安全性検証装置の機能的構成を示すブロック図である。
【図２】理想機能記述データのデータ構造図である。
【図３】理想機能Ｆ記述データの具体例を示す説明図である。
【図４】公開鍵暗号理想機能における局所的インタフェースを説明するための模式図である。
【図５】零知識証明理想機能における非局所的インタフェースを説明するための模式図である。
【図６】付加情報が付与された理想機能記述データのデータ構造図である。
【図７】攻撃者規則データの一例を示す説明図である。
【図８】プロトコル規則の一例を示す説明図である。
【図９】暗号プロトコルの安全性検証処理の手順を示すフローチャートである。
【図１０】実施の形態１の局所性判定処理の手順を示すフローチャートである。
【図１１】実施の形態２の局所性判定処理の手順を示すフローチャートである。
【図１２】実施の形態１および２の暗号プロトコル安全性検証装置１００のハードウェア構成を示すブロック図である。
【符号の説明】
【００８７】
１０１ 入力受付部
１０２ 局所判定部
１０３ 攻撃者規則生成部
１０４ プロトコル変換部
１０５ 導出部
１０６ 検証部
１１０ 攻撃者規則データ
１１１ プロトコル規則データ
１１３ 規則データ
３０１〜３０２ インタフェース記述
【特許請求の範囲】
【請求項１】
検証対象の暗号プロトコルの部品であって汎用結合可能安全性で定義される理想機能の記述である理想機能記述データの入力を受け付ける入力受付手段と、
入力された前記理想機能記述データに含まれる処理の記述が、処理の要求元のパーティ以外のパーティおよび攻撃者以外のパーティとのメッセージの授受の処理を行わない局所的処理の記述を含むか否かを判断する局所判定手段と、
前記理想機能記述データから、前記局所的処理の記述のみからなる攻撃者規則データを生成する攻撃者規則生成手段と、
前記攻撃者規則データに基づいて前記検証対象の暗号プロトコルの安全性を検証する検証手段と、
を備えたことを特徴とする暗号プロトコル安全性検証装置。
【請求項２】
前記局所判定手段は、前記理想機能記述データの処理の記述を解析して、前記局所的処理の記述を含むか否かを判断し、処理の記述に前記局所的処理であるか否かを示す付加情報を付加し、
前記攻撃者規則生成手段は、前記付加情報に基づいて前記理想機能記述データから前記局所的処理の記述を抽出して、前記攻撃者規則データを生成することを特徴とする請求項１に記載の暗号プロトコル安全性検証装置。
【請求項３】
前記理想機能記述データは、処理の記述に前記局所的処理であるか否かを示す付加情報が付加されており、
前記局所判定手段は、前記付加情報に基づいて、前記理想機能記述データに前記局所的処理の記述を含むか否かを判断し、
前記攻撃者規則生成手段は、前記付加情報に基づいて前記理想機能記述データから前記局所的処理の記述を抽出して、前記攻撃者規則データを生成することを特徴とする請求項１に記載の暗号プロトコル安全性検証装置。
【請求項４】
前記検証対象の暗号プロトコルの記述である暗号プロトコル記述データのプロトコル規則と前記攻撃者規則データとから、安全性検証のための判断情報を導出する導出手段、をさらに備え、
前記検証手段は、導出された判断情報に基づいて前記検証対象の暗号プロトコルの安全性を検証することを特徴とする請求項１〜３のいずれか一つに記載の暗号プロトコル安全性検証装置。
【請求項５】
入力受付手段によって、検証対象の暗号プロトコルの部品であって汎用結合可能安全性で定義される理想機能の記述である理想機能記述データの入力を受け付けるステップと、
局所判断手段によって、入力された前記理想機能記述データに含まれる処理の記述が、処理の要求元のパーティ以外のパーティおよび攻撃者以外のパーティとのメッセージの授受の処理を行わない局所的処理の記述を含むか否かを判断するステップと、
攻撃者規則生成手段によって、前記理想機能記述データから、前記局所的処理の記述のみからなる攻撃者規則データを生成するステップと、
検証手段によって、前記攻撃者規則データに基づいて前記検証対象の暗号プロトコルの安全性を検証するステップと、
を含むことを特徴とする暗号プロトコル安全性検証方法。
【請求項６】
検証対象の暗号プロトコルの部品であって汎用結合可能安全性で定義される理想機能の記述である理想機能記述データの入力を受け付けるステップと、
入力された前記理想機能記述データに含まれる処理の記述が、処理の要求元のパーティ以外のパーティおよび攻撃者以外のパーティとのメッセージの授受の処理を行わない局所的処理の記述を含むか否かを判断するステップと、
前記理想機能記述データから、前記局所的処理の記述のみからなる攻撃者規則データを生成するステップと、
前記攻撃者規則データに基づいて前記検証対象の暗号プロトコルの安全性を検証するステップと、
をコンピュータに実行させる暗号プロトコル安全性検証プログラム。
【請求項１】
検証対象の暗号プロトコルの部品であって汎用結合可能安全性で定義される理想機能の記述である理想機能記述データの入力を受け付ける入力受付手段と、
入力された前記理想機能記述データに含まれる処理の記述が、処理の要求元のパーティ以外のパーティおよび攻撃者以外のパーティとのメッセージの授受の処理を行わない局所的処理の記述を含むか否かを判断する局所判定手段と、
前記理想機能記述データから、前記局所的処理の記述のみからなる攻撃者規則データを生成する攻撃者規則生成手段と、
前記攻撃者規則データに基づいて前記検証対象の暗号プロトコルの安全性を検証する検証手段と、
を備えたことを特徴とする暗号プロトコル安全性検証装置。
【請求項２】
前記局所判定手段は、前記理想機能記述データの処理の記述を解析して、前記局所的処理の記述を含むか否かを判断し、処理の記述に前記局所的処理であるか否かを示す付加情報を付加し、
前記攻撃者規則生成手段は、前記付加情報に基づいて前記理想機能記述データから前記局所的処理の記述を抽出して、前記攻撃者規則データを生成することを特徴とする請求項１に記載の暗号プロトコル安全性検証装置。
【請求項３】
前記理想機能記述データは、処理の記述に前記局所的処理であるか否かを示す付加情報が付加されており、
前記局所判定手段は、前記付加情報に基づいて、前記理想機能記述データに前記局所的処理の記述を含むか否かを判断し、
前記攻撃者規則生成手段は、前記付加情報に基づいて前記理想機能記述データから前記局所的処理の記述を抽出して、前記攻撃者規則データを生成することを特徴とする請求項１に記載の暗号プロトコル安全性検証装置。
【請求項４】
前記検証対象の暗号プロトコルの記述である暗号プロトコル記述データのプロトコル規則と前記攻撃者規則データとから、安全性検証のための判断情報を導出する導出手段、をさらに備え、
前記検証手段は、導出された判断情報に基づいて前記検証対象の暗号プロトコルの安全性を検証することを特徴とする請求項１〜３のいずれか一つに記載の暗号プロトコル安全性検証装置。
【請求項５】
入力受付手段によって、検証対象の暗号プロトコルの部品であって汎用結合可能安全性で定義される理想機能の記述である理想機能記述データの入力を受け付けるステップと、
局所判断手段によって、入力された前記理想機能記述データに含まれる処理の記述が、処理の要求元のパーティ以外のパーティおよび攻撃者以外のパーティとのメッセージの授受の処理を行わない局所的処理の記述を含むか否かを判断するステップと、
攻撃者規則生成手段によって、前記理想機能記述データから、前記局所的処理の記述のみからなる攻撃者規則データを生成するステップと、
検証手段によって、前記攻撃者規則データに基づいて前記検証対象の暗号プロトコルの安全性を検証するステップと、
を含むことを特徴とする暗号プロトコル安全性検証方法。
【請求項６】
検証対象の暗号プロトコルの部品であって汎用結合可能安全性で定義される理想機能の記述である理想機能記述データの入力を受け付けるステップと、
入力された前記理想機能記述データに含まれる処理の記述が、処理の要求元のパーティ以外のパーティおよび攻撃者以外のパーティとのメッセージの授受の処理を行わない局所的処理の記述を含むか否かを判断するステップと、
前記理想機能記述データから、前記局所的処理の記述のみからなる攻撃者規則データを生成するステップと、
前記攻撃者規則データに基づいて前記検証対象の暗号プロトコルの安全性を検証するステップと、
をコンピュータに実行させる暗号プロトコル安全性検証プログラム。
【図１】
【図２】
【図３】
【図４】
【図５】
【図６】
【図７】
【図８】
【図９】
【図１０】
【図１１】
【図１２】
【図２】
【図３】
【図４】
【図５】
【図６】
【図７】
【図８】
【図９】
【図１０】
【図１１】
【図１２】
【公開番号】特開２００８−３５１１７（Ｐ２００８−３５１１７Ａ）
【公開日】平成２０年２月１４日（２００８．２．１４）
【国際特許分類】
【出願番号】特願２００６−２０５２６１（Ｐ２００６−２０５２６１）
【出願日】平成１８年７月２７日（２００６．７．２７）
【出願人】（０００００３０７８）株式会社東芝 (54,554)
【Ｆターム（参考）】
【公開日】平成２０年２月１４日（２００８．２．１４）
【国際特許分類】
【出願日】平成１８年７月２７日（２００６．７．２７）
【出願人】（０００００３０７８）株式会社東芝 (54,554)
【Ｆターム（参考）】
[ Back to top ]