2016 Fiscal Year Annual Research Report
Formal verification of anonymity for timed security protocols
| 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 |
従来，プログラム理論やソフトウェア工学の分野においては，ソフトウェアの正しさを論理的に検証する手法（形式手法，数理的技法，あるいはフォーマルメソッドなどと呼ばれる）が研究されており，当該研究分野の中心テーマのひとつとなっている．なかでも，暗号プロトコルを対象とした形式手法は世界的な注目を集めており，秘匿性（盗聴した暗号文を度のように組み合わせても平文を取り出すことができないこと）などが研究されている．
本研究では，スマートフォン，ロボット，車載ソフトウェア等のいわゆる実時間システムに対する匿名性（「誰がやったのかがわからない」ことを示す，プライバシの基本的な性質），すなわち時間匿名性を対象とし，そのモデル化と効率的な検証手法の開発を行うことで，安全・安心なＩＣＴ社会の構築に貢献することを目指している．最終年度にあたる平成２８年度では，時間匿名性のモデル化を行い，シミュレーション技法に基づく匿名性検証の適用を可能とした．具体的には，プロトコルの通信等の処理を行う部分（本体部と呼ぶ）に対して，時間経過・時間制約に関わる部分（時間部と呼ぶ）を記述・追加するモデル化手法を提案し，本体部の匿名性を示してから時間部まで含むシステムの時間匿名性にまで拡張する，段階的な検証手法を考案した．さらに，処理時間を考えない範囲では匿名性が成り立つが，処理時間に関する時間制約まで考慮すると匿名性が成り立たなくなるような例題を対象に，定理証明ソフトウェアＬａｒｃｈ Ｐｒｏｖｅｒを使った計算機による検証を行った．定理証明ソフトウェアを使った理由は，この例題の本体部は有限状態であるが，時間部まで加えたシステムは本質的に無限状態となるためである．対象としたシステムが時間匿名性を満たすには，時間制約の修正が必要である．この検証実験を通じて，時間制約に関する仕様の修正についてのノウハウを得ることもできた．
|
