ダイナミックに変化する知識・信念の論理学的分析手法の研究

知识信念动态变化的逻辑分析方法研究

基本信息

批准号：
04J07439
负责人：
長谷部浩二
金额：
$ 2.18万
依托单位：
National Institute of Advanced Industrial Science and Technology (2006)Keio University (2004-2005)
依托单位国家：
日本
项目类别：
Grant-in-Aid for JSPS Fellows
财政年份：
2004
资助国家：
日本
起止时间：
2004 至 2006
项目状态：
已结题

项目摘要

本年度の前半は,昨年度に引き続き論理的・形式的手法による通信プロトコルの安全性検証法の研究を行った.特に昨年度の研究成果として提起した一階述語論理を基にした論理推論体系Basic Protocol Logicを基にした安全性検証法を中心に,その理論的成果とコンピュータ上での試作実装の成果とを学位論文にまとめ,所属研究機関から学位(哲学博士)を9月に取得した.また本年度の後半は,産業技術総合研究所・システム検証研究センターに移籍し,これまでの論理的・形式的検証の研究を活かしながらソフトウェアの機能安全に関する研究を行った.特に,平成18年度より始まった「戦略的基盤技術高度化支援事業(サポートインダストリ)」のプロジェクトに参加し,機能安全規格IEC61508に準拠した車載用オペレーティングシステム及びミドルウェアの開発における安全性の適合性評価の基礎研究を行った.このプロジェクトで得られたオペレーティングシステムや通信ネットワークの知識をもとに,本研究課題の成果を実時間システムの安全性検証法の研究に繋げて行きたい.また他方で,本年度の前半まで主に研究をしてきた通信プロトコルの安全性検証法について,近年盛んに行われている計算量的アプローチによる通信プロトコルの安全性検証の試みを,Basic Protocol Logicの意味論に取り込む研究を行った.その基本的なアイデアは,通信プロトコルにおいて交換されるメッセージを代数的・記号的なモデルから確率論的なモデルへ拡張することにより暗号の強度に応じた安全性の検証を行うというものであり,今後も継続して研究を行う予定である.

今年上半年，我们继去年的基础上，利用逻辑和形式化方法对通信协议的安全验证方法进行了研究。特别是，我们开发了基于一阶谓词逻辑的逻辑推理系统Basic Protocol，这是去年作为研究成果提出的。他专注于基于Logic的安全验证方法，在博士论文中总结了自己的理论成果和在计算机上原型实现的结果，并于9月下旬从所属研究机构获得了学位（哲学博士学位）。今年，产业技术综合研究所系统验证研究中心2006年转入“战略基础技术支撑产业”，利用之前在逻辑和形式验证方面的研究成果，进行软件功能安全方面的研究，参与了“功能安全标准I”项目。我们在符合EC61508的车载操作系统和中间件的开发中进行了安全合规性评估的基础研究。基于从该项目中获得的操作系统和通信网络的知识，我们将利用操作系统和通信网络的知识在这个项目中获得的成果来评估这个研究课题的成果。我想把这个和时间系统的安全验证方法的研究联系起来。另一方面，我想利用近年来流行的计算方法来研究通信协议的安全验证方法，我主要研究了通信协议的安全验证方法。直到今年上半年才开始研究尝试验证通信协议的安全性，Basic。我们进行了研究以纳入协议逻辑的语义。基本思想是将通信协议中交换的消息从代数/符号模型扩展到概率模型，从而允许根据我们计划的加密强度来交换消息。以便将来继续进行这项研究。