2013 Fiscal Year Annual Research Report
| Project/Area Number |
22300005
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
住井 英二郎 東北大学, 情報科学研究科, 准教授 (00333550)
|
|---|
| Project Period (FY) |
2010-04-01 – 2015-03-31
|
| Keywords | 理論計算機科学 / 計算モデル / 分散プロセス計算 |
|---|
| Research Abstract |
環境双模倣(environmental bisimulation)の主要な応用の一つである、高階(higher-order)ないし一階(first-order)の暗号プロセス計算におけるセキュリティプロトコルの形式的検証を、より現実的・実用的な手法とするため、一般的な技術書等でしばしば用いられる「ナレーション記法」から、形式的なプロトコル記述・検証体系であるAbadiとGordonのspi計算（の一種）への機械的変換アルゴリズムを定義・定式化した。同様の変換は住井・立沢・米澤による研究[情報処理学会論文誌：プログラミング45(SIG12(PRO23)):1-10]や、Briais-Nestmannによる研究[TGC'05]もあるが、本研究はより一般的・より機械的（人手による注釈が少ない）であり、セキュリティに関する基礎理論の主要研究者が多く集まるワークショップFCS'13において全15頁の査読つき論文が予稿集に採録、口頭発表された。
また、セキュリティプロトコルの秘密性(secrecy)や真正性(authenticity)といった性質だけでなく、認可(authorization)プロトコルの正しさの一種を検証するFournet-Gordon-Maffeisの理論[CSF'07]を、現実的な認可プロトコル例に適用するとともに、その際に必要となった自明でない拡張に関する研究を行った（未発表、今後発表予定）。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究課題の第一義的な研究目的は「研究代表者らの環境双模倣の理論を発展させ、公開通信路上でソフトウェアを送受信・実行する高階オープンシステムを数理的に検証する基盤を確立する」ことである。その中心となる分散（すなわちロケーションつきの）高階π計算における環境双模倣の理論は、すでに確立されている[Pierard-Sumii LICS'12]。一方、「現実的なソフトウェアの（少なくとも）本質的な部分を実際に検証することができるツールを開発する」という部分については、人手による証明は論文においていくつか示したものの、まだ「ツール」と呼べるようなものが完成するには至っておらず、次年度の課題である。
|
| Strategy for Future Research Activity |
環境双模倣の機械的検証に向けて、定理証明支援器Coq上で環境双模倣の定義を形式化し、いくつかの例を形式的に証明する。具体的にはSatoとSumiiの高階値呼び応用π計算[Sato-Sumii APLAS'09]とその環境双模倣をCoq上で定義し、当該論文の二つの主な例（ソフトウェアアップデートシステムおよびWebメールシステム）の環境双模倣による安全性証明を形式化する。環境双模倣は様々な（高階の）言語に対して定義することが可能だが、高階値呼び応用π計算およびそれに対する環境双模倣は最も定義が複雑なものの一つであり、人手による証明は誤りが起きやすいと考えられる。Coq上で定義および自明でない例の証明を形式化し、それらに必要なライブラリを整備することにより、誤りの可能性が極めて小さい検証ツールを提供するとともに、その有効性を確認する。
|
