(57)【特許請求の範囲】
【請求項１】
通信プロトコルの参加者の集合からプロセスと環境の２つ組の集合への関数によって表わされる通信プロトコル仕様を入力する通信プロトコル仕様入力手段と、
前記通信プロトコル仕様入力手段で入力された通信プロトコル仕様を、プロトコルを実行した時に起り得る全参加者の状態遷移列の集合を生成する生成規則に、変換する通信プロトコル仕様変換手段と、
通信プロトコルに期待され、全参加者の状態遷移列の集合に関する論理式として表わされる安全性を入力する安全性入力手段と、
前記通信プロトコル仕様変換手段からの全参加者の状態遷移列の集合の生成規則および前記安全性入力手段からの安全性を表わす論理式が入力され、全参加者の状態遷移列の集合の生成規則から生成される全参加者の状態遷移列の集合について、安全性を表わす論理式の真偽を判定する検証手段と
を具備することを特徴とする通信プロトコルの安全性検証装置。
【請求項２】
通信プロトコルの参加者の状態をプロセスと環境の２つ組として記憶する記憶手段と、
前記記憶手段で記憶された通信プロトコルの参加者の集合からプロセスと環境の２つ組の集合への関数によって表わされる通信プロトコル仕様を入力する通信プロトコル仕様入力手段と、
前記通信プロトコル仕様入力手段で入力された通信プロトコル仕様を、プロトコルを実行した時に起り得る全参加者の状態遷移列の集合を生成する生成規則に、変換する通信プロトコル仕様変換手段と、
通信プロトコルに期待され、全参加者の状態遷移列の集合に関する論理式として表わされる安全性を入力する安全性入力手段と、
前記通信プロトコル仕様変換手段からの全参加者の状態遷移列の集合の生成規則および前記安全性入力手段からの安全性を表わす論理式が入力され、全参加者の状態遷移列の集合の生成規則から生成される全参加者の状態遷移列の集合について、安全性を表わす論理式の真偽を判定する検証手段と、
前記検証手段によって判定された結果を出力する出力手段と
を具備することを特徴とする通信プロトコルの安全性検証装置。
【請求項３】
出力手段の判定結果は、検証手段における論理式の真偽判定手段が真偽の判定を完了した場合はその真偽であり、真偽の判定を完了しなかった場合は完了しなかった理由であることを特徴とする請求項２記載の通信プロトコルの安全性検証装置。
【請求項４】
安全性入力手段で入力として用いられる論理式は、等式および原子論理式から、否定演算子−、論理和演算子∨、論理積演算子∧、全称演算子∀x、存在演算子∃xを含む各演算子を用いて帰納的に生成される論理式であることを特徴とする請求項１、２又は３記載の通信プロトコルの安全性検証装置。
【請求項５】
検証手段における論理式の真偽判定手段として、定理証明システムを用いることを特徴とする請求項１、２、３又は４記載の通信プロトコルの安全性検証装置。
【請求項６】
検証手段における論理式の真偽判定手段として、モデル検証システムを用いることを特徴とする請求項１、２、３又は４記載の通信プロトコルの安全性検証装置。
【請求項７】
通信プロトコルの参加者の集合からプロセスと環境の２つ組の集合への関数によって表わされる通信プロトコル仕様を入力する通信プロトコル仕様入力ステップと、
前記通信プロトコル仕様入力ステップで入力された通信プロトコル仕様を、プロトコルを実行した時に起り得る全参加者の状態遷移列の集合を生成する生成規則に、変換する通信プロトコル仕様変換ステップと、
通信プロトコルに期待され、全参加者の状態遷移列の集合に関する論理式として表わされる安全性を入力する安全性入力ステップと、
前記通信プロトコル仕様変換ステップからの全参加者の状態遷移列の集合の生成規則および前記安全性入力ステップからの安全性を表わす論理式が入力され、全参加者の状態遷移列の集合の生成規則から生成される全参加者の状態遷移列の集合について、安全性を表わす論理式の真偽を判定する検証ステップと
よりなることを特徴とする通信プロトコルの安全性検証方法。
【請求項８】
通信プロトコルの参加者の状態をプロセスと環境の２つ組として記憶する記憶ステップと、
前記記憶ステップで記憶された通信プロトコルの参加者の集合からプロセスと環境の２つ組の集合への関数によって表わされる通信プロトコル仕様を入力する通信プロトコル仕様入力ステップと、
前記通信プロトコル仕様入力ステップで入力された通信プロトコル仕様を、プロトコルを実行した時に起り得る全参加者の状態遷移列の集合を生成する生成規則に、変換する通信プロトコル仕様変換ステップと、
通信プロトコルに期待され、全参加者の状態遷移列の集合に関する論理式として表わされる安全性を入力する安全性入力ステップと、
前記通信プロトコル仕様変換ステップからの全参加者の状態遷移列の集合の生成規則および前記安全性入力ステップからの安全性を表わす論理式が入力され、全参加者の状態遷移列の集合の生成規則から生成される全参加者の状態遷移列の集合について、安全性を表わす論理式の真偽を判定する検証ステップと、
前記検証ステップによって判定された結果を出力する出力ステップと
よりなることを特徴とする通信プロトコルの安全性検証方法。
【請求項９】
通信プロトコルの参加者の集合からプロセスと環境の２つ組の集合への関数によって表わされる通信プロトコル仕様を入力する通信プロトコル仕様入力手順、
前記通信プロトコル仕様入力手順で入力された通信プロトコル仕様を、プロトコルを実行した時に起り得る全参加者の状態遷移列の集合を生成する生成規則に、変換する通信プロトコル仕様変換手順、
通信プロトコルに期待され、全参加者の状態遷移列の集合に関する論理式として表わされる安全性を入力する安全性入力手順、
前記通信プロトコル仕様変換手順からの全参加者の状態遷移列の集合の生成規則および前記安全性入力手順からの安全性を表わす論理式が入力され、全参加者の状態遷移列の集合の生成規則から生成される全参加者の状態遷移列の集合について、安全性を表わす論理式の真偽を判定する検証手順
をコンピュータに実行させるための通信プロトコルの安全性検証プログラム。
【請求項１０】
通信プロトコルの参加者の集合からプロセスと環境の２つ組の集合への関数によって表わされる通信プロトコル仕様を入力する通信プロトコル仕様入力手順、
前記通信プロトコル仕様入力手順で入力された通信プロトコル仕様を、プロトコルを実行した時に起り得る全参加者の状態遷移列の集合を生成する生成規則に、変換する通信プロトコル仕様変換手順、
通信プロトコルに期待され、全参加者の状態遷移列の集合に関する論理式として表わされる安全性を入力する安全性入力手順、
前記通信プロトコル仕様変換手順からの全参加者の状態遷移列の集合の生成規則および前記安全性入力手順からの安全性を表わす論理式が入力され、全参加者の状態遷移列の集合の生成規則から生成される全参加者の状態遷移列の集合について、安全性を表わす論理式の真偽を判定する検証手順
をコンピュータに実行させるための通信プロトコルの安全性検証プログラムを記録したコンピュータ読み取り可能な記録媒体。
【発明の詳細な説明】
【０００１】
【発明の属する技術分野】
本発明は通信の安全性を検証することに係り、特に、通信の方法を定める通信プロトコルの性質を調べることにより、通信プロトコルを用いた通信の安全性を検証する通信プロトコルの安全性検証装置及び方法、通信プロトコルの安全性検証プログラム及びそのプログラムを記録した記録媒体に関するものである。
【０００２】
【従来の技術】
通信の参加者の状態を通信の参加者が行おうとしているメッセージの送信やメッセージの受信などの動作の列であるプロセスを用いて表現し、通信プロトコルの参加者の状態の集合として表現された通信プロトコル仕様を入力し、通信プロトコル仕様を参加者が行う動作の履歴の列の集合を生成する規則に変換し、参加者が行う動作の履歴の列の集合に関する論理式によって表現された安全性を入力し、動作の履歴の列の集合を生成する規則によって生成される動作の履歴の列の集合についての動作の履歴の列の集合に関する論理式の真偽を判定する通信プロトコルの安全性検証装置が知られている。
【０００３】
【発明が解決しようとする課題】
通信の参加者の状態をプロセスとして表現する従来方法は表現が簡潔であるが、行うべき動作を終了した参加者のプロセスは空な動作列になるため、プロセスからは参加者がこれまで行ってきた動作に関する情報を得られないという欠点がある。このため従来手法では参加者の行う動作の履歴の列の情報を考え、安全性をこの集合に関する性質として与えている。しかし、この手法では安全性に関する記述が繁雑になりがちであるという欠点がある。この欠点は、通信プロトコルに分岐がある場合には特に顕著である。
【０００４】
本発明は上記の事情に鑑みてなされたもので、安全性を簡潔に記述し入力できる通信プロトコルの安全性検証装置及び方法、通信プロトコルの安全性検証プログラム及びそのプログラムを記録した記録媒体を提供することを目的とする。
【０００５】
【課題を解決するための手段】
上記目的を達成するために本発明の通信プロトコルの安全性検証装置は、通信の参加者の状態をプロセスと環境の２つ組を用いて表現することを最も主要な特徴とし、通信プロトコルの参加者の集合からプロセスと環境の２つ組の集合への関数によって表わされる通信プロトコル仕様を入力する通信プロトコル仕様入力手段と、前記通信プロトコル仕様入力手段で入力された通信プロトコル仕様をプロトコルを実行した時に起り得る全参加者の状態遷移列（大域状態の遷移列）の集合を生成する生成規則に変換する通信プロトコル仕様変換手段と、通信プロトコルに期待され全参加者の状態遷移列（大域状態の遷移列）の集合に関する論理式として表わされる安全性を入力する安全性入力手段と、前記通信プロトコル仕様変換手段からの全参加者の状態遷移列（大域状態の遷移列）の集合の生成規則および前記安全性入力手段からの安全性を表わす論理式が入力され全参加者の状態遷移列（大域状態の遷移列）の集合の生成規則から生成される全参加者の状態遷移列（大域状態の遷移列）の集合について安全性を表わす論理式の真偽を判定する検証手段とを具備することを特徴とするものである。
【０００６】
また、本発明の通信プロトコルの安全性検証方法は、通信プロトコルの参加者の集合からプロセスと環境の２つ組の集合への関数によって表わされる通信プロトコル仕様を入力する通信プロトコル仕様入力ステップと、前記通信プロトコル仕様入力ステップで入力された通信プロトコル仕様をプロトコルを実行した時に起り得る全参加者の状態遷移列（大域状態の遷移列）の集合を生成する生成規則に変換する通信プロトコル仕様変換ステップと、通信プロトコルに期待され全参加者の状態遷移列（大域状態の遷移列）の集合に関する論理式として表わされる安全性を入力する安全性入力ステップと、前記通信プロトコル仕様変換ステップからの全参加者の状態遷移列（大域状態の遷移列）の集合の生成規則および前記安全性入力ステップからの安全性を表わす論理式が入力され全参加者の状態遷移列（大域状態の遷移列）の集合の生成規則から生成される全参加者の状態遷移列（大域状態の遷移列）の集合について安全性を表わす論理式の真偽を判定する検証ステップとよりなることを特徴とする。
【０００７】
また、本発明の通信プロトコルの安全性検証プログラムは、通信プロトコルの参加者の集合からプロセスと環境の２つ組の集合への関数によって表わされる通信プロトコル仕様を入力する通信プロトコル仕様入力手順、前記通信プロトコル仕様入力手順で入力された通信プロトコル仕様をプロトコルを実行した時に起り得る全参加者の状態遷移列の集合を生成する生成規則に変換する通信プロトコル仕様変換手順、通信プロトコルに期待され全参加者の状態遷移列の集合に関する論理式として表わされる安全性を入力する安全性入力手順、前記通信プロトコル仕様変換手順からの全参加者の状態遷移列の集合の生成規則および前記安全性入力手順からの安全性を表わす論理式が入力され全参加者の状態遷移列の集合の生成規則から生成される全参加者の状態遷移列の集合について安全性を表わす論理式の真偽を判定する検証手順をコンピュータに実行させるためのものである。
【０００８】
本発明にあっては、通信の参加者の状態をプロセスのみではなく、プロセスに出現する変数への値の束縛を表す環境も同時に用いて表現するため、検証する安全性の論理式の中に参加者のプロセスおよび環境に関する情報を用いることができる。このため、本発明の目的である安全性を簡潔に記述し入力できる通信プロトコルの安全性検証装置が構成できるようになる。
【０００９】
【発明の実施の形態】
以下図面を参照して本発明の実施形態例を詳細に説明する。
【００１０】
図１は本発明の一実施形態例に係る通信プロトコルの安全性検証装置を示す構成説明図である。
【００１１】
図１の通信プロトコルの安全性検証装置は、
通信プロトコルの参加者の状態をプロセスと環境の２つ組として記憶し、通信プロトコルの参加者の集合からプロセスと環境の２つ組の集合への関数によって表わされる通信プロトコル仕様を入力する通信プロトコル仕様入力部１１、および、
前記通信プロトコル仕様入力部１１で入力された通信プロトコル仕様を、プロトコルを実行した時に起り得る全参加者の状態遷移列（大域状態の遷移列）の集合を生成する生成規則に、変換する通信プロトコル仕様変換部１２、および、
通信プロトコルに期待され、全参加者の状態遷移列（大域状態の遷移列）の集合に関する論理式として表わされる安全性を入力する安全性入力部１３、および、
前記通信プロトコル仕様変換部１２からの全参加者の状態遷移列（大域状態の遷移列）の集合の生成規則および前記安全性入力部１３からの安全性を表わす論理式が入力され、全参加者の状態遷移列（大域状態の遷移列）の集合の生成規則から生成される全参加者の状態遷移列（大域状態の遷移列）の集合について、安全性を表わす論理式の真偽を判定する検証部１４、および、
前記検証部１４によって判定された結果を出力する出力部１５から構成される。
【００１２】
これを動作するには、
１．通信プロトコル仕様入力部１１で通信プロトコルの仕様を入力し、
２．通信プロトコル仕様変換部１２で通信プロトコルの仕様を大域状態の遷移列の集合の生成規則に変換し、
３．安全性入力部１３で通信プロトコルに期待される安全性を大域状態の遷移列の集合についての論理式として入力し、
４．検証部１４を動作させ、大域状態の遷移列の集合の生成規則によって生成される大域状態の遷移列の集合について、大域状態の遷移列の集合についての論理式の真偽を判定し、
５．出力部１５によって判定結果を出力する。
【００１３】
次に、用語の定義を行った後、各部について具体的に述べる。
【００１４】
〔１〕  用語の定義
以降の説明で用いる用語を定義する。
【００１５】
［数項］…数項変数記号の集合およびデータの集合が与えられているとする。このとき、数項の集合を次のように定義する。
【００１６】
・ｘが数項変数記号のとき、２つ組（Varnat,x）は数項である。
【００１７】
・ｄがデータのとき、２つ組（Nat,d）は数項である。
【００１８】
［項］…変数記号の集合、数項の集合、項の組をつくる演算、ハッシュ演算、および暗号化演算が与えられているとする。このとき、項の集合を次のように帰納的に定義する。
【００１９】
・Ｘが変数記号のとき、２つ組（Variable,X）は項である。この項は変数を表す。
【００２０】
・Ａが数項であるとき、２つ組（Agent,A）は項である。この項は参加者の名前を表す。
【００２１】
・Ｋが数項であるとき、２つ組（Key,K）は項である。この項は暗号化あるいは復号化に用いられる鍵を表す。
【００２２】
・Ｎが数項であるとき、（Number,N）は項である。この項は数を表す。
【００２３】
・Ｎが数項であるとき、（Nonce,N）は項である。この項は乱数やタイムスタンプなどの一度だけ用いられる秘密の数を表す。
【００２４】
・ｎが非負整数で、M1,・・・,Mnがそれぞれ項であるとき、（n＋1）個組（Tuple,M1,・・・,Mn）は項である。この項はM1,・・・,Mnを要素とするｎ個組を表す。
【００２５】
・Ｍが項であるとき、２つ組（Hash,M）は項である。この項はＭにハッシュ演算を行なって得られるものを表す。
【００２６】
・Ｍが項であり、Ｋが数項であるとき、３つ組（Crypt,M,K）は項である。この項はＭを鍵Ｋを用いて与えられた暗号化演算を行なって得られるものを表す。
【００２７】
［数項環境］…数項変数記号の集合から数項の集合への部分関数を数項環境と呼ぶ。
【００２８】
［項環境］…変数記号の集合から項への部分関数を項環境と呼ぶ。
【００２９】
［環境］…et，enが項環境、数項環境であるとき、２つ組（et,en）を環境と呼ぶ。
【００３０】
［イベント］…項の集合および数項の集合が与えられているとする。このとき、イベントを次のように帰納的に定義する。
【００３１】
・Ｍが項であるとき、２つ組（Send,M）はイベントである。このイベントはＭの送信を表す。
【００３２】
・Ｍが項であるとき、２つ組（Recv,M）はイベントである。このイベントはＭの送信を表す。
【００３３】
・ｘが数項変数記号であるとき、（New,x）はイベントである。このイベントは秘密の数ｘの生成を表す。
【００３４】
・Ｑがプロセスと環境についての述語であるとき、（Assert,Q）はイベントである。プロセスＰおよび環境ｅに対してＱが成り立つとき、Q(P,e）が成り立つという。
【００３５】
・Ｘが変数記号であり、Ｍが項であるとき、（Let,X,M）はイベントである。このイベントは変数ＸへのＭの代入を表す。
【００３６】
・ｘが数項変数記号であり、Ｎが数項であるとき、（Letnat x,N）はイベントである。このイベントは数項変数ｘへのＮの代入を表す。
【００３７】
［プロセス］…イベントの列をプロセスと呼ぶ。プロセスＰの先頭にイベントevを付け加えて得られるプロセスをev:Pと書く。
【００３８】
［局所状態］…プロセスと環境の２つ組を局所状態と呼ぶ。
【００３９】
［大域状態］…参加者の集合から局所状態の集合への関数を大域状態と呼ぶ。ｓが大域状態であるとき、ｓの参加者ｉにおける値をs(i）と書く。
【００４０】
［状態遷移列］…状態遷移列の集合を次のように帰納的に定義する。
【００４１】
・ｓが状態であるとき、２つ組（Stａte,s）は状態遷移列である。
【００４２】
・ｉが参加者の集合の要素であり、ｔが状態遷移列であり、lsが局所状態であり、evがイベントとであるとき、５つ組（Transit,i,ls,ev,t）は状態遷移列である。
【００４３】
［局所状態取得関数］…状態遷移列の集合と参加者の集合からなる直積集合から局所状態の集合への関数getstateを次のように帰納的に定義する。状態遷移列ｔおよび参加者ｉにおけるgetstateの値（getstate(t,i）は、
・ある大域状態ｓについて、t = (State,s）と表わされるとき、getstate(t,i) = s(i)である。
【００４４】
・ある状態遷移列t'、局所状態ls、イベントevについて、t = (Transit,i,ls,ev,t')と表わされるとき、getstate(t,i) = lsである。
【００４５】
・ある状態遷移列t'、参加者ｊ、局所状態ls、イベントevについて、t = (Transit,i,ls,ev,t'）と表わされ、かつ、ｊがｉと異なるとき、getstate(t,i) = getstate(t',i）である。
【００４６】
［項評価関数eval］…項Ｍ、項環境et、および数項環境enについて、eval((et,en),M）は、Ｍに次の２つの操作を順に行なって得られる項である。
【００４７】
・Ｍに出現する数項変数ｘのうちen(x）が値を持つもの全てについて、Ｍ中のｘの出現を全てen(x）に置きかえる。
【００４８】
・Ｍに出現する項変数Ｘのうちet(X）が値を持つもの全てについて、Ｍ中のＸの出現を全てet(X）に置きかえる。
【００４９】
［数項評価関数evalnat］…数項ｎおよび数項環境enについて、数項evalnat(en,n）は、en(n）が値を持つときevalnat(en,n) = en(n）であり、en(n）が値を持たないときevalnat(en,n) = nである。
【００５０】
［マッチング関数］…環境ｅ、項Ｍ、および項M'に対して環境match(e,M,M'）はeval(e,M) = eval(e',M'）となるe'のうち、定義域の集合が最も小さいものである。
【００５１】
〔２〕  仕様入力部
仕様入力部１１では通信プロトコルの仕様および各参加者の初期状態を表す大域状態が入力される。大域状態は、通信の参加者の集合からプロセスと環境の２つ組の集合への関数として入力される。
【００５２】
たとえばNeedhamとSchroederらによる共有鍵認証のプロトコル（参考文献：R.Needham and M,Schroeder:Using encryption for authentication in large networks of computers,Communications of ACM Vol.8 (1) 18-36,1990 )では、数１、数２、および数３によってそれぞれ与えられるInitiator，ResponderおよびServerのプロセスを用いて、数４の大域状態で与えられる。ただし、x1→v1,x2→v2,・・・はx1,x2,・・・をそれぞれv1,v2,・・・に対応づける関数である。
【数１】
0003764392.tif 000002
【００５３】
【数２】
0003764392.tif 000003
【００５４】
【数３】
0003764392.tif 000004
【００５５】
【数４】
0003764392.tif 000005
【００５６】
〔３〕  仕様変換部
仕様変換部１２は仕様入力部１１から入力された仕様を、このプロトコルを実行したときに起り得る状態遷移列の集合を生成する規則に変換し、検証部（主計算部）１４に出力する。
【００５７】
入力された仕様ｓを次の生成規則に変換する。この生成規則はこのプロトコルを実行した際の可能な大域状態の遷移列の集合traceを帰納的に定義する。
【００５８】
・(State,s）はtraceの要素である。
【００５９】
・traceの要素ｔ、参加者ｉ、項Ｍ、項M'、プロセスＰおよび環境ｅが以下の条件を満たすとき、
−getstate(t,i) = ((Send,M):P,e）である。
【００６０】
−eval(e,M) = M'である。
【００６１】
(Transit,i,(P,e),(Send,M'),t）はtraceの要素である。
【００６２】
・traceの要素ｔ、参加者ｉ、項Ｍ、項M'、プロセスＰ、および環境ｅが以下の条件を満たすとき、
−getstate(t,i) = ((Recv,M):P,e）である。
【００６３】
−traceに(Send,M'）が出現する。
【００６４】
−letmatch(e,M,M') = e'である。
【００６５】
(Transit,i,(P,e'),(Recv,M'),t）はtraceの要素である。
【００６６】
・traceの要素ｔ、参加者ｉ、数項変数ｘ、データｎ、プロセスＰ、項環境ｅｔ、および数項環境enが以下の条件を満たすとき、
−getstate(t,i) = ((New,x):P,(et,en)）である。
【００６７】
−ｎはｔに出現しないデータである。
【００６８】
(Transit,i,(P,(et,en')),(New,n),t）はtraceの要素である。ただし、en'はen'(x) = (Nat,n）かつｘと異なる数項変数ｙについてen'(y) = en(y）となる数項環境である。
【００６９】
・traceの要素ｔ、参加者の集合の要素ｉ、プロセスＰ、および環境ｅが以下の条件を満たすとき、
−getstate(t,i) = ((Assert,Q):P,e）である。
【００７０】
−Q(P,e）が成り立つ。
【００７１】
(Transit,i,(P,e),(Assert,Q),t）はtraceの要素である。
【００７２】
・traceの要素ｔ、参加者の集合の要素ｉ、項Ｍ、項M'、プロセスＰ、項環境et、数項環境en、および項変数Ｘが以下の条件を満たすとき、
−getstate(t,i) = ((Let,X,M):P,(et,en)）である。
【００７３】
−eval(et,en)M = M'である。
【００７４】
(Transit,i,(P,et',en),(Let,X,M'),t）はtraceの要素である。ただし、et'はet'(X) = M'、かつ、Ｘと異なる項変数Ｙについてet'(Y) = et(Y）となる項環境である。
【００７５】
・traceの要素ｔ、参加者の集合の要素ｉ、数項ｎ、数項n'、プロセスＰ、項環境et、数項環境en、および項変数ｘが以下の条件を満たすとき、
−getstate(t,i) = ((Letnat,x,n):P,(et,en)）である。
【００７６】
−evalnat(en,n) = n'である。
【００７７】
(Transit,i,(P,(et,en')),(Letnat,x,n'),t）はtraceの要素である。ただし、en'はen'(x) = n'、かつ、ｘと異なる数項変数ｙについてen'(y) = en(y）となる数項環境である。
【００７８】
〔４〕  安全性入力部
安全性入力部１３では、仕様入力部１１で入力する通信プロトコル仕様によって定められる通信プロトコルが持つと期待される安全性を、大域状態の遷移列の集合に関する論理式の集合として入力する。ここで入力として用いられる論理式は、検証部１４のもつ論理式の真偽判定手段によって判定可能な論理式であり、等式および原子論理式から、否定演算子−、論理和演算子∨、論理積演算子∧、全称演算子∀x、存在演算子∃xおよびその他の各演算子を用いて帰納的に生成される論理式であり、原子論理式および等式の中には、局所状態取得関数getstate,n個組からその各要素を取り出す関数、列から先頭の要素および先頭の要素を除いた残りの要素を取り出す関数およびその他の各関数記号、そして大域状態の遷移列を表す変数traceを用いることができる。また、この論理式の集合として、原子論理式の再帰的定義を含めることができる。安全性入力部１３で入力される安全性を記述する論理式の中で、大域状態の遷移列を表す変数traceおよび、traceの要素から参加者の状態を取り出す関数getstateを用いることができるため、参加者の状態、特に参加者の環境を直接参照することができ、安全性の記述を簡潔に行うことができる。
【００７９】
たとえば上記NeedhamとSchroederによる共有鍵認識プロトコルに期待される性質の１つを数５のように表す。これはある参加者がResponderとしてプロトコルの実行を完了した場合に、対応するInitiatorが存在するという認証についての性質を表す。ただしここでは、論理式tr' ⊂trは、tr' = trであるか、あるいはあるtr"，ｉ，ｓおよびｅについてtr = (Transit,i,s,e,tr")となりかつtr"⊂trとなる場合に真である。
【数５】
0003764392.tif 000006
【００８０】
〔５〕  検証部
検証部１４は、仕様変換部１２から入力された大域状態の遷移列の生成規則によって生成される大域状態の遷移列の集合traceに対し、安全性入力部１３から入力された大域状態の遷移列の集合に関する論理式が成立するか否かを判定する。論理式に含まれる変数traceを生成された大域状態の遷移列の集合として解釈する。
【００８１】
参加者の状態をプロセスと環境を用いて表現しているため、getstate関数の値を計算し、参加者の状態であるプロセスと環境を取り出すことが可能になっている。
【００８２】
たとえば、数６に示した大域環境によって与えられるプロトコル仕様を仕様変換部１２によって変換され、状態遷移列の集合を生成する規則となって入力された場合、この生成規則によって検証部で生成される集合traceには、その要素の１つとして数７に示した遷移状態列が含まれる。検証部１４はこのような集合stateを含む論理式について、その真偽を判定する。
【数６】
0003764392.tif 000007
【００８３】
【数７】
0003764392.tif 000008
【００８４】
以上の論理式の真偽判定のために定理証明システムIsabelleを利用することができる。（参考文献：L.C.Paulson,The Foundation of a Genetic Theorem Prover,Journal of Automated Reasoning Vol.5 363-397,1989)また、モデル検証システム（参考文献：E.M.Clarke,Orna Grumberg and Doron Peled,Model Checing,MIT Press,2000）を利用することもできる。
【００８５】
定理証明システムIsabelle上では、仕様変換部１２に相当する仕様変換を行う関数runの定義は数８〜数１１、数１２〜数１６、および、数１７〜数２２で与えられ、先に例に挙げたNeedhamとSchroederらによる共有鍵認証のプロトコルの定義は、数２３〜数２４で与えられる。以上の入力をIsabelleに与え、Isabelle上では数２５で与えられる先に例に挙げた数５の安全性をIsabelleの対話的証明機能を用いて証明することにより、NeedhamとSchroederによる公開鍵認証のプロトコルに期待される安全性の１つである数５の安全性を検証できる。
【００８６】
【数８】
0003764392.tif 000009
【００８７】
【数９】
0003764392.tif 000010
【００８８】
【数１０】
0003764392.tif 000011
【００８９】
【数１１】
0003764392.tif 000012
【００９０】
【数１２】
0003764392.tif 000013
【００９１】
【数１３】
0003764392.tif 000014
【００９２】
【数１４】
0003764392.tif 000015
【００９３】
【数１５】
0003764392.tif 000016
【００９４】
【数１６】
0003764392.tif 000017
【００９５】
【数１７】
0003764392.tif 000018
【００９６】
【数１８】
0003764392.tif 000019
【００９７】
【数１９】
0003764392.tif 000020
【００９８】
【数２０】
0003764392.tif 000021
【００９９】
【数２１】
0003764392.tif 000022
【０１００】
【数２２】
0003764392.tif 000023
【０１０１】
【数２３】
0003764392.tif 000024
【０１０２】
【数２４】
0003764392.tif 000025
【０１０３】
【数２５】
0003764392.tif 000026
【０１０４】
〔６〕  出力部
出力部１５は検証部１４によって判定された判定結果を出力する。判定結果は検証部１４における論理式の真偽判定システムが真偽の判定を完了した場合は、その真偽であり、何らかの理由によって真偽の判定を完了しなかった場合は完了しなかった理由である。
【０１０５】
尚、前記実施形態例における通信プロトコルの安全性検証方法は、具体的にはパソコン等のコンピュータにより、予め所定の通信プロトコルの安全性検証プログラムに基いて実行される。前記通信プロトコルの安全性検証プログラムは所定のコンピュータ読み取り可能な記録媒体に記録することができる。
【０１０６】
すなわち、本発明の実施形態例に係る通信プロトコルの安全性検証プログラムは、通信プロトコルの参加者の集合からプロセスと環境の２つ組の集合への関数によって表わされる通信プロトコル仕様を入力する通信プロトコル仕様入力手順、前記通信プロトコル仕様入力手順で入力された通信プロトコル仕様をプロトコルを実行した時に起り得る全参加者の状態遷移列の集合を生成する生成規則に変換する通信プロトコル仕様変換手順、通信プロトコルに期待され全参加者の状態遷移列の集合に関する論理式として表わされる安全性を入力する安全性入力手順、前記通信プロトコル仕様変換手順からの全参加者の状態遷移列の集合の生成規則および前記安全性入力手順からの安全性を表わす論理式が入力され全参加者の状態遷移列の集合の生成規則から生成される全参加者の状態遷移列の集合について安全性を表わす論理式の真偽を判定する検証手順をコンピュータに実行させる。
【０１０７】
【発明の効果】
以上説明したように、本発明によれば、通信プロトコルの仕様およびそのプロトコルを用いて行われる通信に期待される安全性を入力し、プロトコルに従った通信が期待される性質を満すか否かを判定する安全性検証装置を構成することができる。またその際に、通信の参加者の状態をプロセスおよび環境を用いて表現することにより、安全性をこれらを用いて従来法よりも簡潔に記述することが可能になる。
【図面の簡単な説明】
【図１】本発明の一実施形態例に係る通信プロトコルの安全性検証装置を示す構成説明図である。
【符号の説明】
１１  通信プロトコル仕様入力部
１２  通信プロトコル仕様変換部
１３  安全性入力部
１４  検証部
１５  出力部
【図１】
0003764392.tif 000027