プロトコル安全性検証装置、方法及びプログラム
【課題】ワンモア偽造不可能性を満たすブラインド署名を用いたプロトコルの安全性を検証し得るプロトコルの安全性の検証技術を提供する。
【解決手段】ブラインド署名が一対一偽造不可能性を満たすとした場合に、プロトコルが安全か判定する安全性判定部１と、ブラインド署名がワンモア偽造不可能性を満たすか判定するワンモア偽造不可能性判定部２と、ブラインド署名が所定の条件を満たすか判定する条件判定部３と、安全性判定部１においてプロトコルは安全であると判定され、ワンモア偽造不可能性判定部２においてブラインド署名はワンモア偽造不可能性を満たすと判定され、条件判定部３において条件を満たすと判定された場合に、プロトコルは安全であると判定する最終判定部４と、を含む。
【解決手段】ブラインド署名が一対一偽造不可能性を満たすとした場合に、プロトコルが安全か判定する安全性判定部１と、ブラインド署名がワンモア偽造不可能性を満たすか判定するワンモア偽造不可能性判定部２と、ブラインド署名が所定の条件を満たすか判定する条件判定部３と、安全性判定部１においてプロトコルは安全であると判定され、ワンモア偽造不可能性判定部２においてブラインド署名はワンモア偽造不可能性を満たすと判定され、条件判定部３において条件を満たすと判定された場合に、プロトコルは安全であると判定する最終判定部４と、を含む。
【発明の詳細な説明】
【技術分野】
【０００１】
この発明は、情報セキュリティ技術に関する。特に、ブラインド署名を用いた通信方式（プロトコル）の安全性を自動的に検証する技術に関する。
【背景技術】
【０００２】
電子現金や電子投票など、利用者の匿名性が要求される通信においては、例えば特許文献１に記載されているブラインド署名と呼ばれる署名方式が用いられることがある。ブラインド署名は、次の５個のアルゴリズムから構成される。
【０００３】
（１）鍵生成アルゴリズムG
（２）ブラインドアルゴリズムB
（３）署名アルゴリズムS
（４）アンブラインドアルゴリズムU
（５）検証アルゴリズムV
ブラインド署名方式は次のように用いられる。
【０００４】
まず、鍵生成アルゴリズムによって署名鍵skおよび検証鍵vkを生成し、vkをネットワー上に公開し、skは特定の参加者である署名者のみに与える。
【０００５】
ネットワーク上の参加者は、任意に選んだメッセージmについての、署名鍵skで署名された署名σを得るために、乱数rを生成し、ブラインド化アルゴリズムBを用いてB(m,r,vk)を計算し、その計算結果βを署名者に送信する。
【０００６】
署名者は、署名アルゴリズムSを用いてS(β,sk)を計算し、その計算結果σを参加者に送り返す。
【０００７】
参加者は、アンブラインドアルゴリズムUを用いてU(m,σ,r,vk)を計算し、その結果σ'をmとともに第三者である検証者に送信する。
【０００８】
検証者は、検証アルゴリズムVを用いてV(σ',m,vk)を計算し、その計算結果が１である場合に、σ'がmについての正しい署名であると認める。
【０００９】
このとき、検証者に与えられるσ'が上記の手順に従って生成されたものである場合には、検証アルゴリズムは必ず１を出力する。また、検証アルゴリズムが１を出力しない場合は、σ'は上記の手順に依らず不正に生成されたと判断される。
【００１０】
上記の手順によらないにもかかわらず検証アルゴリズムが１を出力することが起こらない場合、このブラインド署名は「偽造不能性」を持つという。また、署名者がβを解析しても、mについての情報を得られないとき、このブラインド署名は「ブラインド性」を持つという。
【００１１】
ブラインド署名を投票プロトコルに用いる場合、たとえば選挙管理委員会のような組織が署名者となって投票に署名し、投票の参加者は自らの投票についての署名を得ることで投票の正しさを検証者に証明することができる。このとき、偽造不能性により、投票の水増しなどが防止されていることを保障でき、ブラインド性によって、投票内容を選挙管理員会に秘密にしたまま署名を得ることができるという匿名性に相当する性質が保障できると期待される。
【００１２】
ブラインド署名の偽造不能性は、より厳密には通常次のような性質として定式化される。すなわち、検証アルゴリズムVが１を出力するようなmとσ'の組の個数は、署名者が署名アルゴリズムを実行した回数以下である。この性質は「ワンモア偽造不能性」とよばれる。以上のような性質を満たすブラインド署名が、非特許文献１に記載されている。
【００１３】
ブラインド署名を用いる、例えば投票プロトコルのようなプロトコルの安全性を検査する場合、ブラインド署名の偽造不能性およびブラインド性を仮定して、プロトコルの安全性を検査する。一般にこのような安全性検査は、専門家の人手で行われるが、検査に多大な労力と時間が必要となり、また検査の進め方に誤りがある可能性もある。
【００１４】
このため、プロトコルの自動検査方式が提案されている（例えば、非特許文献２参照。）。ブラインド署名を用いるプロトコルの安全性を検査する方法も提案されている。
【００１５】
しかしながら、既存の自動検査方法を用いて、ブラインド署名を用いるプロトコルを扱うために、ワンモア偽造不能性よりも強い性質を仮定して検査を行う場合がある（非特許文献３）。これは、ワンモア偽造不能性は、既存の自動検査方法の枠組みに適用することが困難であるためである。非特許文献３の方法では、ワンモア偽造不能性よりも強い性質として、一対一偽造不能性を仮定している。
【００１６】
一対一偽造不可能性は、検証アルゴリズムVが１を出力するようなmとσ'の組の集合から、署名アルゴリズムSへの入力βの集合への一対一対応が存在し、次の（１）及び（２）の性質を満たすものをいう。
【００１７】
（１）参加者が(m,σ')に対応するβを送信する時点で、この参加者はmを知っている。
（２）参加者はV(m,σ')=1となるσ'を送信するより前に、署名アルゴリズムSの出力S(β,sk)を受信している。
【先行技術文献】
【特許文献】
【００１８】
【特許文献１】米国特許第４７５９０６３号明細書
【非特許文献】
【００１９】
【非特許文献１】M. Bellare and C. Namprempre, "The One-More-RSA-Inversion Problem and the Security of Chaum's Blind Signature Scheme," Journal of Cryptology (2003) 16:p.185-215.
【非特許文献２】Bruno Blanchet, "Automatic Verification of Correspondences for Security Protocols," Journal of Computer Security, 17(4):p.363-434, July 2009.
【非特許文献３】Steve Kremer and Mark D. Ryan, "Analysis of an Electronic Voting Protocol in the Applied Pi-Calculus," In M. Sagiv (ed.), ESOP'05, LNCS 3444, p.186-200. Springer, 2005.
【発明の概要】
【発明が解決しようとする課題】
【００２０】
このように、非特許文献３に記載されたプロトコルの安全性検証方法では、そのプロトコルが用いるブラインド署名が一対一偽造不可能性を有する必要がある。
【００２１】
しかしながら、あるブラインド署名が一対一偽造不能性を満たす場合にはそのブラインド署名はワンモア偽造不能性を満たすが、あるブラインド署名がワンモア偽造不能性を満たす場合にはそのブラインド署名は一対一偽造不能性を満たすとは限らない。すなわち、ワンモア偽造不可能性を満たすブラインド署名が、一対一偽造不可能性を満たすとは限らない。
【００２２】
このため、非特許文献３に記載されたプロトコルの安全性検証方法では、ワンモア偽造不可能性を満たすブラインド署名を用いたプロトコルの安全性を検証することはできない。
【００２３】
この発明の課題は、ワンモア偽造不可能性を満たすブラインド署名を用いたプロトコルの安全性を検証し得るプロトコル安全性検証装置、方法、プログラムを提供することである。
【課題を解決するための手段】
【００２４】
この発明の一態様によるプロトコル安全性検証装置は、ブラインド署名を用いるプロトコルの安全性を検証するプロトコル安全性検証装置であって、ブラインド署名が一対一偽造不可能性を満たすとした場合に、プロトコルが安全か判定する安全性判定部と、ブラインド署名がワンモア偽造不可能性を満たすか判定するワンモア偽造不可能性判定部と、ブラインド署名の検証アルゴリズムの関数をV(m)として、V(m)=V’(H(f(m)))の関係を満たす関数V’、ハッシュ関数H及び関数fが存在するという条件を満たすか判定する条件判定部と、安全性判定部においてプロトコルは安全であると判定され、ワンモア偽造不可能性判定部においてブラインド署名はワンモア偽造不可能性を満たすと判定され、条件判定部において条件を満たすと判定された場合に、プロトコルは安全であると判定する最終判定部と、を含む。
【発明の効果】
【００２５】
ワンモア偽造不可能性を満たすブラインド署名を用いたプロトコルの安全性を検証し得る。
【図面の簡単な説明】
【００２６】
【図１】実施形態のプロトコル安全性検証装置の構成を説明するためのブロック図。
【図２】実施形態のプロトコル安全性検証装置を説明するためのフローチャート。
【発明を実施するための形態】
【００２７】
以下、図面を参照してこの発明の一実施形態を説明する。
【００２８】
プロトコル安全性検証装置及び方法の一実施形態を以下に示す。
【００２９】
プロトコル安全性検証装置は、図１に示すように、安全性判定部１、ワンモア偽造不可能性判定部２、条件判定部３、最終判定部４、第一記憶部５、第二記憶部６を例えば含む。プロトコル安全性検証装置は、図２に例示されたプロトコル安全性検証方法の各ステップの処理を行う。
【００３０】
プロトコル仕様情報及びプロトコル安全性仕様情報が、安全性判定部１に入力される。プロトコル仕様情報は、プロトコルの仕様に関する情報であり、局所状態の有限集合Ｓ及び局所遷移規則の集合Ｒの組（Ｓ，Ｒ）から例えば構成される。プロトコル安全性仕様情報は、プロトコルの安全性の仕様に関する情報であり、大域状態ｓ０及び論理式Ｐから例えば構成される。
【００３１】
安全性判定部１は、入力されたプロトコル仕様情報及びプロトコル安全性仕様情報に基づいて、そのプロトコルが用いるブラインド署名が一対一偽造不可能性を満たすとした場合に、そのプロトコルが安全か判定する（ステップＳ１）。一対一偽造不可能性の定義については、背景技術の欄を参照こと。プロトコルの安全性についての情報は、最終判定部４に送信される。この実施形態では、プロトコルが安全であると判定された場合には真である旨の情報が最終判定部４に送信され、プロトコルが安全ではないと判定された場合には偽である旨の情報が最終判定部４に送信される。
【００３２】
安全性判定部１は、例えば非特許文献３に記載された手法を用いて安全性の判定を行う。以下、安全性判定部１による安全性の判定処理の概要を簡単に説明する。
【００３３】
まず、安全性判定部１は、所定の初期状態から所定の遷移規則に基づいて遷移可能な状態を全て抽出する。所定の初期状態及び所定の遷移規則は、プロトコル仕様情報及びプロトコル安全性仕様情報により定められる。
【００３４】
つぎに、安全性判定部１は、抽出された遷移可能な全ての状態のそれぞれにおいて、論理式Ｐを満たすかどうかを判断する。遷移可能な全ての状態のそれぞれにおいて所定の安全性を定義する論理式Ｐが満たされている場合には、そのプロトコルは安全であると判断することができる。一方、遷移可能な状態の中で論理式Ｐを満たさないものがある場合には、そのプロトコルは安全ではないと判断する。
【００３５】
論理式Ｐは、所定の安全性を定義するものであり、安全性判定部１に入力されるプロトコル安全性仕様情報により定められる。
【００３６】
このように、安全性判定部により判断された安全性は、論旨式Ｐで定義された安全性を満たすという意味での安全性を意味する。
【００３７】
ワンモア偽造不可能性判定部２は、プロトコルが用いるブラインド署名がワンモア偽造不可能性を満たすか判定する（ステップＳ２）。ワンモア偽造不可能性を満たすかどうかについての情報は、最終判定部４に送信される。この実施形態では、ワンモア偽造不可能性を満たす場合には真である旨の情報が最終判定部４に送信され、ワンモア偽造不可能性を満たさない場合には偽である旨の情報が最終判定部４に送信される。
【００３８】
以下、ワンモア偽造不可能性判定部２による安全性の判定処理の概要を簡単に説明する。ワンモア偽造不可能性を満たすブラインド署名についての情報を第一記憶部５に予め記憶しておく。ブラインド署名についての情報とは、例えばブラインド署名の識別子である。
【００３９】
ワンモア偽造不可能性判定部２は、第一記憶部５を参照してブラインド署名がワンモア偽造不可能性を満たすか判定する。例えば、判定の対象となるプロトコルが用いるブラインド署名の識別子をキーとして第一記憶部５を参照して、一致する識別子があればそのブラインド署名はワンモア偽造不可能性を満たすと判定することができ、一致する識別子がなければそのブラインド署名はワンモア偽造不可能性を満たさないと判定することができる。
【００４０】
条件判定部３は、安全性の評価の対象となるプロトコルのブランド署名が、所定の条件を満たすか判定する（ステップＳ３）。所定の条件を満たすかどうかについての情報は、最終判定部４に送信される。この実施形態では、所定の条件を満たすと判定された場合には真である旨の情報が最終判定部４に送信され、所定の条件を満たさないと判定された場合には偽である旨の情報が最終判定部４に送信される。
【００４１】
所定の条件とは、ブラインド署名の検証アルゴリズムの関数をVとし、検証アルゴリズムの関数Vにおいて、メッセージmの代わりに、メッセージに由来する値のハッシュ値が入力として用いられているかどうかという条件である。より、厳密には、任意のビット列σ' ,m,vkについて、V(σ',m,vk)=V’(σ',H(f(m,vk)),vk)の関係を満たす関数V’、ハッシュ関数H及び関数fが存在するという条件である。
【００４２】
σ及びvkを所与とすることによりV(σ',m,vk)をメッセージmの関数V(m)としてみれば、この所定の条件は、V(m)=V’(H(f(m)))の関係を満たす関数V’、ハッシュ関数H及び関数fが存在するという条件と同じである。
【００４３】
以下、条件判定部３による所定の条件を満たすかどうかの判定処理の概要を簡単に説明する。所定の条件を満たすブラインド署名についての情報を第二記憶部６予め記憶しておく。ブラインド署名についての情報とは、例えばブラインド署名の識別子である。
【００４４】
条件判定部３は、第二記憶部６を参照して所定の条件を満たすか判定する。例えば、判定の対象となるプロトコルが用いるブラインド署名の識別子をキーとして第二記憶部６を参照して、一致する識別子があればそのブラインド署名は所定の条件を満たすと判定することができ、一致する識別子がなければそのブラインド署名は所定の条件を満たさないと判定することができる。
【００４５】
ブラインド署名が、（１）ワンモア偽造不可能性を満たし、かつ、（２）上記所定の条件を満たす場合には、このブラインド署名は、一対一偽造不可能性を満たすことを発明者は見出した。その証明は、ここでは省略する。
【００４６】
上記（１）及び（２）の条件を満たす場合には、そのブラインド署名は一対一偽造不可能性を満たすため、非特許文献３に記載された既存のプロトコル安全性検証手法を用いることができる。この発明は、この原理を用いて、ワンモア偽造不可能性を満たすブラインド署名を用いたプロトコルの安全性を検証する。
【００４７】
最終判定部４は、安全性判定部１においてプロトコルは安全であると判定され、ワンモア偽造不可能性判定部２においてブラインド署名はワンモア偽造不可能性を満たすと判定され、条件判定部３において上記所定の条件を満たすと判定された場合に、プロトコルは安全であると判定する（ステップＳ４）。この実施形態では、最終判定部４は、安全性判定部１、ワンモア偽造不可能性判定部２及び条件判定部３のそれぞれから真である旨の情報を取得した場合には、プロトコルは安全であると判定する。安全性判定部１、ワンモア偽造不可能性判定部２及び条件判定部３の少なくともひとつから偽である旨の情報を取得した場合には、プロトコルは安全でないと判定する。
【００４８】
このように、上記所定の条件を満たすかどうかを判定することにより、ワンモア偽造不可能性を満たすブラインド署名を用いたプロトコルの安全性を検証し得る。
【００４９】
［変形例等］
安全性の判定の対象となるプロトコルが、ワンモア偽造不可能性を有することがわかっている場合には、ワンモア偽造不可能性判定部２の処理を省くことができる。言い換えれば、プロトコル安全性検証装置は、ワンモア偽造不可能性判定部２を備えていなくてもよい。
【００５０】
プロトコル安全性検証装置の各部間のデータのやり取りは直接行われてもよいし、図示していない記憶部を介して行われてもよい。
【００５１】
その他、この発明は上述の実施形態に限定されるものではない。例えば、上述の各種の処理は、記載に従って時系列に実行されるのみならず、処理を実行する装置の処理能力あるいは必要に応じて並列的にあるいは個別に実行されてもよい。
【００５２】
また、上述の構成をコンピュータによって実現する場合、各装置が有すべき各部の処理内容はプログラムによって記述される。そして、このプログラムをコンピュータで実行することにより、各部がコンピュータ上で実現される。
【００５３】
この処理内容を記述したプログラムは、コンピュータで読み取り可能な記録媒体に記録しておくことができる。コンピュータで読み取り可能な記録媒体としては、例えば、磁気記録装置、光ディスク、光磁気記録媒体、半導体メモリ等どのようなものでもよい。
【００５４】
その他、この発明の趣旨を逸脱しない範囲で適宜変更が可能であることはいうまでもない。
【符号の説明】
【００５５】
１ 安全性判定部
２ ワンモア偽造不可能性判定部
３ 条件判定部
４ 最終判定部
５ 第一記憶部
６ 第二記憶部
【技術分野】
【０００１】
この発明は、情報セキュリティ技術に関する。特に、ブラインド署名を用いた通信方式（プロトコル）の安全性を自動的に検証する技術に関する。
【背景技術】
【０００２】
電子現金や電子投票など、利用者の匿名性が要求される通信においては、例えば特許文献１に記載されているブラインド署名と呼ばれる署名方式が用いられることがある。ブラインド署名は、次の５個のアルゴリズムから構成される。
【０００３】
（１）鍵生成アルゴリズムG
（２）ブラインドアルゴリズムB
（３）署名アルゴリズムS
（４）アンブラインドアルゴリズムU
（５）検証アルゴリズムV
ブラインド署名方式は次のように用いられる。
【０００４】
まず、鍵生成アルゴリズムによって署名鍵skおよび検証鍵vkを生成し、vkをネットワー上に公開し、skは特定の参加者である署名者のみに与える。
【０００５】
ネットワーク上の参加者は、任意に選んだメッセージmについての、署名鍵skで署名された署名σを得るために、乱数rを生成し、ブラインド化アルゴリズムBを用いてB(m,r,vk)を計算し、その計算結果βを署名者に送信する。
【０００６】
署名者は、署名アルゴリズムSを用いてS(β,sk)を計算し、その計算結果σを参加者に送り返す。
【０００７】
参加者は、アンブラインドアルゴリズムUを用いてU(m,σ,r,vk)を計算し、その結果σ'をmとともに第三者である検証者に送信する。
【０００８】
検証者は、検証アルゴリズムVを用いてV(σ',m,vk)を計算し、その計算結果が１である場合に、σ'がmについての正しい署名であると認める。
【０００９】
このとき、検証者に与えられるσ'が上記の手順に従って生成されたものである場合には、検証アルゴリズムは必ず１を出力する。また、検証アルゴリズムが１を出力しない場合は、σ'は上記の手順に依らず不正に生成されたと判断される。
【００１０】
上記の手順によらないにもかかわらず検証アルゴリズムが１を出力することが起こらない場合、このブラインド署名は「偽造不能性」を持つという。また、署名者がβを解析しても、mについての情報を得られないとき、このブラインド署名は「ブラインド性」を持つという。
【００１１】
ブラインド署名を投票プロトコルに用いる場合、たとえば選挙管理委員会のような組織が署名者となって投票に署名し、投票の参加者は自らの投票についての署名を得ることで投票の正しさを検証者に証明することができる。このとき、偽造不能性により、投票の水増しなどが防止されていることを保障でき、ブラインド性によって、投票内容を選挙管理員会に秘密にしたまま署名を得ることができるという匿名性に相当する性質が保障できると期待される。
【００１２】
ブラインド署名の偽造不能性は、より厳密には通常次のような性質として定式化される。すなわち、検証アルゴリズムVが１を出力するようなmとσ'の組の個数は、署名者が署名アルゴリズムを実行した回数以下である。この性質は「ワンモア偽造不能性」とよばれる。以上のような性質を満たすブラインド署名が、非特許文献１に記載されている。
【００１３】
ブラインド署名を用いる、例えば投票プロトコルのようなプロトコルの安全性を検査する場合、ブラインド署名の偽造不能性およびブラインド性を仮定して、プロトコルの安全性を検査する。一般にこのような安全性検査は、専門家の人手で行われるが、検査に多大な労力と時間が必要となり、また検査の進め方に誤りがある可能性もある。
【００１４】
このため、プロトコルの自動検査方式が提案されている（例えば、非特許文献２参照。）。ブラインド署名を用いるプロトコルの安全性を検査する方法も提案されている。
【００１５】
しかしながら、既存の自動検査方法を用いて、ブラインド署名を用いるプロトコルを扱うために、ワンモア偽造不能性よりも強い性質を仮定して検査を行う場合がある（非特許文献３）。これは、ワンモア偽造不能性は、既存の自動検査方法の枠組みに適用することが困難であるためである。非特許文献３の方法では、ワンモア偽造不能性よりも強い性質として、一対一偽造不能性を仮定している。
【００１６】
一対一偽造不可能性は、検証アルゴリズムVが１を出力するようなmとσ'の組の集合から、署名アルゴリズムSへの入力βの集合への一対一対応が存在し、次の（１）及び（２）の性質を満たすものをいう。
【００１７】
（１）参加者が(m,σ')に対応するβを送信する時点で、この参加者はmを知っている。
（２）参加者はV(m,σ')=1となるσ'を送信するより前に、署名アルゴリズムSの出力S(β,sk)を受信している。
【先行技術文献】
【特許文献】
【００１８】
【特許文献１】米国特許第４７５９０６３号明細書
【非特許文献】
【００１９】
【非特許文献１】M. Bellare and C. Namprempre, "The One-More-RSA-Inversion Problem and the Security of Chaum's Blind Signature Scheme," Journal of Cryptology (2003) 16:p.185-215.
【非特許文献２】Bruno Blanchet, "Automatic Verification of Correspondences for Security Protocols," Journal of Computer Security, 17(4):p.363-434, July 2009.
【非特許文献３】Steve Kremer and Mark D. Ryan, "Analysis of an Electronic Voting Protocol in the Applied Pi-Calculus," In M. Sagiv (ed.), ESOP'05, LNCS 3444, p.186-200. Springer, 2005.
【発明の概要】
【発明が解決しようとする課題】
【００２０】
このように、非特許文献３に記載されたプロトコルの安全性検証方法では、そのプロトコルが用いるブラインド署名が一対一偽造不可能性を有する必要がある。
【００２１】
しかしながら、あるブラインド署名が一対一偽造不能性を満たす場合にはそのブラインド署名はワンモア偽造不能性を満たすが、あるブラインド署名がワンモア偽造不能性を満たす場合にはそのブラインド署名は一対一偽造不能性を満たすとは限らない。すなわち、ワンモア偽造不可能性を満たすブラインド署名が、一対一偽造不可能性を満たすとは限らない。
【００２２】
このため、非特許文献３に記載されたプロトコルの安全性検証方法では、ワンモア偽造不可能性を満たすブラインド署名を用いたプロトコルの安全性を検証することはできない。
【００２３】
この発明の課題は、ワンモア偽造不可能性を満たすブラインド署名を用いたプロトコルの安全性を検証し得るプロトコル安全性検証装置、方法、プログラムを提供することである。
【課題を解決するための手段】
【００２４】
この発明の一態様によるプロトコル安全性検証装置は、ブラインド署名を用いるプロトコルの安全性を検証するプロトコル安全性検証装置であって、ブラインド署名が一対一偽造不可能性を満たすとした場合に、プロトコルが安全か判定する安全性判定部と、ブラインド署名がワンモア偽造不可能性を満たすか判定するワンモア偽造不可能性判定部と、ブラインド署名の検証アルゴリズムの関数をV(m)として、V(m)=V’(H(f(m)))の関係を満たす関数V’、ハッシュ関数H及び関数fが存在するという条件を満たすか判定する条件判定部と、安全性判定部においてプロトコルは安全であると判定され、ワンモア偽造不可能性判定部においてブラインド署名はワンモア偽造不可能性を満たすと判定され、条件判定部において条件を満たすと判定された場合に、プロトコルは安全であると判定する最終判定部と、を含む。
【発明の効果】
【００２５】
ワンモア偽造不可能性を満たすブラインド署名を用いたプロトコルの安全性を検証し得る。
【図面の簡単な説明】
【００２６】
【図１】実施形態のプロトコル安全性検証装置の構成を説明するためのブロック図。
【図２】実施形態のプロトコル安全性検証装置を説明するためのフローチャート。
【発明を実施するための形態】
【００２７】
以下、図面を参照してこの発明の一実施形態を説明する。
【００２８】
プロトコル安全性検証装置及び方法の一実施形態を以下に示す。
【００２９】
プロトコル安全性検証装置は、図１に示すように、安全性判定部１、ワンモア偽造不可能性判定部２、条件判定部３、最終判定部４、第一記憶部５、第二記憶部６を例えば含む。プロトコル安全性検証装置は、図２に例示されたプロトコル安全性検証方法の各ステップの処理を行う。
【００３０】
プロトコル仕様情報及びプロトコル安全性仕様情報が、安全性判定部１に入力される。プロトコル仕様情報は、プロトコルの仕様に関する情報であり、局所状態の有限集合Ｓ及び局所遷移規則の集合Ｒの組（Ｓ，Ｒ）から例えば構成される。プロトコル安全性仕様情報は、プロトコルの安全性の仕様に関する情報であり、大域状態ｓ０及び論理式Ｐから例えば構成される。
【００３１】
安全性判定部１は、入力されたプロトコル仕様情報及びプロトコル安全性仕様情報に基づいて、そのプロトコルが用いるブラインド署名が一対一偽造不可能性を満たすとした場合に、そのプロトコルが安全か判定する（ステップＳ１）。一対一偽造不可能性の定義については、背景技術の欄を参照こと。プロトコルの安全性についての情報は、最終判定部４に送信される。この実施形態では、プロトコルが安全であると判定された場合には真である旨の情報が最終判定部４に送信され、プロトコルが安全ではないと判定された場合には偽である旨の情報が最終判定部４に送信される。
【００３２】
安全性判定部１は、例えば非特許文献３に記載された手法を用いて安全性の判定を行う。以下、安全性判定部１による安全性の判定処理の概要を簡単に説明する。
【００３３】
まず、安全性判定部１は、所定の初期状態から所定の遷移規則に基づいて遷移可能な状態を全て抽出する。所定の初期状態及び所定の遷移規則は、プロトコル仕様情報及びプロトコル安全性仕様情報により定められる。
【００３４】
つぎに、安全性判定部１は、抽出された遷移可能な全ての状態のそれぞれにおいて、論理式Ｐを満たすかどうかを判断する。遷移可能な全ての状態のそれぞれにおいて所定の安全性を定義する論理式Ｐが満たされている場合には、そのプロトコルは安全であると判断することができる。一方、遷移可能な状態の中で論理式Ｐを満たさないものがある場合には、そのプロトコルは安全ではないと判断する。
【００３５】
論理式Ｐは、所定の安全性を定義するものであり、安全性判定部１に入力されるプロトコル安全性仕様情報により定められる。
【００３６】
このように、安全性判定部により判断された安全性は、論旨式Ｐで定義された安全性を満たすという意味での安全性を意味する。
【００３７】
ワンモア偽造不可能性判定部２は、プロトコルが用いるブラインド署名がワンモア偽造不可能性を満たすか判定する（ステップＳ２）。ワンモア偽造不可能性を満たすかどうかについての情報は、最終判定部４に送信される。この実施形態では、ワンモア偽造不可能性を満たす場合には真である旨の情報が最終判定部４に送信され、ワンモア偽造不可能性を満たさない場合には偽である旨の情報が最終判定部４に送信される。
【００３８】
以下、ワンモア偽造不可能性判定部２による安全性の判定処理の概要を簡単に説明する。ワンモア偽造不可能性を満たすブラインド署名についての情報を第一記憶部５に予め記憶しておく。ブラインド署名についての情報とは、例えばブラインド署名の識別子である。
【００３９】
ワンモア偽造不可能性判定部２は、第一記憶部５を参照してブラインド署名がワンモア偽造不可能性を満たすか判定する。例えば、判定の対象となるプロトコルが用いるブラインド署名の識別子をキーとして第一記憶部５を参照して、一致する識別子があればそのブラインド署名はワンモア偽造不可能性を満たすと判定することができ、一致する識別子がなければそのブラインド署名はワンモア偽造不可能性を満たさないと判定することができる。
【００４０】
条件判定部３は、安全性の評価の対象となるプロトコルのブランド署名が、所定の条件を満たすか判定する（ステップＳ３）。所定の条件を満たすかどうかについての情報は、最終判定部４に送信される。この実施形態では、所定の条件を満たすと判定された場合には真である旨の情報が最終判定部４に送信され、所定の条件を満たさないと判定された場合には偽である旨の情報が最終判定部４に送信される。
【００４１】
所定の条件とは、ブラインド署名の検証アルゴリズムの関数をVとし、検証アルゴリズムの関数Vにおいて、メッセージmの代わりに、メッセージに由来する値のハッシュ値が入力として用いられているかどうかという条件である。より、厳密には、任意のビット列σ' ,m,vkについて、V(σ',m,vk)=V’(σ',H(f(m,vk)),vk)の関係を満たす関数V’、ハッシュ関数H及び関数fが存在するという条件である。
【００４２】
σ及びvkを所与とすることによりV(σ',m,vk)をメッセージmの関数V(m)としてみれば、この所定の条件は、V(m)=V’(H(f(m)))の関係を満たす関数V’、ハッシュ関数H及び関数fが存在するという条件と同じである。
【００４３】
以下、条件判定部３による所定の条件を満たすかどうかの判定処理の概要を簡単に説明する。所定の条件を満たすブラインド署名についての情報を第二記憶部６予め記憶しておく。ブラインド署名についての情報とは、例えばブラインド署名の識別子である。
【００４４】
条件判定部３は、第二記憶部６を参照して所定の条件を満たすか判定する。例えば、判定の対象となるプロトコルが用いるブラインド署名の識別子をキーとして第二記憶部６を参照して、一致する識別子があればそのブラインド署名は所定の条件を満たすと判定することができ、一致する識別子がなければそのブラインド署名は所定の条件を満たさないと判定することができる。
【００４５】
ブラインド署名が、（１）ワンモア偽造不可能性を満たし、かつ、（２）上記所定の条件を満たす場合には、このブラインド署名は、一対一偽造不可能性を満たすことを発明者は見出した。その証明は、ここでは省略する。
【００４６】
上記（１）及び（２）の条件を満たす場合には、そのブラインド署名は一対一偽造不可能性を満たすため、非特許文献３に記載された既存のプロトコル安全性検証手法を用いることができる。この発明は、この原理を用いて、ワンモア偽造不可能性を満たすブラインド署名を用いたプロトコルの安全性を検証する。
【００４７】
最終判定部４は、安全性判定部１においてプロトコルは安全であると判定され、ワンモア偽造不可能性判定部２においてブラインド署名はワンモア偽造不可能性を満たすと判定され、条件判定部３において上記所定の条件を満たすと判定された場合に、プロトコルは安全であると判定する（ステップＳ４）。この実施形態では、最終判定部４は、安全性判定部１、ワンモア偽造不可能性判定部２及び条件判定部３のそれぞれから真である旨の情報を取得した場合には、プロトコルは安全であると判定する。安全性判定部１、ワンモア偽造不可能性判定部２及び条件判定部３の少なくともひとつから偽である旨の情報を取得した場合には、プロトコルは安全でないと判定する。
【００４８】
このように、上記所定の条件を満たすかどうかを判定することにより、ワンモア偽造不可能性を満たすブラインド署名を用いたプロトコルの安全性を検証し得る。
【００４９】
［変形例等］
安全性の判定の対象となるプロトコルが、ワンモア偽造不可能性を有することがわかっている場合には、ワンモア偽造不可能性判定部２の処理を省くことができる。言い換えれば、プロトコル安全性検証装置は、ワンモア偽造不可能性判定部２を備えていなくてもよい。
【００５０】
プロトコル安全性検証装置の各部間のデータのやり取りは直接行われてもよいし、図示していない記憶部を介して行われてもよい。
【００５１】
その他、この発明は上述の実施形態に限定されるものではない。例えば、上述の各種の処理は、記載に従って時系列に実行されるのみならず、処理を実行する装置の処理能力あるいは必要に応じて並列的にあるいは個別に実行されてもよい。
【００５２】
また、上述の構成をコンピュータによって実現する場合、各装置が有すべき各部の処理内容はプログラムによって記述される。そして、このプログラムをコンピュータで実行することにより、各部がコンピュータ上で実現される。
【００５３】
この処理内容を記述したプログラムは、コンピュータで読み取り可能な記録媒体に記録しておくことができる。コンピュータで読み取り可能な記録媒体としては、例えば、磁気記録装置、光ディスク、光磁気記録媒体、半導体メモリ等どのようなものでもよい。
【００５４】
その他、この発明の趣旨を逸脱しない範囲で適宜変更が可能であることはいうまでもない。
【符号の説明】
【００５５】
１ 安全性判定部
２ ワンモア偽造不可能性判定部
３ 条件判定部
４ 最終判定部
５ 第一記憶部
６ 第二記憶部
【特許請求の範囲】
【請求項１】
ブラインド署名を用いるプロトコルの安全性を検証するプロトコル安全性検証装置であって、
上記ブラインド署名が一対一偽造不可能性を満たすとした場合に、上記プロトコルが安全か判定する安全性判定部と、
上記ブラインド署名がワンモア偽造不可能性を満たすか判定するワンモア偽造不可能性判定部と、
上記ブラインド署名による署名の対象となるメッセージをmとし、上記ブラインド署名の検証アルゴリズムの関数をV(m)として、V(m)=V’(H(f(m)))の関係を満たす関数V’、ハッシュ関数H及び関数fが存在するという条件を満たすか判定する条件判定部と、
上記安全性判定部において上記プロトコルは安全であると判定され、上記ワンモア偽造不可能性判定部において上記ブラインド署名はワンモア偽造不可能性を満たすと判定され、上記条件判定部において上記条件を満たすと判定された場合に、上記プロトコルは安全であると判定する最終判定部と、
を含むプロトコル安全性検証装置。
【請求項２】
請求項１のプロトコル安全性検証装置において、
ワンモア偽造不可能性を満たすブラインド署名についての情報を記憶する第一記憶部を更に含み、
上記ワンモア偽造不可能性判定部は、上記第一記憶部を参照して上記ブランド署名がワンモア偽造不可能性を満たすか判定する、
プロトコル安全性検証装置。
【請求項３】
請求項１又は２のプロトコル安全性検証装置において、
上記条件を満たすブラインド署名についての情報を記憶する第二記憶部を更に含み、
上記条件判定部は、上記第二記憶部を参照して上記ブラインド署名が上記条件を満たすか判定する、
プロトコル安全性検証装置。
【請求項４】
ブラインド署名を用いるプロトコルの安全性を検証するプロトコル安全性検証方法であって、
安全性判定部が、上記ブラインド署名が一対一偽造不可能性を満たすとした場合に、上記プロトコルが安全か判定する安全性判定ステップと、
ワンモア偽造不可能性判定部が、上記ブラインド署名がワンモア偽造不可能性を満たすか判定するワンモア偽造不可能性判定ステップと、
条件判定部が、上記ブラインド署名による署名の対象となるメッセージをmとし、上記ブラインド署名の検証アルゴリズムの関数をV(m)として、V(m)=V’(H(f(m)))の関係を満たす関数V’、ハッシュ関数H及び関数fが存在するという条件を満たすか判定する条件判定ステップと、
最終判定部が、上記安全性判定ステップにおいて上記プロトコルは安全であると判定され、上記ワンモア偽造不可能性判定ステップにおいて上記ブラインド署名はワンモア偽造不可能性を満たすと判定され、上記条件判定ステップにおいて上記条件を満たすと判定された場合に、上記プロトコルは安全であると判定する最終判定ステップと、
を含むプロトコル安全性検証方法。
【請求項５】
請求項１から３のプロトコル安全性検証装置の各部としてコンピュータを機能させるためのプログラム。
【請求項１】
ブラインド署名を用いるプロトコルの安全性を検証するプロトコル安全性検証装置であって、
上記ブラインド署名が一対一偽造不可能性を満たすとした場合に、上記プロトコルが安全か判定する安全性判定部と、
上記ブラインド署名がワンモア偽造不可能性を満たすか判定するワンモア偽造不可能性判定部と、
上記ブラインド署名による署名の対象となるメッセージをmとし、上記ブラインド署名の検証アルゴリズムの関数をV(m)として、V(m)=V’(H(f(m)))の関係を満たす関数V’、ハッシュ関数H及び関数fが存在するという条件を満たすか判定する条件判定部と、
上記安全性判定部において上記プロトコルは安全であると判定され、上記ワンモア偽造不可能性判定部において上記ブラインド署名はワンモア偽造不可能性を満たすと判定され、上記条件判定部において上記条件を満たすと判定された場合に、上記プロトコルは安全であると判定する最終判定部と、
を含むプロトコル安全性検証装置。
【請求項２】
請求項１のプロトコル安全性検証装置において、
ワンモア偽造不可能性を満たすブラインド署名についての情報を記憶する第一記憶部を更に含み、
上記ワンモア偽造不可能性判定部は、上記第一記憶部を参照して上記ブランド署名がワンモア偽造不可能性を満たすか判定する、
プロトコル安全性検証装置。
【請求項３】
請求項１又は２のプロトコル安全性検証装置において、
上記条件を満たすブラインド署名についての情報を記憶する第二記憶部を更に含み、
上記条件判定部は、上記第二記憶部を参照して上記ブラインド署名が上記条件を満たすか判定する、
プロトコル安全性検証装置。
【請求項４】
ブラインド署名を用いるプロトコルの安全性を検証するプロトコル安全性検証方法であって、
安全性判定部が、上記ブラインド署名が一対一偽造不可能性を満たすとした場合に、上記プロトコルが安全か判定する安全性判定ステップと、
ワンモア偽造不可能性判定部が、上記ブラインド署名がワンモア偽造不可能性を満たすか判定するワンモア偽造不可能性判定ステップと、
条件判定部が、上記ブラインド署名による署名の対象となるメッセージをmとし、上記ブラインド署名の検証アルゴリズムの関数をV(m)として、V(m)=V’(H(f(m)))の関係を満たす関数V’、ハッシュ関数H及び関数fが存在するという条件を満たすか判定する条件判定ステップと、
最終判定部が、上記安全性判定ステップにおいて上記プロトコルは安全であると判定され、上記ワンモア偽造不可能性判定ステップにおいて上記ブラインド署名はワンモア偽造不可能性を満たすと判定され、上記条件判定ステップにおいて上記条件を満たすと判定された場合に、上記プロトコルは安全であると判定する最終判定ステップと、
を含むプロトコル安全性検証方法。
【請求項５】
請求項１から３のプロトコル安全性検証装置の各部としてコンピュータを機能させるためのプログラム。
【図１】
【図２】
【図２】
【公開番号】特開２０１３−３８５７２（Ｐ２０１３−３８５７２Ａ）
【公開日】平成２５年２月２１日（２０１３．２．２１）
【国際特許分類】
【出願番号】特願２０１１−１７２６２９（Ｐ２０１１−１７２６２９）
【出願日】平成２３年８月８日（２０１１．８．８）
【出願人】（０００００４２２６）日本電信電話株式会社 (13,992)
【Ｆターム（参考）】
【公開日】平成２５年２月２１日（２０１３．２．２１）
【国際特許分類】
【出願日】平成２３年８月８日（２０１１．８．８）
【出願人】（０００００４２２６）日本電信電話株式会社 (13,992)
【Ｆターム（参考）】
[ Back to top ]