TOP > 研究報告検索 > 等式付木構造自動機械にもとづく自動検証器

等式付木構造自動機械にもとづく自動検証器

研究報告コード R070000226
整理番号 R070000226
掲載日 2008年4月11日
研究者
  • 大崎 人士
研究者所属機関
報告名称 等式付木構造自動機械にもとづく自動検証器
報告概要 高度情報化社会の基盤となる通信システムが安全かつ確実に動作することは,ますます重要になっています。銀行システム,電子商取引などの経済活動にとどまらず,交通システム,通信システムや国防システムにいたるまで,あらゆる場面で通信ネットワークの障害は社会生活に深刻な影響を及ぼします。インターネットのような,公衆ネットワーク回線を通じての通信においては,特に,暗号化による通信の秘密の保護が必要ですが,そこでは破られにくい暗号法の技術と共に,暗号化法を通信網の中で正しく生かして使う技術が必要です。例えば,正規の(想定する)データ受取人になりすまして,暗号を解くための鍵を不正に入手されるようでは,いかに破られにくい暗号法を使用していても,データの秘匿性を保つことはできません。つまり,鍵を不正に入手して略号化されたデータを入手されるなどという攻撃を避けるための技術が要請されます。これを「通信手順の安全性」といいます。通信手順の安全性を確保することは,解読が困難な暗号化法を考案する技術とは独立のものです。なぜなら,秘密のデータを暗号化して受信者に伝えるとしても,暗号法には復号法が必ずあり(さもないと受信者はデータを読み取れない),復号化の方法も受信者に伝える必要があります。このときに,暗号化にもちいるトリック(多くの場合は,鍵)を横取りされないような通信手順が必要となるのです。ここで問題となるのは,「なりすまし」などの悪意の第三者からの攻撃が決して成功しないことをどのようにして確かめるのかです。本研究では,情報科学における基礎技術を応用して,情報システムの安全性を検証するための技術について研究しました。具体的には,書換系およびツリーオートマトンの理論による数理的基礎を発展させて,リアクティブシステムの安全性を自動的に検証するための技術を開発し,実際に,自動検証ソフトウエアACTAS(「検証システム」と呼ぶ)を作成しました。
画像

※ 画像をクリックすると拡大します。

R070000226_01SUM.gif R070000226_02SUM.gif R070000226_03SUM.gif R070000226_04SUM.gif
研究分野
  • オートマトン理論
  • 計算機システム開発
関連発表論文 (1) 大崎人士,Jean-Marc Talbot, Sophie Tison, Yves Roos : “Monotone AC-Tree Automata”. In proceedings of 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'05), Montego Bay (Jamaica). Lecture Notes in Computer Science, Springer-Verlag (2005年12月発表予定)
(2) 大崎人士,高井利憲:“ACTAS: A System Design for Associative and Commutative Tree Automata Theory”. In proceedings of 5th International Workshop on Rule-Based Programming (RULE'04) , Electronic Notes in Theoretical Computer Science, 124巻,97-111頁,Elsevier Science, 2005.
(3) 大崎人士,関浩之,高井利憲:“Recognizing Boolean Closed A-Tree Languages wlth Membership Conditional Rewriting Mechanism”. In proceedings of 14th International Conference on Rewriting Techniques and Applications (RTA'03) , Lecture Notes in Computer Science, 2706巻, 483-198頁,Springer-Verlag, 2003.
(4) 大崎人士,高井利憲:“Equational Tree Automata: Towards Automated Verification of Network Protocols”.京都大学数理解析研究所講究録,1318号,48-52頁,京都大学,2003.
(5) 大崎人士,高井利憲:“Decidability and Closure Properties of Equational Tree Languages”. In proceedings of 13th International Conference on Rewriting Techniques and Applications (RTA'02) , Lecture Notes in Computer Science, 2378巻,114-128頁,Springer-Verlag, 2002 .
(6) 大崎人士,Joe Hendrix Jose Meseguer : “Sufficient Completeness Checking with Propositional Tree Automata”. 産業技術総合研究所研究速報 AIST-PS-2005-013,産業技術総合研究所,2005.
研究制度
  • 戦略的創造研究推進事業 さきがけタイプ(旧若手個人研究推進事業を含む)/機能と構成
研究報告資料
  • 大崎 人士. 等式付木構造自動機械にもとづく自動検証器. 個人型研究さきがけタイプ研究報告会 先進情報システムとその構成に向けて 「機能と構成」領域 講演要旨集 第Ⅲ期研究者(研究期間2002-2005), 2005. p.25 - 32.

PAGE TOP