(57)【要約】【課題】合成可能な理想機能実現装置を提供する。【解決手段】理想機能実現装置Ｆ１０であって、ｓｕｐ（ｈ，ｘ）とＡを入力としｌｅａｋ（Ａ，ｓｕｐ（ｈ，ｘ））を出力するｌｅａｋメッセージ作成部１１と、ｈとｘを入力としｓｕｐ（ｈ，ｘ）を出力するｓｕｐｐｒｅｓｓ関数計算部１２と、ｉｎｐｕｔ（Ａ，ｘ）が入力された場合にｈとＡとｘを出力し、攻撃者からｉｎｆ（Ｂ，ｚ）が入力された場合にｈとＢを出力し、ｉｎｔ＿ｃｏｍｐ（ｈ）が入力された場合にｈを出力するヒストリー記録部１３と、ｈを入力としｉｎｔ＿ｃｏｍｐ（ｈ）を出力するｉｎｔ＿ｃｏｍｐ関数計算部１４と、ｈを入力としｃｋ（ｈ）を出力するｃｋ（ｈ）判定部１５と、ｃｋ（ｈ）とｈを入力としｏｕｔ＿ｃｏｍｐ（ｈ）を出力するｏｕｔ＿ｃｏｍｐ関数計算部１６と、ｏｕｔ＿ｃｏｍｐ（ｈ）とＢを入力としｏｕｔｐｕｔ（Ｂ，ｗ）を出力するｏｕｔｐｕｔメッセージ作成部１７を備える。【選択図】図１
2012078456.tif 000002
【特許請求の範囲】
【請求項１】
ｌｅａｋメッセージ作成部と、ｓｕｐｐｒｅｓｓ関数計算部と、ヒストリー記録部と、ｉｎｔ＿ｃｏｍｐ関数計算部と、ｃｋ（ｈ）判定部と、ｏｕｔ＿ｃｏｍｐ関数計算部と、ｏｕｔｐｕｔメッセージ作成部とを備える理想機能実現装置であって、
ｉｎｐｕｔメッセージは、二つの引数を持ち、理想機能実現装置への入力の際に作成されるメッセージであるものとし、
ｉｎｆメッセージは、二つの引数を持ち、攻撃者から理想機能実現装置への入力の際に作成されるメッセージであるものとし、
ｌｅａｋメッセージは、二つの引数を持ち、理想機能実現装置から攻撃者への出力の際に作成されるメッセージであるものとし、
ｏｕｔｐｕｔメッセージは、二つの引数を持ち、理想機能実現装置からの出力の際に作成されるメッセージであるものとし、
ｓｕｐｐｒｅｓｓ関数は、二つの引数を持ち、一方の引数に依存して他方の引数の一部または全部を隠蔽することを特徴とする多項式時間関数であるものとし、
ｉｎｔ＿ｃｏｍｐ関数は、一つの引数を持ち、理想機能実現装置の種類によって入出力が異なる確率的多項式時間関数であるものとし、
ｃｋ関数は、一つの引数を持ち、入力された引数の値に応じてｔｒｕｅもしくはｆａｌｓｅのいずれかの計算結果を出力する関数であって、予め定められた多項式時間述語であるものとし、
ｏｕｔ＿ｃｏｍｐ関数は、一つの引数を持ち、理想機能実現装置の種類によって入出力が異なる確率的多項式時間関数であるものとし、
ｉｎｐｕｔメッセージをｉｎｐｕｔ（引数，引数）と、ｉｎｆメッセージをｉｎｆ（引数，引数）と、ｌｅａｋメッセージをｌｅａｋ（引数，引数）と、ｏｕｔｐｕｔメッセージをｏｕｔｐｕｔ（引数，引数）と、ｓｕｐｐｒｅｓｓ関数をｓｕｐ（引数，引数）と、ｉｎｔ＿ｃｏｍｐ関数をｉｎｔ＿ｃｏｍｐ（引数）と、ｃｋ関数をｃｋ（引数）と、ｏｕｔ＿ｃｏｍｐ関数をｏｕｔ＿ｃｏｍｐ（引数）とそれぞれ表すものとし、
Ａ，Ｂ，ｘ，ｚ，ｗ，ｈ，Ｐ，Ｑ，Ｒ，Ｓを任意の記号列とし、
前記理想機能実現装置にｉｎｐｕｔ（Ａ，ｘ）が入力された場合に、
前記ヒストリー記録部は、前記ｉｎｐｕｔ（Ａ，ｘ）を入力とし、前記ｈが空であれば、当該空であるｈをｈ＝ｉｎｐｕｔ（Ａ，ｘ）に更新し、前記ｈが空でなく、ｈ＝Ｐであれば、当該空でないｈをｈ＝Ｐ．ｉｎｐｕｔ（Ａ，ｘ）に更新して、当該更新されたｈと、前記Ａと、前記ｘとを出力し、
前記ｓｕｐｐｒｅｓｓ関数計算部は、ｈ＝ｉｎｐｕｔ（Ａ，ｘ）、もしくはｈ＝Ｐ．ｉｎｐｕｔ（Ａ，ｘ）に更新されたｈと、前記ｘとを入力とし、ｓｕｐ（ｈ，ｘ）を計算して、当該ｓｕｐ（ｈ，ｘ）を出力し、
前記ｌｅａｋメッセージ作成部は、前記ｓｕｐ（ｈ，ｘ）と前記Ａとを入力とし、ｌｅａｋ（Ａ，ｓｕｐ（ｈ，ｘ））を作成して、当該ｌｅａｋ（Ａ，ｓｕｐ（ｈ，ｘ））を任意の攻撃者に出力し、
任意の攻撃者から前記理想機能実現装置にｉｎｆ（Ｂ，ｚ）が入力された場合に、
前記ヒストリー記録部は、前記ｉｎｆ（Ｂ，ｚ）を入力とし、前記ｈが空であれば、当該空であるｈをｈ＝ｉｎｆ（Ｂ，ｚ）に更新し、前記ｈが空でなく、ｈ＝Ｑであれば、当該空でないｈをｈ＝Ｑ．ｉｎｆ（Ｂ，ｚ）に更新して、当該更新されたｈと、前記Ｂとを出力し、
前記ｉｎｔ＿ｃｏｍｐ関数計算部は、ｈ＝ｉｎｆ（Ｂ，ｚ）、もしくはｈ＝Ｑ．ｉｎｆ（Ｂ，ｚ）に更新されたｈを入力とし、ｉｎｔ＿ｃｏｍｐ（ｈ）を計算して、当該ｉｎｔ＿ｃｏｍｐ（ｈ）を出力し、
前記ヒストリー記録部は、前記ｉｎｔ＿ｃｏｍｐ（ｈ）を入力とし、前記ｈがｈ＝Ｒであれば、当該ｈをｈ＝Ｒ．ｉｎｔ＿ｃｏｍｐ（ｈ）に更新して、当該更新されたｈを出力し、
前記ｃｋ（ｈ）判定部は、ｈ＝Ｒ．ｉｎｔ＿ｃｏｍｐ（ｈ）に更新されたｈを入力とし、ｃｋ（ｈ）を計算し、当該計算結果であるｃｋ（ｈ）＝ｔｒｕｅもしくはｃｋ（ｈ）＝ｆａｌｓｅのいずれかを出力し、
前記ｏｕｔ＿ｃｏｍｐ関数計算部は、前記ｃｋ（ｈ）判定部により出力されたｃｋ（ｈ）と、前記ヒストリー記録部によりｈ＝Ｒ．ｉｎｔ＿ｃｏｍｐ（ｈ）に更新されたｈとを入力とし、ｃｋ（ｈ）＝ｔｒｕｅである場合に、ｏｕｔ＿ｃｏｍｐ（ｈ）を計算し、当該ｏｕｔ＿ｃｏｍｐ（ｈ）を出力し、
前記ｏｕｔｐｕｔメッセージ作成部は、前記ｏｕｔ＿ｃｏｍｐ（ｈ）と、前記Ｂとを入力とし、前記ｗにｗ＝ｏｕｔ＿ｃｏｍｐ（ｈ）を代入して、ｏｕｔｐｕｔ（Ｂ，ｗ）を作成し、当該ｏｕｔｐｕｔ（Ｂ，ｗ）を出力し、
前記ヒストリー記録部は、前記ｏｕｔｐｕｔ（Ｂ，ｗ）を入力とし、前記ｈがｈ＝Ｓであれば、当該ｈをｈ＝Ｓ．ｏｕｔｐｕｔ（Ｂ，ｗ）に更新すること
を特徴とする理想機能実現装置。
【請求項２】
請求項１に記載の理想機能実現装置であって、
ｃｏｍｍｉｔ，ｓｉｄ．ｘを任意の記号列とし、
前記ＡがＡ＝ｃｏｍｍｉｔ，前記ｘがｘ＝ｓｉｄ．ｘであるものとし、
前記ｓｕｐｐｒｅｓｓ関数計算部のｓｕｐ（ｈ，ｓｉｄ．ｘ）の計算結果がｓｕｐ（ｈ，ｓｉｄ．ｘ）＝ｓｉｄとなること
を特徴とする理想機能ｃｏｍｍｉｔｍｅｎｔのｈｉｄｉｎｇに相当する理想機能実現装置。
【請求項３】
請求項１に記載の理想機能実現装置であって、
ｃｏｍｍｉｔ，ｏｐｅｎ，ａｃｃｅｐｔ，ｏｕｔ，ｓｉｄ．ｘを任意の記号列とし、
前記ＡがＡ＝ｃｏｍｍｉｔ，ｏｐｅｎのいずれかであり、前記ＢがＢ＝ａｃｃｅｐｔ，ｏｕｔのいずれかであり、前記ｚがｚ＝ｓｉｄ．ｘであるものとし、
前記ｓｕｐｐｒｅｓｓ関数計算部のｓｕｐ（ｈ，ｘ）の計算結果がｓｕｐ（ｈ，ｘ）＝ｘとなり、
前記ｉｎｔ＿ｃｏｍｐ関数計算部のｉｎｔ＿ｃｏｍｐ（ｈ）の計算結果がｉｎｔ＿ｃｏｍｐ（ｈ）＝ｓｉｄとなり、
前記ｃｋ（ｈ）判定部のｃｋ（ｈ）の計算結果が、ｈの末尾がｉｎｆ（ａｃｃｅｐｔ，ｓｉｄ．ｘ）．ｓｉｄであって、ｈの一部にｉｎｐｕｔ（ｃｏｍｍｉｔ，ｓｉｄ．ｘ）がある場合にはｃｋ（ｈ）＝ｔｒｕｅとなり、
ｈの末尾がｉｎｆ（ｏｕｔ，ｓｉｄ．ｘ）．ｓｉｄであって、ｈの一部にｉｎｐｕｔ（ｃｏｍｍｉｔ，ｓｉｄ．ｘ）があり、その後にｉｎｐｕｔ（ｏｐｅｎ，ｓｉｄ．ｘ）がある場合にはｃｋ（ｈ）＝ｔｒｕｅとなり、
前記ｏｕｔ＿ｃｏｍｐ関数計算部のｏｕｔ＿ｃｏｍｐ（ｈ）の計算結果が、ｈの末尾がｉｎｆ（ａｃｃｅｐｔ，ｓｉｄ．ｘ）．ｓｉｄである場合にはｏｕｔ＿ｃｏｍｐ（ｈ）＝ｓｉｄとなり、
ｈの末尾がｉｎｆ（ｏｕｔ，ｓｉｄ．ｘ）．ｓｉｄである場合にはｏｕｔ＿ｃｏｍｐ（ｈ）＝ｓｉｄ．ｘとなること
を特徴とする理想機能ｃｏｍｍｉｔｍｅｎｔのｃｏｍｐｌｅｔｅｎｅｓｓかつｓｏｕｎｄｎｅｓｓに相当する理想機能実現装置。
【請求項４】
請求項２、３の理想機能実現装置を合成することを特徴とする理想機能ｃｏｍｍｉｔｍｅｎｔに相当する理想機能実現装置。
【請求項５】
請求項１に記載の理想機能実現装置であって、
ｓｅｎｄｅｒ＿ｉｎｐｕｔ，ｓｉｄ．ｘを任意の記号列とし、
前記ＡがＡ＝ｓｅｎｄｅｒ＿ｉｎｐｕｔ，前記ｘがｘ＝ｓｉｄ．ｘであるものとし、
前記ｓｕｐｐｒｅｓｓ関数計算部のｓｕｐ（ｈ，ｓｉｄ．ｘ）の計算結果がｓｕｐ（ｈ，ｓｉｄ．ｘ）＝ｓｉｄとなること
を特徴とする理想機能ｏｂｌｉｖｉｏｕｓ ｔｒａｎｓｆｅｒのｓｅｎｄｅｒ ｈｉｄｉｎｇに相当する理想機能実現装置。
【請求項６】
請求項１に記載の理想機能実現装置であって、
ｒｅｃｅｉｖｅｒ＿ｉｎｐｕｔ，ｓｉｄ．ｘを任意の記号列とし、
前記ＡがＡ＝ｒｅｃｅｉｖｅｒ＿ｉｎｐｕｔ，前記ｘがｘ＝ｓｉｄ．ｘであるものとし、
前記ｓｕｐｐｒｅｓｓ関数計算部のｓｕｐ（ｈ，ｓｉｄ．ｘ）の計算結果がｓｕｐ（ｈ，ｓｉｄ．ｘ）＝ｓｉｄとなること
を特徴とする理想機能ｏｂｌｉｖｉｏｕｓ ｔｒａｎｓｆｅｒのｒｅｃｅｉｖｅｒ ｈｉｄｉｎｇに相当する理想機能実現装置。
【請求項７】
請求項１に記載の理想機能実現装置であって、
ｓｅｎｄｅｒ＿ｉｎｐｕｔ，ｒｅｃｅｉｖｅｒ＿ｉｎｐｕｔ，ｏｕｔ，ｓｉｄを任意の記号列とし、
前記ＡがＡ＝ｓｅｎｄｅｒ＿ｉｎｐｕｔ，ｒｅｃｅｉｖｅｒ＿ｉｎｐｕｔのいずれかであり、前記ＢがＢ＝ｏｕｔであり、前記ｚがｚ＝ｓｉｄであるものとし、
前記ｓｕｐｐｒｅｓｓ関数計算部のｓｕｐ（ｈ，ｘ）の計算結果がｓｕｐ（ｈ，ｘ）＝ｘとなり、
前記ｉｎｔ＿ｃｏｍｐ関数計算部のｉｎｔ＿ｃｏｍｐ（ｈ）の計算結果がｉｎｔ＿ｃｏｍｐ（ｈ）＝ｓｉｄとなり、
前記ｃｋ（ｈ）判定部のｃｋ（ｈ）の計算結果が、ｈの末尾がｉｎｆ（ｏｕｔ，ｓｉｄ）．ｓｉｄであって、ｈの一部にｉｎｐｕｔ（ｓｅｎｄｅｒ＿ｉｎｐｕｔ，ｓｉｄ．（ｘ１，ｘ２））およびｉｎｐｕｔ（ｒｅｃｅｉｖｅｒ＿ｉｎｐｕｔ，ｓｉｄ．ｉ）がある場合にはｃｋ（ｈ）＝ｔｒｕｅとなり、
前記ｏｕｔ＿ｃｏｍｐ関数計算部のｏｕｔ＿ｃｏｍｐ（ｈ）の計算結果が、ｈの末尾がｉｎｆ（ｏｕｔ，ｓｉｄ）．ｓｉｄであって、ｈの一部にｉｎｐｕｔ（ｓｅｎｄｅｒ＿ｉｎｐｕｔ，ｓｉｄ．（ｘ１，ｘ２））およびｉｎｐｕｔ（ｒｅｃｅｉｖｅｒ＿ｉｎｐｕｔ，ｓｉｄ．ｉ）がある場合にはｏｕｔ＿ｃｏｍｐ（ｈ）＝ｘｉとなること
を特徴とする理想機能ｏｂｌｉｖｉｏｕｓ ｔｒａｎｓｆｅｒのｃｏｍｐｌｅｔｅｎｅｓｓに相当する理想機能実現装置。
【請求項８】
請求項５、６、７の理想機能実現装置を合成することを特徴とする理想機能ｏｂｌｉｖｉｏｕｓ ｔｒａｎｓｆｅｒに相当する理想機能実現装置。
【請求項９】
ｌｅａｋメッセージ作成部と、ｓｕｐｐｒｅｓｓ関数計算部と、ヒストリー記録部と、ｉｎｔ＿ｃｏｍｐ関数計算部と、ｃｋ（ｈ）判定部と、ｏｕｔ＿ｃｏｍｐ関数計算部と、ｏｕｔｐｕｔメッセージ作成部とを備える理想機能実現装置を制御する理想機能実現方法であって、
ｉｎｐｕｔメッセージは、二つの引数を持ち、理想機能実現装置への入力の際に計算される関数であるものとし、
ｉｎｆメッセージは、二つの引数を持ち、攻撃者から理想機能実現装置への入力の際に計算される関数であるものとし、
ｌｅａｋメッセージは、二つの引数を持ち、理想機能実現装置から攻撃者への出力の際に計算される関数であるものとし、
ｏｕｔｐｕｔメッセージは、二つの引数を持ち、理想機能実現装置からの出力の際に計算される関数であるものとし、
ｓｕｐｐｒｅｓｓ関数は、二つの引数を持ち、一方の引数に依存して他方の引数の一部または全部を隠蔽することを特徴とする多項式時間関数であるものとし、
ｉｎｔ＿ｃｏｍｐ関数は、一つの引数を持ち、理想機能実現装置の種類によって入出力が異なる確率的多項式時間関数であるものとし、
ｃｋ関数は、一つの引数を持ち、入力された引数の値に応じてｔｒｕｅもしくはｆａｌｓｅのいずれかの計算結果を出力する関数であって、予め定められた多項式時間述語であるものとし、
ｏｕｔ＿ｃｏｍｐ関数は、一つの引数を持ち、理想機能実現装置の種類によって入出力が異なる確率的多項式時間関数であるものとし、
ｉｎｐｕｔメッセージをｉｎｐｕｔ（引数，引数）と、ｉｎｆメッセージをｉｎｆ（引数，引数）と、ｌｅａｋメッセージをｌｅａｋ（引数，引数）と、ｏｕｔｐｕｔメッセージをｏｕｔｐｕｔ（引数，引数）と、ｓｕｐｐｒｅｓｓ関数をｓｕｐ（引数，引数）と、ｉｎｔ＿ｃｏｍｐ関数をｉｎｔ＿ｃｏｍｐ（引数）と、ｃｋ関数をｃｋ（引数）と、ｏｕｔ＿ｃｏｍｐ関数をｏｕｔ＿ｃｏｍｐ（引数）とそれぞれ表すものとし、
Ａ，Ｂ，ｘ，ｚ，ｗ，ｈ，Ｐ，Ｑ，Ｒ，Ｓを任意の記号列とし、
前記理想機能実現装置にｉｎｐｕｔ（Ａ，ｘ）が入力された場合に、
前記ヒストリー記録部が、前記ｉｎｐｕｔ（Ａ，ｘ）を入力とし、前記ｈが空であれば、当該空であるｈをｈ＝ｉｎｐｕｔ（Ａ，ｘ）に更新し、前記ｈが空でなく、ｈ＝Ｐであれば、当該空でないｈをｈ＝Ｐ．ｉｎｐｕｔ（Ａ，ｘ）に更新して、当該更新されたｈと、前記Ａと、前記ｘとを出力し、
前記ｓｕｐｐｒｅｓｓ関数計算部が、ｈ＝ｉｎｐｕｔ（Ａ，ｘ）、もしくはｈ＝Ｐ．ｉｎｐｕｔ（Ａ，ｘ）に更新されたｈと、前記ｘとを入力とし、ｓｕｐ（ｈ，ｘ）を計算して、当該ｓｕｐ（ｈ，ｘ）を出力し、
前記ｌｅａｋメッセージ作成部が、前記ｓｕｐ（ｈ，ｘ）と前記Ａとを入力とし、ｌｅａｋ（Ａ，ｓｕｐ（ｈ，ｘ））を作成して、当該ｌｅａｋ（Ａ，ｓｕｐ（ｈ，ｘ））を任意の攻撃者に出力し、
任意の攻撃者から前記理想機能実現装置にｉｎｆ（Ｂ，ｚ）が入力された場合に、
前記ヒストリー記録部が、前記ｉｎｆ（Ｂ，ｚ）を入力とし、前記ｈが空であれば、当該空であるｈをｈ＝ｉｎｆ（Ｂ，ｚ）に更新し、前記ｈが空でなく、ｈ＝Ｑであれば、当該空でないｈをｈ＝Ｑ．ｉｎｆ（Ｂ，ｚ）に更新して、当該更新されたｈと、前記Ｂとを出力し、
前記ｉｎｔ＿ｃｏｍｐ関数計算部が、ｈ＝ｉｎｆ（Ｂ，ｚ）、もしくはｈ＝Ｑ．ｉｎｆ（Ｂ，ｚ）に更新されたｈを入力とし、ｉｎｔ＿ｃｏｍｐ（ｈ）を計算して、当該ｉｎｔ＿ｃｏｍｐ（ｈ）を出力し、
前記ヒストリー記録部が、前記ｉｎｔ＿ｃｏｍｐ（ｈ）を入力とし、前記ｈがｈ＝Ｒであれば、当該ｈをｈ＝Ｒ．ｉｎｔ＿ｃｏｍｐ（ｈ）に更新して、当該更新されたｈを出力し、
前記ｃｋ（ｈ）判定部が、ｈ＝Ｒ．ｉｎｔ＿ｃｏｍｐ（ｈ）に更新されたｈを入力とし、ｃｋ（ｈ）を計算し、当該計算結果であるｃｋ（ｈ）＝ｔｒｕｅもしくはｃｋ（ｈ）＝ｆａｌｓｅのいずれかを出力し、
前記ｏｕｔ＿ｃｏｍｐ関数計算部が、前記ｃｋ（ｈ）判定部により出力されたｃｋ（ｈ）と、前記ヒストリー記録部によりｈ＝Ｒ．ｉｎｔ＿ｃｏｍｐ（ｈ）に更新されたｈとを入力とし、ｃｋ（ｈ）＝ｔｒｕｅである場合に、ｏｕｔ＿ｃｏｍｐ（ｈ）を計算し、当該ｏｕｔ＿ｃｏｍｐ（ｈ）を出力し、
前記ｏｕｔｐｕｔメッセージ作成部が、前記ｏｕｔ＿ｃｏｍｐ（ｈ）と、前記Ｂとを入力とし、前記ｗにｗ＝ｏｕｔ＿ｃｏｍｐ（ｈ）を代入して、ｏｕｔｐｕｔ（Ｂ，ｗ）を作成し、当該ｏｕｔｐｕｔ（Ｂ，ｗ）を出力し、
前記ヒストリー記録部が、前記ｏｕｔｐｕｔ（Ｂ，ｗ）を入力とし、前記ｈがｈ＝Ｓであれば、当該ｈをｈ＝Ｓ．ｏｕｔｐｕｔ（Ｂ，ｗ）に更新すること
を特徴とする理想機能実現方法。
【請求項１０】
コンピュータを請求項１から８のいずれかに記載の理想機能実現装置として機能させるためのプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は合成可能な理想機能実現装置、方法、プログラムに関する。
【背景技術】
【０００２】
従来のセキュリティ要求仕様の主な記述方法では、プロトコルの実行にあるアクセスを持つ攻撃者と、その攻撃者に対してプロトコルの安全性が破られないことを証明するチャレンジャーとの間でのゲームという形で表現されていた。そして、攻撃者がそのゲームに勝つ確率がごくわずかである場合に、そのプロトコルは安全であるとしていた。これに対して、安全なプロトコルの理想的な振る舞いを理想機能として表現して、プロトコルのセキュリティ要求仕様を記述する方法がある。そこでは、攻撃者がプロトコルにアクセスして導く振る舞いと、理想的に安全な機能にアクセスして導く振る舞いに変わりがない場合に、そのプロトコルは安全であるとしている。理想機能による安全性の定義は、ゲームに基づく安全性よりも強い安全性が定義でき、特にインターネットのような攻撃者がさまざまな攻撃手法を利用できる状況で、その安全性定義の重要性が増している。
【発明の概要】
【発明が解決しようとする課題】
【０００３】
ゲーム形式による安全性の記述は、プロトコル設計者の念頭にあるセキュリティ要件を表現しやすく、いくつかの要求仕様の連言も、そのゲームを並べて書くだけで表現される。しかし、あるセキュリティ要求使用を満たすプロトコルをサブルーチンとして利用するプロトコルがあるセキュリティ要求仕様を満たすことを証明する場合、ゲーム形式ではｒｅｄｕｃｔｉｏｎとよばれる複雑な議論が必要で、その安全性証明が難しいという課題がある。一方、理想機能による安全性の証明では、そのような場合、サブルーチンを理想機能で置き換えるだけでよく、安全性証明が簡単になる。したがって、サブルーチンを組み合わせて達成されるような複雑なセキュリティ要求仕様では、理想機能での表現が重要である。しかし、複雑な複合的セキュリティ要求仕様を正しく理想機能で表現することは非常に難しいという課題があった。本発明では、この複合的な理想機能をより簡単に生成することができる理想機能実現装置が提供される。
【課題を解決するための手段】
【０００４】
本発明の理想機能実現装置は、ｌｅａｋメッセージ作成部と、ｓｕｐｐｒｅｓｓ関数計算部と、ヒストリー記録部と、ｉｎｔ＿ｃｏｍｐ関数計算部と、ｃｋ（ｈ）判定部と、ｏｕｔ＿ｃｏｍｐ関数計算部と、ｏｕｔｐｕｔメッセージ作成部とを備える。
【０００５】
理想機能実現装置にｉｎｐｕｔ（Ａ，ｘ）が入力された場合に、ヒストリー記録部は、ｉｎｐｕｔ（Ａ，ｘ）を入力とし、ｈが空であれば、当該空であるｈをｈ＝ｉｎｐｕｔ（Ａ，ｘ）に更新し、ｈが空でなく、ｈ＝Ｐであれば、当該空でないｈをｈ＝Ｐ．ｉｎｐｕｔ（Ａ，ｘ）に更新して、当該更新されたｈと、Ａと、ｘとを出力する。ｓｕｐｐｒｅｓｓ関数計算部は、ｈ＝ｉｎｐｕｔ（Ａ，ｘ）、もしくはｈ＝Ｐ．ｉｎｐｕｔ（Ａ，ｘ）に更新されたｈと、ｘとを入力とし、ｓｕｐ（ｈ，ｘ）を計算して、当該ｓｕｐ（ｈ，ｘ）を出力する。ｌｅａｋメッセージ作成部は、ｓｕｐ（ｈ，ｘ）とＡとを入力とし、ｌｅａｋ（Ａ，ｓｕｐ（ｈ，ｘ））を作成して、当該ｌｅａｋ（Ａ，ｓｕｐ（ｈ，ｘ））を任意の攻撃者に出力する。
【０００６】
任意の攻撃者から理想機能実現装置にｉｎｆ（Ｂ，ｚ）が入力された場合に、ヒストリー記録部は、ｉｎｆ（Ｂ，ｚ）を入力とし、ｈが空であれば、当該空であるｈをｈ＝ｉｎｆ（Ｂ，ｚ）に更新し、ｈが空でなく、ｈ＝Ｑであれば、当該空でないｈをｈ＝Ｑ．ｉｎｆ（Ｂ，ｚ）に更新して、当該更新されたｈと、Ｂとを出力する。ｉｎｔ＿ｃｏｍｐ関数計算部は、ｈ＝ｉｎｆ（Ｂ，ｚ）、もしくはｈ＝Ｑ．ｉｎｆ（Ｂ，ｚ）に更新されたｈを入力とし、ｉｎｔ＿ｃｏｍｐ（ｈ）を計算して、当該ｉｎｔ＿ｃｏｍｐ（ｈ）を出力する。ヒストリー記録部は、ｉｎｔ＿ｃｏｍｐ（ｈ）を入力とし、ｈがｈ＝Ｒであれば、当該ｈをｈ＝Ｒ．ｉｎｔ＿ｃｏｍｐ（ｈ）に更新して、当該更新されたｈを出力する。ｃｋ（ｈ）判定部は、ｈ＝Ｒ．ｉｎｔ＿ｃｏｍｐ（ｈ）に更新されたｈを入力とし、ｃｋ（ｈ）を計算し、当該計算結果であるｃｋ（ｈ）＝ｔｒｕｅもしくはｃｋ（ｈ）＝ｆａｌｓｅのいずれかを出力する。ｏｕｔ＿ｃｏｍｐ関数計算部は、ｃｋ（ｈ）判定部により出力されたｃｋ（ｈ）と、ヒストリー記録部によりｈ＝Ｒ．ｉｎｔ＿ｃｏｍｐ（ｈ）に更新されたｈとを入力とし、ｃｋ（ｈ）＝ｔｒｕｅである場合に、ｏｕｔ＿ｃｏｍｐ（ｈ）を計算し、当該ｏｕｔ＿ｃｏｍｐ（ｈ）を出力する。ｏｕｔｐｕｔメッセージ作成部は、ｏｕｔ＿ｃｏｍｐ（ｈ）と、Ｂとを入力とし、ｗにｗ＝ｏｕｔ＿ｃｏｍｐ（ｈ）を代入して、ｏｕｔｐｕｔ（Ｂ，ｗ）を作成し、当該ｏｕｔｐｕｔ（Ｂ，ｗ）を出力する。ヒストリー記録部は、ｏｕｔｐｕｔ（Ｂ，ｗ）を入力とし、ｈがｈ＝Ｓであれば、当該ｈをｈ＝Ｓ．ｏｕｔｐｕｔ（Ｂ，ｗ）に更新する。
【発明の効果】
【０００７】
本発明の理想機能実現装置が上記の構成を備えることにより、理想機能実現装置同士が互いに合成可能となる。このことはすなわち理想機能が互いに合成可能であることを意味する。このため、ゲーム形式のセキュリティ要求仕様表現の利点である要求の連言の記述が理想機能においても可能となる。従って、いくつかの基本的なセキュリティ要求仕様に対応する理想機能から、それら要求仕様を組み合わせた複雑な要求仕様に対応する理想機能を簡単に生成することができる。これにより、設計が難しかった理想機能の設計が簡単になり、あるセキュリティ要求仕様にもとづくプロトコルの安全性証明も、より容易になる。
【図面の簡単な説明】
【０００８】
【図１】実施例１の理想機能実現装置Ｆの構成を示すブロック図。
【図２】実施例１の理想機能実現装置Ｆの動作を示すフローチャート。
【図３】実施例１の理想機能実現装置Ｆのｓｕｐ（ｈ，ｘ）の計算例を示す図。
【図４】実施例１の理想機能実現装置Ｆのヒストリー記録部が備えるｈを示す図。
【図５】変形例１の理想機能実現装置Ｆ１の構成を示すブロック図。
【図６】変形例１の理想機能実現装置Ｆ１の動作を示すフローチャート。
【図７】変形例１の理想機能実現装置Ｆ２の構成を示すブロック図。
【図８】変形例１の理想機能実現装置Ｆ２の構成を示すブロック図。
【図９】変形例１の理想機能実現装置Ｆ２の動作を示すフローチャート。
【図１０】変形例２の理想機能実現装置Ｆ３の構成を示すブロック図。
【図１１】変形例２の理想機能実現装置Ｆ３の動作を示すフローチャート。
【図１２】変形例２の理想機能実現装置Ｆ４の構成を示すブロック図。
【図１３】変形例２の理想機能実現装置Ｆ４の動作を示すフローチャート。
【図１４】変形例２の理想機能実現装置Ｆ５の構成を示すブロック図。
【図１５】変形例２の理想機能実現装置Ｆ５の構成を示すブロック図。
【図１６】変形例２の理想機能実現装置Ｆ５の動作を示すフローチャート。
【発明を実施するための形態】
【０００９】
以下、本発明の実施の形態について、詳細に説明する。なお、同じ機能を有する構成部には同じ番号を付す。
【実施例１】
【００１０】
まず、本発明の理想機能実現装置で用いられるメッセージ、および関数について説明する。なお、下記のメッセージ、および関数の理想機能実現装置内での具体的な動作については後述するものとする。本発明の理想機能実現装置では、ｉｎｐｕｔメッセージ、ｉｎｆメッセージ、ｌｅａｋメッセージ、ｏｕｔｐｕｔメッセージ、ｓｕｐｐｒｅｓｓ関数、ｉｎｔ＿ｃｏｍｐ関数、ｃｋ関数、ｏｕｔ＿ｃｏｍｐ関数が用いられる。ｉｎｐｕｔメッセージは、二つの引数を持ち、理想機能実現装置への入力の際に作成されるメッセージである。ｉｎｆメッセージは、二つの引数を持ち、攻撃者から理想機能実現装置への入力の際に作成されるメッセージである。ｉｎｐｕｔ、ｉｎｆメッセージは、理想機能実現装置への２種類の入力（ｉｎｐｕｔ，ｉｎｆ）を区別するためのラベルを意味する。ｌｅａｋメッセージは、二つの引数を持ち、理想機能実現装置から攻撃者への出力の際に作成されるメッセージである。ｏｕｔｐｕｔメッセージは、二つの引数を持ち、理想機能実現装置からの出力の際に作成されるメッセージである。ｌｅａｋ、ｏｕｔｐｕｔメッセージは、理想機能実現装置からの２種類の出力（ｌｅａｋ，ｏｕｔｐｕｔ）を区別するためのラベルを意味する。
【００１１】
ｓｕｐｐｒｅｓｓ関数は、二つの引数を持ち、一方の引数に依存して他方の引数の一部または全部を隠蔽することを特徴とする多項式時間関数である。多項式時間関数とは、ある多項式ｆ（ｘ）があって、入力データの長さをｎとしたとき、ｆ（ｎ）ステップ内で、答えを出力するアルゴリズムである。ｉｎｔ＿ｃｏｍｐ関数は、一つの引数を持ち、理想機能実現装置の種類によって入出力が異なる確率的多項式時間関数である。確率的多項式時間関数とは、ある多項式ｆ（ｘ）があって、入力データの長さをｎとしたとき、ｆ（ｎ）ステップ内で、答えを出力するアルゴリズムであり、計算途中で乱数を発生させることで、その結果が確率的に決まるという性質をもつ。ｃｋ関数（以下、ｃｈｅｃｋ述語とも書く）は、一つの引数を持ち、入力された引数の値に応じてｔｒｕｅもしくはｆａｌｓｅのいずれかの計算結果を出力する関数であって、予め定められた多項式時間述語である。多項式時間述語とは、ある多項式ｆ（ｘ）があって、入力データの長さをｎとしたとき、ｆ（ｎ）ステップ内で真偽を判定するアルゴリズムである。ｏｕｔ＿ｃｏｍｐ関数は、一つの引数を持ち、理想機能実現装置の種類によって入出力が異なる確率的多項式時間関数である。  また、ｉｎｐｕｔメッセージをｉｎｐｕｔ（引数，引数）と、ｉｎｆメッセージをｉｎｆ（引数，引数）と、ｌｅａｋメッセージをｌｅａｋ（引数，引数）と、ｏｕｔｐｕｔメッセージをｏｕｔｐｕｔ（引数，引数）と、ｓｕｐｐｒｅｓｓ関数をｓｕｐ（引数，引数）と、ｉｎｔ＿ｃｏｍｐ関数をｉｎｔ＿ｃｏｍｐ（引数）と、ｃｋ関数をｃｋ（引数）と、ｏｕｔ＿ｃｏｍｐ関数をｏｕｔ＿ｃｏｍｐ（引数）とそれぞれ表すものとする。また、本発明の実施例１にかかる理想機能実現装置Ｆ（１０）では任意の記号列Ａ，Ｂ，ｘ，ｚ，ｗ，ｈ，Ｐ，Ｑ，Ｒ，Ｓが用いられるものとする。
【００１２】
図１、２を参照して、本発明の理想機能実現装置Ｆ（１０）の動作について詳細に説明する。図１は理想機能実現装置Ｆ（１０）の構成を示すブロック図である。図２は理想機能実現装置Ｆ（１０）の動作を示すフローチャートである。本発明の理想機能実現装置Ｆ（１０）は、ｌｅａｋメッセージ作成部１１と、ｓｕｐｐｒｅｓｓ関数計算部１２と、ヒストリー記録部１３と、ｉｎｔ＿ｃｏｍｐ関数計算部１４と、ｃｋ（ｈ）判定部１５と、ｏｕｔ＿ｃｏｍｐ関数計算部１６と、ｏｕｔｐｕｔメッセージ作成部１７とを備える。また理想機能実現装置Ｆ（１０）への入出力の種別を表すａｃｔｉｏｎ ｎａｍｅと呼ばれるシンボルが有限個与えられている。入力させるａｃｔｉｏｎ ｎａｍｅの集合を集合Ｉ（Ｆ）９２、出力させるａｃｔｉｏｎ ｎａｍｅの集合を集合Ｏ（Ｆ）９３として与えられている。また記号列ｘ（９４）が与えられている。Ａは集合Ｉ（Ｆ）９２の元であり、Ｂは集合Ｏ（Ｆ）９３の元であるものとする。理想機能実現装置Ｆ（１０）にａｃｔｉｏｎ ｎａｍｅＡを入力するとき、ｉｎｐｕｔメッセージである、ｉｎｐｕｔ（Ａ，ｘ）が作成される。ここで、記号列ｘはセッションＩＤと入力値との対とする。
【００１３】
理想機能実現装置Ｆ（１０）にｉｎｐｕｔ（Ａ，ｘ）が入力された場合に、ヒストリー記録部１３は、このｉｎｐｕｔ（Ａ，ｘ）を入力とし（Ｓ１０１）、ｈが空であれば、当該空であるｈをｈ＝ｉｎｐｕｔ（Ａ，ｘ）に更新し、ｈが空でなく、ｈが任意の記号列Ｐであれば、当該空でないｈをｈ＝Ｐ．ｉｎｐｕｔ（Ａ，ｘ）に更新して（Ｓ１０２）、当該更新されたｈと、Ａと、ｘとを出力する。ｓｕｐｐｒｅｓｓ関数計算部１２は、ｈ＝ｉｎｐｕｔ（Ａ，ｘ）、もしくはｈ＝Ｐ．ｉｎｐｕｔ（Ａ，ｘ）に更新されたｈと、ｘとを入力とし、ｓｕｐ（ｈ，ｘ）を計算して（Ｓ１０３）、当該ｓｕｐ（ｈ，ｘ）を出力する。ｌｅａｋメッセージ作成部１１は、ｓｕｐ（ｈ，ｘ）とＡとを入力とし、ｌｅａｋ（Ａ，ｓｕｐ（ｈ，ｘ））を作成して（Ｓ１０４）、当該ｌｅａｋ（Ａ，ｓｕｐ（ｈ，ｘ））を攻撃者９１に出力する（Ｓ１０５）。ここでｌｅａｋメッセージについて説明を補足する。理想機能実現装置Ｆ（１０）になんらかの入力があった場合（本実施例ではｉｎｐｕｔ（Ａ，ｘ））、そのイベントの発生が攻撃者９１に知らされ、一部の情報が漏れることがある。この情報の流れを理想機能実現装置Ｆ（１０）から攻撃者９１への出力として、ｌｅａｋメッセージでラベル付けし、この情報を他の出力（ｏｕｔｐｕｔ）と区別する。本実施例では、理想機能実現装置Ｆ（１０）への入力ｉｎｐｕｔ（Ａ，ｘ）に対して、攻撃者９１にｌｅａｋ（Ａ，ｓｕｐ（ｈ，ｘ））が出力（リーク）される。
【００１４】
攻撃者９１から理想機能実現装置Ｆ（１０）にｉｎｆ（Ｂ，ｚ）が入力された場合に、ヒストリー記録部１３は、ｉｎｆ（Ｂ，ｚ）を入力とし（Ｓ１０６）、ｈが空であれば、当該空であるｈをｈ＝ｉｎｆ（Ｂ，ｚ）に更新し、ｈが空でなく、ｈが任意の記号列Ｑであれば、当該空でないｈをｈ＝Ｑ．ｉｎｆ（Ｂ，ｚ）に更新して（Ｓ１０７）、当該更新されたｈと、Ｂとを出力する。ここで、ｉｎｆ（Ｂ，ｚ）は後述するｏｕｔｐｕｔ（Ｂ，ｗ）の出力を促す攻撃者９１からのメッセージ入力を意味している。ここで、引数ｚは理想機能実現装置Ｆ（１０）に与える影響を表す。ｉｎｔ＿ｃｏｍｐ関数計算部１４は、ｈ＝ｉｎｆ（Ｂ，ｚ）、もしくはｈ＝Ｑ．ｉｎｆ（Ｂ，ｚ）に更新されたｈを入力とし、ｉｎｔ＿ｃｏｍｐ（ｈ）を計算して（Ｓ１０８）、当該ｉｎｔ＿ｃｏｍｐ（ｈ）を出力する。ヒストリー記録部１３は、ｉｎｔ＿ｃｏｍｐ（ｈ）を入力とし、ｈが任意の記号列Ｒであれば、当該ｈをｈ＝Ｒ．ｉｎｔ＿ｃｏｍｐ（ｈ）に更新して（Ｓ１０９）、当該更新されたｈを出力する。ｃｋ（ｈ）判定部１５は、ｈ＝Ｒ．ｉｎｔ＿ｃｏｍｐ（ｈ）に更新されたｈを入力とし、ｃｋ（ｈ）を計算し（Ｓ１１０）、当該計算結果であるｃｋ（ｈ）＝ｔｒｕｅもしくはｃｋ（ｈ）＝ｆａｌｓｅのいずれかを出力する。ｏｕｔ＿ｃｏｍｐ関数計算部１６は、ｃｋ（ｈ）判定部１５により出力されたｃｋ（ｈ）と、ヒストリー記録部１３によりｈ＝Ｒ．ｉｎｔ＿ｃｏｍｐ（ｈ）に更新されたｈとを入力とし、ｃｋ（ｈ）＝ｔｒｕｅである場合に（Ｓ１１１）、ｏｕｔ＿ｃｏｍｐ（ｈ）を計算し（Ｓ１１２）、当該ｏｕｔ＿ｃｏｍｐ（ｈ）を出力する。ｏｕｔｐｕｔメッセージ作成部１７は、ｏｕｔ＿ｃｏｍｐ（ｈ）と、Ｂとを入力とし、ｗにｗ＝ｏｕｔ＿ｃｏｍｐ（ｈ）を代入して、ｏｕｔｐｕｔ（Ｂ，ｗ）を作成し（Ｓ１１３）、当該ｏｕｔｐｕｔ（Ｂ，ｗ）を理想機能実現装置Ｆ（１０）の外部に出力する（Ｓ１１４）。ヒストリー記録部１３は、ｏｕｔｐｕｔ（Ｂ，ｗ）を入力とし、ｈが任意の記号列Ｓであれば、当該ｈをｈ＝Ｓ．ｏｕｔｐｕｔ（Ｂ，ｗ）に更新する（Ｓ１１５）。
【００１５】
次に、図３を参照してｓｕｐｐｒｅｓｓ関数計算部１２の動作についてさらに詳細に説明する。図３は理想機能実現装置Ｆのｓｕｐ（ｈ，ｘ）の計算例を示す図である。ｓｕｐｐｒｅｓｓ関数計算部１２は、入力された二つの引数に対してｓｕｐ（引数，引数）を計算する。前述のとおり、ｓｕｐｐｒｅｓｓ関数は一方の引数に依存して他方の引数の一部または全部を隠蔽することを特徴とする多項式時間関数である。図３の例では引数ｈの状況によって、引数ｘ（記号列）の一部を文字”‐”で置き換えることにより、隠蔽する。例えば引数ｈ＝ｈ１、ｘ＝ｘ１ｘ２ｘ３ｘ４ｘ５ｘ６ｘ７ｘ８であるとき、ｓｕｐ（ｈ，ｘ）の計算結果はｘ１ｘ２ｘ３ｘ４を文字”‐”で置き換えた‐‐‐‐ｘ５ｘ６ｘ７ｘ８となる。従って、記号列ｘの一部であるｘ１ｘ２ｘ３ｘ４は隠蔽され、ｘ５ｘ６ｘ７ｘ８はリークされる。記号列ｘの隠蔽／リーク結果は引数ｈの状況によって異なるので、例えば引数ｈ＝ｈ２であるとき、ｓｕｐ（ｈ，ｘ）＝ｘ１ｘ２ｘ３ｘ４‐‐‐‐となり、引数ｈ＝ｈ３であるとき、ｓｕｐ（ｈ，ｘ）＝ｘ１‐‐‐‐‐‐ｘ８となる。
【００１６】
次に、図４を参照して、ヒストリー記録部１３の動作についてさらに詳細に説明する。図４は理想機能実現装置Ｆのヒストリー記録部が備えるｈを示す図である。ヒストリー記録部１３は入力列の発生を発生順に記録する変数ｈ（ヒストリー）を備えている。前述のとおり、理想機能実現装置Ｆ（１０）にｉｎｐｕｔ（Ａ，ｘ）が入力された場合に、ヒストリー記録部１３は、このｉｎｐｕｔ（Ａ，ｘ）を入力とし（Ｓ１０１）、ｈが空であれば、当該空であるｈをｈ＝ｉｎｐｕｔ（Ａ，ｘ）に更新し、ｈが空でなく、ｈが任意の記号列Ｐであれば、当該空でないｈをｈ＝Ｐ．ｉｎｐｕｔ（Ａ，ｘ）に更新する（Ｓ１０２）。図４の例では、ヒストリー記録部１３にｉｎｐｕｔ（Ａ，ｘ）が入力されたとき、ｈが空であったものとし、この場合ｈがｈ＝ｉｎｐｕｔ（Ａ，ｘ）に更新されることを示している。続いてこの例では、攻撃者９１から理想機能実現装置Ｆ（１０）にｉｎｆ（Ｂ，ｚ）が入力される。この場合、前述の通りヒストリー記録部１３は、ｉｎｆ（Ｂ，ｚ）を入力とし（Ｓ１０６）、ｈが空であれば、当該空であるｈをｈ＝ｉｎｆ（Ｂ，ｚ）に更新し、ｈが空でなく、ｈが任意の記号列Ｑであれば、当該空でないｈをｈ＝Ｑ．ｉｎｆ（Ｂ，ｚ）に更新する（Ｓ１０７）。この例では、ｉｎｆ（Ｂ，ｚ）が入力されたとき、ｈ＝ｉｎｐｕｔ（Ａ，ｘ）であるので、ｈは空でなく、ｉｎｐｕｔ（Ａ，ｘ）は任意の記号列Ｑに該当する。従ってｈはｈ＝ｉｎｐｕｔ（Ａ，ｘ）．ｉｎｆ（Ｂ，ｚ）に更新される。このようにしてステップ１０９ではあらたにｉｎｔ＿ｃｏｍｐ（ｈ）がｈに記録され、ｈ＝ｉｎｐｕｔ（Ａ，ｘ）．ｉｎｆ（Ｂ，ｚ）．ｉｎｔ＿ｃｏｍｐ（ｈ）となり、ステップ１１５ではあらたにｏｕｔｐｕｔ（Ｂ，ｗ）がｈに記録され、ｈ＝ｉｎｐｕｔ（Ａ，ｘ）．ｉｎｆ（Ｂ，ｚ）．ｉｎｔ＿ｃｏｍｐ（ｈ）．ｏｕｔｐｕｔ（Ｂ，ｗ）となる。このようにしてヒストリー記録部１３への入力については時系列順に、直前の入力列の末尾に記号”．”を介して結合されｈに記録されるものとする。
【００１７】
以上のように理想機能実現装置の構成を定めることにより、理想機能実現装置は互いに合成することが可能となる。以下に２つの理想機能実現装置Ｆ１１、Ｆ１２の合成方法を示す。理想機能実現装置Ｆ１１、Ｆ１２のｓｕｐｐｒｅｓｓ関数を各々ｓｕｐ１１、ｓｕｐ１２、ｉｎｔ＿ｃｏｍｐ関数を各々ｉｎｔ＿ｃｏｍｐ１１、ｉｎｔ＿ｃｏｍｐ１２、ｏｕｔ＿ｃｏｍｐ関数を各々ｏｕｔ＿ｃｏｍｐ１１、ｏｕｔ＿ｃｏｍｐ１２、ｃｈｅｃｋ述語（ｃｋ関数）を各々ｃｋ１１、ｃｋ１２とする。また、ｈ（ヒストリー）の、Ｉ（Ｆ）、Ｏ（Ｆ）に関する入力以外の入力をすべて消去し、ｉｎｔ＿ｃｏｍｐ関数の計算結果の入力について、理想機能実現装置Ｆに関する値のみを残した後のリストをｈ↓Ｆと書くことにする。この時、理想機能実現装置Ｆ１１、Ｆ１２を合成した理想機能実現装置Ｆ１１∧Ｆ１２は次のように定まる。
【００１８】
Ｆ１１∧Ｆ１２に入力されるａｃｔｉｏｎ ｎａｍｅの集合を集合Ｉ（Ｆ１１∧Ｆ１２）とすれば、Ｉ（Ｆ１１∧Ｆ１２）：＝Ｉ（Ｆ１１）∪Ｉ（Ｆ１２）となる。同様に、Ｆ１１∧Ｆ１２から出力するａｃｔｉｏｎ ｎａｍｅの集合を集合Ｏ（Ｆ１１∧Ｆ１２）とすると、Ｏ（Ｆ１１∧Ｆ１２）：＝Ｏ（Ｆ１１）∪Ｏ（Ｆ１２）となる。Ｆ１１∧Ｆ１２のｓｕｐｐｒｅｓｓ関数はｓｕｐ１１（ｈ，ｓｕｐ１２（ｈ，ｘ））とする。Ｆ１１∧Ｆ１２のｉｎｔ＿ｃｏｍｐ関数はｉｎｔ＿ｃｏｍｐ１１∪ｉｎｔ＿ｃｏｍｐ１２とする。すなわち、入力ｈに対し、｛（ｉｎｔ＿ｃｏｍｐ１１（ｈ），Ｆ１１），（ｉｎｔ＿ｃｏｍｐ１２（ｈ），Ｆ１２）｝を戻値とする。Ｆ１１∧Ｆ１２のｏｕｔ＿ｃｏｍｐ関数は、ｏｕｔ＿ｃｏｍｐ１１（ｈ）＝ｏｕｔ＿ｃｏｍｐ１２（ｈ）のとき、この値とする。ｏｕｔ＿ｃｏｍｐ１１（ｈ）≠ｏｕｔ＿ｃｏｍｐ１２（ｈ）のときは、値を出力しない。Ｆ１１∧Ｆ１２のｃｈｅｃｋ述語はｃｋ１１（ｈ↓Ｆ１１）∧ｃｋ１２（ｈ↓Ｆ１２）とする。
【００１９】
このようにして二つの理想機能実現装置Ｆ１１、Ｆ１２の合成が実現する。すなわち、理想機能実現装置Ｆ１１で実現される理想機能と、理想機能実現装置Ｆ１２で実現される理想機能との合成が実現することを意味する。理想機能実現装置Ｆ１１、Ｆ１２の合成により生成した理想機能実現装置Ｆ１１∧Ｆ１２は、次のような性質を持つ。「プロトコルπがＦ１１およびＦ１２を満たす」ことと「プロトコルπがＦ１１∧Ｆ１２を満たす」ことは同値である。これにより、ゲーム形式のセキュリティ要求仕様表現の利点である要求の連言の記述が理想機能においても可能となる。
【００２０】
［変形例１］
以下に理想機能実現装置の合成の例として、一般に知られている理想機能ｃｏｍｍｉｔｍｅｎｔを二つの理想機能実現装置の合成により実現する例（変形例１）について述べる。具体的には、理想機能実現装置Ｆ１（理想機能ｃｏｍｍｉｔｍｅｎｔのｈｉｄｉｎｇを実現する理想機能実現装置）と、理想機能実現装置Ｆ２（理想機能ｃｏｍｍｉｔｍｅｎｔのｃｏｍｐｌｅｔｅｎｅｓｓかつｓｏｕｎｄｎｅｓｓを実現する理想機能実現装置）を用いて、理想機能ｃｏｍｍｉｔｍｅｎｔを実現する理想機能実現装置Ｆ１∧Ｆ２を合成する。
【００２１】
図５、６を参照して理想機能ｃｏｍｍｉｔｍｅｎｔのｈｉｄｉｎｇを実現する理想機能実現装置Ｆ１（１０−１）の動作を説明する。図５は理想機能実現装置Ｆ１（１０−１）の構成を示すブロック図である。図６は理想機能実現装置Ｆ１（１０−１）の動作を示すフローチャートである。集合Ｉ（Ｆ１）９２−１の元としてｃｏｍｍｉｔが与えられている。集合Ｏ（Ｆ１）９３−１は空集合である。従って、理想機能実現装置Ｆ１（１０−１）においては攻撃者９１からのｉｎｆメッセージの入力とそれ以降の動作は行われない。また、記号列ｘ（９４−１）はｓｉｄ．ｘである。この理想機能実現装置Ｆ１（１０−１）においては、ｓｕｐｐｒｅｓｓ関数をｓｕｐ１（引数、引数）と表すこととし、ｓｕｐ１（ｈ，ｓｉｄ．ｘ）の計算結果がｓｕｐ１（ｈ，ｓｉｄ．ｘ）＝ｓｉｄとなることが予め定められている。従って、理想機能実現装置Ｆ１（１０−１）の動作は以下のようになる。
【００２２】
理想機能実現装置Ｆ１（１０−１）にｉｎｐｕｔ（ｃｏｍｍｉｔ，ｓｉｄ．ｘ）が入力された場合に、ヒストリー記録部１３は、このｉｎｐｕｔ（ｃｏｍｉｔ，ｓｉｄ．ｘ）を入力とし（Ｓ１０１−１）、ｈが空であれば、当該空であるｈをｈ＝ｉｎｐｕｔ（ｃｏｍｍｉｔ，ｓｉｄ．ｘ）に更新し、ｈが空でなく、ｈが任意の記号列Ｐであれば、当該空でないｈをｈ＝Ｐ．ｉｎｐｕｔ（ｃｏｍｍｉｔ，ｓｉｄ．ｘ）に更新して（Ｓ１０２−１）、当該更新されたｈと、ｃｏｍｍｉｔと、ｓｉｄ．ｘとを出力する。ｓｕｐｐｒｅｓｓ関数計算部１２は、ｈ＝ｉｎｐｕｔ（ｃｏｍｍｉｔ，ｓｉｄ．ｘ）、もしくはｈ＝Ｐ．ｉｎｐｕｔ（ｃｏｍｍｉｔ，ｓｉｄ．ｘ）に更新されたｈと、ｓｉｄ．ｘとを入力とし、ｓｕｐ１（ｈ，ｓｉｄ．ｘ）を計算して（Ｓ１０３−１）、当該ｓｕｐ１（ｈ，ｓｉｄ．ｘ）を出力する。ｌｅａｋメッセージ作成部１１は、ｓｕｐ１（ｈ，ｓｉｄ．ｘ）＝ｓｉｄとｃｏｍｍｉｔとを入力とし、ｌｅａｋ（ｃｏｍｍｉｔ，ｓｉｄ）を作成して（Ｓ１０４−１）、当該ｌｅａｋ（ｃｏｍｍｉｔ，ｓｉｄ）を攻撃者９１に出力する（Ｓ１０５−１）。
【００２３】
次に、図７、８、９を参照して理想機能ｃｏｍｍｉｔｍｅｎｔのｃｏｍｐｌｅｔｅｎｅｓｓかつｓｏｕｎｄｎｅｓｓを実現する理想機能実現装置Ｆ２（１０−２）の動作を説明する。図７、８は理想機能実現装置Ｆ２（１０−２）の構成を示すブロック図である。図９は理想機能実現装置Ｆ２（１０−２）の動作を示すフローチャートである。集合Ｉ（Ｆ２）９２−２の元としてｃｏｍｍｉｔ、ｏｐｅｎが与えられている。集合Ｏ（Ｆ２）９３−２の元としてａｃｃｅｐｔ、ｏｕｔが与えられている。また、記号列ｘ（９４−２）には変更はなく、記号列ｘのままである。この理想機能実現装置Ｆ２（１０−２）においては、ｓｕｐｐｒｅｓｓ関数、ｉｎｔ＿ｃｏｍｐ関数、ｃｋ関数、ｏｕｔ＿ｃｏｍｐ関数をそれぞれｓｕｐ２（引数、引数）、ｉｎｔ＿ｃｏｍｐ２（引数）、ｃｋ２（引数）、ｏｕｔ＿ｃｏｍｐ２（引数）と表すこととし、ｓｕｐ２（ｈ，ｘ）の計算結果がｓｕｐ２（ｈ，ｘ）＝ｘ、ｉｎｔ＿ｃｏｍｐ２（ｈ）の計算結果がｉｎｔ＿ｃｏｍｐ２（ｈ）＝ｓｉｄとなることが予め定められている。ｃｋ２（引数）、ｏｕｔ＿ｃｏｍｐ２（引数）のふるまいについては後述する。従って、理想機能実現装置Ｆ２（１０−２）の動作は以下のようになる。
【００２４】
理想機能実現装置Ｆ２（１０−２）にｉｎｐｕｔ（ｃｏｍｍｉｔ，ｘ）もしくはｉｎｐｕｔ（ｏｐｅｎ，ｘ）が入力された場合に、ヒストリー記録部１３は、このｉｎｐｕｔ（ｃｏｍｉｔ，ｘ）もしくはｉｎｐｕｔ（ｏｐｅｎ，ｘ）を入力とし（Ｓ１０１−２）、ｈが空であれば、当該空であるｈをｈ＝ｉｎｐｕｔ（ｃｏｍｍｉｔ，ｘ）もしくはｈ＝ｉｎｐｕｔ（ｏｐｅｎ，ｘ）に更新し、ｈが空でなく、ｈが任意の記号列Ｐであれば、当該空でないｈをｈ＝Ｐ．ｉｎｐｕｔ（ｃｏｍｍｉｔ，ｘ）もしくはｈ＝Ｐ．ｉｎｐｕｔ（ｏｐｅｎ，ｘ）に更新して（Ｓ１０２−２）、当該更新されたｈと、ｃｏｍｍｉｔもしくはｏｐｅｎと、ｘとを出力する。ｓｕｐｐｒｅｓｓ関数計算部１２は、ｈ＝ｉｎｐｕｔ（ｃｏｍｍｉｔ，ｘ）もしくはｈ＝ｉｎｐｕｔ（ｏｐｅｎ，ｘ）、もしくはｈ＝Ｐ．ｉｎｐｕｔ（ｃｏｍｍｉｔ，ｘ）もしくはｈ＝Ｐ．ｉｎｐｕｔ（ｏｐｅｎ，ｘ）に更新されたｈと、ｘとを入力とし、ｓｕｐ２（ｈ，ｘ）を計算して（Ｓ１０３−２）、当該ｓｕｐ２（ｈ，ｘ）を出力する。ｌｅａｋメッセージ作成部１１は、ｓｕｐ２（ｈ，ｘ）＝ｘとｃｏｍｍｉｔもしくはｏｐｅｎとを入力とし、ｌｅａｋ（ｃｏｍｍｉｔ，ｘ）もしくはｌｅａｋ（ｏｐｅｎ，ｘ）を作成して（Ｓ１０４−２）、当該ｌｅａｋ（ｃｏｍｍｉｔ，ｘ）もしくはｌｅａｋ（ｏｐｅｎ，ｘ）を攻撃者９１に出力する（Ｓ１０５−２）。
【００２５】
攻撃者９１から理想機能実現装置Ｆ２（１０−２）にｉｎｆ（ａｃｃｅｐｔ，ｓｉｄ．ｘ）もしくはｉｎｆ（ｏｕｔ，ｓｉｄ．ｘ）が入力された場合に、ヒストリー記録部１３は、ｉｎｆ（ａｃｃｅｐｔ，ｓｉｄ．ｘ）もしくはｉｎｆ（ｏｕｔ，ｓｉｄ．ｘ）を入力とし（Ｓ１０６−２）、ｈが空であれば、当該空であるｈをｈ＝ｉｎｆ（ａｃｃｅｐｔ，ｓｉｄ．ｘ）もしくはｈ＝ｉｎｆ（ｏｕｔ，ｓｉｄ．ｘ）に更新し、ｈが空でなく、ｈが任意の記号列Ｑであれば、当該空でないｈをｈ＝Ｑ．ｉｎｆ（ａｃｃｅｐｔ，ｓｉｄ．ｘ）もしくはｈ＝Ｑ．ｉｎｆ（ｏｕｔ，ｓｉｄ．ｘ）に更新して（Ｓ１０７−２）、当該更新されたｈと、ａｃｃｅｐｔもしくはｏｕｔを出力する。ｉｎｔ＿ｃｏｍｐ関数計算部１４は、ｈ＝ｉｎｆ（ａｃｃｅｐｔ，ｓｉｄ．ｘ）もしくはｈ＝ｉｎｆ（ｏｕｔ，ｓｉｄ．ｘ）、もしくはｈ＝Ｑ．ｉｎｆ（ａｃｃｅｐｔ，ｓｉｄ．ｘ）もしくはｈ＝Ｑ．ｉｎｆ（ｏｕｔ，ｓｉｄ．ｘ）に更新されたｈを入力とし、ｉｎｔ＿ｃｏｍｐ２（ｈ）を計算して（Ｓ１０８−２）、当該ｉｎｔ＿ｃｏｍｐ２（ｈ）を出力する。ヒストリー記録部１３は、ｉｎｔ＿ｃｏｍｐ２（ｈ）＝ｓｉｄを入力とし、ｈが任意の記号列Ｒであれば、当該ｈをｈ＝Ｒ．ｓｉｄに更新して（Ｓ１０９−２）、当該更新されたｈを出力する。ｃｋ（ｈ）判定部１５は、ｈ＝Ｒ．ｓｉｄに更新されたｈを入力とし、ｃｋ２（ｈ）を計算し（Ｓ１１０−２）、当該計算結果であるｃｋ２（ｈ）＝ｔｒｕｅもしくはｃｋ２（ｈ）＝ｆａｌｓｅのいずれかを出力する。ここで、ｈの末尾がｉｎｆ（ａｃｃｅｐｔ，ｓｉｄ．ｘ）．ｓｉｄであって、ｈの一部にｉｎｐｕｔ（ｃｏｍｍｉｔ，ｓｉｄ．ｘ）がある場合にはｃｋ２（ｈ）＝ｔｒｕｅと判定する。また、ｈの末尾がｉｎｆ（ｏｕｔ，ｓｉｄ．ｘ）．ｓｉｄであって、ｈの一部にｉｎｐｕｔ（ｃｏｍｍｉｔ，ｓｉｄ．ｘ）があり、その後にｉｎｐｕｔ（ｏｐｅｎ，ｓｉｄ．ｘ）がある場合にもｃｋ（ｈ）＝ｔｒｕｅと判定する。次に、ｏｕｔ＿ｃｏｍｐ関数計算部１６は、ｃｋ（ｈ）判定部１５により出力されたｃｋ２（ｈ）と、ヒストリー記録部１３によりｈ＝Ｒ．ｓｉｄに更新されたｈとを入力とし、ｃｋ２（ｈ）＝ｔｒｕｅである場合に（Ｓ１１１−２）、ｏｕｔ＿ｃｏｍｐ２（ｈ）を計算し（Ｓ１１２−２）、当該ｏｕｔ＿ｃｏｍｐ２（ｈ）を出力する。ここで、ｈの末尾がｉｎｆ（ａｃｃｅｐｔ，ｓｉｄ．ｘ）．ｓｉｄである場合にはｏｕｔ＿ｃｏｍｐ２（ｈ）＝ｓｉｄとなり、ｈの末尾がｉｎｆ（ｏｕｔ，ｓｉｄ．ｘ）．ｓｉｄである場合にはｏｕｔ＿ｃｏｍｐ２（ｈ）＝ｓｉｄ．ｘとなる。ｏｕｔｐｕｔメッセージ作成部１７は、ｏｕｔ＿ｃｏｍｐ２（ｈ）と、ａｃｃｅｐｔもしくはｏｕｔを入力とし、ｗにｗ＝ｏｕｔ＿ｃｏｍｐ２（ｈ）を代入して、ｏｕｔｐｕｔ（ａｃｃｅｐｔ，ｗ）もしくはｏｕｔｐｕｔ（ｏｕｔ，ｗ）を作成し（Ｓ１１３−２）、ｏｕｔｐｕｔ（ａｃｃｅｐｔ，ｗ）もしくはｏｕｔｐｕｔ（ｏｕｔ，ｗ）を理想機能実現装置Ｆ２（１０−２）の外部に出力する（Ｓ１１４−２）。ヒストリー記録部１３は、ｏｕｔｐｕｔ（ａｃｃｅｐｔ，ｗ）もしくはｏｕｔｐｕｔ（ｏｕｔ，ｗ）を入力とし、ｈが任意の記号列Ｓであれば、当該ｈをｈ＝Ｓ．ｏｕｔｐｕｔ（ａｃｃｅｐｔ，ｗ）もしくはｈ＝Ｓ．ｏｕｔｐｕｔ（ｏｕｔ，ｗ）に更新する（Ｓ１１５−２）。このように構成された理想機能実現装置Ｆ１と理想機能実現装置Ｆ２とを合成して得られる理想機能実現装置Ｆ１∧Ｆ２は一般に知られている理想機能ｃｏｍｍｉｔｍｅｎｔを実現する。
【００２６】
［変形例２］
以下に理想機能実現装置の合成の例として、一般に知られている理想機能ｏｂｌｉｖｉｏｕｓ ｔｒａｎｓｆｅｒを二つの理想機能実現装置の合成により実現する例（変形例２）について述べる。具体的には、理想機能実現装置Ｆ３（理想機能ｏｂｌｉｖｉｏｕｓ ｔｒａｎｓｆｅｒのｓｅｎｄｅｒ ｈｉｄｉｎｇを実現する理想機能実現装置）と、理想機能実現装置Ｆ４（理想機能ｏｂｌｉｖｉｏｕｓ ｔｒａｎｓｆｅｒのｒｅｃｅｉｖｅｒ ｈｉｄｉｎｇを実現する理想機能実現装置）と、理想機能実現装置Ｆ５（理想機能ｏｂｌｉｖｉｏｕｓ ｔｒａｎｓｆｅｒのｃｏｍｐｌｅｔｅｎｅｓｓを実現する理想機能実現装置）を用いて、理想機能ｏｂｌｉｖｉｏｕｓ ｔｒａｎｓｆｅｒを実現する理想機能実現装置Ｆ３∧Ｆ４∧Ｆ５を合成する。
【００２７】
図１０、１１を参照して理想機能ｏｂｌｉｖｉｏｕｓ ｔｒａｎｓｆｅｒのｓｅｎｄｅｒ ｈｉｄｉｎｇを実現する理想機能実現装置Ｆ３（１０−３）の動作を説明する。図１０は理想機能実現装置Ｆ３（１０−３）の構成を示すブロック図である。図１１は理想機能実現装置Ｆ３（１０−３）の動作を示すフローチャートである。集合Ｉ（Ｆ３）９２−３の元としてｓｅｎｄｅｒ＿ｉｎｐｕｔが与えられている。集合Ｏ（Ｆ３）９３−３は空集合である。従って、理想機能実現装置Ｆ３（１０−３）においては攻撃者９１からのｉｎｆメッセージの入力とそれ以降の動作は行われない。また、記号列ｘ（９４−３）はｓｉｄ．ｘである。この理想機能実現装置Ｆ３（１０−３）においては、ｓｕｐｐｒｅｓｓ関数をｓｕｐ３（引数、引数）と表すこととし、ｓｕｐ３（ｈ，ｓｉｄ．ｘ）の計算結果がｓｕｐ３（ｈ，ｓｉｄ．ｘ）＝ｓｉｄとなることが予め定められている。従って、理想機能実現装置Ｆ３（１０−３）の動作は以下のようになる。
【００２８】
理想機能実現装置Ｆ３（１０−３）にｉｎｐｕｔ（ｓｅｎｄｅｒ＿ｉｎｐｕｔ，ｓｉｄ．ｘ）が入力された場合に、ヒストリー記録部１３は、このｉｎｐｕｔ（ｓｅｎｄｅｒ＿ｉｎｐｕｔ，ｓｉｄ．ｘ）を入力とし（Ｓ１０１−３）、ｈが空であれば、当該空であるｈをｈ＝ｉｎｐｕｔ（ｓｅｎｄｅｒ＿ｉｎｐｕｔ，ｓｉｄ．ｘ）に更新し、ｈが空でなく、ｈが任意の記号列Ｐであれば、当該空でないｈをｈ＝Ｐ．ｉｎｐｕｔ（ｓｅｎｄｅｒ＿ｉｎｐｕｔ，ｓｉｄ．ｘ）に更新して（Ｓ１０２−３）、当該更新されたｈと、ｓｅｎｄｅｒ＿ｉｎｐｕｔと、ｓｉｄ．ｘとを出力する。ｓｕｐｐｒｅｓｓ関数計算部１２は、ｈ＝ｉｎｐｕｔ（ｓｅｎｄｅｒ＿ｉｎｐｕｔ，ｓｉｄ．ｘ）、もしくはｈ＝Ｐ．ｉｎｐｕｔ（ｓｅｎｄｅｒ＿ｉｎｐｕｔ，ｓｉｄ．ｘ）に更新されたｈと、ｓｉｄ．ｘとを入力とし、ｓｕｐ３（ｈ，ｓｉｄ．ｘ）を計算して（Ｓ１０３−３）、当該ｓｕｐ３（ｈ，ｓｉｄ．ｘ）を出力する。ｌｅａｋメッセージ作成部１１は、ｓｕｐ３（ｈ，ｓｉｄ．ｘ）＝ｓｉｄとｓｅｎｄｅｒ＿ｉｎｐｕｔとを入力とし、ｌｅａｋ（ｓｅｎｄｅｒ＿ｉｎｐｕｔ，ｓｉｄ）を作成して（Ｓ１０４−３）、当該ｌｅａｋ（ｓｅｎｄｅｒ＿ｉｎｐｕｔ，ｓｉｄ）を攻撃者９１に出力する（Ｓ１０５−３）。
【００２９】
次に、図１２、１３を参照して理想機能ｏｂｌｉｖｉｏｕｓ ｔｒａｎｓｆｅｒのｒｅｃｅｉｖｅｒ ｈｉｄｉｎｇを実現する理想機能実現装置Ｆ４（１０−４）の動作を説明する。図１２は理想機能実現装置Ｆ４（１０−４）の構成を示すブロック図である。図１３は理想機能実現装置Ｆ４（１０−４）の動作を示すフローチャートである。集合Ｉ（Ｆ４）９２−４の元としてｒｅｃｅｉｖｅｒ＿ｉｎｐｕｔが与えられている。集合Ｏ（Ｆ４）９３−４は空集合である。従って、理想機能実現装置Ｆ４（１０−４）においては攻撃者９１からのｉｎｆメッセージの入力とそれ以降の動作は行われない。また、記号列ｘ（９４−４）はｓｉｄ．ｘである。この理想機能実現装置Ｆ４（１０−４）においては、ｓｕｐｐｒｅｓｓ関数をｓｕｐ４（引数、引数）と表すこととし、ｓｕｐ４（ｈ，ｓｉｄ．ｘ）の計算結果がｓｕｐ４（ｈ，ｓｉｄ．ｘ）＝ｓｉｄとなることが予め定められている。従って、理想機能実現装置Ｆ４（１０−４）の動作は以下のようになる。
【００３０】
理想機能実現装置Ｆ４（１０−４）にｉｎｐｕｔ（ｒｅｃｅｉｖｅｒ＿ｉｎｐｕｔ，ｓｉｄ．ｘ）が入力された場合に、ヒストリー記録部１３は、このｉｎｐｕｔ（ｒｅｃｅｉｖｅｒ＿ｉｎｐｕｔ，ｓｉｄ．ｘ）を入力とし（Ｓ１０１−４）、ｈが空であれば、当該空であるｈをｈ＝ｉｎｐｕｔ（ｒｅｃｅｉｖｅｒ＿ｉｎｐｕｔ，ｓｉｄ．ｘ）に更新し、ｈが空でなく、ｈが任意の記号列Ｐであれば、当該空でないｈをｈ＝Ｐ．ｉｎｐｕｔ（ｒｅｃｅｉｖｅｒ＿ｉｎｐｕｔ，ｓｉｄ．ｘ）に更新して（Ｓ１０２−４）、当該更新されたｈと、ｒｅｃｅｉｖｅｒ＿ｉｎｐｕｔと、ｓｉｄ．ｘとを出力する。ｓｕｐｐｒｅｓｓ関数計算部１２は、ｈ＝ｉｎｐｕｔ（ｒｅｃｅｉｖｅｒ＿ｉｎｐｕｔ，ｓｉｄ．ｘ）、もしくはｈ＝Ｐ．ｉｎｐｕｔ（ｒｅｃｅｉｖｅｒ＿ｉｎｐｕｔ，ｓｉｄ．ｘ）に更新されたｈと、ｓｉｄ．ｘとを入力とし、ｓｕｐ４（ｈ，ｓｉｄ．ｘ）を計算して（Ｓ１０３−４）、当該ｓｕｐ４（ｈ，ｓｉｄ．ｘ）を出力する。ｌｅａｋメッセージ作成部１１は、ｓｕｐ４（ｈ，ｓｉｄ．ｘ）＝ｓｉｄとｒｅｃｅｉｖｅｒ＿ｉｎｐｕｔとを入力とし、ｌｅａｋ（ｒｅｃｅｉｖｅｒ＿ｉｎｐｕｔ，ｓｉｄ）を作成して（Ｓ１０４−４）、当該ｌｅａｋ（ｒｅｃｅｉｖｅｒ＿ｉｎｐｕｔ，ｓｉｄ）を攻撃者９１に出力する（Ｓ１０５−４）。
【００３１】
次に、図１４、１５、１６を参照して理想機能ｏｂｌｉｖｉｏｕｓ ｔｒａｎｓｆｅｒのｃｏｍｐｌｅｔｅｎｅｓｓを実現する理想機能実現装置Ｆ５（１０−５）の動作を説明する。図１４、１５は理想機能実現装置Ｆ５（１０−５）の構成を示すブロック図である。図１６は理想機能実現装置Ｆ５（１０−５）の動作を示すフローチャートである。集合Ｉ（Ｆ５）９２−５の元としてｓｅｎｄｅｒ＿ｉｎｐｕｔ、ｒｅｃｅｉｖｅｒ＿ｉｎｐｕｔが与えられている。集合Ｏ（Ｆ５）９３−５の元としてｏｕｔが与えられている。また、記号列ｘ（９４−５）には変更はなく、記号列ｘのままである。この理想機能実現装置Ｆ５（１０−５）においては、ｓｕｐｐｒｅｓｓ関数、ｉｎｔ＿ｃｏｍｐ関数、ｃｋ関数、ｏｕｔ＿ｃｏｍｐ関数をそれぞれｓｕｐ５（引数、引数）、ｉｎｔ＿ｃｏｍｐ５（引数）、ｃｋ５（引数）、ｏｕｔ＿ｃｏｍｐ５（引数）と表すこととし、ｓｕｐ５（ｈ，ｘ）の計算結果がｓｕｐ５（ｈ，ｘ）＝ｘ、ｉｎｔ＿ｃｏｍｐ５（ｈ）の計算結果がｉｎｔ＿ｃｏｍｐ５（ｈ）＝ｓｉｄとなることが予め定められている。ｃｋ５（引数）、ｏｕｔ＿ｃｏｍｐ５（引数）のふるまいについては後述する。従って、理想機能実現装置Ｆ５（１０−５）の動作は以下のようになる。
【００３２】
理想機能実現装置Ｆ５（１０−５）にｉｎｐｕｔ（ｓｅｎｄｅｒ＿ｉｎｐｕｔ，ｘ）もしくはｉｎｐｕｔ（ｒｅｃｅｉｖｅｒ＿ｉｎｐｕｔ，ｘ）が入力された場合に、ヒストリー記録部１３は、このｉｎｐｕｔ（ｓｅｎｄｅｒ＿ｉｎｐｕｔ，ｘ）もしくはｉｎｐｕｔ（ｒｅｃｅｉｖｅｒ＿ｉｎｐｕｔ，ｘ）を入力とし（Ｓ１０１−５）、ｈが空であれば、当該空であるｈをｈ＝ｉｎｐｕｔ（ｓｅｎｄｅｒ＿ｉｎｐｕｔ，ｘ）もしくはｈ＝ｉｎｐｕｔ（ｒｅｃｅｉｖｅｒ＿ｉｎｐｕｔ，ｘ）に更新し、ｈが空でなく、ｈが任意の記号列Ｐであれば、当該空でないｈをｈ＝Ｐ．ｉｎｐｕｔ（ｓｅｎｄｅｒ＿ｉｎｐｕｔ，ｘ）もしくはｈ＝Ｐ．ｉｎｐｕｔ（ｒｅｃｅｉｖｅｒ＿ｉｎｐｕｔ，ｘ）に更新して（Ｓ１０２−５）、当該更新されたｈと、ｓｅｎｄｅｒ＿ｉｎｐｕｔもしくはｒｅｃｅｉｖｅｒ＿ｉｎｐｕｔと、ｘとを出力する。ｓｕｐｐｒｅｓｓ関数計算部１２は、ｈ＝ｉｎｐｕｔ（ｓｅｎｄｅｒ＿ｉｎｐｕｔ，ｘ）もしくはｈ＝ｉｎｐｕｔ（ｒｅｃｅｉｖｅｒ＿ｉｎｐｕｔ，ｘ）、もしくはｈ＝Ｐ．ｉｎｐｕｔ（ｓｅｎｄｅｒ＿ｉｎｐｕｔ，ｘ）もしくはｈ＝Ｐ．ｉｎｐｕｔ（ｒｅｃｅｉｖｅｒ＿ｉｎｐｕｔ，ｘ）に更新されたｈと、ｘとを入力とし、ｓｕｐ５（ｈ，ｘ）を計算して（Ｓ１０３−５）、当該ｓｕｐ５（ｈ，ｘ）を出力する。ｌｅａｋメッセージ作成部１１は、ｓｕｐ５（ｈ，ｘ）＝ｘとｓｅｎｄｅｒ＿ｉｎｐｕｔもしくはｒｅｃｅｉｖｅｒ＿ｉｎｐｕｔとを入力とし、ｌｅａｋ（ｓｅｎｄｅｒ＿ｉｎｐｕｔ，ｘ）もしくはｌｅａｋ（ｒｅｃｅｉｖｅｒ＿ｉｎｐｕｔ，ｘ）を作成して（Ｓ１０４−５）、当該ｌｅａｋ（ｓｅｎｄｅｒ＿ｉｎｐｕｔ，ｘ）もしくはｌｅａｋ（ｒｅｃｅｉｖｅｒ＿ｉｎｐｕｔ，ｘ）を攻撃者９１に出力する（Ｓ１０５−５）。
【００３３】
攻撃者９１から理想機能実現装置Ｆ５（１０−５）にｉｎｆ（ｏｕｔ，ｓｉｄ）が入力された場合に、ヒストリー記録部１３は、ｉｎｆ（ｏｕｔ，ｓｉｄ）を入力とし（Ｓ１０６−５）、ｈが空であれば、当該空であるｈをｈ＝ｉｎｆ（ｏｕｔ，ｓｉｄ）に更新し、ｈが空でなく、ｈが任意の記号列Ｑであれば、当該空でないｈをｈ＝Ｑ．ｉｎｆ（ｏｕｔ，ｓｉｄ）に更新して（Ｓ１０７−５）、当該更新されたｈと、ｏｕｔを出力する。ｉｎｔ＿ｃｏｍｐ関数計算部１４は、ｈ＝ｉｎｆ（ｏｕｔ，ｓｉｄ）、もしくはｈ＝Ｑ．ｉｎｆ（ｏｕｔ，ｓｉｄ）に更新されたｈを入力とし、ｉｎｔ＿ｃｏｍｐ５（ｈ）を計算して（Ｓ１０８−５）、当該ｉｎｔ＿ｃｏｍｐ５（ｈ）を出力する。ヒストリー記録部１３は、ｉｎｔ＿ｃｏｍｐ５（ｈ）＝ｓｉｄを入力とし、ｈが任意の記号列Ｒであれば、当該ｈをｈ＝Ｒ．ｓｉｄに更新して（Ｓ１０９−５）、当該更新されたｈを出力する。ｃｋ（ｈ）判定部１５は、ｈ＝Ｒ．ｓｉｄに更新されたｈを入力とし、ｃｋ５（ｈ）を計算し（Ｓ１１０−５）、当該計算結果であるｃｋ５（ｈ）＝ｔｒｕｅもしくはｃｋ５（ｈ）＝ｆａｌｓｅのいずれかを出力する。ここで、ｈの末尾がｉｎｆ（ｏｕｔ，ｓｉｄ）．ｓｉｄであって、ｈの一部にｉｎｐｕｔ（ｓｅｎｄｅｒ＿ｉｎｐｕｔ，ｓｉｄ．（ｘ１，ｘ２））およびｉｎｐｕｔ（ｒｅｃｅｉｖｅｒ＿ｉｎｐｕｔ，ｓｉｄ．ｉ）がある場合にはｃｋ５（ｈ）＝ｔｒｕｅと判定する。次に、ｏｕｔ＿ｃｏｍｐ関数計算部１６は、ｃｋ（ｈ）判定部１５により出力されたｃｋ５（ｈ）と、ヒストリー記録部１３によりｈ＝Ｒ．ｓｉｄに更新されたｈとを入力とし、ｃｋ５（ｈ）＝ｔｒｕｅである場合に（Ｓ１１１−５）、ｏｕｔ＿ｃｏｍｐ５（ｈ）を計算し（Ｓ１１２−５）、当該ｏｕｔ＿ｃｏｍｐ５（ｈ）を出力する。ここで、ｈの末尾がｉｎｆ（ｏｕｔ，ｓｉｄ）．ｓｉｄであって、ｈの一部にｉｎｐｕｔ（ｓｅｎｄｅｒ＿ｉｎｐｕｔ，ｓｉｄ．（ｘ１，ｘ２））およびｉｎｐｕｔ（ｒｅｃｅｉｖｅｒ＿ｉｎｐｕｔ，ｓｉｄ．ｉ）がある場合にはｏｕｔ＿ｃｏｍｐ５（ｈ）＝ｘｉとなる。ｏｕｔｐｕｔメッセージ作成部１７は、ｏｕｔ＿ｃｏｍｐ５（ｈ）と、ｏｕｔを入力とし、ｗにｗ＝ｏｕｔ＿ｃｏｍｐ５（ｈ）を代入して、ｏｕｔｐｕｔ（ｏｕｔ，ｗ）を作成し（Ｓ１１３−５）、ｏｕｔｐｕｔ（ｏｕｔ，ｗ）を理想機能実現装置Ｆ５（１０−５）の外部に出力する（Ｓ１１４−５）。ヒストリー記録部１３は、ｏｕｔｐｕｔ（ｏｕｔ，ｗ）を入力とし、ｈが任意の記号列Ｓであれば、当該ｈをｈ＝Ｓ．ｏｕｔｐｕｔ（ｏｕｔ，ｗ）に更新する（Ｓ１１５−５）。このように構成された理想機能実現装置Ｆ３、Ｆ４、Ｆ５を合成して得られる理想機能実現装置Ｆ３∧Ｆ４∧Ｆ５は一般に知られている理想機能ｏｂｌｉｖｉｏｕｓ ｔｒａｎｓｆｅｒを実現する。
【００３４】
以上のように、本発明の理想機能実現装置によれば、理想機能実現装置同士が互いに合成可能となるため、ゲーム形式のセキュリティ要求仕様表現の利点である要求の連言の記述が理想機能においても可能となる。従って、いくつかの基本的なセキュリティ要求仕様に対応する理想機能から、それら要求仕様を組み合わせた複雑な要求仕様に対応する理想機能を簡単に生成することができる。これにより、設計が難しかった理想機能の設計が簡単になり、あるセキュリティ要求仕様にもとづくプロトコルの安全性証明も、より容易になる。
【００３５】
また、上述の各種の処理は、記載に従って時系列に実行されるのみならず、処理を実行する装置の処理能力あるいは必要に応じて並列的にあるいは個別に実行されてもよい。その他、本発明の趣旨を逸脱しない範囲で適宜変更が可能であることはいうまでもない。
【００３６】
また、上述の構成をコンピュータによって実現する場合、各装置が有すべき機能の処理内容はプログラムによって記述される。そして、このプログラムをコンピュータで実行することにより、上記処理機能がコンピュータ上で実現される。
【００３７】
この処理内容を記述したプログラムは、コンピュータで読み取り可能な記録媒体に記録しておくことができる。コンピュータで読み取り可能な記録媒体としては、例えば、磁気記録装置、光ディスク、光磁気記録媒体、半導体メモリ等どのようなものでもよい。
【００３８】
また、このプログラムの流通は、例えば、そのプログラムを記録したＤＶＤ、ＣＤ−ＲＯＭ等の可搬型記録媒体を販売、譲渡、貸与等することによって行う。さらに、このプログラムをサーバコンピュータの記憶装置に格納しておき、ネットワークを介して、サーバコンピュータから他のコンピュータにそのプログラムを転送することにより、このプログラムを流通させる構成としてもよい。
【００３９】
このようなプログラムを実行するコンピュータは、例えば、まず、可搬型記録媒体に記録されたプログラムもしくはサーバコンピュータから転送されたプログラムを、一旦、自己の記憶装置に格納する。そして、処理の実行時、このコンピュータは、自己の記録媒体に格納されたプログラムを読み取り、読み取ったプログラムに従った処理を実行する。また、このプログラムの別の実行形態として、コンピュータが可搬型記録媒体から直接プログラムを読み取り、そのプログラムに従った処理を実行することとしてもよく、さらに、このコンピュータにサーバコンピュータからプログラムが転送されるたびに、逐次、受け取ったプログラムに従った処理を実行することとしてもよい。また、サーバコンピュータから、このコンピュータへのプログラムの転送は行わず、その実行指示と結果取得のみによって処理機能を実現する、いわゆるＡＳＰ（Application Service Provider）型のサービスによって、上述の処理を実行する構成としてもよい。なお、本形態におけるプログラムには、電子計算機による処理の用に供する情報であってプログラムに準ずるもの（コンピュータに対する直接の指令ではないがコンピュータの処理を規定する性質を有するデータ等）を含むものとする。
【００４０】
また、この形態では、コンピュータ上で所定のプログラムを実行させることにより、本装置を構成することとしたが、これらの処理内容の少なくとも一部をハードウェア的に実現することとしてもよい。
【図１】
2012078456.tif 000003
【図２】
2012078456.tif 000004
【図３】
2012078456.tif 000005
【図４】
2012078456.tif 000006
【図５】
2012078456.tif 000007
【図６】
2012078456.tif 000008
【図７】
2012078456.tif 000009
【図８】
2012078456.tif 000010
【図９】
2012078456.tif 000011
【図１０】
2012078456.tif 000012
【図１１】
2012078456.tif 000013
【図１２】
2012078456.tif 000014
【図１３】
2012078456.tif 000015
【図１４】
2012078456.tif 000016
【図１５】
2012078456.tif 000017
【図１６】
2012078456.tif 000018