2015 Fiscal Year Research-status Report
セキュリティプロトコルの時間匿名性に対する形式検証法の研究
| Project/Area Number |
26330166
|
|---|
| Research Institution | Aichi Institute of Technology |
|---|
Principal Investigator |
河辺 義信 愛知工業大学, 情報科学部, 准教授 (80396184)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
伊藤 暢浩 愛知工業大学, 情報科学部, 教授 (40314075)
|
|---|
| Project Period (FY) |
2014-04-01 – 2017-03-31
|
| Keywords | 匿名性 / 実時間システム / 時間匿名性 / 形式検証 / セキュリティプロトコル |
|---|
| Outline of Annual Research Achievements |
従来，プログラム理論やソフトウェア工学の分野においては，ソフトウェアの正しさを論理的に検証する手法（形式手法，数理的技法，あるいはフォーマルメソッドなどと呼ばれる）が研究されており，当該研究分野の中心テーマのひとつとなっている．なかでも，暗号プロトコルを対象とした形式手法は世界的な注目を集めており，秘匿性（盗聴した暗号文を度のように組み合わせても平文を取り出すことができないこと）などが研究されている．
本研究では，スマートフォン，ロボット，車載ソフトウェア等のいわゆる実時間システムに対する匿名性（「誰がやったのかがわからない」ことを示す，プライバシの基本的な性質），すなわち時間匿名性を対象とし，そのモデル化と効率的な検証手法の開発を行うことで，安全・安心なＩＣＴ社会の構築に貢献することを目指している．二年目にあたる平成２７年度では，前年度にモデル化の事例研究として行った実時間システムを題材に，Ｉ／Ｏオートマトン理論で開発されているシミュレーション技法によるトレース包含の証明手法を適用することで，その正しさを検証した．この検証実験は直接匿名性を示すものではなかったものの，トレース集合で表される性質一般を対象としており，トレース集合の持つ性質として定義できる匿名性も同様に検証できると考えられる．これにより，時間匿名性を自動あるいは半自動で検証するための一定の目処が立ったと言える．一方で今年度には，時間匿名性検証技術の適用分野の探索として，複数のロボットを実時間制御するアルゴリズムの提案・評価を行った．具体的には，ＳＣＲＡＭと呼ばれるアルゴリズムを，ロボットの故障・交代を考慮するよう拡張（ＢＡＲアルゴリズム）し，その有効性を確認している．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
今年度は，初年度にモデル化を行った実時間システム（エンジン制御ユニットのソフトウェア）を題材・対象として，時間パラメータを持つシステムに対するトレース包含に関する証明実験を行ったことになる．今回の実験結果は，トレース集合で表される性質一般についての仕様と実装の対応関係の検証に相当し，これは匿名性（トレース集合の性質として定義可能）にも直接的に拡張・適用できると考えられる．とくに，本研究で今年度に行った検証実験を通じ，我々は時間パラメータの扱いや時間パラメータを変更・更新するアクションの扱いについて，とくに定理証明ソフトウェアを用いる際にどのようにすればよいか，ノウハウを得ることができた．前年度では，実時間システムを従来型の（無限状態を許す）Ｉ／Ｏオートマトンとして記述して匿名性を示すという方向性をとっている．今年度は，この方向性に沿ってさらにすすめ，時間匿名性のモデル化と検証にあたり本質的にどのような項目を示すべきか，また今回得られたノウハウをどのように活用すればよいか，その方針を明らかにできたと言える．最終年度には，時間匿名性検証理論を完成させることで，この方針を具体的にまとめてゆく．一方で今年度には，実時間システムを対象とした匿名性検証の題材の探索として，災害救助ロボットなどを対象とするロボカップレスキューの分野から，自律分散ロボットの協調行動に関するアルゴリズムの検討を行っている．このアルゴリズムは，実時間システムとして動作する全ロボットの行動終了時刻が最も早くなるように，各ロボットの移動先を割り当てるものである．時間匿名性検証の今後の有力な検証候補と言える．
|
| Strategy for Future Research Activity |
今後は，前年度および今年度において明らかにした時間システムのモデル化方法や時間匿名性の検証条件をまとめることで，さまざまなセキュリティプロトコル，分散システム，および分散アルゴリズム（実時間システム）の時間匿名性の検証理論を完成させる．これは，無限状態システムや有限非有界システムに対する時間匿名性の検証を可能とすることを想定しつつ，定理証明ソフトウェアを使った半自動の検証技術とする予定である．また，適切な規模の検証実験を行い，有効性を示してゆきたい．
|
| Causes of Carryover |
研究分担者の海外出張旅費（国際会議参加）について，初年度と同程度の金額の旅費を見込んでいたが，今年度は中国開催と比較的近場であったことから，出張旅費が想定よりも少なく済む形となった．また，初年度に持ち越したコンピュータ購入についても，ひとまず今年度行った予備実験向けには，研究代表者の現状手持ちの設備で実験が完了できたため，購入を見送っている．
|
| Expenditure Plan for Carryover Budget |
最終年度ということもあり，成果発表等の出張旅費に多くを当てたいと考えている．また，最終実験実施用およびデモ用としてのコンピュータの購入を考えている．
|
