近似的なシミュレーション関係の確認に用いられる測度分解装置及びプログラム
【課題】近似的なシミュレーション関係の確認に用いられる測度分解装置及びプログラムを提供すること。
【解決手段】第１の入力測度と同値な測度の集合及び第２の入力測度と同値な測度の集合をリストアップし、前記第１の入力測度と同値な測度のうちの１つと前記第２の入力測度と同値な測度のうちの１つとから構成される対の集合を生成する対リストアップユニットと、対間の距離が一定以下である対をチェックする対チェックユニットと、前記対間の距離が一定以下である対に対して、対の距離を縮める操作を行って分解後の測度を生成する対調整ユニットと、前記分解後の測度のそれぞれを同値な測度に写すことにより同値遷移後の測度の対を生成する同値遷移ユニットと、前記同値遷移後の測度の対からなる対リストを記憶する対リスト保存メモリと、前記対リスト保存メモリに記憶されている対リストから、未使用の同値遷移後の測度の対を選択して出力する対選択ユニットとを具備する。
【解決手段】第１の入力測度と同値な測度の集合及び第２の入力測度と同値な測度の集合をリストアップし、前記第１の入力測度と同値な測度のうちの１つと前記第２の入力測度と同値な測度のうちの１つとから構成される対の集合を生成する対リストアップユニットと、対間の距離が一定以下である対をチェックする対チェックユニットと、前記対間の距離が一定以下である対に対して、対の距離を縮める操作を行って分解後の測度を生成する対調整ユニットと、前記分解後の測度のそれぞれを同値な測度に写すことにより同値遷移後の測度の対を生成する同値遷移ユニットと、前記同値遷移後の測度の対からなる対リストを記憶する対リスト保存メモリと、前記対リスト保存メモリに記憶されている対リストから、未使用の同値遷移後の測度の対を選択して出力する対選択ユニットとを具備する。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、タスクＰＩＯＡ（Task-Structured Probabilistic I/O Automata）を用いた暗号プロトコルの安全性証明に関する。
【背景技術】
【０００２】
暗号プロトコルの解析方法には様々なものがあるが、プロトコルをタスクＰＩＯＡを用いて表現し、汎用的結合可能性のフレームワークを用いて解析する方法が知られている（例えば「非特許文献１」参照。）。この解析方法は、タスクＰＩＯＡで表現した現実プロトコルから理想プロトコルへのインプリメンテーション（implementation）関係を示すことによりプロトコルの安全性を証明するというものである。一般に、シミュレーション（simulation）関係が満たされるとき、インプリメンテーション関係も満たされる。そこで、実際にインプリメンテーション関係を示す際には、インプリメンテーション関係よりも証明が容易なシミュレーション関係の存在を証明する。この場合、証明可能なプロトコルの範囲はシミュレーション関係を満たすプロトコルに制限される。
【０００３】
上記非特許文献１の解析方法は、厳密なシミュレーション関係を用いるものであるが、シミュレーション関係の条件を緩和したいくつかの近似的なシミュレーション関係が提案されている。厳密なシミュレーション関係を確認する操作の一部は自動化されている（例えば「非特許文献２」参照。）。しかしながら、近似的なシミュレーション関係を確認する操作（例えば「非特許文献３」参照。）については自動化されていない。
【非特許文献１】R.Canetti et al., "Using Task-Structured Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol", IACR e-print/2005/452, 2005.
【非特許文献２】櫟粛之,「Task-PIOAに基づくIdeal-Functionality実現の証明の自動化」，信学技報AI2006-18
【非特許文献３】R.Segala and A.Turrini, “Approximated Computationally Bounded Simulation Relations for Probabilistic Automata”, IEEE-Computer-Security-Foundations-Symposium-2007
【発明の開示】
【発明が解決しようとする課題】
【０００４】
本発明は、近似的なシミュレーション関係を確認する操作については自動化されていない点に鑑みてなされたものであり、近似的なシミュレーション関係の確認に用いられ、特に、これまでの厳密なシミュレーション関係の確認の際には必要ではなかった測度分解操作を行う測度分解装置及びプログラムを提供することを目的とする。
【課題を解決するための手段】
【０００５】
本発明の一観点に係る測度分解装置は、入力された第１の入力測度と第２の入力測度のそれぞれを分解する測度分解装置である。該測度分解装置は、前記第１の入力測度と同値な測度の集合及び前記第２の入力測度と同値な測度の集合をリストアップし、前記第１の入力測度と同値な測度のうちの１つと前記第２の入力測度と同値な測度のうちの１つとから構成される対の集合を生成する対リストアップユニットと、対間の距離が一定以下である対をチェックする対チェックユニットと、前記対間の距離が一定以下である対に対して、対の距離を縮める操作を行って分解後の測度を生成する対調整ユニットと、前記分解後の測度のそれぞれを同値な測度に写すことにより同値遷移後の測度の対を生成する同値遷移ユニットと、前記同値遷移後の測度の対からなる対リストを記憶する対リスト保存メモリと、前記対リスト保存メモリに記憶されている対リストから、未使用の同値遷移後の測度の対を選択して出力する対選択ユニットとを具備する。
【発明の効果】
【０００６】
本発明によれば、近似的なシミュレーション関係の確認に用いられる測度分解装置及びプログラムを提供できる。
【発明を実施するための最良の形態】
【０００７】
以下、図面を参照しながら本発明の実施形態を説明する。本実施形態では近似的なシミュレーション関係の確認に用いられる測度分解装置について説明する。この当該装置は、コンピュータを測度分解装置として機能させるためのプログラムとして実現することも可能である。
【０００８】
本実施形態では、以下の性質を持つ関係を、確認の対象となる関係とする。
【０００９】
（１）２つの測度に関して、近似的な関係Ｒεの元となっている厳密な関係Ｒについて、Ｒが成立しているならば、２つの測度のトレースが等しくなるような関係。すなわちμ１Ｒμ２→ｔｄｉｓｔ（μ１）＝ｔｄｉｓｔ（μ２）である。
【００１０】
（２）分解前の測度について当該関係Ｒεが成立するとは、分解後の測度について誤差のない厳密な関係Ｒが成立することを意味するような関係。ここで、測度はμ１Ｒεμ２→μ’１Ｒμ’２，μ１＝（１−ε）μ’１＋εμ”１，μ２＝（１−ε）μ’２＋εμ”２のように分解できる。ただし、εは微小な値である。
【００１１】
ここで、本実施形態に係る測度分解装置の具体的構成を説明する前に、関連する概念としてＰＩＯＡの定義、タスクＰＩＯＡ及びタスクスケジューラの定義、ならびにシミュレーション関係の定義についてそれぞれ説明する。
【００１２】
先ず、測度については、例えば非特許文献１の「2.1.1 Probability-measures」の項において定義されている。
【００１３】
ＰＩＯＡについては、例えば非特許文献１の「Definition 2.5」の項において定義されている。ＰＩＯＡ（Probabilistic I/O Automata；確率的入出力オートマトン）は、Ｑを状態の可算集合，ｑ￣∈Ｑを初期状態，Ｉを入力アクションの可算集合，Ｏを出力アクションの可算集合，Ｈを内部アクションの可算集合，Ｄ⊆（Ｑ×（Ｉ∪Ｏ∪Ｈ）×Ｄｉｓｃ（Ｑ））を遷移関係とするとき、Ρ＝（Ｑ，ｑ￣，Ｉ，Ｏ，Ｈ，Ｄ）で表される。Ｉ∪Ｏ∪ＨをＡと表記し、Ρの「アクション」と呼ぶ。なお、表記「ｑ￣」において本来ならば「￣」は「ｑ」の直上に記されるが、本明細書では「ｑ￣」と表記している。Ｉ∪ＯをＥと表記し、Ρの「外部アクション」と呼ぶ。ＰＩＯＡ Ρの「実行フラグメント」とは、状態とアクションの有限又は無限の列であって状態で始まるものである。実行フラグメントのうち最初の状態が初期状態であるものを「実行」と呼ぶ。「トレース」とは、実行フラグメントを外部アクションに制限したものである。
【００１４】
タスクＰＩＯＡ及びタスクスケジューラについては、例えば非特許文献１の「Definition 3.1」「Definition 3.2」の項においてそれぞれ定義されている。Τ＝（Ρ，Ｒ）の対を「タスクＰＩＯＡ」と呼ぶ。Ρ＝（Ｑ，（ｑ）￣，Ｉ，Ｏ，Ｈ，Ｄ）はＰＩＯＡであり、Ｒは、ｌｏｃａｌｌｙ−ｃｏｎｔｒｏｌｌｅｄ ａｃｔｉｏｎ（Ｏ∪Ｈ）上の同値類である。なお、集合Ｓにおいてａ，ｂ，ｃ∈Ｓに対し、二項関係〜が反射律（ａ〜ａ）、対称律（ａ〜ｂ⇒ｂ〜ａ）、推移律（ａ〜ｂかつｂ〜ｃ⇒ａ〜ｃ）を満たすとき、「〜」は同値関係という。ここで、Ｒの要素を「タスク（ｔａｓｋ）」という。Τ＝（Ρ，Ｒ）を閉じたタスクＰＩＯＡとする。Τの「タスクスケジュラ」は、Ｒ内のタスクの有限個または無限個の列ρ＝Ｔ１Ｔ２・・・と定義される。タスクＰＩＯＡの実行フラグメントの分布は、タスクスケジューラ内のタスクを順に施していくことによって刻々と変化する。このプロセス（確率的な実行）を記述するのがａｐｐｌｙ関数である。ａｐｐｌｙ関数は、有限の実行フラグメント上の離散確率測度とタスクスケジュールの対を入力とし、実行フラグメント上の離散確率測度を出力する関数である。ここで、μを実行フラグメント上の確率測度とするとき、ｔｄｉｓｔ（μ）はμに含まれる各実行フラグメントに対してトレースをとることによって得られる像測度である。
【００１５】
ここで、タスクＰＩＯＡの動作履歴について、一例を挙げて説明する。
【００１６】
先ず「実行フラグメント(execution fragment)」は、状態から始まりアクションと状態が交互に出現する列のことであり、例えば１／２｛ｑ０ａ１ｑ１ａ２ｑ２ａ３ｑ３＋ｑ０ａ１ｑ’１ａ’２ｑ’２ａ’３ｑ’３｝で表される。但し、ｑ０，ｑ１，ｑ２，ｑ３，ｑ’１，ｑ’２，ｑ’３，ｑ’’２∈Ｑ（状態）であり、ａ１，ａ２，ａ’１，ａ’２∈Ｅ（外部アクション）であり、ａ3，ａ’3∈Ｈ（内部アクション）であるとする。
【００１７】
「実行(execution)」とは、初期状態から始まる実行フラグメントのことである。ＰＩＯＡであるΡについての実行の全ての集合をｅｘｅｃｓ（Ρ）と表記する。
【００１８】
トレース(trace)とは、実行フラグメントを外部アクションに制限して得られる列のことであり、例えば上記に対応するものは、１／２｛ａ１ａ２＋ａ１ａ’２｝と表すことができる。ここで、ａ１ａ２はｑ０ａ１ｑ１ａ２ｑ２ａ３ｑ３に対応し、ａ１ａ’２はｑ０ａ１ｑ’１ａ’２ａ’３ｑ’３に対応する。
【００１９】
「tdist」とは、各トレースの出現確率を表す確率分布のことである。
【００２０】
「遷移」とは、ａｐｐｌｙ関数によって、実行フラグメント上の分布にタスクスケジューラの列を作用させて、新しい分布に写すことをいう。遷移の一例は、例えばｑ０ａ１ｑ１→１／２｛ｑ０ａ１ｑ１ａ２ｑ’２＋ｑ０ａ１ｑ１ａ２ｑ’’２｝と表される。
【００２１】
シミュレーション関係については、例えば非特許文献１の「Definition 3.23」「Definition 3.24」「Definition 3.25」の項において定義されている。
【００２２】
図１に示すようなタスクスケジュール間の対応付け写像が存在するとき、RはSimulation（シミュレーション）関係であるという。厳密には、シミュレーション関係は次のように定義される。
【００２３】
Τ１＝（Ρ１，Ｒ１），Τ２＝（Ρ２，Ｒ２）をｃｏｍｐａｒａｂｌｅであってｃｌｏｓｅｄであり、ａｃｔｉｏｎ−ｄｅｔｅｒｍｉｎｉｓｔｉｃなタスクＰＩＯＡｓとする。Ｒは、Ρ１の有限ｅｘｅｃｕｔｉｏｎ上の離散分布からΡ２の有限ｅｘｅｃｕｔｉｏｎ上の離散分布への関係であり、ε１Ｒε２ならば、ｔｄｉｓｔ（ε１）＝ｔｄｉｓｔ（ε２）とする。また、ｃ：（Ｒ＊１×Ｒ１）→Ｒ＊２とする。開始条件すなわちδ（ｑ￣１）Ｒδ（ｑ￣２）を満たし、ステップ条件すなわちε１Ｒε２でρ１∈Ｒ＊１であり、ε１がρ１とｃｏｎｓｉｓｔｅｎｔであり、ε２がｆｕｌｌ（ｃ）（ρ１）とｃｏｎｓｉｓｔｅｎｔであって、Ｔ∈Ｒ１とする。このとき、ε’１Ε（Ｒ）ε’２，ε’１＝ａｐｐｌｙ（ε１，Ｔ），ε’２＝ａｐｐｌｙ（ε２，ｃ（ρ１，Ｔ））を満たすとき、ＲはΤ１からΤ２へのシミュレーション関係である。
【００２４】
関連する概念としては以上である。次に、冒頭で述べた確認の対象となる関係、すなわち近似的なシミュレーション関係を次のように定義する。
【００２５】
２つの実行の上の測度μ１，μ２を以下のように分解する。
【００２６】
μ１＝（１−ε）μ’１＋εμ’’１
μ２＝（１−ε）μ’２＋εμ’’２
ここで、εは微小な値である。μ’１Ｒμ’２となる分解方法が存在するとき、近似的なシミュレーション関係（μ１Ｒεμ２）が成り立つと定義する。ここで、Ｒは厳密なシミュレーション関係を表す。
【００２７】
シミュレーション関係の確認について説明する。シミュレーション関係の確認は３つの段階、すなわち（１）実システムのタスクＰＩＯＡモデルと理想システムのタスクＰＩＯＡモデルとを構成する段階、（２）中間システムを構成する段階、（３）実システムから中間システムへのシミュレーション関係、及び中間システムから理想システムへのシミュレーション関係の確認を行う段階を有する。このうち、（３）の段階のみが自動化されており、これを自動実行するユニットを「関係自動確認ユニット」と呼ぶことにする。関係自動確認ユニットについては例えば非特許文献２に記載されている。
【００２８】
図２は、一実施形態に係る近似的なシミュレーション関係の自動確認装置を示すブロック図である。この装置は２つの測度を入力とし、これらが近似的なシミュレーション関係を充足するかそれとも不充足であるかを結果として出力する装置であって、測度分解ユニット１と、関係自動確認ユニット２と、結果判定部３と、終了判定部４とを具備する。
【００２９】
図３は、図２に示される近似的なシミュレーション関係の自動確認装置の動作手順を示すフローチャートである。先ず測度分解ユニット１に測度が入力される（ステップＳ１）。測度分解ユニット１はこの入力された測度を分解し、いくつかの分解パターンを出力する（ステップＳ２）。測度分解ユニット１が測度をどのように分解するかについては後述する。分解された測度は、関係自動確認ユニット２に送られる。関係自動確認ユニット２は、分解された測度について、これがシミュレーション関係を充足するかそれとも不充足であるかを確認し、その結果を出力する（ステップＳ３）。次に、結果判定部３は、ステップ３において出力された結果が「充足」であれば、その旨を出力して処理を終了し、「不充足」であればステップＳ５に移行する（ステップＳ４）。ステップＳ５では、ステップＳ２において得られている分解パターンの全てについて関係確認を試したかを終了判定部４が判定する。全ての分解パターンについて関係確認を行っていないならば、その分解パターンが測度分解ユニット１から出力され、関係自動確認ユニット２に与えられるよう、制御はステップＳ２に移行する。全ての分解パターンについて関係確認を終えており、全て「不充足」の結果となっているならば、終了判定部４はその旨を出力して処理を終了する。
【００３０】
なお、図２に示される自動確認装置の構成及びその動作手順はあくまで一例であって、実施形態に係る測度分解ユニットは、これとは別の装置構成に適用することができる。
【００３１】
従来のシミュレーション関係の自動確認装置は、本実施形態のような測度分解ユニットを備えておらず、入力された測度を分解することなく、関係自動確認ユニットによりシミュレーション関係を充足するか否かを確認するものである。
【００３２】
測度分解ユニット１は、本実施形態の冒頭で説明した性質を持つような近似的なシミュレーション関係を確認するために用いられ、図４に示されるように、コントローラ１０と、対リストアップユニット１１と、対チェックユニット１２と、対調整ユニット１３と、同値遷移ユニット１４と、対リスト保存メモリ１５と、対選択ユニット１６とを具備する。
【００３３】
コントローラ１０は、当該測度分解ユニット１が何回目に呼び出されたかを管理している。これは、図３のステップＳ５に示した処理（全ての分解パターンを試したかどうかの判定）に関係する。コントローラ１０は、測度分解ユニット１が最初に呼び出されたときは、入力された測度を対リストアップユニット１１に渡し、当該測度の分解処理が行われるようにする。そして測度分解ユニット１の２回目以降の呼び出しの際には、対選択ユニット１６を制御し、対リスト保存メモリ１５に保存されている未使用の測度（分解された測度）が出力されるようにする。
【００３４】
測度分解ユニット１には、暗号プロトコルの実行履歴である実行が測度として入力される。ここで、２つの測度（第１の入力測度μ１と第２の入力測度μ２）が測度分解ユニット１に入力され、測度分解ユニット１が第１の入力測度と第２の入力測度のそれぞれを分解するものとする。μ１，μ２は、状態とアクションが交互に出現するような列であり、アクションには、入力アクション、出力アクション、内部アクションがある。
【００３５】
対リストアップユニット１１は、第１の入力測度μ１と同値な測度の集合と、第２の入力測度μ２と同値な測度の集合とをリストアップし、第１の入力測度μ１と同値な測度のうちの１つと、第２の入力測度μ２と同値な測度のうちの１つとにより構成される対の集合を作る。
【００３６】
具体的には、対リストアップユニット１１はμ１，μ２に対してｔｄｉｓｔ（μｉ）を計算する。これは、μ１，μ２について、入力アクションと出力アクションのみを残すことによって得られる。次に、対リストアップユニット１１はｔｄｉｓｔ（μｉ）＝ｔｄｉｓｔ（μｉ，ｊｉ）となるような、測度μｉ，ｊｉをリストアップする。つまり、μｉ，ｊｉは、状態と内部アクションの違いは無視して、入力アクションと出力アクションについて比較したときに、μｉと同じになるものである。
【００３７】
対チェックユニット１２は、対の間の距離が一定以下であるかをチェックする。
【００３８】
具体的には、対チェックユニット１２は全ての対（μ1，ｊ1，μ2，ｊ2），（ｊ１＝１，．．．，ｍ，ｊ２＝１，．．．，ｎ）について、各実行フラグメントαに対する測度の差を求め、その総和すなわち
【数１】
【００３９】
を計算し、この値がε以下になる対をリストアップする。その結果、残った対を（μ1，ｊ1，μ2，ｊ2），（ｊ１＝１，．．．，ｍ’，ｊ２＝１，．．．，ｎ’）とする。
【００４０】
対調整ユニット１３は、対チェックユニット１２によるチェックを通過した対、すなわち対間の距離が一定以下である対に対して、対の距離を縮める操作を行う。
【００４１】
具体的には、対チェックユニット１２によるチェックの結果、残った対すなわち（μ1，ｊ1，μ2，ｊ2），（ｊ１＝１，．．．，ｍ’，ｊ２＝１，．．．，ｎ’）について、対調整ユニット１３は
μ１，ｊ１＝（１−ε）μ’１，ｊ１＋εμ’’１，ｊ１’
μ２，ｊ２＝（１−ε）μ’２，ｊ２＋εμ’’２，ｊ２’
μ’１，ｊ１＝μ’２，ｊ２＝ｍｉｎ（μ１，ｊ１，μ２，ｊ２）となるような分解後の測度を生成する。尚、各実行フラグメントαに対してμ’１，ｊ１（α）＝μ’２，ｊ２（α）＝ｍｉｎ（μ１，ｊ１（α），μ２，ｊ２（α））である。
【００４２】
同値遷移ユニット１４は、このようにして対調整ユニット１３により生成された対をなす測度のそれぞれを同値な測度に写す。これにより同値遷移後の測度の対を生成する。同値遷移後の測度の対は、対リストとして対リスト保存メモリ１５に格納される。
【００４３】
具体的には、
【数２】
【００４４】
とするとき、
【数３】
【００４５】
となる分布を考える。同値遷移ユニット１４は、
【数４】
【００４６】
を対リストメモリ１５に加える。
【００４７】
なお、「ｉ」が添え字「ｊ」の添え字である場合に、本明細書では、「ｊｉ」（例えば「ｊ１」「ｊ２」）と表記している箇所もあるが、両者の意味するところは同じである。また、表記「μ~」において本来ならば「~」は「μ」の直上に記されるが、本明細書では「μ~」と表記している。
【００４８】
図５にμ１の同値類及びμ２の同値類をそれぞれ示す。また、μ１の同値類について、遷移した同値な測度の一例としてμ~’１，２を図６に示す。
【００４９】
対選択ユニット１６は、コントローラ１０から呼び出されるたびに、対リスト保存メモリ１５の中から１つの測度を選択して出力する。対選択ユニット１６が一度出力した測度については、「使用済み」としてチェックが付与される。「使用済み」とチェックされた測度が以後出力され、関係自動確認に用いられることがないよう対選択ユニット１６は制御を行う。
【００５０】
以上説明した本発明の実施形態によれば、近似的なシミュレーション関係の確認に用いられ、入力された測度に対して測度分解操作を行う測度分解ユニット及びプログラムを提供することができる。
【００５１】
なお、本発明は上記実施形態そのままに限定されるものではなく、実施段階ではその要旨を逸脱しない範囲で構成要素を変形して具体化できる。また、上記実施形態に開示されている複数の構成要素の適宜な組み合わせにより、種々の発明を形成できる。例えば、実施形態に示される全構成要素から幾つかの構成要素を削除してもよい。さらに、異なる実施形態にわたる構成要素を適宜組み合わせてもよい。
【図面の簡単な説明】
【００５２】
【図１】シミュレーション関係を説明するための図
【図２】一実施形態に係る近似的なシミュレーション関係の自動確認装置を示すブロック図
【図３】図２に示される近似的なシミュレーション関係の自動確認装置の動作手順を示すフローチャート
【図４】一実施形態に係る測度分解ユニットを示すブロック図
【図５】μ１の同値類及びμ２の同値類をそれぞれ示す図
【図６】同値遷移の一例を示す図
【符号の説明】
【００５３】
１…測度分解ユニット；
２…関係自動確認ユニット；
３…結果判定部；
４…終了判定部；
１０…コントローラ；
１１…対リストアップユニット；
１２…対チェックユニット；
１３…対調整ユニット；
１４…同値遷移ユニット；
１５…対リスト保存メモリ；
１６…対選択ユニット
【技術分野】
【０００１】
本発明は、タスクＰＩＯＡ（Task-Structured Probabilistic I/O Automata）を用いた暗号プロトコルの安全性証明に関する。
【背景技術】
【０００２】
暗号プロトコルの解析方法には様々なものがあるが、プロトコルをタスクＰＩＯＡを用いて表現し、汎用的結合可能性のフレームワークを用いて解析する方法が知られている（例えば「非特許文献１」参照。）。この解析方法は、タスクＰＩＯＡで表現した現実プロトコルから理想プロトコルへのインプリメンテーション（implementation）関係を示すことによりプロトコルの安全性を証明するというものである。一般に、シミュレーション（simulation）関係が満たされるとき、インプリメンテーション関係も満たされる。そこで、実際にインプリメンテーション関係を示す際には、インプリメンテーション関係よりも証明が容易なシミュレーション関係の存在を証明する。この場合、証明可能なプロトコルの範囲はシミュレーション関係を満たすプロトコルに制限される。
【０００３】
上記非特許文献１の解析方法は、厳密なシミュレーション関係を用いるものであるが、シミュレーション関係の条件を緩和したいくつかの近似的なシミュレーション関係が提案されている。厳密なシミュレーション関係を確認する操作の一部は自動化されている（例えば「非特許文献２」参照。）。しかしながら、近似的なシミュレーション関係を確認する操作（例えば「非特許文献３」参照。）については自動化されていない。
【非特許文献１】R.Canetti et al., "Using Task-Structured Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol", IACR e-print/2005/452, 2005.
【非特許文献２】櫟粛之,「Task-PIOAに基づくIdeal-Functionality実現の証明の自動化」，信学技報AI2006-18
【非特許文献３】R.Segala and A.Turrini, “Approximated Computationally Bounded Simulation Relations for Probabilistic Automata”, IEEE-Computer-Security-Foundations-Symposium-2007
【発明の開示】
【発明が解決しようとする課題】
【０００４】
本発明は、近似的なシミュレーション関係を確認する操作については自動化されていない点に鑑みてなされたものであり、近似的なシミュレーション関係の確認に用いられ、特に、これまでの厳密なシミュレーション関係の確認の際には必要ではなかった測度分解操作を行う測度分解装置及びプログラムを提供することを目的とする。
【課題を解決するための手段】
【０００５】
本発明の一観点に係る測度分解装置は、入力された第１の入力測度と第２の入力測度のそれぞれを分解する測度分解装置である。該測度分解装置は、前記第１の入力測度と同値な測度の集合及び前記第２の入力測度と同値な測度の集合をリストアップし、前記第１の入力測度と同値な測度のうちの１つと前記第２の入力測度と同値な測度のうちの１つとから構成される対の集合を生成する対リストアップユニットと、対間の距離が一定以下である対をチェックする対チェックユニットと、前記対間の距離が一定以下である対に対して、対の距離を縮める操作を行って分解後の測度を生成する対調整ユニットと、前記分解後の測度のそれぞれを同値な測度に写すことにより同値遷移後の測度の対を生成する同値遷移ユニットと、前記同値遷移後の測度の対からなる対リストを記憶する対リスト保存メモリと、前記対リスト保存メモリに記憶されている対リストから、未使用の同値遷移後の測度の対を選択して出力する対選択ユニットとを具備する。
【発明の効果】
【０００６】
本発明によれば、近似的なシミュレーション関係の確認に用いられる測度分解装置及びプログラムを提供できる。
【発明を実施するための最良の形態】
【０００７】
以下、図面を参照しながら本発明の実施形態を説明する。本実施形態では近似的なシミュレーション関係の確認に用いられる測度分解装置について説明する。この当該装置は、コンピュータを測度分解装置として機能させるためのプログラムとして実現することも可能である。
【０００８】
本実施形態では、以下の性質を持つ関係を、確認の対象となる関係とする。
【０００９】
（１）２つの測度に関して、近似的な関係Ｒεの元となっている厳密な関係Ｒについて、Ｒが成立しているならば、２つの測度のトレースが等しくなるような関係。すなわちμ１Ｒμ２→ｔｄｉｓｔ（μ１）＝ｔｄｉｓｔ（μ２）である。
【００１０】
（２）分解前の測度について当該関係Ｒεが成立するとは、分解後の測度について誤差のない厳密な関係Ｒが成立することを意味するような関係。ここで、測度はμ１Ｒεμ２→μ’１Ｒμ’２，μ１＝（１−ε）μ’１＋εμ”１，μ２＝（１−ε）μ’２＋εμ”２のように分解できる。ただし、εは微小な値である。
【００１１】
ここで、本実施形態に係る測度分解装置の具体的構成を説明する前に、関連する概念としてＰＩＯＡの定義、タスクＰＩＯＡ及びタスクスケジューラの定義、ならびにシミュレーション関係の定義についてそれぞれ説明する。
【００１２】
先ず、測度については、例えば非特許文献１の「2.1.1 Probability-measures」の項において定義されている。
【００１３】
ＰＩＯＡについては、例えば非特許文献１の「Definition 2.5」の項において定義されている。ＰＩＯＡ（Probabilistic I/O Automata；確率的入出力オートマトン）は、Ｑを状態の可算集合，ｑ￣∈Ｑを初期状態，Ｉを入力アクションの可算集合，Ｏを出力アクションの可算集合，Ｈを内部アクションの可算集合，Ｄ⊆（Ｑ×（Ｉ∪Ｏ∪Ｈ）×Ｄｉｓｃ（Ｑ））を遷移関係とするとき、Ρ＝（Ｑ，ｑ￣，Ｉ，Ｏ，Ｈ，Ｄ）で表される。Ｉ∪Ｏ∪ＨをＡと表記し、Ρの「アクション」と呼ぶ。なお、表記「ｑ￣」において本来ならば「￣」は「ｑ」の直上に記されるが、本明細書では「ｑ￣」と表記している。Ｉ∪ＯをＥと表記し、Ρの「外部アクション」と呼ぶ。ＰＩＯＡ Ρの「実行フラグメント」とは、状態とアクションの有限又は無限の列であって状態で始まるものである。実行フラグメントのうち最初の状態が初期状態であるものを「実行」と呼ぶ。「トレース」とは、実行フラグメントを外部アクションに制限したものである。
【００１４】
タスクＰＩＯＡ及びタスクスケジューラについては、例えば非特許文献１の「Definition 3.1」「Definition 3.2」の項においてそれぞれ定義されている。Τ＝（Ρ，Ｒ）の対を「タスクＰＩＯＡ」と呼ぶ。Ρ＝（Ｑ，（ｑ）￣，Ｉ，Ｏ，Ｈ，Ｄ）はＰＩＯＡであり、Ｒは、ｌｏｃａｌｌｙ−ｃｏｎｔｒｏｌｌｅｄ ａｃｔｉｏｎ（Ｏ∪Ｈ）上の同値類である。なお、集合Ｓにおいてａ，ｂ，ｃ∈Ｓに対し、二項関係〜が反射律（ａ〜ａ）、対称律（ａ〜ｂ⇒ｂ〜ａ）、推移律（ａ〜ｂかつｂ〜ｃ⇒ａ〜ｃ）を満たすとき、「〜」は同値関係という。ここで、Ｒの要素を「タスク（ｔａｓｋ）」という。Τ＝（Ρ，Ｒ）を閉じたタスクＰＩＯＡとする。Τの「タスクスケジュラ」は、Ｒ内のタスクの有限個または無限個の列ρ＝Ｔ１Ｔ２・・・と定義される。タスクＰＩＯＡの実行フラグメントの分布は、タスクスケジューラ内のタスクを順に施していくことによって刻々と変化する。このプロセス（確率的な実行）を記述するのがａｐｐｌｙ関数である。ａｐｐｌｙ関数は、有限の実行フラグメント上の離散確率測度とタスクスケジュールの対を入力とし、実行フラグメント上の離散確率測度を出力する関数である。ここで、μを実行フラグメント上の確率測度とするとき、ｔｄｉｓｔ（μ）はμに含まれる各実行フラグメントに対してトレースをとることによって得られる像測度である。
【００１５】
ここで、タスクＰＩＯＡの動作履歴について、一例を挙げて説明する。
【００１６】
先ず「実行フラグメント(execution fragment)」は、状態から始まりアクションと状態が交互に出現する列のことであり、例えば１／２｛ｑ０ａ１ｑ１ａ２ｑ２ａ３ｑ３＋ｑ０ａ１ｑ’１ａ’２ｑ’２ａ’３ｑ’３｝で表される。但し、ｑ０，ｑ１，ｑ２，ｑ３，ｑ’１，ｑ’２，ｑ’３，ｑ’’２∈Ｑ（状態）であり、ａ１，ａ２，ａ’１，ａ’２∈Ｅ（外部アクション）であり、ａ3，ａ’3∈Ｈ（内部アクション）であるとする。
【００１７】
「実行(execution)」とは、初期状態から始まる実行フラグメントのことである。ＰＩＯＡであるΡについての実行の全ての集合をｅｘｅｃｓ（Ρ）と表記する。
【００１８】
トレース(trace)とは、実行フラグメントを外部アクションに制限して得られる列のことであり、例えば上記に対応するものは、１／２｛ａ１ａ２＋ａ１ａ’２｝と表すことができる。ここで、ａ１ａ２はｑ０ａ１ｑ１ａ２ｑ２ａ３ｑ３に対応し、ａ１ａ’２はｑ０ａ１ｑ’１ａ’２ａ’３ｑ’３に対応する。
【００１９】
「tdist」とは、各トレースの出現確率を表す確率分布のことである。
【００２０】
「遷移」とは、ａｐｐｌｙ関数によって、実行フラグメント上の分布にタスクスケジューラの列を作用させて、新しい分布に写すことをいう。遷移の一例は、例えばｑ０ａ１ｑ１→１／２｛ｑ０ａ１ｑ１ａ２ｑ’２＋ｑ０ａ１ｑ１ａ２ｑ’’２｝と表される。
【００２１】
シミュレーション関係については、例えば非特許文献１の「Definition 3.23」「Definition 3.24」「Definition 3.25」の項において定義されている。
【００２２】
図１に示すようなタスクスケジュール間の対応付け写像が存在するとき、RはSimulation（シミュレーション）関係であるという。厳密には、シミュレーション関係は次のように定義される。
【００２３】
Τ１＝（Ρ１，Ｒ１），Τ２＝（Ρ２，Ｒ２）をｃｏｍｐａｒａｂｌｅであってｃｌｏｓｅｄであり、ａｃｔｉｏｎ−ｄｅｔｅｒｍｉｎｉｓｔｉｃなタスクＰＩＯＡｓとする。Ｒは、Ρ１の有限ｅｘｅｃｕｔｉｏｎ上の離散分布からΡ２の有限ｅｘｅｃｕｔｉｏｎ上の離散分布への関係であり、ε１Ｒε２ならば、ｔｄｉｓｔ（ε１）＝ｔｄｉｓｔ（ε２）とする。また、ｃ：（Ｒ＊１×Ｒ１）→Ｒ＊２とする。開始条件すなわちδ（ｑ￣１）Ｒδ（ｑ￣２）を満たし、ステップ条件すなわちε１Ｒε２でρ１∈Ｒ＊１であり、ε１がρ１とｃｏｎｓｉｓｔｅｎｔであり、ε２がｆｕｌｌ（ｃ）（ρ１）とｃｏｎｓｉｓｔｅｎｔであって、Ｔ∈Ｒ１とする。このとき、ε’１Ε（Ｒ）ε’２，ε’１＝ａｐｐｌｙ（ε１，Ｔ），ε’２＝ａｐｐｌｙ（ε２，ｃ（ρ１，Ｔ））を満たすとき、ＲはΤ１からΤ２へのシミュレーション関係である。
【００２４】
関連する概念としては以上である。次に、冒頭で述べた確認の対象となる関係、すなわち近似的なシミュレーション関係を次のように定義する。
【００２５】
２つの実行の上の測度μ１，μ２を以下のように分解する。
【００２６】
μ１＝（１−ε）μ’１＋εμ’’１
μ２＝（１−ε）μ’２＋εμ’’２
ここで、εは微小な値である。μ’１Ｒμ’２となる分解方法が存在するとき、近似的なシミュレーション関係（μ１Ｒεμ２）が成り立つと定義する。ここで、Ｒは厳密なシミュレーション関係を表す。
【００２７】
シミュレーション関係の確認について説明する。シミュレーション関係の確認は３つの段階、すなわち（１）実システムのタスクＰＩＯＡモデルと理想システムのタスクＰＩＯＡモデルとを構成する段階、（２）中間システムを構成する段階、（３）実システムから中間システムへのシミュレーション関係、及び中間システムから理想システムへのシミュレーション関係の確認を行う段階を有する。このうち、（３）の段階のみが自動化されており、これを自動実行するユニットを「関係自動確認ユニット」と呼ぶことにする。関係自動確認ユニットについては例えば非特許文献２に記載されている。
【００２８】
図２は、一実施形態に係る近似的なシミュレーション関係の自動確認装置を示すブロック図である。この装置は２つの測度を入力とし、これらが近似的なシミュレーション関係を充足するかそれとも不充足であるかを結果として出力する装置であって、測度分解ユニット１と、関係自動確認ユニット２と、結果判定部３と、終了判定部４とを具備する。
【００２９】
図３は、図２に示される近似的なシミュレーション関係の自動確認装置の動作手順を示すフローチャートである。先ず測度分解ユニット１に測度が入力される（ステップＳ１）。測度分解ユニット１はこの入力された測度を分解し、いくつかの分解パターンを出力する（ステップＳ２）。測度分解ユニット１が測度をどのように分解するかについては後述する。分解された測度は、関係自動確認ユニット２に送られる。関係自動確認ユニット２は、分解された測度について、これがシミュレーション関係を充足するかそれとも不充足であるかを確認し、その結果を出力する（ステップＳ３）。次に、結果判定部３は、ステップ３において出力された結果が「充足」であれば、その旨を出力して処理を終了し、「不充足」であればステップＳ５に移行する（ステップＳ４）。ステップＳ５では、ステップＳ２において得られている分解パターンの全てについて関係確認を試したかを終了判定部４が判定する。全ての分解パターンについて関係確認を行っていないならば、その分解パターンが測度分解ユニット１から出力され、関係自動確認ユニット２に与えられるよう、制御はステップＳ２に移行する。全ての分解パターンについて関係確認を終えており、全て「不充足」の結果となっているならば、終了判定部４はその旨を出力して処理を終了する。
【００３０】
なお、図２に示される自動確認装置の構成及びその動作手順はあくまで一例であって、実施形態に係る測度分解ユニットは、これとは別の装置構成に適用することができる。
【００３１】
従来のシミュレーション関係の自動確認装置は、本実施形態のような測度分解ユニットを備えておらず、入力された測度を分解することなく、関係自動確認ユニットによりシミュレーション関係を充足するか否かを確認するものである。
【００３２】
測度分解ユニット１は、本実施形態の冒頭で説明した性質を持つような近似的なシミュレーション関係を確認するために用いられ、図４に示されるように、コントローラ１０と、対リストアップユニット１１と、対チェックユニット１２と、対調整ユニット１３と、同値遷移ユニット１４と、対リスト保存メモリ１５と、対選択ユニット１６とを具備する。
【００３３】
コントローラ１０は、当該測度分解ユニット１が何回目に呼び出されたかを管理している。これは、図３のステップＳ５に示した処理（全ての分解パターンを試したかどうかの判定）に関係する。コントローラ１０は、測度分解ユニット１が最初に呼び出されたときは、入力された測度を対リストアップユニット１１に渡し、当該測度の分解処理が行われるようにする。そして測度分解ユニット１の２回目以降の呼び出しの際には、対選択ユニット１６を制御し、対リスト保存メモリ１５に保存されている未使用の測度（分解された測度）が出力されるようにする。
【００３４】
測度分解ユニット１には、暗号プロトコルの実行履歴である実行が測度として入力される。ここで、２つの測度（第１の入力測度μ１と第２の入力測度μ２）が測度分解ユニット１に入力され、測度分解ユニット１が第１の入力測度と第２の入力測度のそれぞれを分解するものとする。μ１，μ２は、状態とアクションが交互に出現するような列であり、アクションには、入力アクション、出力アクション、内部アクションがある。
【００３５】
対リストアップユニット１１は、第１の入力測度μ１と同値な測度の集合と、第２の入力測度μ２と同値な測度の集合とをリストアップし、第１の入力測度μ１と同値な測度のうちの１つと、第２の入力測度μ２と同値な測度のうちの１つとにより構成される対の集合を作る。
【００３６】
具体的には、対リストアップユニット１１はμ１，μ２に対してｔｄｉｓｔ（μｉ）を計算する。これは、μ１，μ２について、入力アクションと出力アクションのみを残すことによって得られる。次に、対リストアップユニット１１はｔｄｉｓｔ（μｉ）＝ｔｄｉｓｔ（μｉ，ｊｉ）となるような、測度μｉ，ｊｉをリストアップする。つまり、μｉ，ｊｉは、状態と内部アクションの違いは無視して、入力アクションと出力アクションについて比較したときに、μｉと同じになるものである。
【００３７】
対チェックユニット１２は、対の間の距離が一定以下であるかをチェックする。
【００３８】
具体的には、対チェックユニット１２は全ての対（μ1，ｊ1，μ2，ｊ2），（ｊ１＝１，．．．，ｍ，ｊ２＝１，．．．，ｎ）について、各実行フラグメントαに対する測度の差を求め、その総和すなわち
【数１】
【００３９】
を計算し、この値がε以下になる対をリストアップする。その結果、残った対を（μ1，ｊ1，μ2，ｊ2），（ｊ１＝１，．．．，ｍ’，ｊ２＝１，．．．，ｎ’）とする。
【００４０】
対調整ユニット１３は、対チェックユニット１２によるチェックを通過した対、すなわち対間の距離が一定以下である対に対して、対の距離を縮める操作を行う。
【００４１】
具体的には、対チェックユニット１２によるチェックの結果、残った対すなわち（μ1，ｊ1，μ2，ｊ2），（ｊ１＝１，．．．，ｍ’，ｊ２＝１，．．．，ｎ’）について、対調整ユニット１３は
μ１，ｊ１＝（１−ε）μ’１，ｊ１＋εμ’’１，ｊ１’
μ２，ｊ２＝（１−ε）μ’２，ｊ２＋εμ’’２，ｊ２’
μ’１，ｊ１＝μ’２，ｊ２＝ｍｉｎ（μ１，ｊ１，μ２，ｊ２）となるような分解後の測度を生成する。尚、各実行フラグメントαに対してμ’１，ｊ１（α）＝μ’２，ｊ２（α）＝ｍｉｎ（μ１，ｊ１（α），μ２，ｊ２（α））である。
【００４２】
同値遷移ユニット１４は、このようにして対調整ユニット１３により生成された対をなす測度のそれぞれを同値な測度に写す。これにより同値遷移後の測度の対を生成する。同値遷移後の測度の対は、対リストとして対リスト保存メモリ１５に格納される。
【００４３】
具体的には、
【数２】
【００４４】
とするとき、
【数３】
【００４５】
となる分布を考える。同値遷移ユニット１４は、
【数４】
【００４６】
を対リストメモリ１５に加える。
【００４７】
なお、「ｉ」が添え字「ｊ」の添え字である場合に、本明細書では、「ｊｉ」（例えば「ｊ１」「ｊ２」）と表記している箇所もあるが、両者の意味するところは同じである。また、表記「μ~」において本来ならば「~」は「μ」の直上に記されるが、本明細書では「μ~」と表記している。
【００４８】
図５にμ１の同値類及びμ２の同値類をそれぞれ示す。また、μ１の同値類について、遷移した同値な測度の一例としてμ~’１，２を図６に示す。
【００４９】
対選択ユニット１６は、コントローラ１０から呼び出されるたびに、対リスト保存メモリ１５の中から１つの測度を選択して出力する。対選択ユニット１６が一度出力した測度については、「使用済み」としてチェックが付与される。「使用済み」とチェックされた測度が以後出力され、関係自動確認に用いられることがないよう対選択ユニット１６は制御を行う。
【００５０】
以上説明した本発明の実施形態によれば、近似的なシミュレーション関係の確認に用いられ、入力された測度に対して測度分解操作を行う測度分解ユニット及びプログラムを提供することができる。
【００５１】
なお、本発明は上記実施形態そのままに限定されるものではなく、実施段階ではその要旨を逸脱しない範囲で構成要素を変形して具体化できる。また、上記実施形態に開示されている複数の構成要素の適宜な組み合わせにより、種々の発明を形成できる。例えば、実施形態に示される全構成要素から幾つかの構成要素を削除してもよい。さらに、異なる実施形態にわたる構成要素を適宜組み合わせてもよい。
【図面の簡単な説明】
【００５２】
【図１】シミュレーション関係を説明するための図
【図２】一実施形態に係る近似的なシミュレーション関係の自動確認装置を示すブロック図
【図３】図２に示される近似的なシミュレーション関係の自動確認装置の動作手順を示すフローチャート
【図４】一実施形態に係る測度分解ユニットを示すブロック図
【図５】μ１の同値類及びμ２の同値類をそれぞれ示す図
【図６】同値遷移の一例を示す図
【符号の説明】
【００５３】
１…測度分解ユニット；
２…関係自動確認ユニット；
３…結果判定部；
４…終了判定部；
１０…コントローラ；
１１…対リストアップユニット；
１２…対チェックユニット；
１３…対調整ユニット；
１４…同値遷移ユニット；
１５…対リスト保存メモリ；
１６…対選択ユニット
【特許請求の範囲】
【請求項１】
入力された第１の入力測度と第２の入力測度のそれぞれを分解する測度分解装置であって、
前記第１の入力測度と同値な測度の集合及び前記第２の入力測度と同値な測度の集合をリストアップし、前記第１の入力測度と同値な測度のうちの１つと前記第２の入力測度と同値な測度のうちの１つとから構成される対の集合を生成する対リストアップユニットと、
対間の距離が一定以下である対をチェックする対チェックユニットと、
前記対間の距離が一定以下である対に対して、対の距離を縮める操作を行って分解後の測度を生成する対調整ユニットと、
前記分解後の測度のそれぞれを同値な測度に写すことにより同値遷移後の測度の対を生成する同値遷移ユニットと、
前記同値遷移後の測度の対からなる対リストを記憶する対リスト保存メモリと、
前記対リスト保存メモリに記憶されている対リストから、未使用の同値遷移後の測度の対を選択して出力する対選択ユニットとを具備する測度分解装置。
【請求項２】
前記第１及び第２の測度として、暗号プロトコルの実行履歴である実行を入力する請求項１記載の測度分解装置。
【請求項３】
前記対チェックユニットは、全ての対について各実行フラグメントに対する測度の差を求めると共に、その総和を求め、前記総和が所定値以下となる対を前記対間の距離が一定以下である対としてチェックする請求項１記載の測度分解装置。
【請求項４】
前記対間の距離が一定以下である対が（μ1，ｊ1，μ2，ｊ2），（ｊ１＝１，．．．，ｍ’，ｊ２＝１，．．．，ｎ’）であるとき、
μ１，ｊ１＝（１−ε）μ’１，ｊ１＋εμ’’１，ｊ１’
μ２，ｊ２＝（１−ε）μ’２，ｊ２＋εμ’’２，ｊ２’
μ’１，ｊ１＝μ’２，ｊ２＝ｍｉｎ（μ１，ｊ１，μ２，ｊ２）となるような分解後の測度を生成する請求項１記載の測度分解装置。
【請求項５】
入力された第１の入力測度と第２の入力測度のそれぞれを分解する測度分解プログラムであって、
コンピュータを、
前記第１の入力測度と同値な測度の集合及び前記第２の入力測度と同値な測度の集合をリストアップし、前記第１の入力測度と同値な測度のうちの１つと前記第２の入力測度と同値な測度のうちの１つとから構成される対の集合を生成する対リストアップユニット、
対間の距離が一定以下である対をチェックする対チェックユニット、
前記対間の距離が一定以下である対に対して、対の距離を縮める操作を行って分解後の測度を生成する対調整ユニット、
前記分解後の測度のそれぞれを同値な測度に写すことにより同値遷移後の測度の対を生成する同値遷移ユニット、
前記同値遷移後の測度の対からなる対リストを記憶する対リスト保存メモリ、
前記対リスト保存メモリに記憶されている対リストから、未使用の同値遷移後の測度の対を選択して出力する対選択ユニットとして機能させるための測度分解プログラム。
【請求項６】
前記第１及び第２の測度として、暗号プロトコルの実行履歴である実行を入力する請求項５記載の測度分解プログラム。
【請求項７】
前記対チェックユニットは、全ての対について各実行フラグメントに対する測度の差を求めると共に、その総和を求め、前記総和が所定値以下となる対を前記対間の距離が一定以下である対としてチェックする請求項５記載の測度分解プログラム。
【請求項８】
前記対間の距離が一定以下である対が（μ1，ｊ1，μ2，ｊ2），（ｊ１＝１，．．．，ｍ’，ｊ２＝１，．．．，ｎ’）であるとき、
μ１，ｊ１＝（１−ε）μ’１，ｊ１＋εμ’’１，ｊ１’
μ２，ｊ２＝（１−ε）μ’２，ｊ２＋εμ’’２，ｊ２’
μ’１，ｊ１＝μ’２，ｊ２＝ｍｉｎ（μ１，ｊ１，μ２，ｊ２）となるような分解後の測度を生成する請求項５記載の測度分解プログラム。
【請求項１】
入力された第１の入力測度と第２の入力測度のそれぞれを分解する測度分解装置であって、
前記第１の入力測度と同値な測度の集合及び前記第２の入力測度と同値な測度の集合をリストアップし、前記第１の入力測度と同値な測度のうちの１つと前記第２の入力測度と同値な測度のうちの１つとから構成される対の集合を生成する対リストアップユニットと、
対間の距離が一定以下である対をチェックする対チェックユニットと、
前記対間の距離が一定以下である対に対して、対の距離を縮める操作を行って分解後の測度を生成する対調整ユニットと、
前記分解後の測度のそれぞれを同値な測度に写すことにより同値遷移後の測度の対を生成する同値遷移ユニットと、
前記同値遷移後の測度の対からなる対リストを記憶する対リスト保存メモリと、
前記対リスト保存メモリに記憶されている対リストから、未使用の同値遷移後の測度の対を選択して出力する対選択ユニットとを具備する測度分解装置。
【請求項２】
前記第１及び第２の測度として、暗号プロトコルの実行履歴である実行を入力する請求項１記載の測度分解装置。
【請求項３】
前記対チェックユニットは、全ての対について各実行フラグメントに対する測度の差を求めると共に、その総和を求め、前記総和が所定値以下となる対を前記対間の距離が一定以下である対としてチェックする請求項１記載の測度分解装置。
【請求項４】
前記対間の距離が一定以下である対が（μ1，ｊ1，μ2，ｊ2），（ｊ１＝１，．．．，ｍ’，ｊ２＝１，．．．，ｎ’）であるとき、
μ１，ｊ１＝（１−ε）μ’１，ｊ１＋εμ’’１，ｊ１’
μ２，ｊ２＝（１−ε）μ’２，ｊ２＋εμ’’２，ｊ２’
μ’１，ｊ１＝μ’２，ｊ２＝ｍｉｎ（μ１，ｊ１，μ２，ｊ２）となるような分解後の測度を生成する請求項１記載の測度分解装置。
【請求項５】
入力された第１の入力測度と第２の入力測度のそれぞれを分解する測度分解プログラムであって、
コンピュータを、
前記第１の入力測度と同値な測度の集合及び前記第２の入力測度と同値な測度の集合をリストアップし、前記第１の入力測度と同値な測度のうちの１つと前記第２の入力測度と同値な測度のうちの１つとから構成される対の集合を生成する対リストアップユニット、
対間の距離が一定以下である対をチェックする対チェックユニット、
前記対間の距離が一定以下である対に対して、対の距離を縮める操作を行って分解後の測度を生成する対調整ユニット、
前記分解後の測度のそれぞれを同値な測度に写すことにより同値遷移後の測度の対を生成する同値遷移ユニット、
前記同値遷移後の測度の対からなる対リストを記憶する対リスト保存メモリ、
前記対リスト保存メモリに記憶されている対リストから、未使用の同値遷移後の測度の対を選択して出力する対選択ユニットとして機能させるための測度分解プログラム。
【請求項６】
前記第１及び第２の測度として、暗号プロトコルの実行履歴である実行を入力する請求項５記載の測度分解プログラム。
【請求項７】
前記対チェックユニットは、全ての対について各実行フラグメントに対する測度の差を求めると共に、その総和を求め、前記総和が所定値以下となる対を前記対間の距離が一定以下である対としてチェックする請求項５記載の測度分解プログラム。
【請求項８】
前記対間の距離が一定以下である対が（μ1，ｊ1，μ2，ｊ2），（ｊ１＝１，．．．，ｍ’，ｊ２＝１，．．．，ｎ’）であるとき、
μ１，ｊ１＝（１−ε）μ’１，ｊ１＋εμ’’１，ｊ１’
μ２，ｊ２＝（１−ε）μ’２，ｊ２＋εμ’’２，ｊ２’
μ’１，ｊ１＝μ’２，ｊ２＝ｍｉｎ（μ１，ｊ１，μ２，ｊ２）となるような分解後の測度を生成する請求項５記載の測度分解プログラム。
【図１】
【図２】
【図３】
【図４】
【図５】
【図６】
【図２】
【図３】
【図４】
【図５】
【図６】
【公開番号】特開２００９−２１０６４８（Ｐ２００９−２１０６４８Ａ）
【公開日】平成２１年９月１７日（２００９．９．１７）
【国際特許分類】
【出願番号】特願２００８−５１１８７（Ｐ２００８−５１１８７）
【出願日】平成２０年２月２９日（２００８．２．２９）
【出願人】（０００００３０７８）株式会社東芝 (54,554)
【Ｆターム（参考）】
【公開日】平成２１年９月１７日（２００９．９．１７）
【国際特許分類】
【出願日】平成２０年２月２９日（２００８．２．２９）
【出願人】（０００００３０７８）株式会社東芝 (54,554)
【Ｆターム（参考）】
[ Back to top ]