2005 Fiscal Year Annual Research Report
ダイナミックに変化する知識・信念の論理学的分析手法の研究
| Project/Area Number |
04J07439
|
|---|
| Research Institution | Keio University |
|---|
Principal Investigator |
長谷部 浩二 慶應義塾大学, 文学部, 特別研究員(PD)
|
|---|
| Keywords | セキュリティ・プロトコル / 安全性検証 / 一階述語論理 / 完全性定理 |
|---|
| Research Abstract |
昨年度に引続き、本年度も主に認証プロトコルの論理的検証法に関する研究を行った。本年度は特に、一階述語論理を基にした認証プロトコルの論理的検証法を考案した。(この論理体系をBasic Protocol Logicと呼ぶ。)その基本的なアイデアは、認証プロトコルにおける基本的なアクションを原子述語記号により表現し、さらに基本的なアクションの列をこれらの原子述語記号の列によって構成された原子論理式で表現するというものである。Basic Protocol Logicに対しては、従来の通常の1階述語論理で与えられてきたタルスキ的な意味論に「アクションの列」の概念を導入した自然な意味論を与えることができ、さらにこの意味論に関して完全性定理の成り立つことを示した。また、証明検索法による証明可能性判定が有限の手続きにより決定可能であることも示した。(なお通常の1階述語論理の証明検索法は、与えられた論理式が証明可能であるときのみ停止することが知られている。)以上の結果から、Basic Protocol Logicの言語で書かれたプロトコルの安全性を示す論理式に対して、もしも証明検索木の全ての枝が閉じればその安全性の形式証明が得られ、そうでなければこのプロトコルに対する攻撃のプロセスが反例として得られる。本年度はさらに、この証明検索法をもとにした安全性検証のアルゴリズムを、プログラミング言語Standard MLを用いて試作実装した。この実装アルゴリズムは証明検索法による反例導出アルゴリズムを抽出したものであり、現在研究中の、安全性の証明可能なプロトコルの自動生成アルゴリズムと融合させた検証法の開発を試みている。
|
Research Products
(1 results)
