2002 Fiscal Year Annual Research Report
算術体系の無矛盾性証明におけるゲーデル解釈の論理的・数理哲学的研究
Project/Area Number |
01J04474
|
Research Institution | Keio University |
Principal Investigator |
長谷部 浩二 慶應義塾大学, 文学研究科, 特別研究員(DC2)
|
Keywords | 帰納的汎関数体系 / 線形論理 / セキュリティ・プロトコル |
Research Abstract |
前年度まで行ってきたゲーデルの汎関数体系Tの拡張の試みや線形論理的手法を用いたその応用の試みに対し,本年度は,前年度で得られた研究成果をもとにその計算論的性質(特に重要な性質であるチャーチ・ロッサー性と強正規化性)について考察を行うとともに,その応用についても考察した.(以上で述べた計算論的性質に関する考察は,現在論文等の形で発表するための準備を行っている.)特に近年,理論情報科学において,情報通信を行う上でのセキュリティ確保の技術を論理学的手法を用いて理論的側面から考察する試み(セキュリティ・プロトコルと呼ばれる)が非常に盛んに行われており,本研究で扱われている型理論の手法がこの分野の研究に対しても有効であることが知られている.本年度はこのセキュリティ・プロトコルの分野への本研究テーマの応用を試みた.本年度は上記で得られた成果をもとに,線形論理的手法と信念論理の手法を組み合わせたセキュリティ・プロトコルの検証理論を考察した.この研究で得られた成果は,2002年5月に神戸大学にて行われた学会「人工知能と知識処理」(電子情報通信学会主催)及び同年10月に慶應義塾大学にて行われた国際会議"International Symposium on Software Security"にて岡田教授と共同で口頭発表を行っている.またこれらの結果は論文でProceedingsに収録されている(詳しくは「研究発表」欄を参照).
|
Research Products
(2 results)
-
[Publications] 岡田光弘, 長谷部浩二: "線形論理に基づいたセキュリティ・プロトコルの論理的検証法"電子情報通信学会「人工知能と知識処理」研究報告. 102.91. 49-54 (2002)
-
[Publications] Koji Hasebe, Mitsuhiro Okada: "A Logical Verification Method for Security Protocols Based on Linear Logic and BAN Logic"Software Security (Hot topic Series of Lecture Notes in Computer Science). No.2609. 422-445 (2003)