"ブラインド署名を用いるプロトコルの安全性を検証するプロトコル安全性検証装置であって、上記ブラインド署名が一対一偽造不可能性を満たすとした場合に、上記プロトコルが安全か判定する安全性判定部と、上記ブラインド署名がワンモア偽造不可能性を満たすか判定するワンモア偽造不可能性判定部と、上記ブラインド署名による署名の対象となるメッセージをmとし、上記ブラインド署名の検証アルゴリズムの関数をVとして、VV’の関係を満たす関数V’、ハッシュ関数H及び関数fが存在するという条件を満たすか判定する条件判定部と、上記安全性判定部において上記プロトコルは安全であると判定され、上記ワンモア偽造不可能性判定部において上記ブラインド署名はワンモア偽造不可能性を満たすと判定され、上記条件判定部において上記条件を満たすと判定された場合に、上記プロトコルは安全であると判定する最終判定部と、を含むプロトコル安全性検証装置。請求項1のプロトコル安全性検証装置において、ワンモア偽造不可能性を満たすブラインド署名についての情報を記憶する第一記憶部を更に含み、上記ワンモア偽造不可能性判定部は、上記第一記憶部を参照して上記ブランド署名がワンモア偽造不可能性を満たすか判定する、プロトコル安全性検証装置。請求項1又は2のプロトコル安全性検証装置において、上記条件を満たすブラインド署名についての情報を記憶する第二記憶部を更に含み、上記条件判定部は、上記第二記憶部を参照して上記ブラインド署名が上記条件を満たすか判定する、プロトコル安全性検証装置。ブラインド署名を用いるプロトコルの安全性を検証するプロトコル安全性検証方法であって、安全性判定部が、上記ブラインド署名が一対一偽造不可能性を満たすとした場合に、上記プロトコルが安全か判定する安全性判定ステップと、ワンモア偽造不可能性判定部が、上記ブラインド署名がワンモア偽造不可能性を満たすか判定するワンモア偽造不可能性判定ステップと、条件判定部が、上記ブラインド署名による署名の対象となるメッセージをmとし、上記ブラインド署名の検証アルゴリズムの関数をVとして、VV’の関係を満たす関数V’、ハッシュ関数H及び関数fが存在するという条件を満たすか判定する条件判定ステップと、最終判定部が、上記安全性判定ステップにおいて上記プロトコルは安全であると判定され、上記ワンモア偽造不可能性判定ステップにおいて上記ブラインド署名はワンモア偽造不可能性を満たすと判定され、上記条件判定ステップにおいて上記条件を満たすと判定された場合に、上記プロトコルは安全であると判定する最終判定ステップと、を含むプロトコル安全性検証方法。請求項1から3のプロトコル安全性検証装置の各部としてコンピュータを機能させるためのプログラム。このように、非特許文献3に記載されたプロトコルの安全性検証方法では、そのプロトコルが用いるブラインド署名が一対一偽造不可能性を有する必要がある。しかしながら、あるブラインド署名が一対一偽造不能性を満たす場合にはそのブラインド署名はワンモア偽造不能性を満たすが、あるブラインド署名がワンモア偽造不能性を満たす場合にはそのブラインド署名は一対一偽造不能性を満たすとは限らない。すなわち、ワンモア偽造不可能性を満たすブラインド署名が、一対一偽造不可能性を満たすとは限らない。このため、非特許文献3に記載されたプロトコルの安全性検証方法では、ワンモア偽造不可能性を満たすブラインド署名を用いたプロトコルの安全性を検証することはできない。この発明の課題は、ワンモア偽造不可能性を満たすブラインド署名を用いたプロトコルの安全性を検証し得るプロトコル安全性検証装置、方法、プログラムを提供することである。この発明の一態様によるプロトコル安全性検証装置は、ブラインド署名を用いるプロトコルの安全性を検証するプロトコル安全性検証装置であって、ブラインド署名が一対一偽造不可能性を満たすとした場合に、プロトコルが安全か判定する安全性判定部と、ブラインド署名がワンモア偽造不可能性を満たすか判定するワンモア偽造不可能性判定部と、ブラインド署名の検証アルゴリズムの関数をVとして、VV’の関係を満たす関数V’、ハッシュ関数H及び関数fが存在するという条件を満たすか判定する条件判定部と、安全性判定部においてプロトコルは安全であると判定され、ワンモア偽造不可能性判定部においてブラインド署名はワンモア偽造不可能性を満たすと判定され、条件判定部において条件を満たすと判定された場合に、プロトコルは安全であると判定する最終判定部と、を含む。ワンモア偽造不可能性を満たすブラインド署名を用いたプロトコルの安全性を検証し得る。以下、図面を参照してこの発明の一実施形態を説明する。プロトコル安全性検証装置及び方法の一実施形態を以下に示す。プロトコル安全性検証装置は、図1に示すように、安全性判定部1、ワンモア偽造不可能性判定部2、条件判定部3、最終判定部4、第一記憶部5、第二記憶部6を例えば含む。プロトコル安全性検証装置は、図2に例示されたプロトコル安全性検証方法の各ステップの処理を行う。プロトコル仕様情報及びプロトコル安全性仕様情報が、安全性判定部1に入力される。プロトコル仕様情報は、プロトコルの仕様に関する情報であり、局所状態の有限集合S及び局所遷移規則の集合Rの組S,Rから例えば構成される。プロトコル安全性仕様情報は、プロトコルの安全性の仕様に関する情報であり、大域状態s0及び論理式Pから例えば構成される。安全性判定部1は、入力されたプロトコル仕様情報及びプロトコル安全性仕様情報に基づいて、そのプロトコルが用いるブラインド署名が一対一偽造不可能性を満たすとした場合に、そのプロトコルが安全か判定するステップS1。一対一偽造不可能性の定義については、背景技術の欄を参照こと。プロトコルの安全性についての情報は、最終判定部4に送信される。この実施形態では、プロトコルが安全であると判定された場合には真である旨の情報が最終判定部4に送信され、プロトコルが安全ではないと判定された場合には偽である旨の情報が最終判定部4に送信される。安全性判定部1は、例えば非特許文献3に記載された手法を用いて安全性の判定を行う。以下、安全性判定部1による安全性の判定処理の概要を簡単に説明する。まず、安全性判定部1は、所定の初期状態から所定の遷移規則に基づいて遷移可能な状態を全て抽出する。所定の初期状態及び所定の遷移規則は、プロトコル仕様情報及びプロトコル安全性仕様情報により定められる。つぎに、安全性判定部1は、抽出された遷移可能な全ての状態のそれぞれにおいて、論理式Pを満たすかどうかを判断する。遷移可能な全ての状態のそれぞれにおいて所定の安全性を定義する論理式Pが満たされている場合には、そのプロトコルは安全であると判断することができる。一方、遷移可能な状態の中で論理式Pを満たさないものがある場合には、そのプロトコルは安全ではないと判断する。論理式Pは、所定の安全性を定義するものであり、安全性判定部1に入力されるプロトコル安全性仕様情報により定められる。このように、安全性判定部により判断された安全性は、論旨式Pで定義された安全性を満たすという意味での安全性を意味する。ワンモア偽造不可能性判定部2は、プロトコルが用いるブラインド署名がワンモア偽造不可能性を満たすか判定するステップS2。ワンモア偽造不可能性を満たすかどうかについての情報は、最終判定部4に送信される。この実施形態では、ワンモア偽造不可能性を満たす場合には真である旨の情報が最終判定部4に送信され、ワンモア偽造不可能性を満たさない場合には偽である旨の情報が最終判定部4に送信される。以下、ワンモア偽造不可能性判定部2による安全性の判定処理の概要を簡単に説明する。ワンモア偽造不可能性を満たすブラインド署名についての情報を第一記憶部5に予め記憶しておく。ブラインド署名についての情報とは、例えばブラインド署名の識別子である。ワンモア偽造不可能性判定部2は、第一記憶部5を参照してブラインド署名がワンモア偽造不可能性を満たすか判定する。例えば、判定の対象となるプロトコルが用いるブラインド署名の識別子をキーとして第一記憶部5を参照して、一致する識別子があればそのブラインド署名はワンモア偽造不可能性を満たすと判定することができ、一致する識別子がなければそのブラインド署名はワンモア偽造不可能性を満たさないと判定することができる。条件判定部3は、安全性の評価の対象となるプロトコルのブランド署名が、所定の条件を満たすか判定するステップS3。所定の条件を満たすかどうかについての情報は、最終判定部4に送信される。この実施形態では、所定の条件を満たすと判定された場合には真である旨の情報が最終判定部4に送信され、所定の条件を満たさないと判定された場合には偽である旨の情報が最終判定部4に送信される。所定の条件とは、ブラインド署名の検証アルゴリズムの関数をVとし、検証アルゴリズムの関数Vにおいて、メッセージmの代わりに、メッセージに由来する値のハッシュ値が入力として用いられているかどうかという条件である。より、厳密には、任意のビット列σmvkについて、VV’vkの関係を満たす関数V’、ハッシュ関数H及び関数fが存在するという条件である。σ及びvkを所与とすることによりVをメッセージmの関数Vとしてみれば、この所定の条件は、VV’の関係を満たす関数V’、ハッシュ関数H及び関数fが存在するという条件と同じである。以下、条件判定部3による所定の条件を満たすかどうかの判定処理の概要を簡単に説明する。所定の条件を満たすブラインド署名についての情報を第二記憶部6予め記憶しておく。ブラインド署名についての情報とは、例えばブラインド署名の識別子である。条件判定部3は、第二記憶部6を参照して所定の条件を満たすか判定する。例えば、判定の対象となるプロトコルが用いるブラインド署名の識別子をキーとして第二記憶部6を参照して、一致する識別子があればそのブラインド署名は所定の条件を満たすと判定することができ、一致する識別子がなければそのブラインド署名は所定の条件を満たさないと判定することができる。ブラインド署名が、1ワンモア偽造不可能性を満たし、かつ、2上記所定の条件を満たす場合には、このブラインド署名は、一対一偽造不可能性を満たすことを発明者は見出した。その証明は、ここでは省略する。上記1及び2の条件を満たす場合には、そのブラインド署名は一対一偽造不可能性を満たすため、非特許文献3に記載された既存のプロトコル安全性検証手法を用いることができる。この発明は、この原理を用いて、ワンモア偽造不可能性を満たすブラインド署名を用いたプロトコルの安全性を検証する。最終判定部4は、安全性判定部1においてプロトコルは安全であると判定され、ワンモア偽造不可能性判定部2においてブラインド署名はワンモア偽造不可能性を満たすと判定され、条件判定部3において上記所定の条件を満たすと判定された場合に、プロトコルは安全であると判定するステップS4。この実施形態では、最終判定部4は、安全性判定部1、ワンモア偽造不可能性判定部2及び条件判定部3のそれぞれから真である旨の情報を取得した場合には、プロトコルは安全であると判定する。安全性判定部1、ワンモア偽造不可能性判定部2及び条件判定部3の少なくともひとつから偽である旨の情報を取得した場合には、プロトコルは安全でないと判定する。このように、上記所定の条件を満たすかどうかを判定することにより、ワンモア偽造不可能性を満たすブラインド署名を用いたプロトコルの安全性を検証し得る。[変形例等]安全性の判定の対象となるプロトコルが、ワンモア偽造不可能性を有することがわかっている場合には、ワンモア偽造不可能性判定部2の処理を省くことができる。言い換えれば、プロトコル安全性検証装置は、ワンモア偽造不可能性判定部2を備えていなくてもよい。プロトコル安全性検証装置の各部間のデータのやり取りは直接行われてもよいし、図示していない記憶部を介して行われてもよい。その他、この発明は上述の実施形態に限定されるものではない。例えば、上述の各種の処理は、記載に従って時系列に実行されるのみならず、処理を実行する装置の処理能力あるいは必要に応じて並列的にあるいは個別に実行されてもよい。また、上述の構成をコンピュータによって実現する場合、各装置が有すべき各部の処理内容はプログラムによって記述される。そして、このプログラムをコンピュータで実行することにより、各部がコンピュータ上で実現される。この処理内容を記述したプログラムは、コンピュータで読み取り可能な記録媒体に記録しておくことができる。コンピュータで読み取り可能な記録媒体としては、例えば、磁気記録装置、光ディスク、光磁気記録媒体、半導体メモリ等どのようなものでもよい。その他、この発明の趣旨を逸脱しない範囲で適宜変更が可能であることはいうまでもない。"