暗号プロトコルの安全性検証装置、安全性検証方法およびプログラム
【課題】暗号プロトコルを安全性レベルに応じて検証することができる。
【解決手段】認証および鍵交換プロトコルにおいて、列挙した暗号プリミティブについて、危殆化情報を有するものがある場合に、安全ではないと判断する。一方、危殆化情報を有するものがない場合に、暗号プリミティブの役割を設定し、安全性の根拠の設定を行い、フローデータと暗号プリミティブの引数の種類と状態とを設定する。そして、設定したフローデータと暗号プリミティブの引数の種類と状態との関係に正しくないものを含む場合に、暗号プロトコルは安全ではないと判断する。一方、フローデータと暗号プリミティブの引数の種類と状態との関係がすべて正しいと判断した場合に、安全性に関する検証項目の選択を行い、満足しないものを含む場合に、暗号プロトコルは安全ではないと判断し、選択した検証項目をすべて満足する場合に、暗号プロトコルは安全であると判断する。
【解決手段】認証および鍵交換プロトコルにおいて、列挙した暗号プリミティブについて、危殆化情報を有するものがある場合に、安全ではないと判断する。一方、危殆化情報を有するものがない場合に、暗号プリミティブの役割を設定し、安全性の根拠の設定を行い、フローデータと暗号プリミティブの引数の種類と状態とを設定する。そして、設定したフローデータと暗号プリミティブの引数の種類と状態との関係に正しくないものを含む場合に、暗号プロトコルは安全ではないと判断する。一方、フローデータと暗号プリミティブの引数の種類と状態との関係がすべて正しいと判断した場合に、安全性に関する検証項目の選択を行い、満足しないものを含む場合に、暗号プロトコルは安全ではないと判断し、選択した検証項目をすべて満足する場合に、暗号プロトコルは安全であると判断する。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、認証や鍵共有などのセキュリティ機能を有する暗号プロトコルに関し、そうした暗号プロトコルの安全性を検証する暗号プロトコルの安全性検証装置、安全性検証方法およびプログラムに関する。
【背景技術】
【０００２】
従来、プロトコル設計者の有するセキュリティ、暗号技術の見識に基づき、ヒューリスティックなアプローチで経験的に、安全な暗号プロトコルが提案されてきた。しかしながら、提案された暗号プロトコルの仕様が公開された後に、セキュリティ上の脆弱性が指摘されるケースが散見された。実際、標準化された暗号プロトコルが製品等を通じて、広く普及した後に、脆弱性が発見される場合、改修に関わるコストが大きな問題となる。
【０００３】
特に、致命的な脆弱性が発見された場合には、経済的な損害の回避を目的とし、ソフトウェアのパッチの充当やハードウェアのチップ・部品の交換など、早急に対処する必要が生じる。したがって、提案された暗号プロトコルや関連製品が普及すればするほど、社会的なインパクトは非常に大きくなり、場合によってはシステム全体が破綻してしまう可能性もある。
【０００４】
そのため、特許文献１および特許文献２に記載の記述では、「汎用結合可能安全性」と呼ばれる概念を利用した、暗号プロトコルの安全性を検証するための装置、方法、プログラムが開示されている。ここで、「汎用結合可能安全性」とは、ある暗号プロトコルがそのセキュリティ機能に関する理想機能を安全に実現するならば、この暗号プロトコルは安全であることを意味している。例えば、ある鍵交換プロトコルが鍵交換理想機能を安全に実現するならば、その鍵交換プロトコルは安全であることが示されたことになる。
【特許文献１】特開２００７−２８４４７号公報
【特許文献２】特開２００８−３５１１７号公報
【発明の開示】
【発明が解決しようとする課題】
【０００５】
上記の先行技術文献において使用されている「汎用結合可能安全性」は、現在最も強力な安全性であると言われており、理想機能はセキュリティ機能に要求されるすべての安全性を網羅する。そのため、ある暗号プロトコルがその理想機能を安全に実現するとき、この暗号プロトコルはセキュリティ機能に要求されるすべての安全性を満足することになる。
【０００６】
しかしながら、暗号プロトコルの安全性と効率性はトレードオフの関係にあり、暗号プロトコルの安全性を高くするにつれて、効率性が低くなっていく。そのため、暗号プロトコルの効率性を重要視するときには、許容される範囲まで安全性を低くしたい。しかしながら、上記の先行技術では、暗号プロトコルの厳密な安全性を検証することはできても、安全性レベルに応じた検証を行うことができない。
【０００７】
そこで、本発明は、上述の課題に鑑みてなされたものであり、暗号プロトコルを安全性レベルに応じて検証することができる暗号プロトコルの安全性検証装置、安全性検証方法およびプログラムを提供することを目的とする。
【課題を解決するための手段】
【０００８】
本発明は、上記の課題を解決するために、以下の事項を提案している。
【０００９】
（１）本発明は、少なくとも認証や鍵共有のセキュリティ機能を有する暗号プロトコルのうち、認証プロトコル及び鍵交換プロトコルの安全性を検証する検証手段を備えた暗号プロトコルの安全性検証装置を提案している。
【００１０】
（２）本発明は、（１）の暗号プロトコルの安全性検証装置について、前記検証手段が、前記認証プロトコルの安全性を検証する検証項目として、認証プロトコルの能動的攻撃安全における検証項目を含むことを特徴とする暗号プロトコルの安全性検証装置を提案している。
【００１１】
（３）本発明は、（２）の暗号プロトコルの安全性検証装置について、前記認証プロトコルの能動的攻撃安全における検証項目として、前記検証手段が、認証対象となる暗号プリミティブが偽造不可能性の性質を有し、該暗号プリミティブの引数がいずれもプロトコルに初めて現れたか、同じセッションにおいて以前にプロトコルに現れたか、別のセッションにおいて繰り返し使用不可能でプロトコルに現れた一時的な公開情報であるか、または、プロトコルに初めて現れたか、同じセッションにおいて以前にプロトコルに現れたか、別のセッションにおいて繰り返し使用不可能でプロトコルに現れた一時的な秘密情報を含んでいるか、あるいは、認証対象となる暗号プリミティブが一方向性の性質を有し、該暗号プリミティブの引数がいずれもプロトコルに初めて現れた一時的な秘密情報を含んでいるか、をチェックすることを特徴とする暗号プロトコルの安全性検証装置を提案している。
【００１２】
（４）本発明は、（１）の暗号プロトコルの安全性検証装置について、前記検証手段が、前記鍵交換プロトコルの安全性を検証する検証項目として、鍵交換プロトコルの能動的攻撃安全、受動的攻撃安全、オフライン辞書攻撃安全、既知鍵攻撃安全、フォワード秘匿性における検証項目を含むことを特徴とする暗号プロトコルの安全性検証装置を提案している。
【００１３】
（５）本発明は、（４）の暗号プロトコルの安全性検証装置について、前記鍵交換プロトコルの能動的攻撃安全における検証項目として、鍵生成対象となる暗号プリミティブの引数に含まれる暗号プリミティブが識別不可能性または一方向性の性質を有し、該暗号プリミティブの引数がいずれもプロトコルに初めて現れた一時的な秘密情報と、別のセッションにおいて繰り返し使用可能でプロトコルに現れた長期的で完全な秘密情報または長期的で不完全な秘密情報を含んでいるか、をチェックすることを特徴とする暗号プロトコルの安全性検証装置を提案している。
【００１４】
（６）本発明は、（４）の暗号プロトコルの安全性検証装置について、前記鍵交換プロトコルの受動的攻撃安全における検証項目として、鍵生成対象となる暗号プリミティブが識別不可能性の性質を有し、該暗号プリミティブの引数がいずれもプロトコルに初めて現れた一時的な秘密情報を含んでいるか、あるいは鍵生成対象となる暗号プリミティブが一方向性の性質を有し、該暗号プリミティブの引数に含まれる暗号プリミティブが識別不可能性の性質を有し、該暗号プリミティブの引数がプロトコルに初めて現れた一時的な秘密情報を含んでいるか、をチェックすることを特徴とする暗号プロトコルの安全性検証装置を提案している。
【００１５】
（７）本発明は、（４）の暗号プロトコルの安全性検証装置について、前記鍵交換プロトコルのオフライン辞書攻撃安全における検証項目として、長期的で不完全な秘密情報を含む暗号プリミティブが一方向性の性質を有し、該暗号プリミティブの引数がいずれもプロトコルに初めて現れたか、同じセッションにおいて以前にプロトコルに現れたか、別のセッションにおいて繰り返し使用不可能でプロトコルに現れた一時的な秘密情報を含んでいるか、をチェックすることを特徴とする暗号プロトコルの安全性検証装置を提案している。
【００１６】
（８）本発明は、（４）の暗号プロトコルの安全性検証装置について、前記鍵交換プロトコルの既知鍵攻撃安全における検証項目として、鍵生成対象となる暗号プリミティブが識別不可能性または一方向性の性質を有し、該暗号プリミティブの引数がいずれもプロトコルに初めて現れたか、同じセッションにおいて以前にプロトコルに現れたか、別のセッションにおいて繰り返し使用不可能でプロトコルに現れた一時的な秘密情報を含んでいるか、をチェックすることを特徴とする暗号プロトコルの安全性検証装置を提案している。
【００１７】
（９）本発明は、（４）の暗号プロトコルの安全性検証装置について、前記鍵交換プロトコルのフォワード秘匿性における検証項目として、鍵生成対象となる暗号プリミティブが識別不可能性または一方向性の性質を有し、該暗号プリミティブの引数がいずれもプロトコルに初めて現れたか、同じセッションにおいて以前にプロトコルに現れたか、別のセッションにおいて繰り返し使用不可能でプロトコルに現れた一時的な秘密情報を含んでいるか、をチェックすることを特徴とする暗号プロトコルの安全性検証装置を提案している。
【００１８】
（１０）本発明は、暗号プロトコルの安全性を検証するための安全性検証方法であって、認証および鍵交換プロトコルにおいて使用されている暗号プリミティブを列挙する第１のステップと、前記列挙した暗号プリミティブについて、危殆化情報の有無を検証し、危殆化情報を有するものがある場合に、前記暗号プロトコルは安全ではないと判断する第２のステップと、該列挙した暗号プリミティブの中に、危殆化情報を有するものがない場合に、前記暗号プリミティブの役割を設定する第３のステップと、前記暗号プリミティブの安全性の根拠の設定を行う第４のステップと、フローの列挙を行う第５のステップと、フローデータと暗号プリミティブの引数の種類と状態とを設定する第６のステップと、該設定したフローデータと暗号プリミティブの引数の種類と状態との関係が正しいか否かを判断し、正しくないものを含む場合に、前記暗号プロトコルは安全ではないと判断する第７のステップと、前記設定したフローデータと暗号プリミティブの引数の種類と状態との関係がすべて正しいと判断した場合に、安全性に関する検証項目の選択を行う第８のステップと、該選択した検証項目をすべて満足するか否かを判断し、満足しないものを含む場合に、前記暗号プロトコルは選択した安全性に関して安全ではないと判断する第９のステップと、前記選択した検証項目をすべて満足する場合に、前記暗号プロトコルは安全であると判断する第１０のステップと、を有することを特徴とする安全性検証方法を提案している。
【００１９】
（１１）本発明は、コンピュータに、暗号プロトコルの安全性を検証するための安全性検証方法を実行させるためのプログラムであって、認証および鍵交換プロトコルにおいて使用されている暗号プリミティブを列挙する第１のステップと、前記列挙した暗号プリミティブについて、危殆化情報の有無を検証し、危殆化情報を有するものがある場合に、前記暗号プロトコルは安全ではないと判断する第２のステップと、該列挙した暗号プリミティブの中に、危殆化情報を有するものがない場合に、前記暗号プリミティブの役割を設定する第３のステップと、前記暗号プリミティブの安全性の根拠の設定を行う第４のステップと、フローの列挙を行う第５のステップと、フローデータと暗号プリミティブの引数の種類と状態とを設定する第６のステップと、該設定したフローデータと暗号プリミティブの引数の種類と状態との関係が正しいか否かを判断し、正しくないものを含む場合に、前記暗号プロトコルは安全ではないと判断する第７のステップと、前記設定したフローデータと暗号プリミティブの引数の種類と状態との関係がすべて正しいと判断した場合に、安全性に関する検証項目の選択を行う第８のステップと、該選択した検証項目をすべて満足するか否かを判断し、満足しないものを含む場合に、前記暗号プロトコルは選択した安全性に関して安全ではないと判断する第９のステップと、前記選択した検証項目をすべて満足する場合に、前記暗号プロトコルは安全であると判断する第１０のステップと、コンピュータに実行させるためのプログラムを提案している。
【発明の効果】
【００２０】
本発明によれば、暗号プロトコルのうち、認証プロトコルと鍵交換プロトコルを安全性レベルに応じて検証することができるという効果がある。
【発明を実施するための最良の形態】
【００２１】
以下、図面を用いて、本発明の実施形態について詳細に説明する。
なお、本実施形態における構成要素は適宜、既存の構成要素等との置き換えが可能であり、また、他の既存の構成要素との組み合わせを含む様々なバリエーションが可能である。したがって、本実施形態の記載をもって、特許請求の範囲に記載された発明の内容を限定するものではない。
【００２２】
＜暗号プロトコルの安全性レベルに関する既存のセキュリティモデル＞
本発明の実施形態の説明に入る前に、暗号プロトコルの安全性レベルに関して、既存のセキュリティモデルを示す。本発明では、計算量理論にもとづいて、暗号プロトコルの安全性を証明するという「証明可能安全性」と呼ばれる概念を用いる。「暗号プロトコルが証明可能安全性を有する」とは、暗号プロトコルの安全性が、ある暗号プリミティブの安全性に帰着することを計算量理論的に証明可能であることである。
【００２３】
ある暗号プロトコルを破る攻撃者を仮定した場合、ある暗号プリミティブを多項式時間で破るマシンを構成可能であることを証明することにより、この暗号プリミティブが破られなければ、暗号プロトコルも破られないことを証明する。本発明では、暗号プロトコルのうち、認証プロトコルと鍵交換プロトコルとを考える。
【００２４】
上記の証明可能安全性において、認証プロトコルではｍａｔｃｈｉｎｇ
ｃｏｎｖｅｒｓａｔｉｏｎ、鍵交換プロトコルではｓｅｍａｎｔｉｃ ｓｅｃｕｒｉｔｙという安全性の概念がある。それぞれの概念に対し、認証・鍵交換プロトコルに要求される安全性に応じて、現実の攻撃モデルを想定し、以下の安全性に分類した。ただし、（）内は、安全性に対応する攻撃を表している。
【００２５】
（１）ｍａｔｃｈｉｎｇ ｃｏｎｖｅｒｓａｔｉｏｎ
認証プロトコルにおいて、攻撃者が一方のパーティから受信したメッセージをそのままもう一方のパーティへ送ること以外に何もできないことを示す。すなわち、攻撃者は、メッセージの改ざんや新規メッセージの送付、メッセージの遮断、メッセージの順番の入れ替えなどの不正を行うことができない。
【００２６】
（１Ａ）能動的攻撃安全（なり済まし攻撃）
ｍａｔｃｈｉｎｇ ｃｏｎｖｅｒｓａｔｉｏｎにおける能動的攻撃安全は、攻撃者がパーティ間の通信を支配しても、認証プロトコルを破ることはできないことを示す。
【００２７】
（２）ｓｅｍａｎｔｉｃ ｓｅｃｕｒｉｔｙ
鍵交換プロトコルにおいて、攻撃者はセッション鍵に関するどんな情報も得ることができないことを示す。すなわち、攻撃者はセッション鍵と乱数を多項式時間で区別することができない。
【００２８】
（２Ａ）能動的攻撃安全（なり済まし攻撃）
ｓｅｍａｎｔｉｃ ｓｅｃｕｒｉｔｙにおける能動的攻撃安全は、攻撃者がパーティ間の通信を支配しても、鍵交換プロトコルを破ることはできないことを示す。
【００２９】
（２Ｂ）受動的攻撃安全（盗聴攻撃）
ｓｅｍａｎｔｉｃ ｓｅｃｕｒｉｔｙにおける受動的攻撃安全は、攻撃者がパーティ間の通信を盗聴しても、鍵交換プロトコルを破ることはできないことを示す。
【００３０】
（２Ｃ）オフライン辞書攻撃安全（オフライン辞書攻撃）
ｓｅｍａｎｔｉｃ ｓｅｃｕｒｉｔｙにおけるオフライン辞書攻撃安全は、攻撃者がパスワード推測用の辞書からオフラインで過去の履歴に一致するパーティのパスワードを探索することはできないことを示す。
【００３１】
（２Ｄ）既知鍵攻撃安全（既知鍵攻撃）
ｓｅｍａｎｔｉｃ ｓｅｃｕｒｉｔｙにおける既知鍵攻撃安全は、攻撃者があるセッション鍵を得ることができたとしても、それとは別のセッション鍵を得ることはできないことを示す。
【００３２】
（２Ｅ）ｆｏｒｗａｒｄ ｓｅｃｒｅｃｙ（長期鍵破壊攻撃）
ｓｅｍａｎｔｉｃ ｓｅｃｕｒｉｔｙにおけるｆｏｒｗａｒｄ
ｓｅｃｒｅｃｙは、攻撃者が秘密鍵やパスワードなどの長期鍵を得ることができたとしても、それ以前に共有されたセッション鍵を得ることはできないことを示す。
【００３３】
ただし、パスワード、長期鍵をそれぞれ使用しない鍵交換プロトコルの場合、（２Ｃ）のオフライン辞書攻撃安全、（２Ｅ）のｆｏｒｗａｒｄ
ｓｅｃｒｅｃｙの安全性はそれぞれ要求されない。
【００３４】
＜暗号プリミティブに設定される情報と記号＞
認証・鍵交換プロトコルにおいて使用されている暗号プリミティブに設定される情報は以下のとおりである。
（Ａ）認証プロトコルにおける認証対象となる暗号プリミティブ（ＡＧＦ）
（Ｂ）鍵交換プロトコルにおける鍵生成対象となる暗号プリミティブ（ＫＧＦ）
（Ｃ）ＡＧＦやＫＧＦの引数に含まれる暗号プリミティブ（ＡＣＰ）
（Ｄ）それ以外の暗号プリミティブ（ＯＣＰ）
【００３５】
＜暗号プリミティブに対して設定される安全性の根拠となる情報＞
上記で設定された暗号プリミティブに対して設定される安全性の根拠となる情報は以下のとおりである。
（Ａ）識別不可能性（ＩＮＤ）: 秘密情報を知らずに、対応する２つの事象を多項式時間で識別することができないことを示す。
（Ｂ）一方向性（ＯＷ）: 秘密情報を知らずに、出力値から入力値を多項式時間で計算することができないことを示す。
（Ｃ）偽造不可能性（ＵＦ）: 秘密情報を知らずに、要求されるメッセージの認証子を多項式時間で生成することができないことを示す。
【００３６】
＜認証・鍵交換プロトコルにおけるすべてのフローデータ及び暗号プリミティブに設定される構成要素＞
認証・鍵交換プロトコルにおけるすべてのフローデータ及び暗号プリミティブに設定される構成要素は以下のとおりである。
（Ａ）フローデータ及び暗号プリミティブの引数の種類
ａ）一般公開情報（ＰＵＢ）
ｂ）特定公開情報（ＩＤ）
ｃ）一時的な公開情報（ＴＰＫ）
ｄ）長期的で完全な秘密情報（ＬＬＫ）
ｅ）長期的で不完全な秘密情報（ＰＷ）
ｆ）一時的な秘密情報（ＴＳＫ）
（Ｂ）フローデータ及び暗号プリミティブの引数の状態
ａ）公開状態で初登場（ＰＦＴ）
ｂ）同じセッションにおいて以前に公開状態で登場（ＰＳＳ）
ｃ）別のセッションにおいて繰り返し使用可能で公開状態で登場（ＰＲＳ）
ｄ）別のセッションにおいて繰り返し使用不可能で公開状態で登場（ＰＮＳ）
ｅ）秘密状態で初登場（ＳＦＴ）
ｆ）同じセッションにおいて以前に秘密状態で登場（ＳＳＳ）
ｇ）別のセッションにおいて繰り返し使用可能で秘密状態で登場（ＳＲＳ）
ｈ）別のセッションにおいて繰り返し使用不可能で秘密状態で登場（ＳＮＳ）
【００３７】
＜認証及び鍵交換プロトコルを安全性レベルに応じて検証する項目＞
また、認証及び鍵交換プロトコルを安全性レベルに応じて検証する項目は、以下の通りである。
【００３８】
＜認証プロトコルに対するｍａｔｃｈｉｎｇ ｃｏｎｖｅｒｓａｔｉｏｎ＞
（Ａ）能動的攻撃安全における検証項目と検証内容
ａ）ＡＧＦがＵＦであり、ＡＧＦの引数がいずれもＴＰＫ−ＰＦＴまたはＴＰＫ−ＰＳＳまたはＴＰＫ−ＰＮＳまたはＴＳＫ−ＳＦＴまたはＴＳＫ−ＳＳＳまたはＴＳＫ−ＳＮＳを含んでいる。
ｂ）ＡＧＦがＯＷであり、ＡＧＦの引数がいずれもＴＳＫ−ＳＦＴを含んでいる。
【００３９】
＜鍵交換プロトコルに対するｓｅｍａｎｔｉｃ ｓｅｃｕｒｉｔｙ＞
（Ｂ）能動的攻撃安全における検証項目と検証内容
ａ）ＡＣＰがＩＮＤまたはＯＷであり、ＡＣＰの引数がいずれもＴＳＫ−ＳＦＴとＬＬＫ−ＳＲＳまたはＰＷ−ＳＲＳを含んでいる。
【００４０】
（Ｃ）受動的攻撃安全における検証項目と検証内容
ａ）ＫＧＦがＩＮＤであり、ＫＧＦの引数がいずれもＴＳＫ−ＳＦＴを含んでいる。
ｂ）ＫＧＦがＯＷであり、ＡＣＰがＩＮＤであり、ＡＣＰの引数がＴＳＫ−ＳＦＴを含んでいる。
【００４１】
（Ｄ）オフライン辞書攻撃安全における検証項目と検証内容
ａ）ＰＷを含むＯＣＰがＯＷであり、ＯＣＰの引数がいずれもＴＳＫ−ＳＦＴまたはＴＳＫ−ＳＳＳまたはＴＳＫ−ＳＮＳを含んでいる。
【００４２】
（Ｅ）既知鍵攻撃安全における検証項目と検証内容
ａ）ＫＧＦがＩＮＤまたはＯＷであり、ＫＧＦの引数がいずれもＴＳＫ−ＳＦＴまたはＴＳＫ−ＳＳＳまたはＴＳＫ−ＳＮＳを含んでいる。
【００４３】
（Ｆ）ｆｏｒｗａｒｄ ｓｅｃｒｅｃｙにおける検証項目と検証内容
ａ）ＫＧＦがＩＮＤまたはＯＷであり、ＫＧＦの引数がいずれもＴＳＫ−ＳＦＴまたはＴＳＫ−ＳＳＳまたはＴＳＫ−ＳＮＳを含んでいる。
【００４４】
＜暗号プロトコルの安全性検証装置の構成＞
図１を用いて、本実施形態に係る暗号プロトコルの安全性検証装置の構成について説明する。本実施形態に係る暗号プロトコルの安全性検証装置は、図１に示すように、暗号プリミティブ列挙部１と、危殆化情報判定部２と、役割設定部３と、安全性根拠設定部４と、フロー列挙部５と、引数設定部６と、設定情報判定部７と、安全性選択部８と、検証項目判定部９と、安全性判定部１０とから構成されている。
【００４５】
暗号プリミティブ列挙部１は、認証・鍵交換プロトコルにおいて使用されている暗号プリミティブをすべて列挙する。危殆化情報判定部２は、列挙された暗号プリミティブに対して危殆化情報があるかどうかを確認する。危殆化情報が１つでもある場合、安全性判定部１０が、認証・鍵交換プロトコルは安全ではないと判定する。
【００４６】
役割設定部３は、列挙された暗号プリミティブのうち、暗号プリミティブの役割である情報、例えば、ＡＧＦ、ＫＧＦ、ＡＣＰ、ＯＣＰを設定する。安全性根拠設定部４は、役割が設定された暗号プリミティブに対して、安全性の根拠となる情報、例えば、ＩＮＤ、ＯＷ、ＵＦを設定する。
【００４７】
フロー列挙部５は、認証・鍵交換プロトコルについて、すべてのフローを列挙する。引数設定部６は、列挙されたフローデータ及び暗号プリミティブについて、フローデータ及び暗号プリミティブの引数の種類、例えば、ＰＵＢ、ＩＤ、ＴＰＫ、ＬＬＫ、ＰＷ、ＴＳＫ等、およびフローデータ及び暗号プリミティブの引数の状態、例えば、ＰＦＴ、ＰＳＳ、ＰＲＳ、ＰＮＳ、ＳＦＴ、ＳＳＳ、ＳＲＳ、ＳＮＳ等の構成要素を設定する。
【００４８】
設定情報判定部７は、図２に示すフローデータ及び暗号プリミティブの引数の種類と状態の関係を示したデータテーブルに基づいて、フローデータ及び暗号プリミティブの引数に関する種類と状態の関係がすべて正しいかどうかを判定する。そして、１つでも正しくない関係がある場合には、安全性判定部１０が、認証・鍵交換プロトコルは安全ではないと判定する。
【００４９】
安全性選択部８は、認証・鍵交換プロトコルにおいて、要求されている安全性を選択する。なお、複数の安全性を選択してもよい。検証項目判定部９は、安全性選択部８が選択した安全性に対して、引数設定部６が設定した情報を用いて、前述した各安全性に関する検証項目を検証する。
【００５０】
ただし、検証項目を検証する前に、認証・鍵交換プロトコルにおける各安全性に応じて、以下の準備を行う。
＜認証プロトコルに対するｍａｔｃｈｉｎｇ ｃｏｎｖｅｒｓａｔｉｏｎ＞
（Ａ）能動的攻撃安全における検証項目
能動的攻撃安全は、なり済まし攻撃に対応し、攻撃者がパーティ間の通信を支配して得られる情報から、相手のパーティに認証させるための情報を生成することができないことを示している。なお、なり済まし攻撃により設定される情報は、すべてのフローである。
【００５１】
設定された情報に対し、プロトコルのフロー順に以下の事項を設定する。ここで、フローデータと引数の状態は更新されていくものとする。ただし、公開状態と秘密状態では、公開状態を優先するものとする。
ａ）ＡＧＦ、ＡＣＰ、ＯＣＰの種類と安全性の根拠
ｂ）ＡＧＦ、ＡＣＰ、ＯＣＰの引数の種類と状態
ｃ）フローデータの種類と状態
【００５２】
なお、ＡＧＦとＡＣＰの引数に暗号プリミティブが入れ子構造になっている場合、ＡＧＦとＡＣＰの引き数の状態を最終段階に設定する。
【００５３】
＜鍵交換プロトコルに対するｓｅｍａｎｔｉｃ ｓｅｃｕｒｉｔｙ＞
（Ａ）能動的攻撃安全における検証項目
能動的攻撃安全は、なり済まし攻撃に対応し、攻撃者がパーティ間の通信を支配して得られる情報から、セッション鍵と乱数を多項式時間で区別することができないことを示している。なお、なり済まし攻撃により設定される情報はすべてのフローである。
【００５４】
設定された情報に対し、プロトコルのフロー順に以下の事項を設定する。ここで、フローデータと引数の状態は更新されていくものとする。ただし、公開状態と秘密状態では、公開状態を優先するものとする。
ａ）ＫＧＦ、ＡＣＰ、ＯＣＰの種類と安全性の根拠
ｂ）ＫＧＦ、ＡＣＰ、ＯＣＰの引数の種類と状態
ｃ）フローデータの種類と状態
【００５５】
なお、ＫＧＦとＡＣＰの引数に暗号プリミティブが入れ子構造になっている場合、ＫＧＦとＡＣＰの引き数の状態を最終段階に設定する。
【００５６】
（Ｂ）受動的攻撃安全における検証項目
受動的攻撃安全は、盗聴攻撃に対応し、攻撃者がパーティ間の通信を盗聴して得られる情報から、セッション鍵と乱数を多項式時間で区別することができないことを示している。なお、盗聴攻撃により設定される情報は、すべてのフローである。
【００５７】
設定された情報に対し、プロトコルのフロー順に以下の事項を設定する。ここで、フローデータと引数の状態は更新されていくものとする。ただし、公開状態と秘密状態では、公開状態を優先するものとする。
ａ）ＫＧＦ、ＡＣＰ、ＯＣＰの種類と安全性の根拠
ｂ）ＫＧＦ、ＡＣＰ、ＯＣＰの引数の種類と状態
ｃ）フローデータの種類と状態
【００５８】
なお、ＫＧＦとＡＣＰの引数に暗号プリミティブが入れ子構造になっている場合、ＫＧＦとＡＣＰの引き数の状態を最終段階に設定する。
【００５９】
（Ｃ）オフライン辞書攻撃安全における検証項目
オフライン辞書攻撃安全は、オフライン辞書攻撃に対応し、攻撃者がパスワード推測用の辞書からパーティのパスワードをオフラインで探索するための過去の履歴から、セッション鍵と乱数を多項式時間で区別することができないことを示している。なお、オフライン辞書攻撃により設定される情報は、すべてのフローである。
【００６０】
設定された情報に対し、プロトコルのフロー順に以下の事項を設定する。ここで、フローデータと引数の状態は更新されていくものとする。ただし、公開状態と秘密状態では、公開状態を優先するものとする。
ａ）ＯＣＰの種類と安全性の根拠
ｂ）ＯＣＰの引数の種類と状態
ｃ）フローデータの種類と状態
【００６１】
（Ｄ）既知鍵攻撃安全における検証項目
既知鍵攻撃安全は、既知鍵攻撃に対応し、攻撃者が別のセッションにおいて得られたセッション鍵から、セッション鍵と乱数を多項式時間で区別することができないことを示している。なお、既知鍵攻撃により設定される情報は、他のすべてのセッションのセッション鍵である。
【００６２】
設定された情報に対し、プロトコルのフロー順に以下の事項を設定する。ここで、フローデータと引数の状態は更新されていくものとする。ただし、公開状態と秘密状態では、公開状態を優先するものとする。
ａ）ＫＧＦ、ＡＣＰ、ＯＣＰの種類と安全性の根拠
ｂ）ＫＧＦ、ＡＣＰ、ＯＣＰの引数の種類と状態
ｃ）フローデータの種類と状態
【００６３】
なお、ＫＧＦとＡＣＰの引数に暗号プリミティブが入れ子構造になっている場合、ＫＧＦとＡＣＰの引き数の状態を最終段階に設定する。
【００６４】
（Ｅ）ｆｏｒｗａｒｄ ｓｅｃｒｅｃｙにおける検証項目
ｆｏｒｗａｒｄ ｓｅｃｒｅｃｙは、長期鍵破壊攻撃に対応し、攻撃者がパーティの端末に侵入して得られた秘密鍵やパスワードなどの長期鍵から、セッション鍵と乱数を多項式時間で区別することができないことを示している。なお、長期鍵破壊攻撃により設定される情報は、長期鍵である。
【００６５】
設定された情報に対し、プロトコルのフロー順に以下の事項を設定する。ここで、フローデータと引数の状態は更新されていくものとする。ただし、公開状態と秘密状態では、公開状態を優先するものとする。この場合、長期鍵は公開情報として扱う。
ａ）ＫＧＦ、ＡＣＰ、ＯＣＰの種類と安全性の根拠
ｂ）ＫＧＦ、ＡＣＰ、ＯＣＰの引数の種類と状態
ｃ）フローデータの種類と状態
【００６６】
なお、ＫＧＦとＡＣＰの引数に暗号プリミティブが入れ子構造になっている場合、ＫＧＦとＡＣＰの引き数の状態を最終段階に設定する。
【００６７】
＜暗号プロトコルの安全性検証装置の処理＞
図３を用いて、暗号プロトコルの安全性検証装置の処理について、説明する。
まず、認証および鍵交換プロトコルにおいて使用されている暗号プリミティブを列挙する（ステップＳ１０１）。次に、列挙した暗号プリミティブについて、危殆化情報の有無を検証し（ステップＳ１０２）、危殆化情報を有するものがある場合（ステップＳ１０２の「Ｎｏ」）に、暗号プロトコルは安全ではないと判断する。
【００６８】
一方、列挙した暗号プリミティブの中に、危殆化情報を有するものがない場合に（ステップＳ１０２の「Ｙｅｓ」）、暗号プリミティブの役割を設定する（ステップＳ１０３）。さらに、暗号プリミティブの安全性の根拠の設定を行い（ステップＳ１０４）、フローの列挙を行って（ステップＳ１０５）、フローデータと暗号プリミティブの引数の種類と状態とを設定する（ステップＳ１０６）。
【００６９】
そして、設定したフローデータと暗号プリミティブの引数の種類と状態との関係が正しいか否かを判断し（ステップＳ１０７）、正しくないものを含む場合に（ステップＳ１０７の「Ｎｏ」）、暗号プロトコルは安全ではないと判断する。一方、設定したフローデータと暗号プリミティブの引数の種類と状態との関係がすべて正しいと判断した場合に（ステップＳ１０７の「Ｙｅｓ」）、安全性に関する検証項目の選択を行う（ステップＳ１０８）。
【００７０】
そして、選択した検証項目をすべて満足するか否かを判断し（ステップＳ１０９）、満足しないものを含む場合に（ステップＳ１０９の「Ｎｏ」）、暗号プロトコルは選択した安全性に関して安全ではないと判断し、選択した検証項目をすべて満足する場合に（ステップＳ１０９の「Ｙｅｓ」）、暗号プロトコルは安全であると判断する。
【００７１】
したがって、本実施形態によれば、暗号プロトコルのうち、認証プロトコルと鍵交換プロトコルを安全性レベルに応じて検証することができる。
【００７２】
なお、上述の一連の処理をプログラムとしてコンピュータ読み取り可能な記録媒体に記録し、この記録媒体に記録されたプログラムを暗号プロトコルの安全性検証装置に読み込ませ、実行することによって本発明の暗号プロトコルの安全性検証装置を実現することができる。
【００７３】
また、ＷＷＷ（Ｗｏｒｌｄ Ｗｉｄｅ Ｗｅｂ）システムを利用している場合であれば、ホームページ提供環境（あるいは表示環境）も含むものとする。また、上記プログラムは、このプログラムを記憶装置等に格納したコンピュータから、伝送媒体を介して、あるいは、伝送媒体中の伝送波により他のコンピュータに伝送されてもよい。ここで、プログラムを伝送する「伝送媒体」は、インターネット等のネットワーク（通信網）や電話回線等の通信回線（通信線）のように情報を伝送する機能を有する媒体のことをいう。
【００７４】
また、上記プログラムは、前述した機能の一部を実現するためのものであっても良い。さらに、前述した機能をコンピュータにすでに記録されているプログラムとの組合せで実現できるもの、いわゆる差分ファイル（差分プログラム）であっても良い。
【００７５】
以上、この発明の実施形態につき、図面を参照して詳述してきたが、具体的な構成はこの実施形態に限られるものではなく、この発明の要旨を逸脱しない範囲の設計等も含まれる。
【図面の簡単な説明】
【００７６】
【図１】本実施形態に係る暗号プロトコルの安全性検証装置の構成を示す図である。
【図２】本実施形態に係るフローデータと暗号プリミティブの引数の種類と状態との関係を示す図である。
【図３】本実施形態に係る暗号プロトコルの安全性検証装置の処理フローである。
【符号の説明】
【００７７】
１・・・暗号プリミティブ列挙部
２・・・危殆化情報判定部
３・・・役割設定部
４・・・安全性根拠設定部
５・・・フロー列挙部
６・・・引数設定部
７・・・設定情報判定部
８・・・安全性選択部
９・・・検証項目判定部
１０・・・安全性判定部
【技術分野】
【０００１】
本発明は、認証や鍵共有などのセキュリティ機能を有する暗号プロトコルに関し、そうした暗号プロトコルの安全性を検証する暗号プロトコルの安全性検証装置、安全性検証方法およびプログラムに関する。
【背景技術】
【０００２】
従来、プロトコル設計者の有するセキュリティ、暗号技術の見識に基づき、ヒューリスティックなアプローチで経験的に、安全な暗号プロトコルが提案されてきた。しかしながら、提案された暗号プロトコルの仕様が公開された後に、セキュリティ上の脆弱性が指摘されるケースが散見された。実際、標準化された暗号プロトコルが製品等を通じて、広く普及した後に、脆弱性が発見される場合、改修に関わるコストが大きな問題となる。
【０００３】
特に、致命的な脆弱性が発見された場合には、経済的な損害の回避を目的とし、ソフトウェアのパッチの充当やハードウェアのチップ・部品の交換など、早急に対処する必要が生じる。したがって、提案された暗号プロトコルや関連製品が普及すればするほど、社会的なインパクトは非常に大きくなり、場合によってはシステム全体が破綻してしまう可能性もある。
【０００４】
そのため、特許文献１および特許文献２に記載の記述では、「汎用結合可能安全性」と呼ばれる概念を利用した、暗号プロトコルの安全性を検証するための装置、方法、プログラムが開示されている。ここで、「汎用結合可能安全性」とは、ある暗号プロトコルがそのセキュリティ機能に関する理想機能を安全に実現するならば、この暗号プロトコルは安全であることを意味している。例えば、ある鍵交換プロトコルが鍵交換理想機能を安全に実現するならば、その鍵交換プロトコルは安全であることが示されたことになる。
【特許文献１】特開２００７−２８４４７号公報
【特許文献２】特開２００８−３５１１７号公報
【発明の開示】
【発明が解決しようとする課題】
【０００５】
上記の先行技術文献において使用されている「汎用結合可能安全性」は、現在最も強力な安全性であると言われており、理想機能はセキュリティ機能に要求されるすべての安全性を網羅する。そのため、ある暗号プロトコルがその理想機能を安全に実現するとき、この暗号プロトコルはセキュリティ機能に要求されるすべての安全性を満足することになる。
【０００６】
しかしながら、暗号プロトコルの安全性と効率性はトレードオフの関係にあり、暗号プロトコルの安全性を高くするにつれて、効率性が低くなっていく。そのため、暗号プロトコルの効率性を重要視するときには、許容される範囲まで安全性を低くしたい。しかしながら、上記の先行技術では、暗号プロトコルの厳密な安全性を検証することはできても、安全性レベルに応じた検証を行うことができない。
【０００７】
そこで、本発明は、上述の課題に鑑みてなされたものであり、暗号プロトコルを安全性レベルに応じて検証することができる暗号プロトコルの安全性検証装置、安全性検証方法およびプログラムを提供することを目的とする。
【課題を解決するための手段】
【０００８】
本発明は、上記の課題を解決するために、以下の事項を提案している。
【０００９】
（１）本発明は、少なくとも認証や鍵共有のセキュリティ機能を有する暗号プロトコルのうち、認証プロトコル及び鍵交換プロトコルの安全性を検証する検証手段を備えた暗号プロトコルの安全性検証装置を提案している。
【００１０】
（２）本発明は、（１）の暗号プロトコルの安全性検証装置について、前記検証手段が、前記認証プロトコルの安全性を検証する検証項目として、認証プロトコルの能動的攻撃安全における検証項目を含むことを特徴とする暗号プロトコルの安全性検証装置を提案している。
【００１１】
（３）本発明は、（２）の暗号プロトコルの安全性検証装置について、前記認証プロトコルの能動的攻撃安全における検証項目として、前記検証手段が、認証対象となる暗号プリミティブが偽造不可能性の性質を有し、該暗号プリミティブの引数がいずれもプロトコルに初めて現れたか、同じセッションにおいて以前にプロトコルに現れたか、別のセッションにおいて繰り返し使用不可能でプロトコルに現れた一時的な公開情報であるか、または、プロトコルに初めて現れたか、同じセッションにおいて以前にプロトコルに現れたか、別のセッションにおいて繰り返し使用不可能でプロトコルに現れた一時的な秘密情報を含んでいるか、あるいは、認証対象となる暗号プリミティブが一方向性の性質を有し、該暗号プリミティブの引数がいずれもプロトコルに初めて現れた一時的な秘密情報を含んでいるか、をチェックすることを特徴とする暗号プロトコルの安全性検証装置を提案している。
【００１２】
（４）本発明は、（１）の暗号プロトコルの安全性検証装置について、前記検証手段が、前記鍵交換プロトコルの安全性を検証する検証項目として、鍵交換プロトコルの能動的攻撃安全、受動的攻撃安全、オフライン辞書攻撃安全、既知鍵攻撃安全、フォワード秘匿性における検証項目を含むことを特徴とする暗号プロトコルの安全性検証装置を提案している。
【００１３】
（５）本発明は、（４）の暗号プロトコルの安全性検証装置について、前記鍵交換プロトコルの能動的攻撃安全における検証項目として、鍵生成対象となる暗号プリミティブの引数に含まれる暗号プリミティブが識別不可能性または一方向性の性質を有し、該暗号プリミティブの引数がいずれもプロトコルに初めて現れた一時的な秘密情報と、別のセッションにおいて繰り返し使用可能でプロトコルに現れた長期的で完全な秘密情報または長期的で不完全な秘密情報を含んでいるか、をチェックすることを特徴とする暗号プロトコルの安全性検証装置を提案している。
【００１４】
（６）本発明は、（４）の暗号プロトコルの安全性検証装置について、前記鍵交換プロトコルの受動的攻撃安全における検証項目として、鍵生成対象となる暗号プリミティブが識別不可能性の性質を有し、該暗号プリミティブの引数がいずれもプロトコルに初めて現れた一時的な秘密情報を含んでいるか、あるいは鍵生成対象となる暗号プリミティブが一方向性の性質を有し、該暗号プリミティブの引数に含まれる暗号プリミティブが識別不可能性の性質を有し、該暗号プリミティブの引数がプロトコルに初めて現れた一時的な秘密情報を含んでいるか、をチェックすることを特徴とする暗号プロトコルの安全性検証装置を提案している。
【００１５】
（７）本発明は、（４）の暗号プロトコルの安全性検証装置について、前記鍵交換プロトコルのオフライン辞書攻撃安全における検証項目として、長期的で不完全な秘密情報を含む暗号プリミティブが一方向性の性質を有し、該暗号プリミティブの引数がいずれもプロトコルに初めて現れたか、同じセッションにおいて以前にプロトコルに現れたか、別のセッションにおいて繰り返し使用不可能でプロトコルに現れた一時的な秘密情報を含んでいるか、をチェックすることを特徴とする暗号プロトコルの安全性検証装置を提案している。
【００１６】
（８）本発明は、（４）の暗号プロトコルの安全性検証装置について、前記鍵交換プロトコルの既知鍵攻撃安全における検証項目として、鍵生成対象となる暗号プリミティブが識別不可能性または一方向性の性質を有し、該暗号プリミティブの引数がいずれもプロトコルに初めて現れたか、同じセッションにおいて以前にプロトコルに現れたか、別のセッションにおいて繰り返し使用不可能でプロトコルに現れた一時的な秘密情報を含んでいるか、をチェックすることを特徴とする暗号プロトコルの安全性検証装置を提案している。
【００１７】
（９）本発明は、（４）の暗号プロトコルの安全性検証装置について、前記鍵交換プロトコルのフォワード秘匿性における検証項目として、鍵生成対象となる暗号プリミティブが識別不可能性または一方向性の性質を有し、該暗号プリミティブの引数がいずれもプロトコルに初めて現れたか、同じセッションにおいて以前にプロトコルに現れたか、別のセッションにおいて繰り返し使用不可能でプロトコルに現れた一時的な秘密情報を含んでいるか、をチェックすることを特徴とする暗号プロトコルの安全性検証装置を提案している。
【００１８】
（１０）本発明は、暗号プロトコルの安全性を検証するための安全性検証方法であって、認証および鍵交換プロトコルにおいて使用されている暗号プリミティブを列挙する第１のステップと、前記列挙した暗号プリミティブについて、危殆化情報の有無を検証し、危殆化情報を有するものがある場合に、前記暗号プロトコルは安全ではないと判断する第２のステップと、該列挙した暗号プリミティブの中に、危殆化情報を有するものがない場合に、前記暗号プリミティブの役割を設定する第３のステップと、前記暗号プリミティブの安全性の根拠の設定を行う第４のステップと、フローの列挙を行う第５のステップと、フローデータと暗号プリミティブの引数の種類と状態とを設定する第６のステップと、該設定したフローデータと暗号プリミティブの引数の種類と状態との関係が正しいか否かを判断し、正しくないものを含む場合に、前記暗号プロトコルは安全ではないと判断する第７のステップと、前記設定したフローデータと暗号プリミティブの引数の種類と状態との関係がすべて正しいと判断した場合に、安全性に関する検証項目の選択を行う第８のステップと、該選択した検証項目をすべて満足するか否かを判断し、満足しないものを含む場合に、前記暗号プロトコルは選択した安全性に関して安全ではないと判断する第９のステップと、前記選択した検証項目をすべて満足する場合に、前記暗号プロトコルは安全であると判断する第１０のステップと、を有することを特徴とする安全性検証方法を提案している。
【００１９】
（１１）本発明は、コンピュータに、暗号プロトコルの安全性を検証するための安全性検証方法を実行させるためのプログラムであって、認証および鍵交換プロトコルにおいて使用されている暗号プリミティブを列挙する第１のステップと、前記列挙した暗号プリミティブについて、危殆化情報の有無を検証し、危殆化情報を有するものがある場合に、前記暗号プロトコルは安全ではないと判断する第２のステップと、該列挙した暗号プリミティブの中に、危殆化情報を有するものがない場合に、前記暗号プリミティブの役割を設定する第３のステップと、前記暗号プリミティブの安全性の根拠の設定を行う第４のステップと、フローの列挙を行う第５のステップと、フローデータと暗号プリミティブの引数の種類と状態とを設定する第６のステップと、該設定したフローデータと暗号プリミティブの引数の種類と状態との関係が正しいか否かを判断し、正しくないものを含む場合に、前記暗号プロトコルは安全ではないと判断する第７のステップと、前記設定したフローデータと暗号プリミティブの引数の種類と状態との関係がすべて正しいと判断した場合に、安全性に関する検証項目の選択を行う第８のステップと、該選択した検証項目をすべて満足するか否かを判断し、満足しないものを含む場合に、前記暗号プロトコルは選択した安全性に関して安全ではないと判断する第９のステップと、前記選択した検証項目をすべて満足する場合に、前記暗号プロトコルは安全であると判断する第１０のステップと、コンピュータに実行させるためのプログラムを提案している。
【発明の効果】
【００２０】
本発明によれば、暗号プロトコルのうち、認証プロトコルと鍵交換プロトコルを安全性レベルに応じて検証することができるという効果がある。
【発明を実施するための最良の形態】
【００２１】
以下、図面を用いて、本発明の実施形態について詳細に説明する。
なお、本実施形態における構成要素は適宜、既存の構成要素等との置き換えが可能であり、また、他の既存の構成要素との組み合わせを含む様々なバリエーションが可能である。したがって、本実施形態の記載をもって、特許請求の範囲に記載された発明の内容を限定するものではない。
【００２２】
＜暗号プロトコルの安全性レベルに関する既存のセキュリティモデル＞
本発明の実施形態の説明に入る前に、暗号プロトコルの安全性レベルに関して、既存のセキュリティモデルを示す。本発明では、計算量理論にもとづいて、暗号プロトコルの安全性を証明するという「証明可能安全性」と呼ばれる概念を用いる。「暗号プロトコルが証明可能安全性を有する」とは、暗号プロトコルの安全性が、ある暗号プリミティブの安全性に帰着することを計算量理論的に証明可能であることである。
【００２３】
ある暗号プロトコルを破る攻撃者を仮定した場合、ある暗号プリミティブを多項式時間で破るマシンを構成可能であることを証明することにより、この暗号プリミティブが破られなければ、暗号プロトコルも破られないことを証明する。本発明では、暗号プロトコルのうち、認証プロトコルと鍵交換プロトコルとを考える。
【００２４】
上記の証明可能安全性において、認証プロトコルではｍａｔｃｈｉｎｇ
ｃｏｎｖｅｒｓａｔｉｏｎ、鍵交換プロトコルではｓｅｍａｎｔｉｃ ｓｅｃｕｒｉｔｙという安全性の概念がある。それぞれの概念に対し、認証・鍵交換プロトコルに要求される安全性に応じて、現実の攻撃モデルを想定し、以下の安全性に分類した。ただし、（）内は、安全性に対応する攻撃を表している。
【００２５】
（１）ｍａｔｃｈｉｎｇ ｃｏｎｖｅｒｓａｔｉｏｎ
認証プロトコルにおいて、攻撃者が一方のパーティから受信したメッセージをそのままもう一方のパーティへ送ること以外に何もできないことを示す。すなわち、攻撃者は、メッセージの改ざんや新規メッセージの送付、メッセージの遮断、メッセージの順番の入れ替えなどの不正を行うことができない。
【００２６】
（１Ａ）能動的攻撃安全（なり済まし攻撃）
ｍａｔｃｈｉｎｇ ｃｏｎｖｅｒｓａｔｉｏｎにおける能動的攻撃安全は、攻撃者がパーティ間の通信を支配しても、認証プロトコルを破ることはできないことを示す。
【００２７】
（２）ｓｅｍａｎｔｉｃ ｓｅｃｕｒｉｔｙ
鍵交換プロトコルにおいて、攻撃者はセッション鍵に関するどんな情報も得ることができないことを示す。すなわち、攻撃者はセッション鍵と乱数を多項式時間で区別することができない。
【００２８】
（２Ａ）能動的攻撃安全（なり済まし攻撃）
ｓｅｍａｎｔｉｃ ｓｅｃｕｒｉｔｙにおける能動的攻撃安全は、攻撃者がパーティ間の通信を支配しても、鍵交換プロトコルを破ることはできないことを示す。
【００２９】
（２Ｂ）受動的攻撃安全（盗聴攻撃）
ｓｅｍａｎｔｉｃ ｓｅｃｕｒｉｔｙにおける受動的攻撃安全は、攻撃者がパーティ間の通信を盗聴しても、鍵交換プロトコルを破ることはできないことを示す。
【００３０】
（２Ｃ）オフライン辞書攻撃安全（オフライン辞書攻撃）
ｓｅｍａｎｔｉｃ ｓｅｃｕｒｉｔｙにおけるオフライン辞書攻撃安全は、攻撃者がパスワード推測用の辞書からオフラインで過去の履歴に一致するパーティのパスワードを探索することはできないことを示す。
【００３１】
（２Ｄ）既知鍵攻撃安全（既知鍵攻撃）
ｓｅｍａｎｔｉｃ ｓｅｃｕｒｉｔｙにおける既知鍵攻撃安全は、攻撃者があるセッション鍵を得ることができたとしても、それとは別のセッション鍵を得ることはできないことを示す。
【００３２】
（２Ｅ）ｆｏｒｗａｒｄ ｓｅｃｒｅｃｙ（長期鍵破壊攻撃）
ｓｅｍａｎｔｉｃ ｓｅｃｕｒｉｔｙにおけるｆｏｒｗａｒｄ
ｓｅｃｒｅｃｙは、攻撃者が秘密鍵やパスワードなどの長期鍵を得ることができたとしても、それ以前に共有されたセッション鍵を得ることはできないことを示す。
【００３３】
ただし、パスワード、長期鍵をそれぞれ使用しない鍵交換プロトコルの場合、（２Ｃ）のオフライン辞書攻撃安全、（２Ｅ）のｆｏｒｗａｒｄ
ｓｅｃｒｅｃｙの安全性はそれぞれ要求されない。
【００３４】
＜暗号プリミティブに設定される情報と記号＞
認証・鍵交換プロトコルにおいて使用されている暗号プリミティブに設定される情報は以下のとおりである。
（Ａ）認証プロトコルにおける認証対象となる暗号プリミティブ（ＡＧＦ）
（Ｂ）鍵交換プロトコルにおける鍵生成対象となる暗号プリミティブ（ＫＧＦ）
（Ｃ）ＡＧＦやＫＧＦの引数に含まれる暗号プリミティブ（ＡＣＰ）
（Ｄ）それ以外の暗号プリミティブ（ＯＣＰ）
【００３５】
＜暗号プリミティブに対して設定される安全性の根拠となる情報＞
上記で設定された暗号プリミティブに対して設定される安全性の根拠となる情報は以下のとおりである。
（Ａ）識別不可能性（ＩＮＤ）: 秘密情報を知らずに、対応する２つの事象を多項式時間で識別することができないことを示す。
（Ｂ）一方向性（ＯＷ）: 秘密情報を知らずに、出力値から入力値を多項式時間で計算することができないことを示す。
（Ｃ）偽造不可能性（ＵＦ）: 秘密情報を知らずに、要求されるメッセージの認証子を多項式時間で生成することができないことを示す。
【００３６】
＜認証・鍵交換プロトコルにおけるすべてのフローデータ及び暗号プリミティブに設定される構成要素＞
認証・鍵交換プロトコルにおけるすべてのフローデータ及び暗号プリミティブに設定される構成要素は以下のとおりである。
（Ａ）フローデータ及び暗号プリミティブの引数の種類
ａ）一般公開情報（ＰＵＢ）
ｂ）特定公開情報（ＩＤ）
ｃ）一時的な公開情報（ＴＰＫ）
ｄ）長期的で完全な秘密情報（ＬＬＫ）
ｅ）長期的で不完全な秘密情報（ＰＷ）
ｆ）一時的な秘密情報（ＴＳＫ）
（Ｂ）フローデータ及び暗号プリミティブの引数の状態
ａ）公開状態で初登場（ＰＦＴ）
ｂ）同じセッションにおいて以前に公開状態で登場（ＰＳＳ）
ｃ）別のセッションにおいて繰り返し使用可能で公開状態で登場（ＰＲＳ）
ｄ）別のセッションにおいて繰り返し使用不可能で公開状態で登場（ＰＮＳ）
ｅ）秘密状態で初登場（ＳＦＴ）
ｆ）同じセッションにおいて以前に秘密状態で登場（ＳＳＳ）
ｇ）別のセッションにおいて繰り返し使用可能で秘密状態で登場（ＳＲＳ）
ｈ）別のセッションにおいて繰り返し使用不可能で秘密状態で登場（ＳＮＳ）
【００３７】
＜認証及び鍵交換プロトコルを安全性レベルに応じて検証する項目＞
また、認証及び鍵交換プロトコルを安全性レベルに応じて検証する項目は、以下の通りである。
【００３８】
＜認証プロトコルに対するｍａｔｃｈｉｎｇ ｃｏｎｖｅｒｓａｔｉｏｎ＞
（Ａ）能動的攻撃安全における検証項目と検証内容
ａ）ＡＧＦがＵＦであり、ＡＧＦの引数がいずれもＴＰＫ−ＰＦＴまたはＴＰＫ−ＰＳＳまたはＴＰＫ−ＰＮＳまたはＴＳＫ−ＳＦＴまたはＴＳＫ−ＳＳＳまたはＴＳＫ−ＳＮＳを含んでいる。
ｂ）ＡＧＦがＯＷであり、ＡＧＦの引数がいずれもＴＳＫ−ＳＦＴを含んでいる。
【００３９】
＜鍵交換プロトコルに対するｓｅｍａｎｔｉｃ ｓｅｃｕｒｉｔｙ＞
（Ｂ）能動的攻撃安全における検証項目と検証内容
ａ）ＡＣＰがＩＮＤまたはＯＷであり、ＡＣＰの引数がいずれもＴＳＫ−ＳＦＴとＬＬＫ−ＳＲＳまたはＰＷ−ＳＲＳを含んでいる。
【００４０】
（Ｃ）受動的攻撃安全における検証項目と検証内容
ａ）ＫＧＦがＩＮＤであり、ＫＧＦの引数がいずれもＴＳＫ−ＳＦＴを含んでいる。
ｂ）ＫＧＦがＯＷであり、ＡＣＰがＩＮＤであり、ＡＣＰの引数がＴＳＫ−ＳＦＴを含んでいる。
【００４１】
（Ｄ）オフライン辞書攻撃安全における検証項目と検証内容
ａ）ＰＷを含むＯＣＰがＯＷであり、ＯＣＰの引数がいずれもＴＳＫ−ＳＦＴまたはＴＳＫ−ＳＳＳまたはＴＳＫ−ＳＮＳを含んでいる。
【００４２】
（Ｅ）既知鍵攻撃安全における検証項目と検証内容
ａ）ＫＧＦがＩＮＤまたはＯＷであり、ＫＧＦの引数がいずれもＴＳＫ−ＳＦＴまたはＴＳＫ−ＳＳＳまたはＴＳＫ−ＳＮＳを含んでいる。
【００４３】
（Ｆ）ｆｏｒｗａｒｄ ｓｅｃｒｅｃｙにおける検証項目と検証内容
ａ）ＫＧＦがＩＮＤまたはＯＷであり、ＫＧＦの引数がいずれもＴＳＫ−ＳＦＴまたはＴＳＫ−ＳＳＳまたはＴＳＫ−ＳＮＳを含んでいる。
【００４４】
＜暗号プロトコルの安全性検証装置の構成＞
図１を用いて、本実施形態に係る暗号プロトコルの安全性検証装置の構成について説明する。本実施形態に係る暗号プロトコルの安全性検証装置は、図１に示すように、暗号プリミティブ列挙部１と、危殆化情報判定部２と、役割設定部３と、安全性根拠設定部４と、フロー列挙部５と、引数設定部６と、設定情報判定部７と、安全性選択部８と、検証項目判定部９と、安全性判定部１０とから構成されている。
【００４５】
暗号プリミティブ列挙部１は、認証・鍵交換プロトコルにおいて使用されている暗号プリミティブをすべて列挙する。危殆化情報判定部２は、列挙された暗号プリミティブに対して危殆化情報があるかどうかを確認する。危殆化情報が１つでもある場合、安全性判定部１０が、認証・鍵交換プロトコルは安全ではないと判定する。
【００４６】
役割設定部３は、列挙された暗号プリミティブのうち、暗号プリミティブの役割である情報、例えば、ＡＧＦ、ＫＧＦ、ＡＣＰ、ＯＣＰを設定する。安全性根拠設定部４は、役割が設定された暗号プリミティブに対して、安全性の根拠となる情報、例えば、ＩＮＤ、ＯＷ、ＵＦを設定する。
【００４７】
フロー列挙部５は、認証・鍵交換プロトコルについて、すべてのフローを列挙する。引数設定部６は、列挙されたフローデータ及び暗号プリミティブについて、フローデータ及び暗号プリミティブの引数の種類、例えば、ＰＵＢ、ＩＤ、ＴＰＫ、ＬＬＫ、ＰＷ、ＴＳＫ等、およびフローデータ及び暗号プリミティブの引数の状態、例えば、ＰＦＴ、ＰＳＳ、ＰＲＳ、ＰＮＳ、ＳＦＴ、ＳＳＳ、ＳＲＳ、ＳＮＳ等の構成要素を設定する。
【００４８】
設定情報判定部７は、図２に示すフローデータ及び暗号プリミティブの引数の種類と状態の関係を示したデータテーブルに基づいて、フローデータ及び暗号プリミティブの引数に関する種類と状態の関係がすべて正しいかどうかを判定する。そして、１つでも正しくない関係がある場合には、安全性判定部１０が、認証・鍵交換プロトコルは安全ではないと判定する。
【００４９】
安全性選択部８は、認証・鍵交換プロトコルにおいて、要求されている安全性を選択する。なお、複数の安全性を選択してもよい。検証項目判定部９は、安全性選択部８が選択した安全性に対して、引数設定部６が設定した情報を用いて、前述した各安全性に関する検証項目を検証する。
【００５０】
ただし、検証項目を検証する前に、認証・鍵交換プロトコルにおける各安全性に応じて、以下の準備を行う。
＜認証プロトコルに対するｍａｔｃｈｉｎｇ ｃｏｎｖｅｒｓａｔｉｏｎ＞
（Ａ）能動的攻撃安全における検証項目
能動的攻撃安全は、なり済まし攻撃に対応し、攻撃者がパーティ間の通信を支配して得られる情報から、相手のパーティに認証させるための情報を生成することができないことを示している。なお、なり済まし攻撃により設定される情報は、すべてのフローである。
【００５１】
設定された情報に対し、プロトコルのフロー順に以下の事項を設定する。ここで、フローデータと引数の状態は更新されていくものとする。ただし、公開状態と秘密状態では、公開状態を優先するものとする。
ａ）ＡＧＦ、ＡＣＰ、ＯＣＰの種類と安全性の根拠
ｂ）ＡＧＦ、ＡＣＰ、ＯＣＰの引数の種類と状態
ｃ）フローデータの種類と状態
【００５２】
なお、ＡＧＦとＡＣＰの引数に暗号プリミティブが入れ子構造になっている場合、ＡＧＦとＡＣＰの引き数の状態を最終段階に設定する。
【００５３】
＜鍵交換プロトコルに対するｓｅｍａｎｔｉｃ ｓｅｃｕｒｉｔｙ＞
（Ａ）能動的攻撃安全における検証項目
能動的攻撃安全は、なり済まし攻撃に対応し、攻撃者がパーティ間の通信を支配して得られる情報から、セッション鍵と乱数を多項式時間で区別することができないことを示している。なお、なり済まし攻撃により設定される情報はすべてのフローである。
【００５４】
設定された情報に対し、プロトコルのフロー順に以下の事項を設定する。ここで、フローデータと引数の状態は更新されていくものとする。ただし、公開状態と秘密状態では、公開状態を優先するものとする。
ａ）ＫＧＦ、ＡＣＰ、ＯＣＰの種類と安全性の根拠
ｂ）ＫＧＦ、ＡＣＰ、ＯＣＰの引数の種類と状態
ｃ）フローデータの種類と状態
【００５５】
なお、ＫＧＦとＡＣＰの引数に暗号プリミティブが入れ子構造になっている場合、ＫＧＦとＡＣＰの引き数の状態を最終段階に設定する。
【００５６】
（Ｂ）受動的攻撃安全における検証項目
受動的攻撃安全は、盗聴攻撃に対応し、攻撃者がパーティ間の通信を盗聴して得られる情報から、セッション鍵と乱数を多項式時間で区別することができないことを示している。なお、盗聴攻撃により設定される情報は、すべてのフローである。
【００５７】
設定された情報に対し、プロトコルのフロー順に以下の事項を設定する。ここで、フローデータと引数の状態は更新されていくものとする。ただし、公開状態と秘密状態では、公開状態を優先するものとする。
ａ）ＫＧＦ、ＡＣＰ、ＯＣＰの種類と安全性の根拠
ｂ）ＫＧＦ、ＡＣＰ、ＯＣＰの引数の種類と状態
ｃ）フローデータの種類と状態
【００５８】
なお、ＫＧＦとＡＣＰの引数に暗号プリミティブが入れ子構造になっている場合、ＫＧＦとＡＣＰの引き数の状態を最終段階に設定する。
【００５９】
（Ｃ）オフライン辞書攻撃安全における検証項目
オフライン辞書攻撃安全は、オフライン辞書攻撃に対応し、攻撃者がパスワード推測用の辞書からパーティのパスワードをオフラインで探索するための過去の履歴から、セッション鍵と乱数を多項式時間で区別することができないことを示している。なお、オフライン辞書攻撃により設定される情報は、すべてのフローである。
【００６０】
設定された情報に対し、プロトコルのフロー順に以下の事項を設定する。ここで、フローデータと引数の状態は更新されていくものとする。ただし、公開状態と秘密状態では、公開状態を優先するものとする。
ａ）ＯＣＰの種類と安全性の根拠
ｂ）ＯＣＰの引数の種類と状態
ｃ）フローデータの種類と状態
【００６１】
（Ｄ）既知鍵攻撃安全における検証項目
既知鍵攻撃安全は、既知鍵攻撃に対応し、攻撃者が別のセッションにおいて得られたセッション鍵から、セッション鍵と乱数を多項式時間で区別することができないことを示している。なお、既知鍵攻撃により設定される情報は、他のすべてのセッションのセッション鍵である。
【００６２】
設定された情報に対し、プロトコルのフロー順に以下の事項を設定する。ここで、フローデータと引数の状態は更新されていくものとする。ただし、公開状態と秘密状態では、公開状態を優先するものとする。
ａ）ＫＧＦ、ＡＣＰ、ＯＣＰの種類と安全性の根拠
ｂ）ＫＧＦ、ＡＣＰ、ＯＣＰの引数の種類と状態
ｃ）フローデータの種類と状態
【００６３】
なお、ＫＧＦとＡＣＰの引数に暗号プリミティブが入れ子構造になっている場合、ＫＧＦとＡＣＰの引き数の状態を最終段階に設定する。
【００６４】
（Ｅ）ｆｏｒｗａｒｄ ｓｅｃｒｅｃｙにおける検証項目
ｆｏｒｗａｒｄ ｓｅｃｒｅｃｙは、長期鍵破壊攻撃に対応し、攻撃者がパーティの端末に侵入して得られた秘密鍵やパスワードなどの長期鍵から、セッション鍵と乱数を多項式時間で区別することができないことを示している。なお、長期鍵破壊攻撃により設定される情報は、長期鍵である。
【００６５】
設定された情報に対し、プロトコルのフロー順に以下の事項を設定する。ここで、フローデータと引数の状態は更新されていくものとする。ただし、公開状態と秘密状態では、公開状態を優先するものとする。この場合、長期鍵は公開情報として扱う。
ａ）ＫＧＦ、ＡＣＰ、ＯＣＰの種類と安全性の根拠
ｂ）ＫＧＦ、ＡＣＰ、ＯＣＰの引数の種類と状態
ｃ）フローデータの種類と状態
【００６６】
なお、ＫＧＦとＡＣＰの引数に暗号プリミティブが入れ子構造になっている場合、ＫＧＦとＡＣＰの引き数の状態を最終段階に設定する。
【００６７】
＜暗号プロトコルの安全性検証装置の処理＞
図３を用いて、暗号プロトコルの安全性検証装置の処理について、説明する。
まず、認証および鍵交換プロトコルにおいて使用されている暗号プリミティブを列挙する（ステップＳ１０１）。次に、列挙した暗号プリミティブについて、危殆化情報の有無を検証し（ステップＳ１０２）、危殆化情報を有するものがある場合（ステップＳ１０２の「Ｎｏ」）に、暗号プロトコルは安全ではないと判断する。
【００６８】
一方、列挙した暗号プリミティブの中に、危殆化情報を有するものがない場合に（ステップＳ１０２の「Ｙｅｓ」）、暗号プリミティブの役割を設定する（ステップＳ１０３）。さらに、暗号プリミティブの安全性の根拠の設定を行い（ステップＳ１０４）、フローの列挙を行って（ステップＳ１０５）、フローデータと暗号プリミティブの引数の種類と状態とを設定する（ステップＳ１０６）。
【００６９】
そして、設定したフローデータと暗号プリミティブの引数の種類と状態との関係が正しいか否かを判断し（ステップＳ１０７）、正しくないものを含む場合に（ステップＳ１０７の「Ｎｏ」）、暗号プロトコルは安全ではないと判断する。一方、設定したフローデータと暗号プリミティブの引数の種類と状態との関係がすべて正しいと判断した場合に（ステップＳ１０７の「Ｙｅｓ」）、安全性に関する検証項目の選択を行う（ステップＳ１０８）。
【００７０】
そして、選択した検証項目をすべて満足するか否かを判断し（ステップＳ１０９）、満足しないものを含む場合に（ステップＳ１０９の「Ｎｏ」）、暗号プロトコルは選択した安全性に関して安全ではないと判断し、選択した検証項目をすべて満足する場合に（ステップＳ１０９の「Ｙｅｓ」）、暗号プロトコルは安全であると判断する。
【００７１】
したがって、本実施形態によれば、暗号プロトコルのうち、認証プロトコルと鍵交換プロトコルを安全性レベルに応じて検証することができる。
【００７２】
なお、上述の一連の処理をプログラムとしてコンピュータ読み取り可能な記録媒体に記録し、この記録媒体に記録されたプログラムを暗号プロトコルの安全性検証装置に読み込ませ、実行することによって本発明の暗号プロトコルの安全性検証装置を実現することができる。
【００７３】
また、ＷＷＷ（Ｗｏｒｌｄ Ｗｉｄｅ Ｗｅｂ）システムを利用している場合であれば、ホームページ提供環境（あるいは表示環境）も含むものとする。また、上記プログラムは、このプログラムを記憶装置等に格納したコンピュータから、伝送媒体を介して、あるいは、伝送媒体中の伝送波により他のコンピュータに伝送されてもよい。ここで、プログラムを伝送する「伝送媒体」は、インターネット等のネットワーク（通信網）や電話回線等の通信回線（通信線）のように情報を伝送する機能を有する媒体のことをいう。
【００７４】
また、上記プログラムは、前述した機能の一部を実現するためのものであっても良い。さらに、前述した機能をコンピュータにすでに記録されているプログラムとの組合せで実現できるもの、いわゆる差分ファイル（差分プログラム）であっても良い。
【００７５】
以上、この発明の実施形態につき、図面を参照して詳述してきたが、具体的な構成はこの実施形態に限られるものではなく、この発明の要旨を逸脱しない範囲の設計等も含まれる。
【図面の簡単な説明】
【００７６】
【図１】本実施形態に係る暗号プロトコルの安全性検証装置の構成を示す図である。
【図２】本実施形態に係るフローデータと暗号プリミティブの引数の種類と状態との関係を示す図である。
【図３】本実施形態に係る暗号プロトコルの安全性検証装置の処理フローである。
【符号の説明】
【００７７】
１・・・暗号プリミティブ列挙部
２・・・危殆化情報判定部
３・・・役割設定部
４・・・安全性根拠設定部
５・・・フロー列挙部
６・・・引数設定部
７・・・設定情報判定部
８・・・安全性選択部
９・・・検証項目判定部
１０・・・安全性判定部
【特許請求の範囲】
【請求項１】
少なくとも認証や鍵共有のセキュリティ機能を有する暗号プロトコルのうち、認証プロトコル及び鍵交換プロトコルの安全性を検証する検証手段を備えた暗号プロトコルの安全性検証装置。
【請求項２】
前記検証手段が、前記認証プロトコルの安全性を検証する検証項目として、認証プロトコルの能動的攻撃安全における検証項目を含むことを特徴とする請求項１に記載の暗号プロトコルの安全性検証装置。
【請求項３】
前記認証プロトコルの能動的攻撃安全における検証項目として、前記検証手段が、認証対象となる暗号プリミティブが偽造不可能性の性質を有し、該暗号プリミティブの引数がいずれもプロトコルに初めて現れたか、同じセッションにおいて以前にプロトコルに現れたか、別のセッションにおいて繰り返し使用不可能でプロトコルに現れた一時的な公開情報であるか、または、プロトコルに初めて現れたか、同じセッションにおいて以前にプロトコルに現れたか、別のセッションにおいて繰り返し使用不可能でプロトコルに現れた一時的な秘密情報を含んでいるか、あるいは、認証対象となる暗号プリミティブが一方向性の性質を有し、該暗号プリミティブの引数がいずれもプロトコルに初めて現れた一時的な秘密情報を含んでいるか、をチェックすることを特徴とする請求項２に記載の暗号プロトコルの安全性検証装置。
【請求項４】
前記検証手段が、前記鍵交換プロトコルの安全性を検証する検証項目として、鍵交換プロトコルの能動的攻撃安全、受動的攻撃安全、オフライン辞書攻撃安全、既知鍵攻撃安全、フォワード秘匿性における検証項目を含むことを特徴とする請求項１に記載の暗号プロトコルの安全性検証装置。
【請求項５】
前記鍵交換プロトコルの能動的攻撃安全における検証項目として、鍵生成対象となる暗号プリミティブの引数に含まれる暗号プリミティブが識別不可能性または一方向性の性質を有し、該暗号プリミティブの引数がいずれもプロトコルに初めて現れた一時的な秘密情報と、別のセッションにおいて繰り返し使用可能でプロトコルに現れた長期的で完全な秘密情報または長期的で不完全な秘密情報を含んでいるか、をチェックすることを特徴とする請求項４に記載の暗号プロトコルの安全性検証装置。
【請求項６】
前記鍵交換プロトコルの受動的攻撃安全における検証項目として、鍵生成対象となる暗号プリミティブが識別不可能性の性質を有し、該暗号プリミティブの引数がいずれもプロトコルに初めて現れた一時的な秘密情報を含んでいるか、あるいは鍵生成対象となる暗号プリミティブが一方向性の性質を有し、該暗号プリミティブの引数に含まれる暗号プリミティブが識別不可能性の性質を有し、該暗号プリミティブの引数がプロトコルに初めて現れた一時的な秘密情報を含んでいるか、をチェックすることを特徴とする請求項４に記載の暗号プロトコルの安全性検証装置。
【請求項７】
前記鍵交換プロトコルのオフライン辞書攻撃安全における検証項目として、長期的で不完全な秘密情報を含む暗号プリミティブが一方向性の性質を有し、該暗号プリミティブの引数がいずれもプロトコルに初めて現れたか、同じセッションにおいて以前にプロトコルに現れたか、別のセッションにおいて繰り返し使用不可能でプロトコルに現れた一時的な秘密情報を含んでいるか、をチェックすることを特徴とする請求項４に記載の暗号プロトコルの安全性検証装置。
【請求項８】
前記鍵交換プロトコルの既知鍵攻撃安全における検証項目として、鍵生成対象となる暗号プリミティブが識別不可能性または一方向性の性質を有し、該暗号プリミティブの引数がいずれもプロトコルに初めて現れたか、同じセッションにおいて以前にプロトコルに現れたか、別のセッションにおいて繰り返し使用不可能でプロトコルに現れた一時的な秘密情報を含んでいるか、をチェックすることを特徴とする請求項４に記載の暗号プロトコルの安全性検証装置。
【請求項９】
前記鍵交換プロトコルのフォワード秘匿性における検証項目として、鍵生成対象となる暗号プリミティブが識別不可能性または一方向性の性質を有し、該暗号プリミティブの引数がいずれもプロトコルに初めて現れたか、同じセッションにおいて以前にプロトコルに現れたか、別のセッションにおいて繰り返し使用不可能でプロトコルに現れた一時的な秘密情報を含んでいるか、をチェックすることを特徴とする請求項４に記載の暗号プロトコルの安全性検証装置。
【請求項１０】
暗号プロトコルの安全性を検証するための安全性検証方法であって、
認証および鍵交換プロトコルにおいて使用されている暗号プリミティブを列挙する第１のステップと、
前記列挙した暗号プリミティブについて、危殆化情報の有無を検証し、危殆化情報を有するものがある場合に、前記暗号プロトコルは安全ではないと判断する第２のステップと、
該列挙した暗号プリミティブの中に、危殆化情報を有するものがない場合に、前記暗号プリミティブの役割を設定する第３のステップと、
前記暗号プリミティブの安全性の根拠の設定を行う第４のステップと、
フローの列挙を行う第５のステップと、
フローデータと暗号プリミティブの引数の種類と状態とを設定する第６のステップと、
該設定したフローデータと暗号プリミティブの引数の種類と状態との関係が正しいか否かを判断し、正しくないものを含む場合に、前記暗号プロトコルは安全ではないと判断する第７のステップと、
前記設定したフローデータと暗号プリミティブの引数の種類と状態との関係がすべて正しいと判断した場合に、安全性に関する検証項目の選択を行う第８のステップと、
該選択した検証項目をすべて満足するか否かを判断し、満足しないものを含む場合に、前記暗号プロトコルは選択した安全性に関して安全ではないと判断する第９のステップと、
前記選択した検証項目をすべて満足する場合に、前記暗号プロトコルは安全であると判断する第１０のステップと、
を有することを特徴とする安全性検証方法。
【請求項１１】
コンピュータに、暗号プロトコルの安全性を検証するための安全性検証方法を実行させるためのプログラムであって、
認証および鍵交換プロトコルにおいて使用されている暗号プリミティブを列挙する第１のステップと、
前記列挙した暗号プリミティブについて、危殆化情報の有無を検証し、危殆化情報を有するものがある場合に、前記暗号プロトコルは安全ではないと判断する第２のステップと、
該列挙した暗号プリミティブの中に、危殆化情報を有するものがない場合に、前記暗号プリミティブの役割を設定する第３のステップと、
前記暗号プリミティブの安全性の根拠の設定を行う第４のステップと、
フローの列挙を行う第５のステップと、
フローデータと暗号プリミティブの引数の種類と状態とを設定する第６のステップと、
該設定したフローデータと暗号プリミティブの引数の種類と状態との関係が正しいか否かを判断し、正しくないものを含む場合に、前記暗号プロトコルは安全ではないと判断する第７のステップと、
前記設定したフローデータと暗号プリミティブの引数の種類と状態との関係がすべて正しいと判断した場合に、安全性に関する検証項目の選択を行う第８のステップと、
該選択した検証項目をすべて満足するか否かを判断し、満足しないものを含む場合に、前記暗号プロトコルは選択した安全性に関して安全ではないと判断する第９のステップと、
前記選択した検証項目をすべて満足する場合に、前記暗号プロトコルは安全であると判断する第１０のステップと、
コンピュータに実行させるためのプログラム。
【請求項１】
少なくとも認証や鍵共有のセキュリティ機能を有する暗号プロトコルのうち、認証プロトコル及び鍵交換プロトコルの安全性を検証する検証手段を備えた暗号プロトコルの安全性検証装置。
【請求項２】
前記検証手段が、前記認証プロトコルの安全性を検証する検証項目として、認証プロトコルの能動的攻撃安全における検証項目を含むことを特徴とする請求項１に記載の暗号プロトコルの安全性検証装置。
【請求項３】
前記認証プロトコルの能動的攻撃安全における検証項目として、前記検証手段が、認証対象となる暗号プリミティブが偽造不可能性の性質を有し、該暗号プリミティブの引数がいずれもプロトコルに初めて現れたか、同じセッションにおいて以前にプロトコルに現れたか、別のセッションにおいて繰り返し使用不可能でプロトコルに現れた一時的な公開情報であるか、または、プロトコルに初めて現れたか、同じセッションにおいて以前にプロトコルに現れたか、別のセッションにおいて繰り返し使用不可能でプロトコルに現れた一時的な秘密情報を含んでいるか、あるいは、認証対象となる暗号プリミティブが一方向性の性質を有し、該暗号プリミティブの引数がいずれもプロトコルに初めて現れた一時的な秘密情報を含んでいるか、をチェックすることを特徴とする請求項２に記載の暗号プロトコルの安全性検証装置。
【請求項４】
前記検証手段が、前記鍵交換プロトコルの安全性を検証する検証項目として、鍵交換プロトコルの能動的攻撃安全、受動的攻撃安全、オフライン辞書攻撃安全、既知鍵攻撃安全、フォワード秘匿性における検証項目を含むことを特徴とする請求項１に記載の暗号プロトコルの安全性検証装置。
【請求項５】
前記鍵交換プロトコルの能動的攻撃安全における検証項目として、鍵生成対象となる暗号プリミティブの引数に含まれる暗号プリミティブが識別不可能性または一方向性の性質を有し、該暗号プリミティブの引数がいずれもプロトコルに初めて現れた一時的な秘密情報と、別のセッションにおいて繰り返し使用可能でプロトコルに現れた長期的で完全な秘密情報または長期的で不完全な秘密情報を含んでいるか、をチェックすることを特徴とする請求項４に記載の暗号プロトコルの安全性検証装置。
【請求項６】
前記鍵交換プロトコルの受動的攻撃安全における検証項目として、鍵生成対象となる暗号プリミティブが識別不可能性の性質を有し、該暗号プリミティブの引数がいずれもプロトコルに初めて現れた一時的な秘密情報を含んでいるか、あるいは鍵生成対象となる暗号プリミティブが一方向性の性質を有し、該暗号プリミティブの引数に含まれる暗号プリミティブが識別不可能性の性質を有し、該暗号プリミティブの引数がプロトコルに初めて現れた一時的な秘密情報を含んでいるか、をチェックすることを特徴とする請求項４に記載の暗号プロトコルの安全性検証装置。
【請求項７】
前記鍵交換プロトコルのオフライン辞書攻撃安全における検証項目として、長期的で不完全な秘密情報を含む暗号プリミティブが一方向性の性質を有し、該暗号プリミティブの引数がいずれもプロトコルに初めて現れたか、同じセッションにおいて以前にプロトコルに現れたか、別のセッションにおいて繰り返し使用不可能でプロトコルに現れた一時的な秘密情報を含んでいるか、をチェックすることを特徴とする請求項４に記載の暗号プロトコルの安全性検証装置。
【請求項８】
前記鍵交換プロトコルの既知鍵攻撃安全における検証項目として、鍵生成対象となる暗号プリミティブが識別不可能性または一方向性の性質を有し、該暗号プリミティブの引数がいずれもプロトコルに初めて現れたか、同じセッションにおいて以前にプロトコルに現れたか、別のセッションにおいて繰り返し使用不可能でプロトコルに現れた一時的な秘密情報を含んでいるか、をチェックすることを特徴とする請求項４に記載の暗号プロトコルの安全性検証装置。
【請求項９】
前記鍵交換プロトコルのフォワード秘匿性における検証項目として、鍵生成対象となる暗号プリミティブが識別不可能性または一方向性の性質を有し、該暗号プリミティブの引数がいずれもプロトコルに初めて現れたか、同じセッションにおいて以前にプロトコルに現れたか、別のセッションにおいて繰り返し使用不可能でプロトコルに現れた一時的な秘密情報を含んでいるか、をチェックすることを特徴とする請求項４に記載の暗号プロトコルの安全性検証装置。
【請求項１０】
暗号プロトコルの安全性を検証するための安全性検証方法であって、
認証および鍵交換プロトコルにおいて使用されている暗号プリミティブを列挙する第１のステップと、
前記列挙した暗号プリミティブについて、危殆化情報の有無を検証し、危殆化情報を有するものがある場合に、前記暗号プロトコルは安全ではないと判断する第２のステップと、
該列挙した暗号プリミティブの中に、危殆化情報を有するものがない場合に、前記暗号プリミティブの役割を設定する第３のステップと、
前記暗号プリミティブの安全性の根拠の設定を行う第４のステップと、
フローの列挙を行う第５のステップと、
フローデータと暗号プリミティブの引数の種類と状態とを設定する第６のステップと、
該設定したフローデータと暗号プリミティブの引数の種類と状態との関係が正しいか否かを判断し、正しくないものを含む場合に、前記暗号プロトコルは安全ではないと判断する第７のステップと、
前記設定したフローデータと暗号プリミティブの引数の種類と状態との関係がすべて正しいと判断した場合に、安全性に関する検証項目の選択を行う第８のステップと、
該選択した検証項目をすべて満足するか否かを判断し、満足しないものを含む場合に、前記暗号プロトコルは選択した安全性に関して安全ではないと判断する第９のステップと、
前記選択した検証項目をすべて満足する場合に、前記暗号プロトコルは安全であると判断する第１０のステップと、
を有することを特徴とする安全性検証方法。
【請求項１１】
コンピュータに、暗号プロトコルの安全性を検証するための安全性検証方法を実行させるためのプログラムであって、
認証および鍵交換プロトコルにおいて使用されている暗号プリミティブを列挙する第１のステップと、
前記列挙した暗号プリミティブについて、危殆化情報の有無を検証し、危殆化情報を有するものがある場合に、前記暗号プロトコルは安全ではないと判断する第２のステップと、
該列挙した暗号プリミティブの中に、危殆化情報を有するものがない場合に、前記暗号プリミティブの役割を設定する第３のステップと、
前記暗号プリミティブの安全性の根拠の設定を行う第４のステップと、
フローの列挙を行う第５のステップと、
フローデータと暗号プリミティブの引数の種類と状態とを設定する第６のステップと、
該設定したフローデータと暗号プリミティブの引数の種類と状態との関係が正しいか否かを判断し、正しくないものを含む場合に、前記暗号プロトコルは安全ではないと判断する第７のステップと、
前記設定したフローデータと暗号プリミティブの引数の種類と状態との関係がすべて正しいと判断した場合に、安全性に関する検証項目の選択を行う第８のステップと、
該選択した検証項目をすべて満足するか否かを判断し、満足しないものを含む場合に、前記暗号プロトコルは選択した安全性に関して安全ではないと判断する第９のステップと、
前記選択した検証項目をすべて満足する場合に、前記暗号プロトコルは安全であると判断する第１０のステップと、
コンピュータに実行させるためのプログラム。
【図１】
【図２】
【図３】
【図２】
【図３】
【公開番号】特開２０１０−１０８６３（Ｐ２０１０−１０８６３Ａ）
【公開日】平成２２年１月１４日（２０１０．１．１４）
【国際特許分類】
【出願番号】特願２００８−１６５３３２（Ｐ２００８−１６５３３２）
【出願日】平成２０年６月２５日（２００８．６．２５）
【国等の委託研究の成果に係る記載事項】（出願人による申告）平成１９年度、独立行政法人情報通信研究機構「ユビキタスネットワークにおける環境に応じたセキュリティプロトコルの自動生成・カスタマイズ技術に関する研究開発」委託研究、産業技術力強化法第１９条の適用を受ける特許出願
【出願人】（５９９１０８２６４）株式会社ＫＤＤＩ研究所 (233)
【Ｆターム（参考）】
【公開日】平成２２年１月１４日（２０１０．１．１４）
【国際特許分類】
【出願日】平成２０年６月２５日（２００８．６．２５）
【国等の委託研究の成果に係る記載事項】（出願人による申告）平成１９年度、独立行政法人情報通信研究機構「ユビキタスネットワークにおける環境に応じたセキュリティプロトコルの自動生成・カスタマイズ技術に関する研究開発」委託研究、産業技術力強化法第１９条の適用を受ける特許出願
【出願人】（５９９１０８２６４）株式会社ＫＤＤＩ研究所 (233)
【Ｆターム（参考）】
[ Back to top ]