ダイナミックに変化する知識・信念の論理学的分析手法の研究
| Project/Area Number |
04J07439
|
|---|
| Research Category |
Grant-in-Aid for JSPS Fellows
|
| Allocation Type | Single-year Grants |
|---|
| Section | 国内 |
|---|
| Research Field |
Philosophy/Ethics
|
|---|
| Research Institution | National Institute of Advanced Industrial Science and Technology (2006)
Keio University (2004-2005) |
|---|
Principal Investigator |
長谷部 浩二 独立行政法人産業技術総合研究所, システム検証研究センター, 特別研究員(PD)
|
|---|
| Project Period (FY) |
2004 – 2006
|
| Project Status |
Completed (Fiscal Year 2006)
|
| Budget Amount *help |
¥3,400,000 (Direct Cost: ¥3,400,000)
Fiscal Year 2006: ¥1,100,000 (Direct Cost: ¥1,100,000)
Fiscal Year 2005: ¥1,100,000 (Direct Cost: ¥1,100,000)
Fiscal Year 2004: ¥1,200,000 (Direct Cost: ¥1,200,000)
|
|---|
| Keywords | 通信プロトコル / 安全性検証 / 形式手法 / 一階述語論理 / 暗号 / 機能安全 / セキュリティ・プロトコル / 完全性定理 / 知識論理 / Compositional losic / 認証プロトコル / 証明検索法 / 反例導出 |
|---|
| Research Abstract |
本年度の前半は,昨年度に引き続き論理的・形式的手法による通信プロトコルの安全性検証法の研究を行った.特に昨年度の研究成果として提起した一階述語論理を基にした論理推論体系Basic Protocol Logicを基にした安全性検証法を中心に,その理論的成果とコンピュータ上での試作実装の成果とを学位論文にまとめ,所属研究機関から学位(哲学博士)を9月に取得した.
また本年度の後半は,産業技術総合研究所・システム検証研究センターに移籍し,これまでの論理的・形式的検証の研究を活かしながらソフトウェアの機能安全に関する研究を行った.特に,平成18年度より始まった「戦略的基盤技術高度化支援事業(サポートインダストリ)」のプロジェクトに参加し,機能安全規格IEC61508に準拠した車載用オペレーティングシステム及びミドルウェアの開発における安全性の適合性評価の基礎研究を行った.このプロジェクトで得られたオペレーティングシステムや通信ネットワークの知識をもとに,本研究課題の成果を実時間システムの安全性検証法の研究に繋げて行きたい.また他方で,本年度の前半まで主に研究をしてきた通信プロトコルの安全性検証法について,近年盛んに行われている計算量的アプローチによる通信プロトコルの安全性検証の試みを,Basic Protocol Logicの意味論に取り込む研究を行った.その基本的なアイデアは,通信プロトコルにおいて交換されるメッセージを代数的・記号的なモデルから確率論的なモデルへ拡張することにより暗号の強度に応じた安全性の検証を行うというものであり,今後も継続して研究を行う予定である.
|
Report
(3 results)
Research Products
(7 results)
