暗号プロトコル安全性検証装置、暗号プロトコル設計装置、暗号プロトコル安全性検証方法、暗号プロトコル設計方法、暗号プロトコル安全性検証プログラムおよび暗号プロトコル設計プログラム
【課題】暗号プロトコルのプリミティブな安全性を確保して、複雑な暗号プロトコルでも安全性検証の労力を軽減すること。
【解決手段】暗号プロトコル安全性検証装置であって、暗号プロトコルの実行に関与するパーティに関する処理が記述された第１記述部と、理想のプロトコルと対応し、暗号プロトコルの実行に関与するパーティおよび暗号プロトコルの実行に関与しない第１の仮想のエンティティに関する処理が記述され、暗号プロトコルの実行に関与しない第２の仮想のエンティティに関する記述を含まない第２記述部とを含み、第１の仮想のエンティティは理想のプロトコルにおける理想機能に対応し、第２の仮想のエンティティは理想のプロトコルにおけるシミュレータに対応する暗号プロトコル仕様データを入力する暗号プロトコル仕様入力処理部１１０と、パーティおよび第１の仮想のエンティティに関する処理の欠陥の有無を検証する形式的検証部１２０を備えた。
【解決手段】暗号プロトコル安全性検証装置であって、暗号プロトコルの実行に関与するパーティに関する処理が記述された第１記述部と、理想のプロトコルと対応し、暗号プロトコルの実行に関与するパーティおよび暗号プロトコルの実行に関与しない第１の仮想のエンティティに関する処理が記述され、暗号プロトコルの実行に関与しない第２の仮想のエンティティに関する記述を含まない第２記述部とを含み、第１の仮想のエンティティは理想のプロトコルにおける理想機能に対応し、第２の仮想のエンティティは理想のプロトコルにおけるシミュレータに対応する暗号プロトコル仕様データを入力する暗号プロトコル仕様入力処理部１１０と、パーティおよび第１の仮想のエンティティに関する処理の欠陥の有無を検証する形式的検証部１２０を備えた。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、暗号プロトコルに欠陥があるか否かの安全性を検証する暗号プロトコル安全性検証装置、暗号プロトコル安全性検証方法、暗号プロトコル安全性検証プログラムおよび、暗号プロトコルの安全性を検証して暗号プロトコルを設計する暗号プロトコル設計装置、暗号プロトコル設計方法および暗号プロトコル設計プログラムに関する。
【背景技術】
【０００２】
暗号学的な手法を利用した暗号プロトコルの安全性を検証する手法としては、従来から形式的検証（ＦＶ：Formal Verification）と計算量理論的証明（Complex-Theoretic Proof）が知られている。
【０００３】
形式的検証は、プロトコルの正当性を暗号プロトコル仕様の記述から形式的に検証する手法である（例えば、非特許文献１参照）。 計算量理論的証明は、プロトコルの安全性を破ることを数学的な問題の困難性に帰着させる手法である。
【０００４】
そして、計算量理論的証明としてmodular アプローチという検証手法が提案されている。このmodular アプローチは、ある仮定の下でプロトコルの安全性を証明しておき、次に、その仮定部分を現実的な状況でも安全なプロトコルに変換するものである。このmodular アプローチに基づいて暗号プロトコルの安全性検証を行う手法として、近年、汎用的結合可能性（ＵＣ：Universal Composability）による証明が提案されている。
【０００５】
このＵＣによる証明は、シミュレーションパラダイムに基づき定式化されており、あるプロトコルπが理想機能(ideal functionality)Ｆを安全に実現しているとは、現実モデルと理想プロセスの２つの系を確率的多項式時間Turing 機械Ｅ(以下、環境Ｅという) が識別できないこと、厳密には、現実モデルの任意の敵Ａに対して、理想プロセスのシミュレータＳが存在し、いかなる環境Ｅによっても２つの系は識別できないことと定義されている。ＵＣでは、あるプロトコルπ が理想機能Ｆを安全に実現していることを証明することができれば、そのプロトコルπをサブルーチンとして呼び出すプロトコルρを実行した場合にも、プロトコルρの中でプロトコルπが何回呼び出されても、プロトコルπの安全性は保たれることがUniversal composability theoremとして証明されている（例えば、非特許文献２参照）。
【０００６】
【非特許文献１】Abadi, M., Rogaway, P.: Reconciling Two Views of Cryptography. In: IFIP International Conference on Theoretical Computer Science. (2000)
【非特許文献２】Canetti, R.: Universally Composable Security: A New Paradigm for Cryptographic Protocols. In: FOCS’01, IEEE(2001) 136−145
【発明の開示】
【発明が解決しようとする課題】
【０００７】
しかしながら、このような従来の暗号プロトコル安全性検証の手法には、以下のような問題がある。形式的検証では、複雑な暗号プロトコルの検証が計算量が多くなり困難であり、またプリミティブの安全性の仮定が必要となってくる。
【０００８】
また、計算量理論的証明では、安全性証明が与えられている暗号プロトコルは限られており、暗号プロトコルに修正を加えると、その修正がわずかなものであっても新たな安全性の証明を付与しなければならず、暗号プロトコルの安全性検証に多大な労力が必要となる。
【０００９】
ＵＣ等のmodular アプローチでは、ある仮定の下でプロトコルの安全性を証明しておき、次に、その仮定部分を現実的な状況でも安全なプロトコルに変換するという構造的な証明方法によって暗号プロトコルの安全性証明の労力を軽減しているが、複雑な暗号プロトコルでは安全性証明の労力を効率的に行うことができない。
【００１０】
本発明は、上記に鑑みてなされたものであって、暗号プロトコルのプリミティブな安全性を確保しつつ、複雑な暗号プロトコルでも安全性検証の労力を軽減することができる暗号プロトコル安全性検証装置、暗号プロトコル設計装置、暗号プロトコル安全性検証方法、暗号プロトコル設計方法、暗号プロトコル安全性検証プログラムおよび暗号プロトコル設計プログラムを提供することを目的とする。
【課題を解決するための手段】
【００１１】
上述した課題を解決し、目的を達成するために、本発明は、現実に暗号プロトコルの実行に関与するパーティに関する処理が記述された第１記述部と、汎用結合可能安全性で定義される理想のプロトコルと対応し、現実に暗号プロトコルの実行に関与するパーティおよび現実に暗号プロトコルの実行に関与しない第１の仮想のエンティティに関する処理が記述され、現実に暗号プロトコルの実行に関与しない第２の仮想のエンティティに関する記述を含まない第２記述部とを含む検証可能な暗号プロトコル仕様データであって、前記第１の仮想のエンティティは、前記理想のプロトコルにおける理想機能に対応し、前記第２の仮想のエンティティは、前記理想のプロトコルにおけるシミュレータに対応する検証可能な暗号プロトコル仕様データにおける前記パーティおよび第１の仮想のエンティティに関する処理の欠陥の有無を、前記検証可能な暗号プロトコル仕様データの記述に基づいて検証する形式的検証手段を備えたことを特徴とする暗号プロトコル安全性検証装置である。
【００１２】
また、本発明は、現実に暗号プロトコルの実行に関与するパーティに関する処理の記述である第１記述部を構成する第１記述部品と、前記第１記述部により安全に実現されることが証明されている、現実に暗号プロトコルの実行に関与するパーティに関する処理と現実に暗号プロトコルの実行に関与しない第１の仮想のエンティティと第２の仮想のエンティティに関する処理の記述である第２記述部を構成する第２記述部品とを記憶する暗号プロトコル部品記憶手段と、前記暗号プロトコル部品記憶手段に記憶された前記第２記述部品と新たに追加した前記第１記述部とを含む暗号プロトコル仕様データを生成する暗号プロトコル仕様設計手段と、前記暗号プロトコル仕様設計手段によって生成された前記暗号プロトコル仕様データに対して、前記第２記述部に対して前記第２の仮想のエンティティに関する記述を削除して、検証可能な暗号プロトコル仕様データを生成する検証可能暗号プロトコル生成手段と、前記検証可能暗号プロトコル仕様生成手段によって生成された前記検証可能な暗号プロトコル仕様データにおける前記パーティおよび前記第１の仮想のエンティティの両方に関する処理の欠陥の有無を、前記検証可能な暗号プロトコル仕様データの記述に基づいて検証する形式的検証手段と、前記形式的検証手段によって欠陥なしと証明された前記検証可能な暗号プロトコル仕様データに基づいて実現可能な暗号プロトコルを生成する暗号プロトコル実行手段と、を備えたことを特徴とする暗号プロトコル設計装置である。
【００１３】
また、本発明は、上記装置に対応する方法およびプログラムである。
【発明の効果】
【００１４】
本発明にかかる暗号プロトコル安全性検証装置、暗号プロトコル安全性検証方法および暗号プロトコル安全性検証プログラムでは、汎用的結合可能安全性で定義される理想機能に関するエンティティを含むとともに攻撃者としてのシミュレータに関する記述が存在しない検証可能な暗号プロトコルの安全性検証を行っている。このため、本発明によれば、計算量的証明における暗号プロトコル仕様と形式的検証における暗号プロトコル仕様とを整合性をとった上で、プリミティブな安全性を計算量的証明により確保しつつ、複雑な暗号プロトコルについては形式的検証による機械的な検証処理により安全性検証の労力を軽減することができるという効果を奏する。
【００１５】
また、本発明にかかる暗号プロトコル設計装置、暗号プロトコル設計方法および暗号プロトコル設計プログラムでは、暗号プロトコル仕様データを設計し、設計した暗号プロトコル仕様データから汎用的結合可能安全性で定義される理想機能に関するエンティティを含むとともに攻撃者としてのシミュレータに関する記述が存在しない検証可能な暗号プロトコルを生成してその安全性検証を行っている。そして、安全性が証明された暗号プロトコル仕様データに基づいて実現可能な暗号プロトコルを生成するので、本発明によれば、計算量的証明における暗号プロトコル仕様と形式的検証における暗号プロトコル仕様とを整合性をとった上で、プリミティブな安全性を計算量的証明により確保しつつ、複雑な暗号プロトコルについては形式的検証による機械的な検証処理により安全性検証の労力を軽減することともに、確実な暗号プロトコルを設計することができるという効果を奏する。
【発明を実施するための最良の形態】
【００１６】
以下に添付図面を参照して、この発明にかかる暗号プロトコル安全性検証装置、暗号プロトコル設計装置、暗号プロトコル安全性検証方法、暗号プロトコル設計方法、暗号プロトコル安全性検証プログラムおよび暗号プロトコル設計プログラムの最良な実施の形態を詳細に説明する。
【００１７】
（実施の形態１）
実施の形態１にかかる暗号プロトコル安全性検証装置は、現実に暗号プロトコルの実行に関与するパーティに関する処理が記述された第１記述部と、汎用的結合可能安全性で定義される理想機能に関するエンティティを含むとともに攻撃者としてのシミュレータに関する記述が存在せず、現実に暗号プロトコルの実行に関与するパーティに関する処理と現実に暗号プロトコルの実行に関与しない第１の仮想のエンティティに関する処理が記述された第２記述部とを含む検証可能な暗号プロトコル仕様データを入力して、当該暗号プロトコル仕様データの安全性を検証するものである。
【００１８】
図１は、実施の形態１にかかる暗号プロトコル安全性検証装置の機能的構成を示すブロック図である。本実施の形態にかかる暗号プロトコル安全性検証装置１００は、図１に示すように、暗号プロトコル仕様入力処理部１１０と、形式的検証部１２０と、検証結果出力部１３０と、初期条件記憶部１４１と、プロトコル記憶部１４２と、定義記憶部１４３と、ユーザ目標記憶部１４４と、デフォルト目標記憶部１４５と、推論規則記憶部１５１と、証明済み文記憶部１５２とを主に備えた構成となっている。
【００１９】
暗号プロトコル仕様入力処理部１１０は、検証可能な暗号プロトコル仕様データの入力処理をおこなう処理部である。検証可能な暗号プロトコル仕様データは、形式的検証（ＦＶ）におけるプロトコル仕様で記述された第１記述部と、計算量的証明のＵＣ（Universal Composability）におけるプロトコル仕様に基づいて記述された第２記述部とからなる暗号プロトコル仕様である。第２記述部では、暗号プロトコルが単にＵＣにおけるプロトコル仕様で記述されているのではなく、ＵＣにおける記述から第１の仮想のエンティティとしての理想機能が付加され、第２の仮想のエンティティとしての攻撃者であるシミュレータの記述が含まれていないものとなっている。すなわち、ＵＣにおける仕様と形式的証明における仕様とを整合性をとって記述して、暗号プロトコルによるプリミティブな安全性を確保しつつ形式的証明による機械的な安全性検証が可能な暗号プロトコル仕様となっている。この暗号プロトコル仕様データには、初期条件部、定義部、プロトコル実行定義部、ゴール部に分割されて記述されている。
【００２０】
形式的検証部１２０は、入力された上記検証可能な暗号プロトコル仕様データに記述された暗号プロトコル仕様に対し形式的検証（ＦＶ）によって安全性の検証を行う処理部であり、後述する第１記述部において現実に暗号プロトコルの実行に関与するパーティおよび第１記述部および第２記述部における現実に暗号プロトコルの実行に関与しない第１の仮想のエンティティの両方に関する処理の欠陥の有無を検証する。形式的検証部１２０は、図１に示すように、プロトコル解析部１２３とデフォルト目標生成部１２１と推論実行部１２２とを有している。
【００２１】
解析部１２３は、検証可能な暗号プロトコル仕様データを解析して、初期条件部、定義部、プロトコル実行定義部、ゴール部を抽出し、初期条件部の記述を初期条件記憶部１４１に、定義部を定義記憶部１４２にそれぞれ保存する処理部である。また、解析部１２３は、検証可能な暗号プロトコル仕様データを解析して、ゴール部を後ろ向き推論において証明すべき目標となる文をユーザ目標としてユーザ目標記憶部１４４に保存する。
【００２２】
デフォルト目標生成部１２１は、検証可能な暗号プロトコル仕様データにおけるプロトコル実行定義部の各段階であるステージの上記パーティおよび仮想パーティの両方に関する処理の記述から後ろ向き推論において証明すべき目標となる文であるデフォルト目標をステージごとに設定してデフォルト目標記憶部１４５に保存する処理部である。ここで、デフォルト目標としては、例えば、各ステージにおいて、送信者がそのメッセージを送信することができたか、受信者がそのメッセージの暗号化部分を復号化できたか、受信者がそのメッセージの暗号化されたあるいはハッシュされたフィールドをどのパーティが伝達したかを決定可能か、受信者はそのメッセージの送信にバインドされた関連文を信じる根拠を有するか等の文が該当する。
【００２３】
推論実行部１２２は、デフォルト目標の文およびユーザ目標の文と、初期条件記憶部１４１あるいは証明済み文記憶部１５２と推論規則記憶部１５１に格納されている推論規則から後向き推論を行って検証可能な暗号プロトコル仕様データに欠陥があるか否か、すなわち暗号プロトコルの安全性を検証する処理部である。具体的には、推論実行部１２２は、プロトコル実行定義部のステージ順に、デフォルト目標の文と等価な文が、検証の初期段階で正しいことを仮定された文を記録している初期条件記憶部１４１あるいは現ステージより以前のステージに対する検証の過程において正しいことが検証された文を記憶している証明済み文記憶部１５２に存在するか否かを検索する。また、推論実行部１２２は、ユーザ目標の文と等価な文が初期条件記憶部１４１あるいは証明済み文記憶部１５２に存在するか否かを検索する。そして、推論実行部１２２は、このような処理を全てのステージのデフォルト目標における全ての文、およびユーザ目標における全ての文について等価な文が初期条件記憶部１４１あるいは証明済み文記憶部１５２に存在した場合に、暗号プロトコルは欠陥なしとしてその安全性を証明する。
【００２４】
検証結果出力部１３０は、推論実行部１２２による暗号プロトコルの安全性の検証結果（安全性あり／なし）をディスプレイ装置などの表示装置やプリンタ装置等に出力する処理部である。
【００２５】
初期条件記憶部１４１は、解析部１２３により暗号プロトコル仕様データから抽出された初期条件部の記述内容、すなわち検証の初期段階で正しいことを仮定された文を保存するものである。プロトコル記憶部１４２は、解析部１２３により暗号プロトコル仕様データから抽出されたプロトコル実行定義部の記述内容を保存するものである。定義記憶部１４３は、解析部１２３により暗号プロトコル仕様データから抽出された定義部の記述内容を保存するものである。ユーザ目標記憶部１４４は、解析部１２３により暗号プロトコル仕様データから抽出されたゴール部の記述内容を保存するものである。
【００２６】
デフォルト目標記憶部１４５は、デフォルト目標生成部１２１によって上述したデフォルト目標を保存するものである。
【００２７】
推論規則記憶部１５１は、前提部や連言形で表現された結論部を有する既存の推論規則が保存されたものであり、本実施の形態では、ＧＮＹ（Gong-Needham-Yahalom） logicから派生した証明推論を定式化した規則であるＢＧＮＹ２の推論規則が保存されている。なお、本実施の形態では、推論実行部１２２が行う後向き推論に対応してＢＧＮＹ２の推論規則が推論規則記憶部１５１に保存されているが、これに限定されるものではなく、実行する推論の手法に応じて任意の推論規則を推論規則記憶部１５１に保存することができる。
【００２８】
証明済み文記憶部１５２は、推論実行部１２２により検証の過程において現ステージより以前のステージで既に欠陥無し（真である）と証明された文を記憶したものである。
【００２９】
これらの初期条件記憶部１４１、プロトコル記憶部１４２、定義記憶部１４３、ユーザ目標記憶部１４４、デフォルト目標記憶部１４５、推論規則記憶部１５１、証明済み文記憶部１５２は、メモリ、ＨＤＤ（Ｈａｒｄ Ｄｉｓｋ Ｄｒｉｖｅ）等の記憶媒体である。
【００３０】
次に、汎用的結合可能性（以下、「ＵＣ」という）の概要を説明する。図２は、ＵＣの概要を説明するための模式図である。図２には、現実にプロトコル実行に関与するパーティＰi間、パーティＰiと攻撃者である敵Ａとのメッセージの授受などをプロトコルπに従って行う現実モデルの系と、この現実モデルに対応して、現実にプロトコル実行に関与するパーティＰi間、攻撃者としてのシミュレータＳとのメッセージの授受などを現実にプロトコル実行に関与しない第１の仮想のエンティティである理想機能Ｆを利用して行う理想プロセスの系とを示している。
【００３１】
ＵＣでは、あるプロトコルπが理想機能（ideal functionality）Ｆを安全に実現しているとは、現実モデルと理想プロセスの２つの系を確率的多項式時間チューリング機械（ＰＰＴ）（以下、「環境Ｅ」という）が識別できないことと定義される。すなわち、現実モデルの任意の敵Ａに対して、理想プロセスのあるシミュレータＳが存在し、いかなる環境Ｅによっても２つの系は識別できない。ＵＣでは、あるプロトコルπが理想機能Ｆを安全に実現していることが証明できれば、そのプロトコルをサブルーチンとして呼び出すプロトコルρを実行した場合にも、プロトコルπがρの中で何回呼び出されても、プロトコルπの安全性は保たれることが証明できる（universal composability theorem）。
【００３２】
ＵＣには、いくつかの定式化があるが、そのうちのひとつの定式化では、シミュレータＳは、理想機能Ｆと各パーティＰiの間で授受されるメッセージの宛先を読むことができるが、そのメッセージの中身までは見ることができない。さらに、シミュレータＳ（敵）は、理想機能Ｆから依頼されてパーティＰiへメッセージの配送を即座に行う。ただし、依頼されても配信しないこともできる。さらに、依頼されていないメッセージを配信することもできる。
【００３３】
また、ＵＣの別の定式化では、理想機能ＦとパーティＰiの間のメッセージの授受はシミュレータを介さず、直接行われる。この場合、シミュレータＳは、理想機能ＦとパーティＰiの間で授受されるメッセージについて、そのパーティがｃｏｒｒｕｐｔされていない限り認識することはできない。ただし、理想機能Ｆが、その仕様上明示的にシミュレータＳに対してメッセージ配信の許可を場合には、シミュレータＳはそのメッセージの内容を知ることができる。
【００３４】
ＵＣでは、暗号プロトコル（またはその一部）は理想機能Ｆと等価である。ここで等価とは、現実モデルにおいて敵Ａが行う任意の攻撃は、理想プロセスにおいてシミュレータＳが行う攻撃と計算量的に識別できないというものである。従って、理想機能Ｆが暗号プロトコルのメッセージの授受や計算の詳細を隠蔽しメッセージの中身を秘匿する仕様になっているならば、現実モデルにおいて、敵Ａがいくらそれら詳細な情報を集めたところで、少なくともその理想機能で記述されている暗号プロトコルの部分に関して、シミュレータＳから見えていない情報を使ったからといって、シミュレータができない攻撃ができるわけではない。
【００３５】
図３は、署名に関する理想機能である署名理想機能ＦSIGの一例を示す説明図である。署名理想機能ＦSIGでは、敵としてのシミュレータＳが検証鍵を付与することが特徴となっている。Ｐiは、現実にプロトコル実行に関与しない仮想的なパーティである。
【００３６】
これに対し、形式的検証（ＦＶ）におけるプロトコルでは、明示的に敵Ｓが仕様記述中には現れてこないので、形式的検証を行う形式的検証部１２０に理想機能を含む仕様記述を入力する際には、検証手法の差異に対する考慮が必要となってくる。本実施の形態では、検証可能な暗号プロトコル仕様として、理想機能Ｆを使用した第２記述部を、シミュレータに関する処理を削除して、理想機能がシミュレータに代わって処理を行う記述にしたプロトコルとしている。
【００３７】
また、署名検証において受理するか拒否するかを決定するのが敵Ｓの役割になっている。敵Ｓからは理想機能ＦSIGの内部の処理は知ることができないが、理想機能ＦSIGが他のパーティと授受するメッセージはシミュレータＳに知られてしまうと定式化されている。
【００３８】
また、理想機能ＦSIGを実現するプロトコル署名スキームＳ＝（ｇｅｎ，ｓｉｇ，ｖｅｒ）に対して、プロトコルπSを図４に示すように定義する。このとき、「スキームＳが適応性選択文書攻撃に対する存在的偽造不可能な署名スキームであることと、プロトコルπSが理想機能ＦSIGを安全に実現することは等価であることが知られている。Ｐiは、現実にプロトコル実行に関与するパーティである。
【００３９】
図５は、実施の形態１にかかる暗号プロトコル安全性検証装置で入力される検証可能な暗号プロトコル仕様データのデータ構造を示す模式図である。図５に示すように、検証可能な暗号プロトコル仕様データ５００には、第１記述部５０１と第２記述部５０２とから構成され、第１記述部５０１には形式的検証（ＦＶ）におけるプロトコル仕様で、現実モデルのプロトコルが記述される。一方、第２記述部５０２では、第１記述部５０１の現実モデルのプロトコルπに対応して理想機能Ｆを利用したプロトコル仕様の記述から、シミュレータＳの処理に関する記述を理想機能がシミュレータに代わって処理を行う記述にしたプロトコルが記述される。
【００４０】
図６は、検証可能な暗号プロトコル仕様データ５００の第１記述部５０１の例を示す説明図である。図６の例では、電子署名を利用した相互認証プロトコルＩＳＯ／ＩＥＣ ９７９８−３の初期バーションの仕様をＩＳＬ２（Interface Specification Language, Version 2）を拡張した言語で記述したものを示してある。暗号プロトコル仕様データは、図６に示すように、定義部、初期条件部、プロトコル実行定義部、ゴール部から構成されており、現実に暗号プロトコル実行に関与するパーティに関する処理が記述されている。
【００４１】
本来、ＩＳＬ２における電子署名の記述仕様は、［ｘ］（ｆ，ｈ）（ｋ）のように定義される。かかる定義は、署名を伴っているメッセージｘを表しており、その署名は、ｘにハッシュ関数ｈを施した上で暗号化関数ｆで暗号化して得られることを示している。ここで、ｋは暗号鍵である。しかしながら、安全性証明が与えられている電子署名方式の多くは、より複雑な形をしており、上のような形で表現されない。また、メッセージと切り離して電子署名だけを送信したい場合、その記述をすることができない。そこで、本実施の形態では、暗号プロトコル仕様記述言語の記述能力を向上させるため、図６のように記述している。
【００４２】
図６の例では、定義部で、署名関数（ＳＩＧＮ ＦＵＮＣＴＩＯＮＳ）がＳｉｇ、検証関数（ＶＥＲＩＦＹ ＦＵＮＣＴＩＯＮＳ）がＶｅｒ、鍵生成関数（ＧＥＮＫＥＹＳ ＦＵＮＣＴＩＯＮＳ）がＧであることを定義している。ここで、定義部の記述において、
Ｓｉｇ ＷＩＴＨ ＫＳ ＩＳＶＥＲＩＦＩＥＤＢＹ Ｖｅｒ
ＷＩＴＨ ＫＶ ＳＵＣＨＴＨＡＴ （ＫＳ；；ＫＶ） ＝ Ｇ（）； ・・・（１）
（１）式の記述は、鍵生成関数Ｇ（）は署名鍵ＫＳと検証鍵ＫＶの対（ＫＳ；；ＫＶ）を生成することを示す。このため、図６の定義部では、鍵生成関数Ｇ（）は署名鍵ＫSＡと検証鍵ＫVＡの対（ＫSＡ；；ＫVＡ）を生成し、また、鍵生成関数Ｇ（）は署名鍵ＫSＢと検証鍵ＫVＢの対（ＫSＢ；；ＫVＢ）を生成することを定義している。
【００４３】
なお、図６の例では、鍵生成関数Ｇは引数を有さない関数としているが、セキュリティパラメータやその他のパラメータを引数とするように構成してもよい。また、鍵生成関数Ｇは決定性の関数である他、確率性の関数として構成することもできる。鍵生成関数をＧを確率性の関数として構成する場合は、鍵生成関数Ｇは呼び出されるたびに、鍵対全体の空間からランダムに選んだ鍵対を生成することになる。
【００４４】
初期条件部、プロトコル実行定義部、ゴール部における仕様記述の意味は以下のとおりである。
【００４５】
＜ｘ＞Ｓｉｇ（ｋ） ：署名関数Ｓｉｇによるメッセージｘの署名。ｋは署名鍵。
ＶｅｒｉｆｉｃａｔｉｏｎＫｅｙ Ｐ Ｖ Ｋ ：パーティＰによる署名の検証アルゴリズムＶの検証鍵はＫである。
Ａ Ｂｅｌｉｅｖｅｓ ＜Ｓｔｍｔ＞ ：パーティＡが＜Ｓｔｍｔ＞を信じる理由があった。
Ａ Ｐｏｓｓｅｓｓｅｓ ＜Ｓｔｍｔ＞ ：パーティＡは、＜Ｓｔｍｔ＞を受信したか、あるいは、受信した複数の＜Ｓｔｍｔ＞の中からその＜Ｓｔｍｔ＞を計算できる。
Ａ Ｒｅｃｅｉｖｅｄ ＜Ｓｔｍｔ＞ ：パーティＡは、＜Ｓｔｍｔ＞を現在のプロトコル実行より前に受け取った、または現在のプロトコル実行よりも前に受け取ったあるメッセージまたはその一部として受け取った。
Ａ Ｃｏｎｖｅｙｅｄ ＜Ｓｔｍｔ＞ ：パーティＡが＜Ｓｔｍｔ＞の現在のプロトコル実行の間の生成者でソースである。
【００４６】
従って、図６において初期条件部は、以下の意味を示している。
・パーティＡは、署名関数Ｓｉｇ、検証関数Ｖｅｒ、署名鍵ＫSＢを現在のプロトコル実行より前に受け取った、または現在のプロトコル実行よりも前に受け取ったあるメッセージまたはその一部として受け取った。
・パーティＡは、署名鍵ＫSＡを受信した。
・パーティＡは、パーティＢによる署名の検証アルゴリズムＶｅｒの検証鍵はＫSＢであることを信じる理由があった。
・パーティＢは、署名関数Ｓｉｇ、検証関数Ｖｅｒ、署名鍵ＫSＡを現在のプロトコル実行より前に受け取った、または現在のプロトコル実行よりも前に受け取ったあるメッセージまたはその一部として受け取った。
・パーティＢは、署名鍵ＫSＢを受信した。
・パーティＢは、パーティＡによる署名の検証アルゴリズムＶｅｒの検証鍵はＫSＡであることを信じる理由があった。
【００４７】
また、図６において、プロトコル実行定義部は以下の意味を示している。ここで、図６の最左端の番号は実行段階を示すステージである。
ステージ１：ＢからＡにメッセージＮｏＢを送信。
ステージ２：ＡからＢに、メッセージＮｏＡ，ＮｏＢ，Ｂ，署名関数ＳｉｇによるメッセージＮｏＡ，ＮｏＢ，Ｂの署名（署名鍵ＫSＡ）を送信。
ステージ３：ＢからＡに、メッセージＮｏＢ２，ＮｏＡ，Ａ，署名関数ＳｉｇによるメッセージＮｏＢ２，ＮｏＡ，Ａの署名（署名鍵ＫSＢ）を送信。
【００４８】
また、図６において、ゴール部は以下の意味を示している。
ステージ１：Ｂは、Ａが署名関数ＳｉｇによるメッセージＮｏＡ，ＮｏＢ，Ｂの署名（署名鍵ＫSＡ）の現在のプロトコル実行の間の生成者でソースであることを信じる理由があった。
ステージ２：Ａは、Ｂが署名関数ＳｉｇによるメッセージＮｏＢ２，ＮｏＡ，Ａの署名（署名鍵ＫSＢ）の現在のプロトコル実行の間の生成者でソースであることを信じる理由があった。
【００４９】
図７−１は、暗号プロトコル仕様における理想機能を使用した記述例を示す説明図である。図７−１では、プロトコル実行定義部における署名のプロトコルと検証のプロトコルの２つを示している。図７−１において、Ｐは、現実にプロトコル実行に関与するパーティ、Ｆは理想機能、Ｓはシミュレータ（敵）を示している。
【００５０】
署名のプロトコルでは、以下の意味を示している。
ステージ１：パーティＰから理想機能Ｆに署名要求送信。
ステージ２：理想機能ＳからシミュレータＳに署名要求送信。
ステージ３：シミュレータＳから理想機能Ｓに署名送信。
ステージ４：理想機能ＳからパーティＰに署名送信。
【００５１】
検証のプロトコルでは、以下の意味を示している。
ステージ１：パーティＰから理想機能Ｆに検証要求送信。
ステージ２：理想機能ＳからシミュレータＳに検証要求送信。
ステージ３：シミュレータＳから理想機能Ｓに検証送信。
ステージ４：理想機能ＳからパーティＰに検証送信。
【００５２】
この図７−１に示すプロトコル仕様では、シミュレータＳについての記述があるが、本実施の形態の検証可能な暗号プロトコル仕様では、ＵＣにおける記述から理想機能のエンティティが付加され、攻撃者としてのシミュレータの記述が削除または理想機能に対する記述に置換されたものとしている。具体的には、シミュレータＳと理想機能Ｆとの間の授受情報を攻撃時に利用可能な情報に置換し、シミュレータに対する理想機能からの即座の配信要求の記述を、理想機能による即座の配信の記述に置換した第２記述部５０２を有する暗号プロトコル仕様となっている。
【００５３】
図７−２は、検証可能な暗号プロトコル仕様データ５００の第２記述部５０２のプロトコル実行定義部の例を示す説明図である。図７−２では、図７−１のプロトコル実行定義部の記述においてシミュレータＳの記述を上記のように置換した署名のプロトコルと検証のプロトコルを示したものとなっている。すなわち、図７−１の署名のプロトコルにおける理想機能ＦからのシミュレータＳに対する署名要求が理想機能による即座の署名の記述に置換され、以下のようになる。
【００５４】
ステージ１：パーティＰから理想機能Ｆに署名要求送信。
ステージ２：理想機能ＳからパーティＰに署名送信。
【００５５】
同様に、検証のプロトコルは以下の意味となる。
ステージ１：パーティＰから理想機能Ｆに検証要求送信。
ステージ２：理想機能ＳからパーティＰに検証送信。
【００５６】
このように、本実施の形態では、シミュレータＳに関する記述を削除した第２記述部５０２を含む暗号プロトコル仕様を入力して暗号プロトコルの安全性検証を行っている。
【００５７】
次に、以上のように構成された本実施の形態にかかる暗号プロトコル安全性検証装置による暗号プロトコルの安全性検証処理について説明する。図８は、実施の形態１の暗号プロトコルの安全性検証処理の手順を示すフローチャートである。
【００５８】
暗号プロトコル仕様入力処理部１１０により図６に示すような第１記述部５０１と図７−２に示すような第２記述部５０２を有する検証可能な暗号プロトコル仕様データ５００が入力されると、形式的検証部１２０の解析部１２１によって暗号プロトコル仕様データを解析し、暗号プロトコル仕様データから初期条件部の記述を抽出して初期条件記憶部１４１に保存する（ステップＳ８０１）。次いで、解析部１２１によって暗号プロトコル仕様データからプロトコル実行定義部の記述を抽出してプロトコル記憶部１４２に保存する（ステップＳ８０２）。同様に、解析部１２１によって暗号プロトコル仕様データから定義部の記述を抽出して定義記憶部１４３に保存する（ステップＳ８０３）。さらに、解析部１２１によって暗号プロトコル仕様データからゴール部の記述を抽出してユーザ目標としてユーザ目標記憶部１４４に保存する（ステップＳ８０４）。なお、ゴール部の存在しない検証可能な暗号プロトコル仕様データ５００の場合には、かかるステップＳ８０４の処理はおこなわれない。
【００５９】
次いで、解析部１２３により、プロトコル記憶部１４２からプロトコル実行定義部の記述を読み出して、プロトコル実行定義部の記述をステージごとの文に分割する（ステップＳ８０５）。なお、図６および図７−１の例では、各ステージが単一の文から構成されているが、各ステージが複数の文から構成される場合もある。そして、定義記憶部１４３に保存されている定義部の記述を参照しながら、ステージごとに推論におけるデフォルト目標を生成し、デフォルト目標記憶部１４５に保存する（ステップＳ８０６）。
【００６０】
そして、推論実行部１２２によってデフォルト目標、ユーザ目標、証明済み文記憶部１５２、推論規則記憶部１５１の推論規則とから推論を実行して暗号プロトコル仕様の安全性を検証する（ステップＳ８０７）。そして、その検証結果として、暗号プロトコル仕様の安全性あり／なし、プロトコル実行定義部のステージごとの欠陥の有無、ゴール部の欠陥の有無が検証結果出力部１３０によって、表示装置等に出力される。
【００６１】
次に、ステップＳ８０７による推論実行部１２２による推論実行処理について説明する。図９−１および図９−２は、推論実行部１２２による推論実行処理の手順を示すフローチャートである。なお、本実施の形態では、後向き推論を行っているが、前向き推論によって安全性証明を実現することも可能である。
【００６２】
個々のデフォルト目標は、一般に、いくつかの連言形の文(論理積で表現される文)を選言形にしたもの(論理和で表現される文)として表現されている。まず、推論実行部１２２は、デフォルト目標記憶部１４５から一つのデフォルト目標を選択する（ステップＳ９０１）。そして、選択したデフォルト目標に含まれる連言形の中の文と等価な文を初期条件記憶部１４１と証明済み文記憶部１５２から検索する（ステップＳ９０２）。ここで、デフォルト目標に含まれる連言形の中の文と等価な文とは、デフォルト目標に含まれる連言形の中の文と同一の文の他、デフォルト目標に含まれる連言形の中の文中の変数に値を代入すると同一になる文をいう。
【００６３】
そして、検索結果がある場合、すなわち選択したデフォルト目標に含まれる連言形の中の文と等価な文が初期条件記憶部１４１あるいは証明済み文記憶部１５に存在した場合には（ステップＳ９０３：Ｙｅｓ）、選択したデフォルト目標から検索された文を含む連言形の部分を削除する（ステップＳ９０４）。一方、ステップＳ９０３において検索結果がなしの場合、すなわち選択したデフォルト目標に含まれる連言形の中の文と等価な文が初期条件記憶部１４１と証明済み文記憶部１５のいずれにも存在しない場合には（ステップＳ９０３：Ｎｏ）、デフォルト目標からの文の削除は行われない。
【００６４】
次に、推論実行部１２２は、デフォルト目標に含まれる連言形の中の文と等価な文を連言形で表現した結論を含む推論規則を推論規則記憶部１５１から検索する（ステップＳ９０５）。ここで、推論規則記憶部に格納されている推論規則は、その結論を連言形で表現された形で格納されているとする。そして、検索結果がある場合、すなわちデフォルト目標に含まれる連言形の中の文と等価な文を連言形で表現した結論を含む推論規則が推論規則記憶部１５１に存在する場合には（ステップＳ９０６：Ｙｅｓ）、デフォルト目標の当該文を検索された推論規則の前提部で置換する（ステップＳ９０７）。一方、ステップＳ９０６において検索結果がない場合、すなわちデフォルト目標に含まれる連言形の中の文と等価な文が、連言形で表現した結論を含む推論規則が推論規則記憶部１５１に存在しない場合には（ステップＳ９０６：Ｎｏ）、置換は行わない。
【００６５】
そして、このようなステップＳ９０２からＳ９０７までの処理を、デフォルト目標の中の全ての文に対して実行する（ステップＳ９０８）。デフォルト目標の中の全ての文に対してステップＳ９０２からＳ９０７までの処理を実行したら、ステップＳ９０４でデフォルト目標の中の全ての文が削除されたか否かを判断する（ステップＳ９０９）。
【００６６】
そして、デフォルト目標の中の全ての文が削除されている場合には（ステップＳ９０９：Ｙｅｓ）、そのデフォルト目標を欠陥なしと判定する（ステップＳ９１０）。一方、デフォルト目標の中の全ての文が削除されていない場合には（ステップＳ９０９：Ｎｏ）、そのデフォルト目標を欠陥ありと判定する（ステップＳ９１１）。そして、検証可能な暗号プロトコルのプロトコル実行定義部のすべてのステージに対して、上記ステップＳ９０１からＳ９１０またはＳ９１１までの処理を実行する（ステップＳ９１２）。
【００６７】
次に、推論実行部１２２は、ユーザ目標記憶部１４４からユーザ目標（すなわちゴール部の記述）を選択する（ステップＳ９１３）。個々のユーザ目標も、いくつかの連言形の文(論理積で表現された文)を選言形にしたもの(論理和で表現された文)として表現されている。そして、選択したユーザ目標に含まれる連言形の中の文と等価な文を初期条件記憶部１４１と証明済み文記憶部１５２から検索する（ステップＳ９１４）。
【００６８】
そして、検索結果がある場合、すなわち選択したユーザ目標に含まれる連言形の中の文と等価な文が初期条件記憶部１４１あるいは証明済み文記憶部１５に存在した場合には（ステップＳ９１５：Ｙｅｓ）、選択したユーザ目標から検索された文を含む連言形の部分を削除する（ステップＳ９１６）。一方、ステップＳ９１５において検索結果がなしの場合、すなわち選択したユーザ目標に含まれる連言形の中の文と等価な文が初期条件記憶部１４１と証明済み文記憶部１５のいずれにも存在しない場合には（ステップＳ９１５：Ｎｏ）、ユーザ目標からの文の削除は行われない。
【００６９】
次に、推論実行部１２２は、ユーザ目標に含まれる連言形の中の文と等価な文を連言形で表現した結論を含む推論規則を推論規則記憶部１５１から検索する（ステップＳ９１７）。そして、検索結果がある場合、すなわちユーザ目標に含まれる連言形の中の文と等価な文を連言形で表現した結論を含む推論規則が推論規則記憶部１５１に存在する場合には（ステップＳ９１８：Ｙｅｓ）、ユーザ目標の当該文を検索された推論規則の前提部で置換する（ステップＳ９１９）。この際、結論部と同じ変数に同一の値を代入した上で置換する。
【００７０】
一方、ステップＳ９１８において検索結果がない場合、すなわちユーザ目標に含まれる連言形の文と等価な文を連言形で表現した結論を含む推論規則が推論規則記憶部１５１に存在しない場合には（ステップＳ９１８：Ｎｏ）、置換は行わない。
【００７１】
そして、このようなステップＳ９１４からＳ９１９までの処理を、ユーザ目標の中の全ての文に対して実行する（ステップＳ９２０）。ユーザ目標の中の全ての文に対してステップＳ９１４からＳ９１９までの処理を実行したら、ステップＳ９１６によりユーザ目標の中の全ての文が削除されたか否かを判断する（ステップＳ９２１）。
【００７２】
そして、ユーザ目標の中の全ての文が削除されている場合には（ステップＳ９２１：Ｙｅｓ）、そのユーザ目標を欠陥なしと判定する（ステップＳ９２２）。一方、ユーザ目標の中の全ての文が削除されていない場合には（ステップＳ９２１：Ｎｏ）、そのユーザ目標を欠陥ありと判定する（ステップＳ９２３）。この場合において、さらに推論規則を変更して同様の処理を繰り返してもよい。
【００７３】
このような推論実行部１２２によるデフォルト目標を利用した推論によって、検証可能な暗号プロトコル仕様データ５００のプロトコル実行定義部の記述の欠陥の有無、すなわち安全性の検証が行われ、またユーザ目標を利用した推論によって、検証可能な暗号プロトコル仕様データ５００のゴール部の記述の欠陥の有無、すなわち安全性の検証が行われることになる。 なお、ゴール部の存在しない検証可能な暗号プロトコル仕様データ５００の場合には、上記ステップＳ９１３からＳ９２２またはＳ９２３までのユーザ目標に対する処理はおこなわれない。
【００７４】
そして、推論実行部１２２による推論による検証結果として、暗号プロトコル仕様の安全性あり／なし、プロトコル実行定義部のステージごとの欠陥の有無、ゴール部の欠陥の有無が検証結果出力部１３０によって、表示装置等に出力される。ここで、プロトコル実行定義部の全ステージで欠陥が存在せず、かつゴール部にも欠陥が存在しない場合には、暗号プロトコル仕様の安全性が証明されたことになる。
【００７５】
このように実施の形態１にかかる暗号プロトコル安全性検証装置１００では、汎用的結合可能安全性で定義される理想機能に関するエンティティを含むとともに攻撃者としてのシミュレータに関する記述が存在しない検証可能な暗号プロトコルの安全性検証を形式的検証部１２０で行うので、計算量的証明における暗号プロトコル仕様と形式的検証における暗号プロトコル仕様とを整合性をとった上で、プリミティブな安全性を計算量的証明により確保しつつ、複雑な暗号プロトコルについては形式的検証による機械的な検証処理により安全性検証の労力を軽減することができる。
【００７６】
（実施の形態２）
実施の形態１にかかる暗号プロトコル安全性検証装置１００は、図６のような第１記述部５０１と図７−２に示すような第２記述部５０２を有する暗号プロトコル仕様データ、すなわち予め検証可能となっている暗号プロトコル仕様データを入力して、暗号プロトコルの安全性検証を行っていたが、この実施の形態２にかかる暗号プロトコル安全性検証装置は、入力された暗号プロトコル仕様データから、検証可能な暗号プロトコル仕様データ５００を生成して、生成された検証可能な暗号プロトコル仕様データ５００の安全性検証を行うものである。
【００７７】
図１０は、実施の形態２にかかる暗号プロトコル安全性検証装置の機能的構成を示すブロック図である。本実施の形態にかかる暗号プロトコル安全性検証装置１０００は、図１０に示すように、暗号プロトコル仕様入力処理部１１０と、検証可能暗号プロトコル仕様生成部１０１０と、形式的検証部１２０と、検証結果出力部１３０と、初期条件記憶部１４１と、プロトコル記憶部１４２と、定義記憶部１４３と、ユーザ目標記憶部１４４と、デフォルト目標記憶部１４５と、推論規則記憶部１５１と、証明済み文記憶部１５２とを主に備えた構成となっている。
【００７８】
ここで、形式的検証部１２０、検証結果出力部１３０、初期条件記憶部１４１、プロトコル記憶部１４２、定義記憶部１４３、ユーザ目標記憶部１４４、デフォルト目標記憶部１４５、推論規則記憶部１５１、証明済み文記憶部１５２は、実施の形態１の暗号プロトコル安全性検証装置１００と同様の構成および機能を有している。
【００７９】
暗号プロトコル仕様入力処理部１１０は、暗号プロトコル仕様データを入力する処理部である。入力する暗号プロトコル仕様データは、形式的検証（ＦＶ）におけるプロトコル仕様で記述された第１記述部５０１と、計算量的証明のＵＣにおけるプロトコル仕様で記述された第２記述部とからなる暗号プロトコル仕様であり、ＵＣによる第２記述部が形式的検証と整合性をとって記述されたものでない点で、実施の形態１で入力される検証可能な暗号プロトコル仕様データ５００と異なっている。
【００８０】
検証可能暗号プロトコル仕様生成部１０１０は、暗号プロトコル仕様入力処理部１１０によって入力された暗号プロトコル仕様データから検証可能な暗号プロトコル仕様データ５００を生成する処理部である。検証可能な暗号プロトコル仕様データ５００は、実施の形態１と同様に、形式的検証（ＦＶ）におけるプロトコル仕様で記述された第１記述部５０１と、計算量的証明のＵＣ（Universal Composability）におけるプロトコル仕様に基づいて記述された第２記述部５０２とからなる暗号プロトコル仕様であり、ＵＣにおける仕様と形式的証明における仕様とを整合性をとって記述したものである。
【００８１】
具体的には、検証可能暗号プロトコル仕様生成部１０１０は、入力した暗号プロトコル仕様データの第２記述部のＵＣにおける記述から理想機能のエンティティが付加し、攻撃者としてのシミュレータの記述を削除して理想機能に対する記述に置換することによって、ＵＣにおける仕様と形式的証明における仕様とを整合性をとって記述された検証可能な暗号プロトコル仕様データ５００を生成している。本実施の形態においても、検証可能な暗号プロトコル仕様データ５００の例としては、実施の形態１と同様に、第１記述部５０１は例えば図６で示した記述であり、第２記述部５０２は図７−２で示した記述である。また、本実施の形態でも、検証可能な暗号プロトコル仕様データ５００は、実施の形態１と同様に、初期条件部、定義部、プロトコル実行定義部、ゴール部に分割されて記述されている。
【００８２】
次に、以上のように構成された本実施の形態にかかる暗号プロトコル安全性検証装置１０００による暗号プロトコルの安全性検証処理について説明する。
【００８３】
暗号プロトコル仕様入力処理部１１０により図６に示すような第１記述部５０１と図７−１に示すような第２記述部を有する暗号プロトコル仕様データが入力されると、検証可能暗号プロトコル仕様生成部１０１０によって、入力された暗号プロトコル仕様データから図６に示すような第１記述部５０１と図７−２に示すような第２記述部５０２を有する検証可能な暗号プロトコル仕様データ５００が生成される。そして、この生成された検証可能な暗号プロトコル仕様データ５００に対して形式的検証部１２０によって暗号プロトコルの安全性検証が行われ、検証結果出力部１３０によって検証結果が出力される。
【００８４】
次に、検証可能暗号プロトコル仕様生成部１０１０による検証可能な暗号プロトコル仕様データ５００の生成処理について説明する。図１１は、検証可能暗号プロトコル仕様生成部１０１０による検証可能な暗号プロトコル仕様データ５００の生成処理の手順を示すフローチャートである。
【００８５】
まず、検証可能暗号プロトコル仕様生成部１０１０は、第２記述部に理想機能のエンティティの記述を追加する（ステップＳ１１０１）。なお、第２記述部に最初から理想機能の記述が存在する場合には、かかるステップＳ１１０１は行われない。そして、検証可能暗号プロトコル仕様生成部１０１０は、第２記述部にシミュレータ（敵）Ｓに関する記述部分があるか否かを調べる（ステップＳ１１０２）。そして、シミュレータ（敵）Ｓに関する記述部分がない場合には（ステップＳ１１０２：Ｎｏ）、そのまま処理を抜ける。
【００８６】
一方、シミュレータ（敵）Ｓに関する記述部分がある場合には（ステップＳ１１０２：Ｙｅｓ）、検証可能暗号プロトコル仕様生成部１０１０は、さらに、第２記述部にシミュレータ（敵）Ｓと理想機能との間の情報の授受の記述があるか否かを調べる（ステップＳ１１０３）。そして、シミュレータ（敵）Ｓと理想機能との間の情報の授受の記述がある場合には（ステップＳ１１０３：Ｙｅｓ）、検証可能暗号プロトコル仕様生成部１０１０は、シミュレータ（敵）Ｓと理想機能との間の授受情報を攻撃に利用可能な情報として変換する（ステップＳ１１０４）。シミュレータ（敵）Ｓと理想機能との間の情報の授受の記述がない場合には（ステップＳ１１０３：Ｎｏ）、かかるＳ１１０４の処理は行わない。
【００８７】
次に、検証可能暗号プロトコル仕様生成部１０１０は、第２記述部にシミュレータ（敵）Ｓが理想機能からパーティへのメッセージの即座の配信を要求される記述があるか否かを調べる（ステップＳ１１０５）。そして、シミュレータ（敵）Ｓが理想機能からパーティへのメッセージの即座の配信を要求される記述がある場合には（ステップＳ１１０５：Ｙｅｓ）、かかる記述を理想機能がパーティへメッセージの即座の配信を行う記述に変換する（ステップＳ１１０６）。一方、シミュレータ（敵）Ｓが理想機能からパーティへのメッセージの即座の配信を要求される記述がない場合には（ステップＳ１１０５：Ｎｏ）、かかるＳ１１０６の処理はおこなわれない。
【００８８】
以上のような処理によって、入力された暗号プロトコル仕様データから、図６や図７−１のような形式的検証部１２０によって検証可能な暗号プロトコル仕様データ５００が生成されることになる。この生成された検証可能な暗号プロトコル仕様データ５００の安全性検証処理は、実施の形態１の図８、図９−１および図９−２で説明した処理と同様に行われ、その検証結果も実施の形態１と同様に検証結果出力部１３０によって表示装置等に出力される。
【００８９】
このように実施の形態２にかかる暗号プロトコル安全性検証装置１０００では、入力された暗号プロトコル仕様データから、検証可能な暗号プロトコル仕様データ５００を生成して、生成された検証可能な暗号プロトコル仕様データ５００の安全性検証を行うので、利用者によって計算量的証明における暗号プロトコル仕様と形式的検証における暗号プロトコル仕様との整合性をとることを意識させることなく、プリミティブな安全性を計算量的証明により確保しつつ、複雑な暗号プロトコルについては形式的検証による機械的な検証処理により安全性検証の労力を軽減することができる。
【００９０】
（変形例）
ＵＣの定式化として、シミュレータは現実に暗号プロトコルの実行に関与するパーティと理想機能の間のメッセージを認識できないとする定式化がある。例えば、図１２は、実施の形態２の変形例における定式化によって定義された認証された通信路の理想機能ＦAUTHである。この理想機能は以下のような処理を行う。
【００９１】
あるパーティＰｉから（ｓｅｎｄ，ｓｉｄ，Ｐｊ，ｍ）というメッセージを受信したときは、ｓｉｄが（Ｐｊ，ｓｉｄ‘）の形をしているか否かを判定する。そして、ｓｉｄが（Ｐｊ，ｓｉｄ‘）の形をしている場合には、（Ｐｊ，ｍ）を記録した上で、（ｓｅｎｄ，ｓｉｄ，Ｐｊ，ｍ）を攻撃者であるシミュレータに送信する。一方、ｓｉｄが（Ｐｊ，ｓｉｄ‘）の形をしていなに場合には、理想機能は、この入力を無視する。
【００９２】
一方、理想機能は、攻撃者であるシミュレータからｓｉｄ＝（Ｐｉ，ｓｉｄ’）の形をしたメッセージ（ｄｅｌｉｖｅｒ，ｓｉｄ，Ｐｊ’，ｍ’）を受信したときは、（Ｐｉ‘，ｍ’）が記録されているか否か、または、Ｐｉがｃｏｒｒｕｐｔされているか否かを判定し、もうしそうならば、パーティＰｊ’に対して、（ｓｅｎｔ，ｓｉｄ，ｍ‘）を出力してから停止する。そうでなければ、単に停止する。
【００９３】
この場合、理想機能からパーティへのメッセージの配信は、理想機能自身が行っている。ただし、その配信を行う前に、理想機能は攻撃者であるシミュレータに対して、これから配信を行う内容を通知している。この通知に対して、シミュレータは、メッセージの送信先のパーティの変更やメッセージの内容を改ざんする機会を与えられている。理想機能は、この変更や改ざんがあった場合は、それらに従ってメッセージを配信する。すなわち、理想機能はメッセージの配信に先立ち、その許可をシミュレータに求めており、理想機能はシミュレータが許可したとおりにメッセージを配信しなければならない。
【００９４】
この変形例における検証可能暗号プロトコル生成手段１０１０は、上のような理想機能に対応する第２記述部に対して、理想機能がパーティへのメッセージ配信を行う前にシミュレータにその配信許可を要求してから配信を行う記述は、理想機能がシミュレータの許可を要求することなく配信を行う記述に置換し、シミュレータと理想機能との間で授受された情報は、攻撃時に利用可能な情報と置換する。
【００９５】
次に、検証可能暗号プロトコル仕様生成部１０１０による検証可能な暗号プロトコル仕様データ５００の生成処理について説明する。図１３は、実施の形態２の変形例にかかる検証可能暗号プロトコル仕様生成部１０１０による検証可能な暗号プロトコル仕様データ５００の生成処理の手順を示すフローチャートである。
【００９６】
まず、検証可能暗号プロトコル仕様生成部１０１０は、第２記述部に理想機能のエンティティの記述を追加する（ステップＳ１３０１）。なお、第２記述部に最初から理想機能の記述が存在する場合には、かかるステップＳ１３０１は行われない。そして、検証可能暗号プロトコル仕様生成部１０１０は、第２記述部にシミュレータ（敵）Ｓに関する記述部分があるか否かを調べる（ステップＳ１３０２）。そして、シミュレータ（敵）Ｓに関する記述部分がない場合には（ステップＳ１３０２：Ｎｏ）、そのまま処理を抜ける。
【００９７】
一方、シミュレータ（敵）Ｓに関する記述部分がある場合には（ステップＳ１３０２：Ｙｅｓ）、検証可能暗号プロトコル仕様生成部１０１０は、さらに、第２記述部にシミュレータ（敵）Ｓと理想機能との間の情報の授受の記述があるか否かを調べる（ステップＳ１３０３）。そして、シミュレータ（敵）Ｓと理想機能との間の情報の授受の記述がある場合には（ステップＳ１３０３：Ｙｅｓ）、検証可能暗号プロトコル仕様生成部１０１０は、シミュレータ（敵）Ｓと理想機能との間の授受情報を攻撃に利用可能な情報として変換する（ステップＳ１３０４）。シミュレータ（敵）Ｓと理想機能との間の情報の授受の記述がない場合には（ステップＳ１３０３：Ｎｏ）、かかるＳ１３０４の処理は行わない。
【００９８】
次に、検証可能暗号プロトコル仕様生成部１０１０は、第２記述部にシミュレータ（敵）Ｓが理想機能からパーティへのメッセージの配信の許可を要求される記述があるか否かを調べる（ステップＳ１３０５）。そして、シミュレータ（敵）Ｓが理想機能からパーティへのメッセージの配信の許可を要求される記述がある場合には（ステップＳ１３０５：Ｙｅｓ）、かかる記述を理想機能が許可を要求することなく直接パーティへメッセージを配信する記述に変換する（ステップＳ１３０６）。一方、シミュレータ（敵）Ｓが理想機能からパーティへのメッセージの配信の許可を要求される記述がない場合には（ステップＳ１３０５：Ｎｏ）、かかるＳ１３０６の処理はおこなわれない。
【００９９】
このように実施の形態２の変形例にかかる暗号プロトコル安全性検証装置１０００では、シミュレータは現実に暗号プロトコルの実行に関与するパーティと理想機能の間のメッセージを認識できないとする定式化のＵＣを含む暗号プロトコル仕様データから、検証可能な暗号プロトコル仕様データ５００を生成して、生成された検証可能な暗号プロトコル仕様データ５００の安全性検証を行うので、利用者によって計算量的証明における暗号プロトコル仕様と形式的検証における暗号プロトコル仕様との整合性をとることを意識させることなく、プリミティブな安全性を計算量的証明により確保しつつ、複雑な暗号プロトコルについては形式的検証による機械的な検証処理により安全性検証の労力を軽減することができる。
【０１００】
（実施の形態３）
実施の形態３は、実施の形態１および２で説明した検証可能暗号プロトコル仕様生成手段および形式的検証手段を使用して暗号プロトコルを設計する暗号プロトコル設計装置である。
【０１０１】
図１４は、実施の形態３にかかる暗号プロトコル設計装置の機能的構成を示すブロック図である。本実施の形態にかかる暗号プロトコル設計装置１２００は、図１４に示すように、暗号プロトコル仕様設計部１２１０と、検証可能暗号プロトコル仕様生成部１０１０と、形式的検証部１２０と、検証結果出力部１３０と、暗号プロトコル実行部１２２０と、初期条件記憶部１４１と、プロトコル記憶部１４２と、定義記憶部１４３と、ユーザ目標記憶部１４４と、デフォルト目標記憶部１４５と、推論規則記憶部１５１と、証明済み文記憶部１５２と、暗号プロトコル部品記憶部１２３０と、暗号プロトコル記憶部１２４０とを主に備えた構成となっている。
【０１０２】
ここで、検証可能暗号プロトコル仕様生成部１０１０、形式的検証部１２０、検証結果出力部１３０、初期条件記憶部１４１、プロトコル記憶部１４２、定義記憶部１４３、ユーザ目標記憶部１４４、デフォルト目標記憶部１４５、推論規則記憶部１５１、証明済み文記憶部１５２は、実施の形態１の暗号プロトコル安全性検証装置１００と同様の構成および機能を有している。
【０１０３】
暗号プロトコル部品記憶部１２３０は、暗号プロトコル仕様データを構成部品を記憶するＨＤＤやメモリなどの記憶媒体である。暗号プロトコル部品記憶部１２３０は、具体的には形式的検証（ＦＶ）におけるプロトコル仕様で記述された第１記述部５０１の構成部品である第１記述部品と、計算量的証明のＵＣにおけるプロトコル仕様で記述された第２記述部の構成部品である第２記述部品が記憶されている。第１記述部品としては、実施の形態１で説明した図６に示す仕様記述を構成する文や語句などが例としてあげられる。また、第２記述部品としては、形式的検証における仕様と整合性をとっていない状態の図７−１に示す仕様記述を構成する文や語句などが例としてあげられる。
【０１０４】
暗号プロトコル仕様設計部１２１０は、暗号プロトコル部品記憶部１２３０に記憶されている第１記述部品と第２記述部品を読み出して、読み出した第１記述部品と第２記述部品から暗号プロトコル仕様データを生成する処理部である。具体的には、暗号プロトコル仕様設計部１２１０は、利用者によって指定された第１記述部品と第２記述部品を暗号プロトコル部品記憶部１２３０から読み出して、第１記述部品と第２記述部品を利用者の指定あるいは任意に組み合わせて暗号プロトコル仕様データの記述を生成する。このように生成された暗号プロトコル仕様データは、暗号プロトコル仕様生成部１０１０によって第２記述部を例えば図７−２に示すような形式的検証（ＦＶ）と整合性ととった検証可能な暗号プロトコル仕様データ５００が生成され、形式的検証部１２０によって安全性の検証が行われる。また、生成された暗号プロトコル仕様データは暗号プロトコル実行部１２２０にも受け渡される。
【０１０５】
暗号プロトコル実行部１２２０は、形式的検証部１２０によって安全性が証明された検証可能な暗号プロトコル仕様データ５００から利用者の指示入力等に従って実行可能な暗号プロトコルを生成し、生成した実行可能な暗号プロトコルを暗号プロトコルに保存する処理部である。
【０１０６】
暗号プロトコル記憶部１２４０は、暗号プロトコル実行部１２２０によって生成された実行可能な暗号プロトコルを記憶するＨＤＤやメモリ等の記憶媒体である。
【０１０７】
次に、以上のように構成された本実施の形態にかかる暗号プロトコル設計装置１２００による暗号プロトコルの設計処理について説明する。図１５は、暗号プロトコル設計装置１２００による暗号プロトコルの設計処理の手順を示すフローチャートである。
【０１０８】
まず、暗号プロトコル仕様設計部１２１０は、利用者の指定等により暗号プロトコル部品記憶部１２３０から生成に必要な第１記述部品、第２記述部品を読み出す（ステップＳ１５０１）。そして、暗号プロトコル仕様設計部１２１０は、読み出した第１記述部品、第２記述部品を利用者の指示等により組み合わせて暗号プロトコル仕様データを生成する（ステップＳ１５０２）。
【０１０９】
次に、検証可能暗号プロトコル仕様生成部１０１０によって、生成された暗号プロトコル仕様データから検証可能な暗号プロトコル仕様データ５００を生成する（ステップＳ１５０３）。ここで、検証可能暗号プロトコル仕様生成部１０１０による検証可能な暗号プロトコル仕様データ５００の生成処理については、図１１で説明した実施の形態２と同様に行われる。すなわち、暗号プロトコル仕様データの第２記述部のＵＣにおける記述から理想機能のエンティティが付加し、攻撃者としてのシミュレータの記述を削除して理想機能に対する記述に置換（シミュレータ（敵）Ｓと理想機能との間の情報の授受の記述をシミュレータ（敵）Ｓと理想機能との間の授受情報を攻撃に利用可能な情報として変換し、シミュレータ（敵）Ｓが理想機能から即座の配信を要求される記述を理想機能が即座の配信を行う記述に変換）することによって、ＵＣにおける仕様と形式的証明における仕様とを整合性をとって記述された検証可能な暗号プロトコル仕様データ５００を生成する。
【０１１０】
次に、検証可能な暗号プロトコル仕様データ５００が生成されたら、形式的検証部１２０によって、この検証可能な暗号プロトコル仕様データ５００の安全性検証を行う（ステップＳ１５０４）。ここで、形式的検証部１２０による検証可能な暗号プロトコル仕様データ５００の安全性検証の処理については、図８、図９−１及び図９−２で説明した実施の形態１および２と同様に行われる。
【０１１１】
形式的検証部１２０による安全性検証処理が完了したら、検証結果出力部１３０はその検証結果を出力するとともに、形式的検証部１２０によって検証可能な暗号プロトコル仕様データ５００に欠陥がないと証明されたか否か、すなわち安全性が証明されたか否かを判断する（ステップＳ１５０５）。そして、検証可能な暗号プロトコル仕様データ５００に欠陥がある場合には（ステップＳ１５０５：Ｎｏ）、ステップＳ１５０１からＳ１５０４までの処理を繰り返す。
【０１１２】
一方、ステップＳ１５０５において、検証可能な暗号プロトコル仕様データ５００に欠陥がない場合、すなわち安全性が証明された場合には（ステップＳ１５０５：Ｙｅｓ）、暗号プロトコル実行部１２２０によって検証可能な暗号プロトコル仕様データ５００から利用者の指示等により実行可能な暗号プロトコルを生成して暗号プロトコル記憶部１２４０に保存する（ステップＳ１５０６）。これにより、安全性が証明された暗号プロトコルが設計されることになる。
【０１１３】
このように実施の形態３にかかる暗号プロトコル設計装置１２００では、第１記述部品と第２記述部品から暗号プロトコル仕様データを生成し、生成した暗号プロトコル仕様データから汎用的結合可能性証明で定義される理想機能に関するエンティティを含むとともに攻撃者としてのシミュレータに関する記述が存在しない検証可能な暗号プロトコルを生成してその安全性検証を行い、安全性が証明された暗号プロトコル仕様データに基づいて実現可能な暗号プロトコルを生成しているので、計算量的証明における暗号プロトコル仕様と形式的検証における暗号プロトコル仕様とを整合性をとった上で、プリミティブな安全性を計算量的証明により確保しつつ、複雑な暗号プロトコルについては形式的検証による機械的な検証処理により安全性検証の労力を軽減することともに、確実な暗号プロトコルを設計することができる。
【０１１４】
実施の形態１および２の暗号プロトコル安全性検証装置、実施の形態３の暗号プロトコル設計装置は、ＣＰＵなどの制御装置と、ＲＯＭ（Read Only Memory）やＲＡＭなどの記憶装置と、ＨＤＤ、ＣＤドライブ装置などの外部記憶装置と、ディスプレイ装置などの表示装置と、キーボードやマウスなどの入力装置を備えており、通常のコンピュータを利用したハードウェア構成となっている。
【０１１５】
実施の形態１および２の暗号プロトコル安全性検証装置で実行される暗号プロトコル安全性検証プログラム、実施の形態３の暗号プロトコル設計装置で実行される暗号プロトコル設計プログラムは、インストール可能な形式又は実行可能な形式のファイルでＣＤ−ＲＯＭ、フレキシブルディスク（ＦＤ）、ＣＤ−Ｒ、ＤＶＤ（Ｄｉｇｉｔａｌ Ｖｅｒｓａｔｉｌｅ Ｄｉｓｋ）等のコンピュータで読み取り可能な記録媒体に記録されて提供される。
【０１１６】
また、実施の形態１および２の暗号プロトコル安全性検証装置で実行される暗号プロトコル安全性検証プログラム、実施の形態３の暗号プロトコル設計装置で実行される暗号プロトコル設計プログラムを、インターネット等のネットワークに接続されたコンピュータ上に格納し、ネットワーク経由でダウンロードさせることにより提供するように構成しても良い。また、実施の形態１および２の暗号プロトコル安全性検証装置で実行される暗号プロトコル安全性検証プログラム、実施の形態３の暗号プロトコル設計装置で実行される暗号プロトコル設計プログラムをインターネット等のネットワーク経由で提供または配布するように構成しても良い。
【０１１７】
また、実施の形態１および２の暗号プロトコル安全性検証装置で実行される暗号プロトコル安全性検証プログラム、実施の形態３の暗号プロトコル設計装置で実行される暗号プロトコル設計プログラムを、ＲＯＭ等に予め組み込んで提供するように構成してもよい。
【０１１８】
実施の形態１および２の暗号プロトコル安全性検証装置で実行される暗号プロトコル安全性検証プログラムは、上述した各部（暗号プロトコル仕様入力処理部１１０、検証可能暗号プロトコル仕様生成部１０１０、形式的検証部１２０、検証結果出力部１３０）を含むモジュール構成となっており、実際のハードウェアとしてはＣＰＵ（プロセッサ）が上記記憶媒体から暗号プロトコル安全性検証プログラムを読み出して実行することにより上記各部が主記憶装置上にロードされ、暗号プロトコル仕様入力処理部１１０、検証可能暗号プロトコル仕様生成部１０１０、形式的検証部１２０、検証結果出力部１３０が主記憶装置上に生成されるようになっている。
【０１１９】
また、実施の形態３の暗号プロトコル設計装置で実行される暗号プロトコル設計プログラムは、上述した各部（暗号プロトコル仕様設計部１２１０、検証可能暗号プロトコル仕様生成部１０１０、形式的検証部１２０、検証結果出力部１３０、暗号プロトコル実行部）を含むモジュール構成となっており、実際のハードウェアとしてはＣＰＵ（プロセッサ）が上記記憶媒体から暗号プロトコル安全性検証プログラムを読み出して実行することにより上記各部が主記憶装置上にロードされ、暗号プロトコル仕様設計部１２１０、検証可能暗号プロトコル仕様生成部１０１０、形式的検証部１２０、検証結果出力部１３０、暗号プロトコル実行部が主記憶装置上に生成されるようになっている。
【０１２０】
なお、本発明は、上記実施の形態そのままに限定されるものではなく、実施段階ではその要旨を逸脱しない範囲で構成要素を変形して具体化することができる。また、上記実施の形態に開示されている複数の構成要素の適宜な組み合わせにより、種々の発明を形成することができる。例えば、実施の形態に示される全構成要素からいくつかの構成要素を削除してもよい。さらに、異なる実施の形態にわたる構成要素を適宜組み合わせても良い。
【図面の簡単な説明】
【０１２１】
【図１】実施の形態１にかかる暗号プロトコル安全性検証装置の機能的構成を示すブロック図である。
【図２】ＵＣの概要を説明するための模式図である。
【図３】署名に関する理想機能である署名理想機能ＦSIGの一例を示す説明図である。
【図４】プロトコルπSの一例を示す説明図である。
【図５】実施の形態１にかかる暗号プロトコル安全検証装置で入力される検証可能な暗号プロトコル仕様データ５００のデータ構造を示す模式図である。
【図６】検証可能な暗号プロトコル仕様データ５００の第１記述部５０１の例を示す説明図である。
【図７−１】暗号プロトコル仕様における理想機能を使用した記述例を示す説明図である。
【図７−２】検証可能な暗号プロトコル仕様データ５００の第２記述部５０２のプロトコル実行定義部の例を示す説明図である。
【図８】実施の形態１の暗号プロトコルの安全性検証処理の手順を示すフローチャートである。
【図９−１】推論実行部１２２による推論実行処理の手順を示すフローチャートである。
【図９−２】推論実行部１２２による推論実行処理の手順を示すフローチャート（図９−１の続き）である。
【図１０】実施の形態２にかかる暗号プロトコル安全性検証装置の機能的構成を示すブロック図である。
【図１１】検証可能暗号プロトコル仕様生成部１０１０による検証可能な暗号プロトコル仕様データ５００の生成処理の手順を示すフローチャートである。
【図１２】認証機能を持ったチャンネルの理想機能である認証チャンネル理想機能ＦAUTHの一例を示す説明図である。
【図１３】実施の形態２の変形例における検証可能暗号プロトコル仕様生成部１０１０による検証可能な暗号プロトコル仕様データ５００の生成処理の手順を示すフローチャートである。
【図１４】実施の形態３にかかるい暗号プロトコル設計装置の機能的構成を示すブロック図である。
【図１５】暗号プロトコル設計装置１２００による暗号プロトコルの設計処理の手順を示すフローチャートである。
【符号の説明】
【０１２２】
１００，１０００ 暗号プロトコル安全性検証装置
１１０ 暗号プロトコル仕様入力処理部
１２０ 形式的検証部
１２１ デフォルト目標生成部
１２２ 推論実行部
１２３ 解析部
１４１ 初期条件記憶部
１４２ プロトコル記憶部
１４３ 定義記憶部
１４４ ユーザ目標記憶部
１４５ デフォルト目標記憶部
１５１ 推論規則記憶部
１５２ 証明済み文記憶部
１０１０ 検証可能暗号プロトコル仕様生成部
１２００ 暗号プロトコル設計装置
１２１０ 暗号プロトコル仕様設計部
１２２０ 暗号プロトコル実行部
１２３０ 暗号プロトコル部品記憶部
１２４０ 暗号プロトコル記憶部
【技術分野】
【０００１】
本発明は、暗号プロトコルに欠陥があるか否かの安全性を検証する暗号プロトコル安全性検証装置、暗号プロトコル安全性検証方法、暗号プロトコル安全性検証プログラムおよび、暗号プロトコルの安全性を検証して暗号プロトコルを設計する暗号プロトコル設計装置、暗号プロトコル設計方法および暗号プロトコル設計プログラムに関する。
【背景技術】
【０００２】
暗号学的な手法を利用した暗号プロトコルの安全性を検証する手法としては、従来から形式的検証（ＦＶ：Formal Verification）と計算量理論的証明（Complex-Theoretic Proof）が知られている。
【０００３】
形式的検証は、プロトコルの正当性を暗号プロトコル仕様の記述から形式的に検証する手法である（例えば、非特許文献１参照）。 計算量理論的証明は、プロトコルの安全性を破ることを数学的な問題の困難性に帰着させる手法である。
【０００４】
そして、計算量理論的証明としてmodular アプローチという検証手法が提案されている。このmodular アプローチは、ある仮定の下でプロトコルの安全性を証明しておき、次に、その仮定部分を現実的な状況でも安全なプロトコルに変換するものである。このmodular アプローチに基づいて暗号プロトコルの安全性検証を行う手法として、近年、汎用的結合可能性（ＵＣ：Universal Composability）による証明が提案されている。
【０００５】
このＵＣによる証明は、シミュレーションパラダイムに基づき定式化されており、あるプロトコルπが理想機能(ideal functionality)Ｆを安全に実現しているとは、現実モデルと理想プロセスの２つの系を確率的多項式時間Turing 機械Ｅ(以下、環境Ｅという) が識別できないこと、厳密には、現実モデルの任意の敵Ａに対して、理想プロセスのシミュレータＳが存在し、いかなる環境Ｅによっても２つの系は識別できないことと定義されている。ＵＣでは、あるプロトコルπ が理想機能Ｆを安全に実現していることを証明することができれば、そのプロトコルπをサブルーチンとして呼び出すプロトコルρを実行した場合にも、プロトコルρの中でプロトコルπが何回呼び出されても、プロトコルπの安全性は保たれることがUniversal composability theoremとして証明されている（例えば、非特許文献２参照）。
【０００６】
【非特許文献１】Abadi, M., Rogaway, P.: Reconciling Two Views of Cryptography. In: IFIP International Conference on Theoretical Computer Science. (2000)
【非特許文献２】Canetti, R.: Universally Composable Security: A New Paradigm for Cryptographic Protocols. In: FOCS’01, IEEE(2001) 136−145
【発明の開示】
【発明が解決しようとする課題】
【０００７】
しかしながら、このような従来の暗号プロトコル安全性検証の手法には、以下のような問題がある。形式的検証では、複雑な暗号プロトコルの検証が計算量が多くなり困難であり、またプリミティブの安全性の仮定が必要となってくる。
【０００８】
また、計算量理論的証明では、安全性証明が与えられている暗号プロトコルは限られており、暗号プロトコルに修正を加えると、その修正がわずかなものであっても新たな安全性の証明を付与しなければならず、暗号プロトコルの安全性検証に多大な労力が必要となる。
【０００９】
ＵＣ等のmodular アプローチでは、ある仮定の下でプロトコルの安全性を証明しておき、次に、その仮定部分を現実的な状況でも安全なプロトコルに変換するという構造的な証明方法によって暗号プロトコルの安全性証明の労力を軽減しているが、複雑な暗号プロトコルでは安全性証明の労力を効率的に行うことができない。
【００１０】
本発明は、上記に鑑みてなされたものであって、暗号プロトコルのプリミティブな安全性を確保しつつ、複雑な暗号プロトコルでも安全性検証の労力を軽減することができる暗号プロトコル安全性検証装置、暗号プロトコル設計装置、暗号プロトコル安全性検証方法、暗号プロトコル設計方法、暗号プロトコル安全性検証プログラムおよび暗号プロトコル設計プログラムを提供することを目的とする。
【課題を解決するための手段】
【００１１】
上述した課題を解決し、目的を達成するために、本発明は、現実に暗号プロトコルの実行に関与するパーティに関する処理が記述された第１記述部と、汎用結合可能安全性で定義される理想のプロトコルと対応し、現実に暗号プロトコルの実行に関与するパーティおよび現実に暗号プロトコルの実行に関与しない第１の仮想のエンティティに関する処理が記述され、現実に暗号プロトコルの実行に関与しない第２の仮想のエンティティに関する記述を含まない第２記述部とを含む検証可能な暗号プロトコル仕様データであって、前記第１の仮想のエンティティは、前記理想のプロトコルにおける理想機能に対応し、前記第２の仮想のエンティティは、前記理想のプロトコルにおけるシミュレータに対応する検証可能な暗号プロトコル仕様データにおける前記パーティおよび第１の仮想のエンティティに関する処理の欠陥の有無を、前記検証可能な暗号プロトコル仕様データの記述に基づいて検証する形式的検証手段を備えたことを特徴とする暗号プロトコル安全性検証装置である。
【００１２】
また、本発明は、現実に暗号プロトコルの実行に関与するパーティに関する処理の記述である第１記述部を構成する第１記述部品と、前記第１記述部により安全に実現されることが証明されている、現実に暗号プロトコルの実行に関与するパーティに関する処理と現実に暗号プロトコルの実行に関与しない第１の仮想のエンティティと第２の仮想のエンティティに関する処理の記述である第２記述部を構成する第２記述部品とを記憶する暗号プロトコル部品記憶手段と、前記暗号プロトコル部品記憶手段に記憶された前記第２記述部品と新たに追加した前記第１記述部とを含む暗号プロトコル仕様データを生成する暗号プロトコル仕様設計手段と、前記暗号プロトコル仕様設計手段によって生成された前記暗号プロトコル仕様データに対して、前記第２記述部に対して前記第２の仮想のエンティティに関する記述を削除して、検証可能な暗号プロトコル仕様データを生成する検証可能暗号プロトコル生成手段と、前記検証可能暗号プロトコル仕様生成手段によって生成された前記検証可能な暗号プロトコル仕様データにおける前記パーティおよび前記第１の仮想のエンティティの両方に関する処理の欠陥の有無を、前記検証可能な暗号プロトコル仕様データの記述に基づいて検証する形式的検証手段と、前記形式的検証手段によって欠陥なしと証明された前記検証可能な暗号プロトコル仕様データに基づいて実現可能な暗号プロトコルを生成する暗号プロトコル実行手段と、を備えたことを特徴とする暗号プロトコル設計装置である。
【００１３】
また、本発明は、上記装置に対応する方法およびプログラムである。
【発明の効果】
【００１４】
本発明にかかる暗号プロトコル安全性検証装置、暗号プロトコル安全性検証方法および暗号プロトコル安全性検証プログラムでは、汎用的結合可能安全性で定義される理想機能に関するエンティティを含むとともに攻撃者としてのシミュレータに関する記述が存在しない検証可能な暗号プロトコルの安全性検証を行っている。このため、本発明によれば、計算量的証明における暗号プロトコル仕様と形式的検証における暗号プロトコル仕様とを整合性をとった上で、プリミティブな安全性を計算量的証明により確保しつつ、複雑な暗号プロトコルについては形式的検証による機械的な検証処理により安全性検証の労力を軽減することができるという効果を奏する。
【００１５】
また、本発明にかかる暗号プロトコル設計装置、暗号プロトコル設計方法および暗号プロトコル設計プログラムでは、暗号プロトコル仕様データを設計し、設計した暗号プロトコル仕様データから汎用的結合可能安全性で定義される理想機能に関するエンティティを含むとともに攻撃者としてのシミュレータに関する記述が存在しない検証可能な暗号プロトコルを生成してその安全性検証を行っている。そして、安全性が証明された暗号プロトコル仕様データに基づいて実現可能な暗号プロトコルを生成するので、本発明によれば、計算量的証明における暗号プロトコル仕様と形式的検証における暗号プロトコル仕様とを整合性をとった上で、プリミティブな安全性を計算量的証明により確保しつつ、複雑な暗号プロトコルについては形式的検証による機械的な検証処理により安全性検証の労力を軽減することともに、確実な暗号プロトコルを設計することができるという効果を奏する。
【発明を実施するための最良の形態】
【００１６】
以下に添付図面を参照して、この発明にかかる暗号プロトコル安全性検証装置、暗号プロトコル設計装置、暗号プロトコル安全性検証方法、暗号プロトコル設計方法、暗号プロトコル安全性検証プログラムおよび暗号プロトコル設計プログラムの最良な実施の形態を詳細に説明する。
【００１７】
（実施の形態１）
実施の形態１にかかる暗号プロトコル安全性検証装置は、現実に暗号プロトコルの実行に関与するパーティに関する処理が記述された第１記述部と、汎用的結合可能安全性で定義される理想機能に関するエンティティを含むとともに攻撃者としてのシミュレータに関する記述が存在せず、現実に暗号プロトコルの実行に関与するパーティに関する処理と現実に暗号プロトコルの実行に関与しない第１の仮想のエンティティに関する処理が記述された第２記述部とを含む検証可能な暗号プロトコル仕様データを入力して、当該暗号プロトコル仕様データの安全性を検証するものである。
【００１８】
図１は、実施の形態１にかかる暗号プロトコル安全性検証装置の機能的構成を示すブロック図である。本実施の形態にかかる暗号プロトコル安全性検証装置１００は、図１に示すように、暗号プロトコル仕様入力処理部１１０と、形式的検証部１２０と、検証結果出力部１３０と、初期条件記憶部１４１と、プロトコル記憶部１４２と、定義記憶部１４３と、ユーザ目標記憶部１４４と、デフォルト目標記憶部１４５と、推論規則記憶部１５１と、証明済み文記憶部１５２とを主に備えた構成となっている。
【００１９】
暗号プロトコル仕様入力処理部１１０は、検証可能な暗号プロトコル仕様データの入力処理をおこなう処理部である。検証可能な暗号プロトコル仕様データは、形式的検証（ＦＶ）におけるプロトコル仕様で記述された第１記述部と、計算量的証明のＵＣ（Universal Composability）におけるプロトコル仕様に基づいて記述された第２記述部とからなる暗号プロトコル仕様である。第２記述部では、暗号プロトコルが単にＵＣにおけるプロトコル仕様で記述されているのではなく、ＵＣにおける記述から第１の仮想のエンティティとしての理想機能が付加され、第２の仮想のエンティティとしての攻撃者であるシミュレータの記述が含まれていないものとなっている。すなわち、ＵＣにおける仕様と形式的証明における仕様とを整合性をとって記述して、暗号プロトコルによるプリミティブな安全性を確保しつつ形式的証明による機械的な安全性検証が可能な暗号プロトコル仕様となっている。この暗号プロトコル仕様データには、初期条件部、定義部、プロトコル実行定義部、ゴール部に分割されて記述されている。
【００２０】
形式的検証部１２０は、入力された上記検証可能な暗号プロトコル仕様データに記述された暗号プロトコル仕様に対し形式的検証（ＦＶ）によって安全性の検証を行う処理部であり、後述する第１記述部において現実に暗号プロトコルの実行に関与するパーティおよび第１記述部および第２記述部における現実に暗号プロトコルの実行に関与しない第１の仮想のエンティティの両方に関する処理の欠陥の有無を検証する。形式的検証部１２０は、図１に示すように、プロトコル解析部１２３とデフォルト目標生成部１２１と推論実行部１２２とを有している。
【００２１】
解析部１２３は、検証可能な暗号プロトコル仕様データを解析して、初期条件部、定義部、プロトコル実行定義部、ゴール部を抽出し、初期条件部の記述を初期条件記憶部１４１に、定義部を定義記憶部１４２にそれぞれ保存する処理部である。また、解析部１２３は、検証可能な暗号プロトコル仕様データを解析して、ゴール部を後ろ向き推論において証明すべき目標となる文をユーザ目標としてユーザ目標記憶部１４４に保存する。
【００２２】
デフォルト目標生成部１２１は、検証可能な暗号プロトコル仕様データにおけるプロトコル実行定義部の各段階であるステージの上記パーティおよび仮想パーティの両方に関する処理の記述から後ろ向き推論において証明すべき目標となる文であるデフォルト目標をステージごとに設定してデフォルト目標記憶部１４５に保存する処理部である。ここで、デフォルト目標としては、例えば、各ステージにおいて、送信者がそのメッセージを送信することができたか、受信者がそのメッセージの暗号化部分を復号化できたか、受信者がそのメッセージの暗号化されたあるいはハッシュされたフィールドをどのパーティが伝達したかを決定可能か、受信者はそのメッセージの送信にバインドされた関連文を信じる根拠を有するか等の文が該当する。
【００２３】
推論実行部１２２は、デフォルト目標の文およびユーザ目標の文と、初期条件記憶部１４１あるいは証明済み文記憶部１５２と推論規則記憶部１５１に格納されている推論規則から後向き推論を行って検証可能な暗号プロトコル仕様データに欠陥があるか否か、すなわち暗号プロトコルの安全性を検証する処理部である。具体的には、推論実行部１２２は、プロトコル実行定義部のステージ順に、デフォルト目標の文と等価な文が、検証の初期段階で正しいことを仮定された文を記録している初期条件記憶部１４１あるいは現ステージより以前のステージに対する検証の過程において正しいことが検証された文を記憶している証明済み文記憶部１５２に存在するか否かを検索する。また、推論実行部１２２は、ユーザ目標の文と等価な文が初期条件記憶部１４１あるいは証明済み文記憶部１５２に存在するか否かを検索する。そして、推論実行部１２２は、このような処理を全てのステージのデフォルト目標における全ての文、およびユーザ目標における全ての文について等価な文が初期条件記憶部１４１あるいは証明済み文記憶部１５２に存在した場合に、暗号プロトコルは欠陥なしとしてその安全性を証明する。
【００２４】
検証結果出力部１３０は、推論実行部１２２による暗号プロトコルの安全性の検証結果（安全性あり／なし）をディスプレイ装置などの表示装置やプリンタ装置等に出力する処理部である。
【００２５】
初期条件記憶部１４１は、解析部１２３により暗号プロトコル仕様データから抽出された初期条件部の記述内容、すなわち検証の初期段階で正しいことを仮定された文を保存するものである。プロトコル記憶部１４２は、解析部１２３により暗号プロトコル仕様データから抽出されたプロトコル実行定義部の記述内容を保存するものである。定義記憶部１４３は、解析部１２３により暗号プロトコル仕様データから抽出された定義部の記述内容を保存するものである。ユーザ目標記憶部１４４は、解析部１２３により暗号プロトコル仕様データから抽出されたゴール部の記述内容を保存するものである。
【００２６】
デフォルト目標記憶部１４５は、デフォルト目標生成部１２１によって上述したデフォルト目標を保存するものである。
【００２７】
推論規則記憶部１５１は、前提部や連言形で表現された結論部を有する既存の推論規則が保存されたものであり、本実施の形態では、ＧＮＹ（Gong-Needham-Yahalom） logicから派生した証明推論を定式化した規則であるＢＧＮＹ２の推論規則が保存されている。なお、本実施の形態では、推論実行部１２２が行う後向き推論に対応してＢＧＮＹ２の推論規則が推論規則記憶部１５１に保存されているが、これに限定されるものではなく、実行する推論の手法に応じて任意の推論規則を推論規則記憶部１５１に保存することができる。
【００２８】
証明済み文記憶部１５２は、推論実行部１２２により検証の過程において現ステージより以前のステージで既に欠陥無し（真である）と証明された文を記憶したものである。
【００２９】
これらの初期条件記憶部１４１、プロトコル記憶部１４２、定義記憶部１４３、ユーザ目標記憶部１４４、デフォルト目標記憶部１４５、推論規則記憶部１５１、証明済み文記憶部１５２は、メモリ、ＨＤＤ（Ｈａｒｄ Ｄｉｓｋ Ｄｒｉｖｅ）等の記憶媒体である。
【００３０】
次に、汎用的結合可能性（以下、「ＵＣ」という）の概要を説明する。図２は、ＵＣの概要を説明するための模式図である。図２には、現実にプロトコル実行に関与するパーティＰi間、パーティＰiと攻撃者である敵Ａとのメッセージの授受などをプロトコルπに従って行う現実モデルの系と、この現実モデルに対応して、現実にプロトコル実行に関与するパーティＰi間、攻撃者としてのシミュレータＳとのメッセージの授受などを現実にプロトコル実行に関与しない第１の仮想のエンティティである理想機能Ｆを利用して行う理想プロセスの系とを示している。
【００３１】
ＵＣでは、あるプロトコルπが理想機能（ideal functionality）Ｆを安全に実現しているとは、現実モデルと理想プロセスの２つの系を確率的多項式時間チューリング機械（ＰＰＴ）（以下、「環境Ｅ」という）が識別できないことと定義される。すなわち、現実モデルの任意の敵Ａに対して、理想プロセスのあるシミュレータＳが存在し、いかなる環境Ｅによっても２つの系は識別できない。ＵＣでは、あるプロトコルπが理想機能Ｆを安全に実現していることが証明できれば、そのプロトコルをサブルーチンとして呼び出すプロトコルρを実行した場合にも、プロトコルπがρの中で何回呼び出されても、プロトコルπの安全性は保たれることが証明できる（universal composability theorem）。
【００３２】
ＵＣには、いくつかの定式化があるが、そのうちのひとつの定式化では、シミュレータＳは、理想機能Ｆと各パーティＰiの間で授受されるメッセージの宛先を読むことができるが、そのメッセージの中身までは見ることができない。さらに、シミュレータＳ（敵）は、理想機能Ｆから依頼されてパーティＰiへメッセージの配送を即座に行う。ただし、依頼されても配信しないこともできる。さらに、依頼されていないメッセージを配信することもできる。
【００３３】
また、ＵＣの別の定式化では、理想機能ＦとパーティＰiの間のメッセージの授受はシミュレータを介さず、直接行われる。この場合、シミュレータＳは、理想機能ＦとパーティＰiの間で授受されるメッセージについて、そのパーティがｃｏｒｒｕｐｔされていない限り認識することはできない。ただし、理想機能Ｆが、その仕様上明示的にシミュレータＳに対してメッセージ配信の許可を場合には、シミュレータＳはそのメッセージの内容を知ることができる。
【００３４】
ＵＣでは、暗号プロトコル（またはその一部）は理想機能Ｆと等価である。ここで等価とは、現実モデルにおいて敵Ａが行う任意の攻撃は、理想プロセスにおいてシミュレータＳが行う攻撃と計算量的に識別できないというものである。従って、理想機能Ｆが暗号プロトコルのメッセージの授受や計算の詳細を隠蔽しメッセージの中身を秘匿する仕様になっているならば、現実モデルにおいて、敵Ａがいくらそれら詳細な情報を集めたところで、少なくともその理想機能で記述されている暗号プロトコルの部分に関して、シミュレータＳから見えていない情報を使ったからといって、シミュレータができない攻撃ができるわけではない。
【００３５】
図３は、署名に関する理想機能である署名理想機能ＦSIGの一例を示す説明図である。署名理想機能ＦSIGでは、敵としてのシミュレータＳが検証鍵を付与することが特徴となっている。Ｐiは、現実にプロトコル実行に関与しない仮想的なパーティである。
【００３６】
これに対し、形式的検証（ＦＶ）におけるプロトコルでは、明示的に敵Ｓが仕様記述中には現れてこないので、形式的検証を行う形式的検証部１２０に理想機能を含む仕様記述を入力する際には、検証手法の差異に対する考慮が必要となってくる。本実施の形態では、検証可能な暗号プロトコル仕様として、理想機能Ｆを使用した第２記述部を、シミュレータに関する処理を削除して、理想機能がシミュレータに代わって処理を行う記述にしたプロトコルとしている。
【００３７】
また、署名検証において受理するか拒否するかを決定するのが敵Ｓの役割になっている。敵Ｓからは理想機能ＦSIGの内部の処理は知ることができないが、理想機能ＦSIGが他のパーティと授受するメッセージはシミュレータＳに知られてしまうと定式化されている。
【００３８】
また、理想機能ＦSIGを実現するプロトコル署名スキームＳ＝（ｇｅｎ，ｓｉｇ，ｖｅｒ）に対して、プロトコルπSを図４に示すように定義する。このとき、「スキームＳが適応性選択文書攻撃に対する存在的偽造不可能な署名スキームであることと、プロトコルπSが理想機能ＦSIGを安全に実現することは等価であることが知られている。Ｐiは、現実にプロトコル実行に関与するパーティである。
【００３９】
図５は、実施の形態１にかかる暗号プロトコル安全性検証装置で入力される検証可能な暗号プロトコル仕様データのデータ構造を示す模式図である。図５に示すように、検証可能な暗号プロトコル仕様データ５００には、第１記述部５０１と第２記述部５０２とから構成され、第１記述部５０１には形式的検証（ＦＶ）におけるプロトコル仕様で、現実モデルのプロトコルが記述される。一方、第２記述部５０２では、第１記述部５０１の現実モデルのプロトコルπに対応して理想機能Ｆを利用したプロトコル仕様の記述から、シミュレータＳの処理に関する記述を理想機能がシミュレータに代わって処理を行う記述にしたプロトコルが記述される。
【００４０】
図６は、検証可能な暗号プロトコル仕様データ５００の第１記述部５０１の例を示す説明図である。図６の例では、電子署名を利用した相互認証プロトコルＩＳＯ／ＩＥＣ ９７９８−３の初期バーションの仕様をＩＳＬ２（Interface Specification Language, Version 2）を拡張した言語で記述したものを示してある。暗号プロトコル仕様データは、図６に示すように、定義部、初期条件部、プロトコル実行定義部、ゴール部から構成されており、現実に暗号プロトコル実行に関与するパーティに関する処理が記述されている。
【００４１】
本来、ＩＳＬ２における電子署名の記述仕様は、［ｘ］（ｆ，ｈ）（ｋ）のように定義される。かかる定義は、署名を伴っているメッセージｘを表しており、その署名は、ｘにハッシュ関数ｈを施した上で暗号化関数ｆで暗号化して得られることを示している。ここで、ｋは暗号鍵である。しかしながら、安全性証明が与えられている電子署名方式の多くは、より複雑な形をしており、上のような形で表現されない。また、メッセージと切り離して電子署名だけを送信したい場合、その記述をすることができない。そこで、本実施の形態では、暗号プロトコル仕様記述言語の記述能力を向上させるため、図６のように記述している。
【００４２】
図６の例では、定義部で、署名関数（ＳＩＧＮ ＦＵＮＣＴＩＯＮＳ）がＳｉｇ、検証関数（ＶＥＲＩＦＹ ＦＵＮＣＴＩＯＮＳ）がＶｅｒ、鍵生成関数（ＧＥＮＫＥＹＳ ＦＵＮＣＴＩＯＮＳ）がＧであることを定義している。ここで、定義部の記述において、
Ｓｉｇ ＷＩＴＨ ＫＳ ＩＳＶＥＲＩＦＩＥＤＢＹ Ｖｅｒ
ＷＩＴＨ ＫＶ ＳＵＣＨＴＨＡＴ （ＫＳ；；ＫＶ） ＝ Ｇ（）； ・・・（１）
（１）式の記述は、鍵生成関数Ｇ（）は署名鍵ＫＳと検証鍵ＫＶの対（ＫＳ；；ＫＶ）を生成することを示す。このため、図６の定義部では、鍵生成関数Ｇ（）は署名鍵ＫSＡと検証鍵ＫVＡの対（ＫSＡ；；ＫVＡ）を生成し、また、鍵生成関数Ｇ（）は署名鍵ＫSＢと検証鍵ＫVＢの対（ＫSＢ；；ＫVＢ）を生成することを定義している。
【００４３】
なお、図６の例では、鍵生成関数Ｇは引数を有さない関数としているが、セキュリティパラメータやその他のパラメータを引数とするように構成してもよい。また、鍵生成関数Ｇは決定性の関数である他、確率性の関数として構成することもできる。鍵生成関数をＧを確率性の関数として構成する場合は、鍵生成関数Ｇは呼び出されるたびに、鍵対全体の空間からランダムに選んだ鍵対を生成することになる。
【００４４】
初期条件部、プロトコル実行定義部、ゴール部における仕様記述の意味は以下のとおりである。
【００４５】
＜ｘ＞Ｓｉｇ（ｋ） ：署名関数Ｓｉｇによるメッセージｘの署名。ｋは署名鍵。
ＶｅｒｉｆｉｃａｔｉｏｎＫｅｙ Ｐ Ｖ Ｋ ：パーティＰによる署名の検証アルゴリズムＶの検証鍵はＫである。
Ａ Ｂｅｌｉｅｖｅｓ ＜Ｓｔｍｔ＞ ：パーティＡが＜Ｓｔｍｔ＞を信じる理由があった。
Ａ Ｐｏｓｓｅｓｓｅｓ ＜Ｓｔｍｔ＞ ：パーティＡは、＜Ｓｔｍｔ＞を受信したか、あるいは、受信した複数の＜Ｓｔｍｔ＞の中からその＜Ｓｔｍｔ＞を計算できる。
Ａ Ｒｅｃｅｉｖｅｄ ＜Ｓｔｍｔ＞ ：パーティＡは、＜Ｓｔｍｔ＞を現在のプロトコル実行より前に受け取った、または現在のプロトコル実行よりも前に受け取ったあるメッセージまたはその一部として受け取った。
Ａ Ｃｏｎｖｅｙｅｄ ＜Ｓｔｍｔ＞ ：パーティＡが＜Ｓｔｍｔ＞の現在のプロトコル実行の間の生成者でソースである。
【００４６】
従って、図６において初期条件部は、以下の意味を示している。
・パーティＡは、署名関数Ｓｉｇ、検証関数Ｖｅｒ、署名鍵ＫSＢを現在のプロトコル実行より前に受け取った、または現在のプロトコル実行よりも前に受け取ったあるメッセージまたはその一部として受け取った。
・パーティＡは、署名鍵ＫSＡを受信した。
・パーティＡは、パーティＢによる署名の検証アルゴリズムＶｅｒの検証鍵はＫSＢであることを信じる理由があった。
・パーティＢは、署名関数Ｓｉｇ、検証関数Ｖｅｒ、署名鍵ＫSＡを現在のプロトコル実行より前に受け取った、または現在のプロトコル実行よりも前に受け取ったあるメッセージまたはその一部として受け取った。
・パーティＢは、署名鍵ＫSＢを受信した。
・パーティＢは、パーティＡによる署名の検証アルゴリズムＶｅｒの検証鍵はＫSＡであることを信じる理由があった。
【００４７】
また、図６において、プロトコル実行定義部は以下の意味を示している。ここで、図６の最左端の番号は実行段階を示すステージである。
ステージ１：ＢからＡにメッセージＮｏＢを送信。
ステージ２：ＡからＢに、メッセージＮｏＡ，ＮｏＢ，Ｂ，署名関数ＳｉｇによるメッセージＮｏＡ，ＮｏＢ，Ｂの署名（署名鍵ＫSＡ）を送信。
ステージ３：ＢからＡに、メッセージＮｏＢ２，ＮｏＡ，Ａ，署名関数ＳｉｇによるメッセージＮｏＢ２，ＮｏＡ，Ａの署名（署名鍵ＫSＢ）を送信。
【００４８】
また、図６において、ゴール部は以下の意味を示している。
ステージ１：Ｂは、Ａが署名関数ＳｉｇによるメッセージＮｏＡ，ＮｏＢ，Ｂの署名（署名鍵ＫSＡ）の現在のプロトコル実行の間の生成者でソースであることを信じる理由があった。
ステージ２：Ａは、Ｂが署名関数ＳｉｇによるメッセージＮｏＢ２，ＮｏＡ，Ａの署名（署名鍵ＫSＢ）の現在のプロトコル実行の間の生成者でソースであることを信じる理由があった。
【００４９】
図７−１は、暗号プロトコル仕様における理想機能を使用した記述例を示す説明図である。図７−１では、プロトコル実行定義部における署名のプロトコルと検証のプロトコルの２つを示している。図７−１において、Ｐは、現実にプロトコル実行に関与するパーティ、Ｆは理想機能、Ｓはシミュレータ（敵）を示している。
【００５０】
署名のプロトコルでは、以下の意味を示している。
ステージ１：パーティＰから理想機能Ｆに署名要求送信。
ステージ２：理想機能ＳからシミュレータＳに署名要求送信。
ステージ３：シミュレータＳから理想機能Ｓに署名送信。
ステージ４：理想機能ＳからパーティＰに署名送信。
【００５１】
検証のプロトコルでは、以下の意味を示している。
ステージ１：パーティＰから理想機能Ｆに検証要求送信。
ステージ２：理想機能ＳからシミュレータＳに検証要求送信。
ステージ３：シミュレータＳから理想機能Ｓに検証送信。
ステージ４：理想機能ＳからパーティＰに検証送信。
【００５２】
この図７−１に示すプロトコル仕様では、シミュレータＳについての記述があるが、本実施の形態の検証可能な暗号プロトコル仕様では、ＵＣにおける記述から理想機能のエンティティが付加され、攻撃者としてのシミュレータの記述が削除または理想機能に対する記述に置換されたものとしている。具体的には、シミュレータＳと理想機能Ｆとの間の授受情報を攻撃時に利用可能な情報に置換し、シミュレータに対する理想機能からの即座の配信要求の記述を、理想機能による即座の配信の記述に置換した第２記述部５０２を有する暗号プロトコル仕様となっている。
【００５３】
図７−２は、検証可能な暗号プロトコル仕様データ５００の第２記述部５０２のプロトコル実行定義部の例を示す説明図である。図７−２では、図７−１のプロトコル実行定義部の記述においてシミュレータＳの記述を上記のように置換した署名のプロトコルと検証のプロトコルを示したものとなっている。すなわち、図７−１の署名のプロトコルにおける理想機能ＦからのシミュレータＳに対する署名要求が理想機能による即座の署名の記述に置換され、以下のようになる。
【００５４】
ステージ１：パーティＰから理想機能Ｆに署名要求送信。
ステージ２：理想機能ＳからパーティＰに署名送信。
【００５５】
同様に、検証のプロトコルは以下の意味となる。
ステージ１：パーティＰから理想機能Ｆに検証要求送信。
ステージ２：理想機能ＳからパーティＰに検証送信。
【００５６】
このように、本実施の形態では、シミュレータＳに関する記述を削除した第２記述部５０２を含む暗号プロトコル仕様を入力して暗号プロトコルの安全性検証を行っている。
【００５７】
次に、以上のように構成された本実施の形態にかかる暗号プロトコル安全性検証装置による暗号プロトコルの安全性検証処理について説明する。図８は、実施の形態１の暗号プロトコルの安全性検証処理の手順を示すフローチャートである。
【００５８】
暗号プロトコル仕様入力処理部１１０により図６に示すような第１記述部５０１と図７−２に示すような第２記述部５０２を有する検証可能な暗号プロトコル仕様データ５００が入力されると、形式的検証部１２０の解析部１２１によって暗号プロトコル仕様データを解析し、暗号プロトコル仕様データから初期条件部の記述を抽出して初期条件記憶部１４１に保存する（ステップＳ８０１）。次いで、解析部１２１によって暗号プロトコル仕様データからプロトコル実行定義部の記述を抽出してプロトコル記憶部１４２に保存する（ステップＳ８０２）。同様に、解析部１２１によって暗号プロトコル仕様データから定義部の記述を抽出して定義記憶部１４３に保存する（ステップＳ８０３）。さらに、解析部１２１によって暗号プロトコル仕様データからゴール部の記述を抽出してユーザ目標としてユーザ目標記憶部１４４に保存する（ステップＳ８０４）。なお、ゴール部の存在しない検証可能な暗号プロトコル仕様データ５００の場合には、かかるステップＳ８０４の処理はおこなわれない。
【００５９】
次いで、解析部１２３により、プロトコル記憶部１４２からプロトコル実行定義部の記述を読み出して、プロトコル実行定義部の記述をステージごとの文に分割する（ステップＳ８０５）。なお、図６および図７−１の例では、各ステージが単一の文から構成されているが、各ステージが複数の文から構成される場合もある。そして、定義記憶部１４３に保存されている定義部の記述を参照しながら、ステージごとに推論におけるデフォルト目標を生成し、デフォルト目標記憶部１４５に保存する（ステップＳ８０６）。
【００６０】
そして、推論実行部１２２によってデフォルト目標、ユーザ目標、証明済み文記憶部１５２、推論規則記憶部１５１の推論規則とから推論を実行して暗号プロトコル仕様の安全性を検証する（ステップＳ８０７）。そして、その検証結果として、暗号プロトコル仕様の安全性あり／なし、プロトコル実行定義部のステージごとの欠陥の有無、ゴール部の欠陥の有無が検証結果出力部１３０によって、表示装置等に出力される。
【００６１】
次に、ステップＳ８０７による推論実行部１２２による推論実行処理について説明する。図９−１および図９−２は、推論実行部１２２による推論実行処理の手順を示すフローチャートである。なお、本実施の形態では、後向き推論を行っているが、前向き推論によって安全性証明を実現することも可能である。
【００６２】
個々のデフォルト目標は、一般に、いくつかの連言形の文(論理積で表現される文)を選言形にしたもの(論理和で表現される文)として表現されている。まず、推論実行部１２２は、デフォルト目標記憶部１４５から一つのデフォルト目標を選択する（ステップＳ９０１）。そして、選択したデフォルト目標に含まれる連言形の中の文と等価な文を初期条件記憶部１４１と証明済み文記憶部１５２から検索する（ステップＳ９０２）。ここで、デフォルト目標に含まれる連言形の中の文と等価な文とは、デフォルト目標に含まれる連言形の中の文と同一の文の他、デフォルト目標に含まれる連言形の中の文中の変数に値を代入すると同一になる文をいう。
【００６３】
そして、検索結果がある場合、すなわち選択したデフォルト目標に含まれる連言形の中の文と等価な文が初期条件記憶部１４１あるいは証明済み文記憶部１５に存在した場合には（ステップＳ９０３：Ｙｅｓ）、選択したデフォルト目標から検索された文を含む連言形の部分を削除する（ステップＳ９０４）。一方、ステップＳ９０３において検索結果がなしの場合、すなわち選択したデフォルト目標に含まれる連言形の中の文と等価な文が初期条件記憶部１４１と証明済み文記憶部１５のいずれにも存在しない場合には（ステップＳ９０３：Ｎｏ）、デフォルト目標からの文の削除は行われない。
【００６４】
次に、推論実行部１２２は、デフォルト目標に含まれる連言形の中の文と等価な文を連言形で表現した結論を含む推論規則を推論規則記憶部１５１から検索する（ステップＳ９０５）。ここで、推論規則記憶部に格納されている推論規則は、その結論を連言形で表現された形で格納されているとする。そして、検索結果がある場合、すなわちデフォルト目標に含まれる連言形の中の文と等価な文を連言形で表現した結論を含む推論規則が推論規則記憶部１５１に存在する場合には（ステップＳ９０６：Ｙｅｓ）、デフォルト目標の当該文を検索された推論規則の前提部で置換する（ステップＳ９０７）。一方、ステップＳ９０６において検索結果がない場合、すなわちデフォルト目標に含まれる連言形の中の文と等価な文が、連言形で表現した結論を含む推論規則が推論規則記憶部１５１に存在しない場合には（ステップＳ９０６：Ｎｏ）、置換は行わない。
【００６５】
そして、このようなステップＳ９０２からＳ９０７までの処理を、デフォルト目標の中の全ての文に対して実行する（ステップＳ９０８）。デフォルト目標の中の全ての文に対してステップＳ９０２からＳ９０７までの処理を実行したら、ステップＳ９０４でデフォルト目標の中の全ての文が削除されたか否かを判断する（ステップＳ９０９）。
【００６６】
そして、デフォルト目標の中の全ての文が削除されている場合には（ステップＳ９０９：Ｙｅｓ）、そのデフォルト目標を欠陥なしと判定する（ステップＳ９１０）。一方、デフォルト目標の中の全ての文が削除されていない場合には（ステップＳ９０９：Ｎｏ）、そのデフォルト目標を欠陥ありと判定する（ステップＳ９１１）。そして、検証可能な暗号プロトコルのプロトコル実行定義部のすべてのステージに対して、上記ステップＳ９０１からＳ９１０またはＳ９１１までの処理を実行する（ステップＳ９１２）。
【００６７】
次に、推論実行部１２２は、ユーザ目標記憶部１４４からユーザ目標（すなわちゴール部の記述）を選択する（ステップＳ９１３）。個々のユーザ目標も、いくつかの連言形の文(論理積で表現された文)を選言形にしたもの(論理和で表現された文)として表現されている。そして、選択したユーザ目標に含まれる連言形の中の文と等価な文を初期条件記憶部１４１と証明済み文記憶部１５２から検索する（ステップＳ９１４）。
【００６８】
そして、検索結果がある場合、すなわち選択したユーザ目標に含まれる連言形の中の文と等価な文が初期条件記憶部１４１あるいは証明済み文記憶部１５に存在した場合には（ステップＳ９１５：Ｙｅｓ）、選択したユーザ目標から検索された文を含む連言形の部分を削除する（ステップＳ９１６）。一方、ステップＳ９１５において検索結果がなしの場合、すなわち選択したユーザ目標に含まれる連言形の中の文と等価な文が初期条件記憶部１４１と証明済み文記憶部１５のいずれにも存在しない場合には（ステップＳ９１５：Ｎｏ）、ユーザ目標からの文の削除は行われない。
【００６９】
次に、推論実行部１２２は、ユーザ目標に含まれる連言形の中の文と等価な文を連言形で表現した結論を含む推論規則を推論規則記憶部１５１から検索する（ステップＳ９１７）。そして、検索結果がある場合、すなわちユーザ目標に含まれる連言形の中の文と等価な文を連言形で表現した結論を含む推論規則が推論規則記憶部１５１に存在する場合には（ステップＳ９１８：Ｙｅｓ）、ユーザ目標の当該文を検索された推論規則の前提部で置換する（ステップＳ９１９）。この際、結論部と同じ変数に同一の値を代入した上で置換する。
【００７０】
一方、ステップＳ９１８において検索結果がない場合、すなわちユーザ目標に含まれる連言形の文と等価な文を連言形で表現した結論を含む推論規則が推論規則記憶部１５１に存在しない場合には（ステップＳ９１８：Ｎｏ）、置換は行わない。
【００７１】
そして、このようなステップＳ９１４からＳ９１９までの処理を、ユーザ目標の中の全ての文に対して実行する（ステップＳ９２０）。ユーザ目標の中の全ての文に対してステップＳ９１４からＳ９１９までの処理を実行したら、ステップＳ９１６によりユーザ目標の中の全ての文が削除されたか否かを判断する（ステップＳ９２１）。
【００７２】
そして、ユーザ目標の中の全ての文が削除されている場合には（ステップＳ９２１：Ｙｅｓ）、そのユーザ目標を欠陥なしと判定する（ステップＳ９２２）。一方、ユーザ目標の中の全ての文が削除されていない場合には（ステップＳ９２１：Ｎｏ）、そのユーザ目標を欠陥ありと判定する（ステップＳ９２３）。この場合において、さらに推論規則を変更して同様の処理を繰り返してもよい。
【００７３】
このような推論実行部１２２によるデフォルト目標を利用した推論によって、検証可能な暗号プロトコル仕様データ５００のプロトコル実行定義部の記述の欠陥の有無、すなわち安全性の検証が行われ、またユーザ目標を利用した推論によって、検証可能な暗号プロトコル仕様データ５００のゴール部の記述の欠陥の有無、すなわち安全性の検証が行われることになる。 なお、ゴール部の存在しない検証可能な暗号プロトコル仕様データ５００の場合には、上記ステップＳ９１３からＳ９２２またはＳ９２３までのユーザ目標に対する処理はおこなわれない。
【００７４】
そして、推論実行部１２２による推論による検証結果として、暗号プロトコル仕様の安全性あり／なし、プロトコル実行定義部のステージごとの欠陥の有無、ゴール部の欠陥の有無が検証結果出力部１３０によって、表示装置等に出力される。ここで、プロトコル実行定義部の全ステージで欠陥が存在せず、かつゴール部にも欠陥が存在しない場合には、暗号プロトコル仕様の安全性が証明されたことになる。
【００７５】
このように実施の形態１にかかる暗号プロトコル安全性検証装置１００では、汎用的結合可能安全性で定義される理想機能に関するエンティティを含むとともに攻撃者としてのシミュレータに関する記述が存在しない検証可能な暗号プロトコルの安全性検証を形式的検証部１２０で行うので、計算量的証明における暗号プロトコル仕様と形式的検証における暗号プロトコル仕様とを整合性をとった上で、プリミティブな安全性を計算量的証明により確保しつつ、複雑な暗号プロトコルについては形式的検証による機械的な検証処理により安全性検証の労力を軽減することができる。
【００７６】
（実施の形態２）
実施の形態１にかかる暗号プロトコル安全性検証装置１００は、図６のような第１記述部５０１と図７−２に示すような第２記述部５０２を有する暗号プロトコル仕様データ、すなわち予め検証可能となっている暗号プロトコル仕様データを入力して、暗号プロトコルの安全性検証を行っていたが、この実施の形態２にかかる暗号プロトコル安全性検証装置は、入力された暗号プロトコル仕様データから、検証可能な暗号プロトコル仕様データ５００を生成して、生成された検証可能な暗号プロトコル仕様データ５００の安全性検証を行うものである。
【００７７】
図１０は、実施の形態２にかかる暗号プロトコル安全性検証装置の機能的構成を示すブロック図である。本実施の形態にかかる暗号プロトコル安全性検証装置１０００は、図１０に示すように、暗号プロトコル仕様入力処理部１１０と、検証可能暗号プロトコル仕様生成部１０１０と、形式的検証部１２０と、検証結果出力部１３０と、初期条件記憶部１４１と、プロトコル記憶部１４２と、定義記憶部１４３と、ユーザ目標記憶部１４４と、デフォルト目標記憶部１４５と、推論規則記憶部１５１と、証明済み文記憶部１５２とを主に備えた構成となっている。
【００７８】
ここで、形式的検証部１２０、検証結果出力部１３０、初期条件記憶部１４１、プロトコル記憶部１４２、定義記憶部１４３、ユーザ目標記憶部１４４、デフォルト目標記憶部１４５、推論規則記憶部１５１、証明済み文記憶部１５２は、実施の形態１の暗号プロトコル安全性検証装置１００と同様の構成および機能を有している。
【００７９】
暗号プロトコル仕様入力処理部１１０は、暗号プロトコル仕様データを入力する処理部である。入力する暗号プロトコル仕様データは、形式的検証（ＦＶ）におけるプロトコル仕様で記述された第１記述部５０１と、計算量的証明のＵＣにおけるプロトコル仕様で記述された第２記述部とからなる暗号プロトコル仕様であり、ＵＣによる第２記述部が形式的検証と整合性をとって記述されたものでない点で、実施の形態１で入力される検証可能な暗号プロトコル仕様データ５００と異なっている。
【００８０】
検証可能暗号プロトコル仕様生成部１０１０は、暗号プロトコル仕様入力処理部１１０によって入力された暗号プロトコル仕様データから検証可能な暗号プロトコル仕様データ５００を生成する処理部である。検証可能な暗号プロトコル仕様データ５００は、実施の形態１と同様に、形式的検証（ＦＶ）におけるプロトコル仕様で記述された第１記述部５０１と、計算量的証明のＵＣ（Universal Composability）におけるプロトコル仕様に基づいて記述された第２記述部５０２とからなる暗号プロトコル仕様であり、ＵＣにおける仕様と形式的証明における仕様とを整合性をとって記述したものである。
【００８１】
具体的には、検証可能暗号プロトコル仕様生成部１０１０は、入力した暗号プロトコル仕様データの第２記述部のＵＣにおける記述から理想機能のエンティティが付加し、攻撃者としてのシミュレータの記述を削除して理想機能に対する記述に置換することによって、ＵＣにおける仕様と形式的証明における仕様とを整合性をとって記述された検証可能な暗号プロトコル仕様データ５００を生成している。本実施の形態においても、検証可能な暗号プロトコル仕様データ５００の例としては、実施の形態１と同様に、第１記述部５０１は例えば図６で示した記述であり、第２記述部５０２は図７−２で示した記述である。また、本実施の形態でも、検証可能な暗号プロトコル仕様データ５００は、実施の形態１と同様に、初期条件部、定義部、プロトコル実行定義部、ゴール部に分割されて記述されている。
【００８２】
次に、以上のように構成された本実施の形態にかかる暗号プロトコル安全性検証装置１０００による暗号プロトコルの安全性検証処理について説明する。
【００８３】
暗号プロトコル仕様入力処理部１１０により図６に示すような第１記述部５０１と図７−１に示すような第２記述部を有する暗号プロトコル仕様データが入力されると、検証可能暗号プロトコル仕様生成部１０１０によって、入力された暗号プロトコル仕様データから図６に示すような第１記述部５０１と図７−２に示すような第２記述部５０２を有する検証可能な暗号プロトコル仕様データ５００が生成される。そして、この生成された検証可能な暗号プロトコル仕様データ５００に対して形式的検証部１２０によって暗号プロトコルの安全性検証が行われ、検証結果出力部１３０によって検証結果が出力される。
【００８４】
次に、検証可能暗号プロトコル仕様生成部１０１０による検証可能な暗号プロトコル仕様データ５００の生成処理について説明する。図１１は、検証可能暗号プロトコル仕様生成部１０１０による検証可能な暗号プロトコル仕様データ５００の生成処理の手順を示すフローチャートである。
【００８５】
まず、検証可能暗号プロトコル仕様生成部１０１０は、第２記述部に理想機能のエンティティの記述を追加する（ステップＳ１１０１）。なお、第２記述部に最初から理想機能の記述が存在する場合には、かかるステップＳ１１０１は行われない。そして、検証可能暗号プロトコル仕様生成部１０１０は、第２記述部にシミュレータ（敵）Ｓに関する記述部分があるか否かを調べる（ステップＳ１１０２）。そして、シミュレータ（敵）Ｓに関する記述部分がない場合には（ステップＳ１１０２：Ｎｏ）、そのまま処理を抜ける。
【００８６】
一方、シミュレータ（敵）Ｓに関する記述部分がある場合には（ステップＳ１１０２：Ｙｅｓ）、検証可能暗号プロトコル仕様生成部１０１０は、さらに、第２記述部にシミュレータ（敵）Ｓと理想機能との間の情報の授受の記述があるか否かを調べる（ステップＳ１１０３）。そして、シミュレータ（敵）Ｓと理想機能との間の情報の授受の記述がある場合には（ステップＳ１１０３：Ｙｅｓ）、検証可能暗号プロトコル仕様生成部１０１０は、シミュレータ（敵）Ｓと理想機能との間の授受情報を攻撃に利用可能な情報として変換する（ステップＳ１１０４）。シミュレータ（敵）Ｓと理想機能との間の情報の授受の記述がない場合には（ステップＳ１１０３：Ｎｏ）、かかるＳ１１０４の処理は行わない。
【００８７】
次に、検証可能暗号プロトコル仕様生成部１０１０は、第２記述部にシミュレータ（敵）Ｓが理想機能からパーティへのメッセージの即座の配信を要求される記述があるか否かを調べる（ステップＳ１１０５）。そして、シミュレータ（敵）Ｓが理想機能からパーティへのメッセージの即座の配信を要求される記述がある場合には（ステップＳ１１０５：Ｙｅｓ）、かかる記述を理想機能がパーティへメッセージの即座の配信を行う記述に変換する（ステップＳ１１０６）。一方、シミュレータ（敵）Ｓが理想機能からパーティへのメッセージの即座の配信を要求される記述がない場合には（ステップＳ１１０５：Ｎｏ）、かかるＳ１１０６の処理はおこなわれない。
【００８８】
以上のような処理によって、入力された暗号プロトコル仕様データから、図６や図７−１のような形式的検証部１２０によって検証可能な暗号プロトコル仕様データ５００が生成されることになる。この生成された検証可能な暗号プロトコル仕様データ５００の安全性検証処理は、実施の形態１の図８、図９−１および図９−２で説明した処理と同様に行われ、その検証結果も実施の形態１と同様に検証結果出力部１３０によって表示装置等に出力される。
【００８９】
このように実施の形態２にかかる暗号プロトコル安全性検証装置１０００では、入力された暗号プロトコル仕様データから、検証可能な暗号プロトコル仕様データ５００を生成して、生成された検証可能な暗号プロトコル仕様データ５００の安全性検証を行うので、利用者によって計算量的証明における暗号プロトコル仕様と形式的検証における暗号プロトコル仕様との整合性をとることを意識させることなく、プリミティブな安全性を計算量的証明により確保しつつ、複雑な暗号プロトコルについては形式的検証による機械的な検証処理により安全性検証の労力を軽減することができる。
【００９０】
（変形例）
ＵＣの定式化として、シミュレータは現実に暗号プロトコルの実行に関与するパーティと理想機能の間のメッセージを認識できないとする定式化がある。例えば、図１２は、実施の形態２の変形例における定式化によって定義された認証された通信路の理想機能ＦAUTHである。この理想機能は以下のような処理を行う。
【００９１】
あるパーティＰｉから（ｓｅｎｄ，ｓｉｄ，Ｐｊ，ｍ）というメッセージを受信したときは、ｓｉｄが（Ｐｊ，ｓｉｄ‘）の形をしているか否かを判定する。そして、ｓｉｄが（Ｐｊ，ｓｉｄ‘）の形をしている場合には、（Ｐｊ，ｍ）を記録した上で、（ｓｅｎｄ，ｓｉｄ，Ｐｊ，ｍ）を攻撃者であるシミュレータに送信する。一方、ｓｉｄが（Ｐｊ，ｓｉｄ‘）の形をしていなに場合には、理想機能は、この入力を無視する。
【００９２】
一方、理想機能は、攻撃者であるシミュレータからｓｉｄ＝（Ｐｉ，ｓｉｄ’）の形をしたメッセージ（ｄｅｌｉｖｅｒ，ｓｉｄ，Ｐｊ’，ｍ’）を受信したときは、（Ｐｉ‘，ｍ’）が記録されているか否か、または、Ｐｉがｃｏｒｒｕｐｔされているか否かを判定し、もうしそうならば、パーティＰｊ’に対して、（ｓｅｎｔ，ｓｉｄ，ｍ‘）を出力してから停止する。そうでなければ、単に停止する。
【００９３】
この場合、理想機能からパーティへのメッセージの配信は、理想機能自身が行っている。ただし、その配信を行う前に、理想機能は攻撃者であるシミュレータに対して、これから配信を行う内容を通知している。この通知に対して、シミュレータは、メッセージの送信先のパーティの変更やメッセージの内容を改ざんする機会を与えられている。理想機能は、この変更や改ざんがあった場合は、それらに従ってメッセージを配信する。すなわち、理想機能はメッセージの配信に先立ち、その許可をシミュレータに求めており、理想機能はシミュレータが許可したとおりにメッセージを配信しなければならない。
【００９４】
この変形例における検証可能暗号プロトコル生成手段１０１０は、上のような理想機能に対応する第２記述部に対して、理想機能がパーティへのメッセージ配信を行う前にシミュレータにその配信許可を要求してから配信を行う記述は、理想機能がシミュレータの許可を要求することなく配信を行う記述に置換し、シミュレータと理想機能との間で授受された情報は、攻撃時に利用可能な情報と置換する。
【００９５】
次に、検証可能暗号プロトコル仕様生成部１０１０による検証可能な暗号プロトコル仕様データ５００の生成処理について説明する。図１３は、実施の形態２の変形例にかかる検証可能暗号プロトコル仕様生成部１０１０による検証可能な暗号プロトコル仕様データ５００の生成処理の手順を示すフローチャートである。
【００９６】
まず、検証可能暗号プロトコル仕様生成部１０１０は、第２記述部に理想機能のエンティティの記述を追加する（ステップＳ１３０１）。なお、第２記述部に最初から理想機能の記述が存在する場合には、かかるステップＳ１３０１は行われない。そして、検証可能暗号プロトコル仕様生成部１０１０は、第２記述部にシミュレータ（敵）Ｓに関する記述部分があるか否かを調べる（ステップＳ１３０２）。そして、シミュレータ（敵）Ｓに関する記述部分がない場合には（ステップＳ１３０２：Ｎｏ）、そのまま処理を抜ける。
【００９７】
一方、シミュレータ（敵）Ｓに関する記述部分がある場合には（ステップＳ１３０２：Ｙｅｓ）、検証可能暗号プロトコル仕様生成部１０１０は、さらに、第２記述部にシミュレータ（敵）Ｓと理想機能との間の情報の授受の記述があるか否かを調べる（ステップＳ１３０３）。そして、シミュレータ（敵）Ｓと理想機能との間の情報の授受の記述がある場合には（ステップＳ１３０３：Ｙｅｓ）、検証可能暗号プロトコル仕様生成部１０１０は、シミュレータ（敵）Ｓと理想機能との間の授受情報を攻撃に利用可能な情報として変換する（ステップＳ１３０４）。シミュレータ（敵）Ｓと理想機能との間の情報の授受の記述がない場合には（ステップＳ１３０３：Ｎｏ）、かかるＳ１３０４の処理は行わない。
【００９８】
次に、検証可能暗号プロトコル仕様生成部１０１０は、第２記述部にシミュレータ（敵）Ｓが理想機能からパーティへのメッセージの配信の許可を要求される記述があるか否かを調べる（ステップＳ１３０５）。そして、シミュレータ（敵）Ｓが理想機能からパーティへのメッセージの配信の許可を要求される記述がある場合には（ステップＳ１３０５：Ｙｅｓ）、かかる記述を理想機能が許可を要求することなく直接パーティへメッセージを配信する記述に変換する（ステップＳ１３０６）。一方、シミュレータ（敵）Ｓが理想機能からパーティへのメッセージの配信の許可を要求される記述がない場合には（ステップＳ１３０５：Ｎｏ）、かかるＳ１３０６の処理はおこなわれない。
【００９９】
このように実施の形態２の変形例にかかる暗号プロトコル安全性検証装置１０００では、シミュレータは現実に暗号プロトコルの実行に関与するパーティと理想機能の間のメッセージを認識できないとする定式化のＵＣを含む暗号プロトコル仕様データから、検証可能な暗号プロトコル仕様データ５００を生成して、生成された検証可能な暗号プロトコル仕様データ５００の安全性検証を行うので、利用者によって計算量的証明における暗号プロトコル仕様と形式的検証における暗号プロトコル仕様との整合性をとることを意識させることなく、プリミティブな安全性を計算量的証明により確保しつつ、複雑な暗号プロトコルについては形式的検証による機械的な検証処理により安全性検証の労力を軽減することができる。
【０１００】
（実施の形態３）
実施の形態３は、実施の形態１および２で説明した検証可能暗号プロトコル仕様生成手段および形式的検証手段を使用して暗号プロトコルを設計する暗号プロトコル設計装置である。
【０１０１】
図１４は、実施の形態３にかかる暗号プロトコル設計装置の機能的構成を示すブロック図である。本実施の形態にかかる暗号プロトコル設計装置１２００は、図１４に示すように、暗号プロトコル仕様設計部１２１０と、検証可能暗号プロトコル仕様生成部１０１０と、形式的検証部１２０と、検証結果出力部１３０と、暗号プロトコル実行部１２２０と、初期条件記憶部１４１と、プロトコル記憶部１４２と、定義記憶部１４３と、ユーザ目標記憶部１４４と、デフォルト目標記憶部１４５と、推論規則記憶部１５１と、証明済み文記憶部１５２と、暗号プロトコル部品記憶部１２３０と、暗号プロトコル記憶部１２４０とを主に備えた構成となっている。
【０１０２】
ここで、検証可能暗号プロトコル仕様生成部１０１０、形式的検証部１２０、検証結果出力部１３０、初期条件記憶部１４１、プロトコル記憶部１４２、定義記憶部１４３、ユーザ目標記憶部１４４、デフォルト目標記憶部１４５、推論規則記憶部１５１、証明済み文記憶部１５２は、実施の形態１の暗号プロトコル安全性検証装置１００と同様の構成および機能を有している。
【０１０３】
暗号プロトコル部品記憶部１２３０は、暗号プロトコル仕様データを構成部品を記憶するＨＤＤやメモリなどの記憶媒体である。暗号プロトコル部品記憶部１２３０は、具体的には形式的検証（ＦＶ）におけるプロトコル仕様で記述された第１記述部５０１の構成部品である第１記述部品と、計算量的証明のＵＣにおけるプロトコル仕様で記述された第２記述部の構成部品である第２記述部品が記憶されている。第１記述部品としては、実施の形態１で説明した図６に示す仕様記述を構成する文や語句などが例としてあげられる。また、第２記述部品としては、形式的検証における仕様と整合性をとっていない状態の図７−１に示す仕様記述を構成する文や語句などが例としてあげられる。
【０１０４】
暗号プロトコル仕様設計部１２１０は、暗号プロトコル部品記憶部１２３０に記憶されている第１記述部品と第２記述部品を読み出して、読み出した第１記述部品と第２記述部品から暗号プロトコル仕様データを生成する処理部である。具体的には、暗号プロトコル仕様設計部１２１０は、利用者によって指定された第１記述部品と第２記述部品を暗号プロトコル部品記憶部１２３０から読み出して、第１記述部品と第２記述部品を利用者の指定あるいは任意に組み合わせて暗号プロトコル仕様データの記述を生成する。このように生成された暗号プロトコル仕様データは、暗号プロトコル仕様生成部１０１０によって第２記述部を例えば図７−２に示すような形式的検証（ＦＶ）と整合性ととった検証可能な暗号プロトコル仕様データ５００が生成され、形式的検証部１２０によって安全性の検証が行われる。また、生成された暗号プロトコル仕様データは暗号プロトコル実行部１２２０にも受け渡される。
【０１０５】
暗号プロトコル実行部１２２０は、形式的検証部１２０によって安全性が証明された検証可能な暗号プロトコル仕様データ５００から利用者の指示入力等に従って実行可能な暗号プロトコルを生成し、生成した実行可能な暗号プロトコルを暗号プロトコルに保存する処理部である。
【０１０６】
暗号プロトコル記憶部１２４０は、暗号プロトコル実行部１２２０によって生成された実行可能な暗号プロトコルを記憶するＨＤＤやメモリ等の記憶媒体である。
【０１０７】
次に、以上のように構成された本実施の形態にかかる暗号プロトコル設計装置１２００による暗号プロトコルの設計処理について説明する。図１５は、暗号プロトコル設計装置１２００による暗号プロトコルの設計処理の手順を示すフローチャートである。
【０１０８】
まず、暗号プロトコル仕様設計部１２１０は、利用者の指定等により暗号プロトコル部品記憶部１２３０から生成に必要な第１記述部品、第２記述部品を読み出す（ステップＳ１５０１）。そして、暗号プロトコル仕様設計部１２１０は、読み出した第１記述部品、第２記述部品を利用者の指示等により組み合わせて暗号プロトコル仕様データを生成する（ステップＳ１５０２）。
【０１０９】
次に、検証可能暗号プロトコル仕様生成部１０１０によって、生成された暗号プロトコル仕様データから検証可能な暗号プロトコル仕様データ５００を生成する（ステップＳ１５０３）。ここで、検証可能暗号プロトコル仕様生成部１０１０による検証可能な暗号プロトコル仕様データ５００の生成処理については、図１１で説明した実施の形態２と同様に行われる。すなわち、暗号プロトコル仕様データの第２記述部のＵＣにおける記述から理想機能のエンティティが付加し、攻撃者としてのシミュレータの記述を削除して理想機能に対する記述に置換（シミュレータ（敵）Ｓと理想機能との間の情報の授受の記述をシミュレータ（敵）Ｓと理想機能との間の授受情報を攻撃に利用可能な情報として変換し、シミュレータ（敵）Ｓが理想機能から即座の配信を要求される記述を理想機能が即座の配信を行う記述に変換）することによって、ＵＣにおける仕様と形式的証明における仕様とを整合性をとって記述された検証可能な暗号プロトコル仕様データ５００を生成する。
【０１１０】
次に、検証可能な暗号プロトコル仕様データ５００が生成されたら、形式的検証部１２０によって、この検証可能な暗号プロトコル仕様データ５００の安全性検証を行う（ステップＳ１５０４）。ここで、形式的検証部１２０による検証可能な暗号プロトコル仕様データ５００の安全性検証の処理については、図８、図９−１及び図９−２で説明した実施の形態１および２と同様に行われる。
【０１１１】
形式的検証部１２０による安全性検証処理が完了したら、検証結果出力部１３０はその検証結果を出力するとともに、形式的検証部１２０によって検証可能な暗号プロトコル仕様データ５００に欠陥がないと証明されたか否か、すなわち安全性が証明されたか否かを判断する（ステップＳ１５０５）。そして、検証可能な暗号プロトコル仕様データ５００に欠陥がある場合には（ステップＳ１５０５：Ｎｏ）、ステップＳ１５０１からＳ１５０４までの処理を繰り返す。
【０１１２】
一方、ステップＳ１５０５において、検証可能な暗号プロトコル仕様データ５００に欠陥がない場合、すなわち安全性が証明された場合には（ステップＳ１５０５：Ｙｅｓ）、暗号プロトコル実行部１２２０によって検証可能な暗号プロトコル仕様データ５００から利用者の指示等により実行可能な暗号プロトコルを生成して暗号プロトコル記憶部１２４０に保存する（ステップＳ１５０６）。これにより、安全性が証明された暗号プロトコルが設計されることになる。
【０１１３】
このように実施の形態３にかかる暗号プロトコル設計装置１２００では、第１記述部品と第２記述部品から暗号プロトコル仕様データを生成し、生成した暗号プロトコル仕様データから汎用的結合可能性証明で定義される理想機能に関するエンティティを含むとともに攻撃者としてのシミュレータに関する記述が存在しない検証可能な暗号プロトコルを生成してその安全性検証を行い、安全性が証明された暗号プロトコル仕様データに基づいて実現可能な暗号プロトコルを生成しているので、計算量的証明における暗号プロトコル仕様と形式的検証における暗号プロトコル仕様とを整合性をとった上で、プリミティブな安全性を計算量的証明により確保しつつ、複雑な暗号プロトコルについては形式的検証による機械的な検証処理により安全性検証の労力を軽減することともに、確実な暗号プロトコルを設計することができる。
【０１１４】
実施の形態１および２の暗号プロトコル安全性検証装置、実施の形態３の暗号プロトコル設計装置は、ＣＰＵなどの制御装置と、ＲＯＭ（Read Only Memory）やＲＡＭなどの記憶装置と、ＨＤＤ、ＣＤドライブ装置などの外部記憶装置と、ディスプレイ装置などの表示装置と、キーボードやマウスなどの入力装置を備えており、通常のコンピュータを利用したハードウェア構成となっている。
【０１１５】
実施の形態１および２の暗号プロトコル安全性検証装置で実行される暗号プロトコル安全性検証プログラム、実施の形態３の暗号プロトコル設計装置で実行される暗号プロトコル設計プログラムは、インストール可能な形式又は実行可能な形式のファイルでＣＤ−ＲＯＭ、フレキシブルディスク（ＦＤ）、ＣＤ−Ｒ、ＤＶＤ（Ｄｉｇｉｔａｌ Ｖｅｒｓａｔｉｌｅ Ｄｉｓｋ）等のコンピュータで読み取り可能な記録媒体に記録されて提供される。
【０１１６】
また、実施の形態１および２の暗号プロトコル安全性検証装置で実行される暗号プロトコル安全性検証プログラム、実施の形態３の暗号プロトコル設計装置で実行される暗号プロトコル設計プログラムを、インターネット等のネットワークに接続されたコンピュータ上に格納し、ネットワーク経由でダウンロードさせることにより提供するように構成しても良い。また、実施の形態１および２の暗号プロトコル安全性検証装置で実行される暗号プロトコル安全性検証プログラム、実施の形態３の暗号プロトコル設計装置で実行される暗号プロトコル設計プログラムをインターネット等のネットワーク経由で提供または配布するように構成しても良い。
【０１１７】
また、実施の形態１および２の暗号プロトコル安全性検証装置で実行される暗号プロトコル安全性検証プログラム、実施の形態３の暗号プロトコル設計装置で実行される暗号プロトコル設計プログラムを、ＲＯＭ等に予め組み込んで提供するように構成してもよい。
【０１１８】
実施の形態１および２の暗号プロトコル安全性検証装置で実行される暗号プロトコル安全性検証プログラムは、上述した各部（暗号プロトコル仕様入力処理部１１０、検証可能暗号プロトコル仕様生成部１０１０、形式的検証部１２０、検証結果出力部１３０）を含むモジュール構成となっており、実際のハードウェアとしてはＣＰＵ（プロセッサ）が上記記憶媒体から暗号プロトコル安全性検証プログラムを読み出して実行することにより上記各部が主記憶装置上にロードされ、暗号プロトコル仕様入力処理部１１０、検証可能暗号プロトコル仕様生成部１０１０、形式的検証部１２０、検証結果出力部１３０が主記憶装置上に生成されるようになっている。
【０１１９】
また、実施の形態３の暗号プロトコル設計装置で実行される暗号プロトコル設計プログラムは、上述した各部（暗号プロトコル仕様設計部１２１０、検証可能暗号プロトコル仕様生成部１０１０、形式的検証部１２０、検証結果出力部１３０、暗号プロトコル実行部）を含むモジュール構成となっており、実際のハードウェアとしてはＣＰＵ（プロセッサ）が上記記憶媒体から暗号プロトコル安全性検証プログラムを読み出して実行することにより上記各部が主記憶装置上にロードされ、暗号プロトコル仕様設計部１２１０、検証可能暗号プロトコル仕様生成部１０１０、形式的検証部１２０、検証結果出力部１３０、暗号プロトコル実行部が主記憶装置上に生成されるようになっている。
【０１２０】
なお、本発明は、上記実施の形態そのままに限定されるものではなく、実施段階ではその要旨を逸脱しない範囲で構成要素を変形して具体化することができる。また、上記実施の形態に開示されている複数の構成要素の適宜な組み合わせにより、種々の発明を形成することができる。例えば、実施の形態に示される全構成要素からいくつかの構成要素を削除してもよい。さらに、異なる実施の形態にわたる構成要素を適宜組み合わせても良い。
【図面の簡単な説明】
【０１２１】
【図１】実施の形態１にかかる暗号プロトコル安全性検証装置の機能的構成を示すブロック図である。
【図２】ＵＣの概要を説明するための模式図である。
【図３】署名に関する理想機能である署名理想機能ＦSIGの一例を示す説明図である。
【図４】プロトコルπSの一例を示す説明図である。
【図５】実施の形態１にかかる暗号プロトコル安全検証装置で入力される検証可能な暗号プロトコル仕様データ５００のデータ構造を示す模式図である。
【図６】検証可能な暗号プロトコル仕様データ５００の第１記述部５０１の例を示す説明図である。
【図７−１】暗号プロトコル仕様における理想機能を使用した記述例を示す説明図である。
【図７−２】検証可能な暗号プロトコル仕様データ５００の第２記述部５０２のプロトコル実行定義部の例を示す説明図である。
【図８】実施の形態１の暗号プロトコルの安全性検証処理の手順を示すフローチャートである。
【図９−１】推論実行部１２２による推論実行処理の手順を示すフローチャートである。
【図９−２】推論実行部１２２による推論実行処理の手順を示すフローチャート（図９−１の続き）である。
【図１０】実施の形態２にかかる暗号プロトコル安全性検証装置の機能的構成を示すブロック図である。
【図１１】検証可能暗号プロトコル仕様生成部１０１０による検証可能な暗号プロトコル仕様データ５００の生成処理の手順を示すフローチャートである。
【図１２】認証機能を持ったチャンネルの理想機能である認証チャンネル理想機能ＦAUTHの一例を示す説明図である。
【図１３】実施の形態２の変形例における検証可能暗号プロトコル仕様生成部１０１０による検証可能な暗号プロトコル仕様データ５００の生成処理の手順を示すフローチャートである。
【図１４】実施の形態３にかかるい暗号プロトコル設計装置の機能的構成を示すブロック図である。
【図１５】暗号プロトコル設計装置１２００による暗号プロトコルの設計処理の手順を示すフローチャートである。
【符号の説明】
【０１２２】
１００，１０００ 暗号プロトコル安全性検証装置
１１０ 暗号プロトコル仕様入力処理部
１２０ 形式的検証部
１２１ デフォルト目標生成部
１２２ 推論実行部
１２３ 解析部
１４１ 初期条件記憶部
１４２ プロトコル記憶部
１４３ 定義記憶部
１４４ ユーザ目標記憶部
１４５ デフォルト目標記憶部
１５１ 推論規則記憶部
１５２ 証明済み文記憶部
１０１０ 検証可能暗号プロトコル仕様生成部
１２００ 暗号プロトコル設計装置
１２１０ 暗号プロトコル仕様設計部
１２２０ 暗号プロトコル実行部
１２３０ 暗号プロトコル部品記憶部
１２４０ 暗号プロトコル記憶部
【特許請求の範囲】
【請求項１】
現実に暗号プロトコルの実行に関与するパーティに関する処理が記述された第１記述部と、汎用結合可能安全性で定義される理想のプロトコルと対応し、現実に暗号プロトコルの実行に関与するパーティおよび現実に暗号プロトコルの実行に関与しない第１の仮想のエンティティに関する処理が記述され、現実に暗号プロトコルの実行に関与しない第２の仮想のエンティティに関する記述を含まない第２記述部とを含む検証可能な暗号プロトコル仕様データであって、前記第１の仮想のエンティティは、前記理想のプロトコルにおける理想機能に対応し、前記第２の仮想のエンティティは、前記理想のプロトコルにおけるシミュレータに対応する検証可能な暗号プロトコル仕様データにおける前記パーティおよび前記第１の仮想のエンティティに関する処理の欠陥の有無を、前記検証可能な暗号プロトコル仕様データの記述に基づいて検証する形式的検証手段
を備えたことを特徴とする暗号プロトコル安全性検証装置。
【請求項２】
前記検証可能な暗号プロトコル仕様データを入力する暗号プロトコル仕様入力処理手段をさらに備え、
前記形式的検証手段は、前記暗号プロトコル仕様入力処理手段によって入力された前記検証可能な暗号プロトコル仕様データ検証可能な暗号プロトコル仕様データにおける前記パーティおよび前記第１の仮想のエンティティの両方に関する処理の欠陥の有無を、前記検証可能な暗号プロトコル仕様データの記述に基づいて検証することを特徴とする請求項１に記載の暗号プロトコル安全性検証装置。
【請求項３】
現実に暗号プロトコルの実行に関与するパーティに関する処理が記述された第１記述部と、現実に暗号プロトコルの実行に関与するパーティおよび現実に暗号プロトコルの実行に関与しない第１の仮想のエンティティおよび第２の仮想のエンティティに関する処理が記述された第２記述部とを含む暗号プロトコル仕様データに対して、前記第２の仮想のエンティティに関する記述を削除して、前記検証可能な暗号プロトコル仕様データを生成する検証可能暗号プロトコル生成手段をさらに備えたことを特徴とする請求項１に記載の暗号プロトコル安全性検証装置。
【請求項４】
前記検証可能暗号プロトコル生成手段は、前記第２記述部に、前記第２の仮想のエンティティに関する記述が存在するか否かを判断し、存在すると判断した場合には、前記第２の仮想のエンティティによる記述を削除して、前記検証可能な暗号プロトコル仕様データを生成することを特徴とする請求項３に記載の暗号プロトコル安全性検証装置。
【請求項５】
前記検証可能暗号プロトコル生成手段は、さらに、前記第２の仮想のエンティティと前記第１の仮想のエンティティとの間の授受情報を攻撃時に利用可能な情報に置換し、前記第２記述部に、前記第２の仮想のエンティティに関する記述が存在すると判断した場合には、前記第１の仮想のエンティティによる前記第２の仮想のエンティティに対する前記パーティへのメッセージ配信の依頼に関する記述を、前記第１の仮想のエンティティが直接前記パーティへメッセージを配信する記述に置換することにより、前記検証可能な暗号プロトコル仕様データを生成することを特徴とする請求項４に記載の暗号プロトコル安全性検証装置。
【請求項６】
前記検証可能暗号プロトコル生成手段は、さらに、前記第２の仮想のエンティティと前記第１の仮想のエンティティとの間の授受情報を攻撃時に利用可能な情報に置換し、前記第２記述部に、前記第２の仮想のエンティティに関する記述が存在すると判断した場合には、前記第１の仮想のエンティティが前記パーティへのメッセージ配信を行う前に前記第２の仮想のエンティティにその配信許可を要求してから配信を行う記述を、前記第１の仮想のエンティティが前記第２の仮想のエンティティの許可を要求することなく配信を行う記述に置換することにより、前記検証可能な暗号プロトコル仕様データを生成することを特徴とする請求項４に記載の暗号プロトコル安全性検証装置。
【請求項７】
暗号プロトコル仕様データの検証の初期過程において、正しいことを仮定された文を記憶する初期条件記憶手段と、
暗号プロトコル仕様データの検証の過程において、正しいことが検証された文を記憶する証明済み文記憶手段と、をさらに備え、
前記形式的検証手段は、
前記第２記述部に含まれるプロトコルの実行処理を記述したプロトコル実行定義部から推論の当面の目標となるデフォルト目標情報を生成するデフォルト目標生成手段と、
前記デフォルト目標生成手段によって生成された前記デフォルト目標情報に含まれる文と等価な文が前記初期条件記憶手段または前記証明済み文記憶手段に存在するか否かを判断し、前記デフォルト目標情報の全ての文が前記初期条件記憶手段または前記証明済み文記憶手段に存在する場合にはそのデフォルト目標情報は正しいと証明されたと推論する推論手段と、
を備えたことを特徴とする請求項１〜５のいずれか一つに記載の暗号プロトコル安全性検証装置。
【請求項８】
前記推論手段は、さらに、前記第２記述部に含まれる最終目標を示すゴール部の記述をユーザ目標として、当該ユーザ情報に含まれる文と等価な文が前記初期条件記憶手段または前記証明済み文記憶手段に存在するか否かを判断し、前記ユーザ目標情報の全ての文が前記初期条件記憶手段または前記証明済み文記憶手段に存在する場合には欠陥なしと証明されたと推論することを特徴とする請求項６に記載の暗号プロトコル安全性検証装置。
【請求項９】
現実に暗号プロトコルの実行に関与するパーティに関する処理の記述である第１記述部を構成する第１記述部品と、前記第１記述部により安全に実現されることが証明されている、現実に暗号プロトコルの実行に関与するパーティに関する処理と現実に暗号プロトコルの実行に関与しない第１の仮想のエンティティと第２の仮想のエンティティに関する処理の記述である第２記述部を構成する第２記述部品とを記憶する暗号プロトコル部品記憶手段と、
前記暗号プロトコル部品記憶手段に記憶された前記第２記述部品と新たに追加した前記第１記述部とを含む暗号プロトコル仕様データを生成する暗号プロトコル仕様設計手段と、
前記暗号プロトコル仕様設計手段によって生成された前記暗号プロトコル仕様データに対して、前記第２記述部に対して前記第２の仮想のエンティティに関する記述を削除して、検証可能な暗号プロトコル仕様データを生成する検証可能暗号プロトコル生成手段と、
前記検証可能暗号プロトコル仕様生成手段によって生成された前記検証可能な暗号プロトコル仕様データにおける前記パーティおよび前記第１の仮想のエンティティの両方に関する処理の欠陥の有無を、前記検証可能な暗号プロトコル仕様データの記述に基づいて検証する形式的検証手段と、
前記形式的検証手段によって欠陥なしと証明された前記検証可能な暗号プロトコル仕様データに基づいて実現可能な暗号プロトコルを生成する暗号プロトコル実行手段と、
を備えたことを特徴とする暗号プロトコル設計装置。
【請求項１０】
現実に暗号プロトコルの実行に関与するパーティに関する処理が記述された第１記述部と、汎用結合可能安全性で定義される理想のプロトコルと対応し、現実に暗号プロトコルの実行に関与するパーティおよび現実に暗号プロトコルの実行に関与しない第１の仮想のエンティティに関する処理が記述され、現実に暗号プロトコルの実行に関与しない第２の仮想のエンティティに関する記述を含まない第２記述部とを含む検証可能な暗号プロトコル仕様データであって、前記第１の仮想のエンティティは、前記理想のプロトコルにおける理想機能に対応し、前記第２の仮想のエンティティは、前記理想のプロトコルにおけるシミュレータに対応する検証可能な暗号プロトコル仕様データにおける前記パーティおよび第１の仮想のエンティティに関する処理の欠陥の有無を、前記検証可能な暗号プロトコル仕様データの記述に基づいて検証する形式的検証ステップ
を含むことを特徴とする暗号プロトコル安全性検証方法。
【請求項１１】
現実に暗号プロトコルの実行に関与するパーティに関する処理の記述である第１記述部を構成する第１記述部品と、前記第１記述部により安全に実現されることが証明されている、現実に暗号プロトコルの実行に関与するパーティに関する処理と現実に暗号プロトコルの実行に関与しない第１の仮想のエンティティと第２の仮想のエンティティに関する処理の記述である第２記述部を構成する第２記述部品とを記憶する暗号プロトコル部品記憶手段に記憶された前記第２記述部品と新たに追加した前記第１記述部とを含む暗号プロトコル仕様データを生成する暗号プロトコル仕様設計ステップと、
前記暗号プロトコル仕様設計ステップによって生成された前記暗号プロトコル仕様データに対して、前記第２記述部に対して前記第２の仮想のエンティティに関する記述を削除して、検証可能な暗号プロトコル仕様データを生成する検証可能暗号プロトコル生成ステップと、
前記検証可能暗号プロトコル仕様生成ステップによって生成された前記検証可能な暗号プロトコル仕様データにおける前記パーティおよび前記第１の仮想のエンティティの両方に関する処理の欠陥の有無を、前記検証可能な暗号プロトコル仕様データの記述に基づいて検証する形式的検証ステップと、
前記形式的検証ステップによって欠陥なしと証明された前記検証可能な暗号プロトコル仕様データに基づいて実現可能な暗号プロトコルを生成する暗号プロトコル実行ステップと、
を含むことを特徴とする暗号プロトコル設計方法。
【請求項１２】
現実に暗号プロトコルの実行に関与するパーティに関する処理が記述された第１記述部と、汎用結合可能安全性で定義される理想のプロトコルと対応し、現実に暗号プロトコルの実行に関与するパーティおよび現実に暗号プロトコルの実行に関与しない第１の仮想のエンティティに関する処理が記述され、現実に暗号プロトコルの実行に関与しない第２の仮想のエンティティに関する記述を含まない第２記述部とを含む検証可能な暗号プロトコル仕様データであって、前記第１の仮想のエンティティは、前記理想のプロトコルにおける理想機能に対応し、前記第２の仮想のエンティティは、前記理想のプロトコルにおけるシミュレータに対応する検証可能な暗号プロトコル仕様データにおける前記パーティおよび第１の仮想のエンティティに関する処理の欠陥の有無を、前記検証可能な暗号プロトコル仕様データの記述に基づいて検証する形式的検証ステップ
をコンピュータに実行させる暗号プロトコル安全性検証プログラム。
【請求項１３】
現実に暗号プロトコルの実行に関与するパーティに関する処理の記述である第１記述部を構成する第１記述部品と、前記第１記述部により安全に実現されることが証明されている、現実に暗号プロトコルの実行に関与するパーティに関する処理と現実に暗号プロトコルの実行に関与しない第１の仮想のエンティティと第２の仮想のエンティティに関する処理の記述である第２記述部を構成する第２記述部品とを記憶する暗号プロトコル部品記憶手段に記憶された前記第２記述部品と新たに追加した前記第１記述部とを含む暗号プロトコル仕様データを生成する暗号プロトコル仕様設計ステップと、
前記暗号プロトコル仕様設計ステップによって生成された前記暗号プロトコル仕様データに対して、前記第２記述部に対して前記第２の仮想のエンティティに関する記述を削除して、検証可能な暗号プロトコル仕様データを生成する検証可能暗号プロトコル生成ステップと、
前記検証可能暗号プロトコル仕様生成ステップによって生成された前記検証可能な暗号プロトコル仕様データにおける前記パーティおよび前記第１の仮想のエンティティの両方に関する処理の欠陥の有無を、前記検証可能な暗号プロトコル仕様データの記述に基づいて検証する形式的検証ステップと、
前記形式的検証ステップによって欠陥なしと証明された前記検証可能な暗号プロトコル仕様データに基づいて実現可能な暗号プロトコルを生成する暗号プロトコル実行ステップと、
をコンピュータに実行させる暗号プロトコル設計プログラム。
【請求項１】
現実に暗号プロトコルの実行に関与するパーティに関する処理が記述された第１記述部と、汎用結合可能安全性で定義される理想のプロトコルと対応し、現実に暗号プロトコルの実行に関与するパーティおよび現実に暗号プロトコルの実行に関与しない第１の仮想のエンティティに関する処理が記述され、現実に暗号プロトコルの実行に関与しない第２の仮想のエンティティに関する記述を含まない第２記述部とを含む検証可能な暗号プロトコル仕様データであって、前記第１の仮想のエンティティは、前記理想のプロトコルにおける理想機能に対応し、前記第２の仮想のエンティティは、前記理想のプロトコルにおけるシミュレータに対応する検証可能な暗号プロトコル仕様データにおける前記パーティおよび前記第１の仮想のエンティティに関する処理の欠陥の有無を、前記検証可能な暗号プロトコル仕様データの記述に基づいて検証する形式的検証手段
を備えたことを特徴とする暗号プロトコル安全性検証装置。
【請求項２】
前記検証可能な暗号プロトコル仕様データを入力する暗号プロトコル仕様入力処理手段をさらに備え、
前記形式的検証手段は、前記暗号プロトコル仕様入力処理手段によって入力された前記検証可能な暗号プロトコル仕様データ検証可能な暗号プロトコル仕様データにおける前記パーティおよび前記第１の仮想のエンティティの両方に関する処理の欠陥の有無を、前記検証可能な暗号プロトコル仕様データの記述に基づいて検証することを特徴とする請求項１に記載の暗号プロトコル安全性検証装置。
【請求項３】
現実に暗号プロトコルの実行に関与するパーティに関する処理が記述された第１記述部と、現実に暗号プロトコルの実行に関与するパーティおよび現実に暗号プロトコルの実行に関与しない第１の仮想のエンティティおよび第２の仮想のエンティティに関する処理が記述された第２記述部とを含む暗号プロトコル仕様データに対して、前記第２の仮想のエンティティに関する記述を削除して、前記検証可能な暗号プロトコル仕様データを生成する検証可能暗号プロトコル生成手段をさらに備えたことを特徴とする請求項１に記載の暗号プロトコル安全性検証装置。
【請求項４】
前記検証可能暗号プロトコル生成手段は、前記第２記述部に、前記第２の仮想のエンティティに関する記述が存在するか否かを判断し、存在すると判断した場合には、前記第２の仮想のエンティティによる記述を削除して、前記検証可能な暗号プロトコル仕様データを生成することを特徴とする請求項３に記載の暗号プロトコル安全性検証装置。
【請求項５】
前記検証可能暗号プロトコル生成手段は、さらに、前記第２の仮想のエンティティと前記第１の仮想のエンティティとの間の授受情報を攻撃時に利用可能な情報に置換し、前記第２記述部に、前記第２の仮想のエンティティに関する記述が存在すると判断した場合には、前記第１の仮想のエンティティによる前記第２の仮想のエンティティに対する前記パーティへのメッセージ配信の依頼に関する記述を、前記第１の仮想のエンティティが直接前記パーティへメッセージを配信する記述に置換することにより、前記検証可能な暗号プロトコル仕様データを生成することを特徴とする請求項４に記載の暗号プロトコル安全性検証装置。
【請求項６】
前記検証可能暗号プロトコル生成手段は、さらに、前記第２の仮想のエンティティと前記第１の仮想のエンティティとの間の授受情報を攻撃時に利用可能な情報に置換し、前記第２記述部に、前記第２の仮想のエンティティに関する記述が存在すると判断した場合には、前記第１の仮想のエンティティが前記パーティへのメッセージ配信を行う前に前記第２の仮想のエンティティにその配信許可を要求してから配信を行う記述を、前記第１の仮想のエンティティが前記第２の仮想のエンティティの許可を要求することなく配信を行う記述に置換することにより、前記検証可能な暗号プロトコル仕様データを生成することを特徴とする請求項４に記載の暗号プロトコル安全性検証装置。
【請求項７】
暗号プロトコル仕様データの検証の初期過程において、正しいことを仮定された文を記憶する初期条件記憶手段と、
暗号プロトコル仕様データの検証の過程において、正しいことが検証された文を記憶する証明済み文記憶手段と、をさらに備え、
前記形式的検証手段は、
前記第２記述部に含まれるプロトコルの実行処理を記述したプロトコル実行定義部から推論の当面の目標となるデフォルト目標情報を生成するデフォルト目標生成手段と、
前記デフォルト目標生成手段によって生成された前記デフォルト目標情報に含まれる文と等価な文が前記初期条件記憶手段または前記証明済み文記憶手段に存在するか否かを判断し、前記デフォルト目標情報の全ての文が前記初期条件記憶手段または前記証明済み文記憶手段に存在する場合にはそのデフォルト目標情報は正しいと証明されたと推論する推論手段と、
を備えたことを特徴とする請求項１〜５のいずれか一つに記載の暗号プロトコル安全性検証装置。
【請求項８】
前記推論手段は、さらに、前記第２記述部に含まれる最終目標を示すゴール部の記述をユーザ目標として、当該ユーザ情報に含まれる文と等価な文が前記初期条件記憶手段または前記証明済み文記憶手段に存在するか否かを判断し、前記ユーザ目標情報の全ての文が前記初期条件記憶手段または前記証明済み文記憶手段に存在する場合には欠陥なしと証明されたと推論することを特徴とする請求項６に記載の暗号プロトコル安全性検証装置。
【請求項９】
現実に暗号プロトコルの実行に関与するパーティに関する処理の記述である第１記述部を構成する第１記述部品と、前記第１記述部により安全に実現されることが証明されている、現実に暗号プロトコルの実行に関与するパーティに関する処理と現実に暗号プロトコルの実行に関与しない第１の仮想のエンティティと第２の仮想のエンティティに関する処理の記述である第２記述部を構成する第２記述部品とを記憶する暗号プロトコル部品記憶手段と、
前記暗号プロトコル部品記憶手段に記憶された前記第２記述部品と新たに追加した前記第１記述部とを含む暗号プロトコル仕様データを生成する暗号プロトコル仕様設計手段と、
前記暗号プロトコル仕様設計手段によって生成された前記暗号プロトコル仕様データに対して、前記第２記述部に対して前記第２の仮想のエンティティに関する記述を削除して、検証可能な暗号プロトコル仕様データを生成する検証可能暗号プロトコル生成手段と、
前記検証可能暗号プロトコル仕様生成手段によって生成された前記検証可能な暗号プロトコル仕様データにおける前記パーティおよび前記第１の仮想のエンティティの両方に関する処理の欠陥の有無を、前記検証可能な暗号プロトコル仕様データの記述に基づいて検証する形式的検証手段と、
前記形式的検証手段によって欠陥なしと証明された前記検証可能な暗号プロトコル仕様データに基づいて実現可能な暗号プロトコルを生成する暗号プロトコル実行手段と、
を備えたことを特徴とする暗号プロトコル設計装置。
【請求項１０】
現実に暗号プロトコルの実行に関与するパーティに関する処理が記述された第１記述部と、汎用結合可能安全性で定義される理想のプロトコルと対応し、現実に暗号プロトコルの実行に関与するパーティおよび現実に暗号プロトコルの実行に関与しない第１の仮想のエンティティに関する処理が記述され、現実に暗号プロトコルの実行に関与しない第２の仮想のエンティティに関する記述を含まない第２記述部とを含む検証可能な暗号プロトコル仕様データであって、前記第１の仮想のエンティティは、前記理想のプロトコルにおける理想機能に対応し、前記第２の仮想のエンティティは、前記理想のプロトコルにおけるシミュレータに対応する検証可能な暗号プロトコル仕様データにおける前記パーティおよび第１の仮想のエンティティに関する処理の欠陥の有無を、前記検証可能な暗号プロトコル仕様データの記述に基づいて検証する形式的検証ステップ
を含むことを特徴とする暗号プロトコル安全性検証方法。
【請求項１１】
現実に暗号プロトコルの実行に関与するパーティに関する処理の記述である第１記述部を構成する第１記述部品と、前記第１記述部により安全に実現されることが証明されている、現実に暗号プロトコルの実行に関与するパーティに関する処理と現実に暗号プロトコルの実行に関与しない第１の仮想のエンティティと第２の仮想のエンティティに関する処理の記述である第２記述部を構成する第２記述部品とを記憶する暗号プロトコル部品記憶手段に記憶された前記第２記述部品と新たに追加した前記第１記述部とを含む暗号プロトコル仕様データを生成する暗号プロトコル仕様設計ステップと、
前記暗号プロトコル仕様設計ステップによって生成された前記暗号プロトコル仕様データに対して、前記第２記述部に対して前記第２の仮想のエンティティに関する記述を削除して、検証可能な暗号プロトコル仕様データを生成する検証可能暗号プロトコル生成ステップと、
前記検証可能暗号プロトコル仕様生成ステップによって生成された前記検証可能な暗号プロトコル仕様データにおける前記パーティおよび前記第１の仮想のエンティティの両方に関する処理の欠陥の有無を、前記検証可能な暗号プロトコル仕様データの記述に基づいて検証する形式的検証ステップと、
前記形式的検証ステップによって欠陥なしと証明された前記検証可能な暗号プロトコル仕様データに基づいて実現可能な暗号プロトコルを生成する暗号プロトコル実行ステップと、
を含むことを特徴とする暗号プロトコル設計方法。
【請求項１２】
現実に暗号プロトコルの実行に関与するパーティに関する処理が記述された第１記述部と、汎用結合可能安全性で定義される理想のプロトコルと対応し、現実に暗号プロトコルの実行に関与するパーティおよび現実に暗号プロトコルの実行に関与しない第１の仮想のエンティティに関する処理が記述され、現実に暗号プロトコルの実行に関与しない第２の仮想のエンティティに関する記述を含まない第２記述部とを含む検証可能な暗号プロトコル仕様データであって、前記第１の仮想のエンティティは、前記理想のプロトコルにおける理想機能に対応し、前記第２の仮想のエンティティは、前記理想のプロトコルにおけるシミュレータに対応する検証可能な暗号プロトコル仕様データにおける前記パーティおよび第１の仮想のエンティティに関する処理の欠陥の有無を、前記検証可能な暗号プロトコル仕様データの記述に基づいて検証する形式的検証ステップ
をコンピュータに実行させる暗号プロトコル安全性検証プログラム。
【請求項１３】
現実に暗号プロトコルの実行に関与するパーティに関する処理の記述である第１記述部を構成する第１記述部品と、前記第１記述部により安全に実現されることが証明されている、現実に暗号プロトコルの実行に関与するパーティに関する処理と現実に暗号プロトコルの実行に関与しない第１の仮想のエンティティと第２の仮想のエンティティに関する処理の記述である第２記述部を構成する第２記述部品とを記憶する暗号プロトコル部品記憶手段に記憶された前記第２記述部品と新たに追加した前記第１記述部とを含む暗号プロトコル仕様データを生成する暗号プロトコル仕様設計ステップと、
前記暗号プロトコル仕様設計ステップによって生成された前記暗号プロトコル仕様データに対して、前記第２記述部に対して前記第２の仮想のエンティティに関する記述を削除して、検証可能な暗号プロトコル仕様データを生成する検証可能暗号プロトコル生成ステップと、
前記検証可能暗号プロトコル仕様生成ステップによって生成された前記検証可能な暗号プロトコル仕様データにおける前記パーティおよび前記第１の仮想のエンティティの両方に関する処理の欠陥の有無を、前記検証可能な暗号プロトコル仕様データの記述に基づいて検証する形式的検証ステップと、
前記形式的検証ステップによって欠陥なしと証明された前記検証可能な暗号プロトコル仕様データに基づいて実現可能な暗号プロトコルを生成する暗号プロトコル実行ステップと、
をコンピュータに実行させる暗号プロトコル設計プログラム。
【図１】
【図２】
【図３】
【図４】
【図５】
【図６】
【図７−１】
【図７−２】
【図８】
【図９−１】
【図９−２】
【図１０】
【図１１】
【図１２】
【図１３】
【図１４】
【図１５】
【図２】
【図３】
【図４】
【図５】
【図６】
【図７−１】
【図７−２】
【図８】
【図９−１】
【図９−２】
【図１０】
【図１１】
【図１２】
【図１３】
【図１４】
【図１５】
【公開番号】特開２００７−２８４４７（Ｐ２００７−２８４４７Ａ）
【公開日】平成１９年２月１日（２００７．２．１）
【国際特許分類】
【出願番号】特願２００５−２１０５３３（Ｐ２００５−２１０５３３）
【出願日】平成１７年７月２０日（２００５．７．２０）
【出願人】（０００００３０７８）株式会社東芝 (54,554)
【Ｆターム（参考）】
【公開日】平成１９年２月１日（２００７．２．１）
【国際特許分類】
【出願日】平成１７年７月２０日（２００５．７．２０）
【出願人】（０００００３０７８）株式会社東芝 (54,554)
【Ｆターム（参考）】
[ Back to top ]