2011 Fiscal Year Research-status Report
| Project/Area Number |
23700024
|
|---|
| Research Institution | Aichi Institute of Technology |
|---|
Principal Investigator |
河辺 義信 愛知工業大学, 情報科学部, 准教授 (80396184)
|
|---|
| Project Period (FY) |
2011-04-28 – 2014-03-31
|
| Keywords | プライバシ / 形式検証 / 無証拠性 / 定理証明 / セキュリティプロトコル |
|---|
| Research Abstract |
従来，プログラム理論やソフトウェア工学の分野においては，ソフトウェアの正しさを論理的に検証する手法（形式手法．数理的技法とも呼ばれる．）が研究されており，当該分野の中心テーマの一つとなっている．なかでも，暗号プロトコルを対象とした形式手法が世界的な注目を集めており，秘匿性（盗聴した暗号文をどのように組み合わせても平文を取り出せないこと）などが研究されている． 本研究では，セキュリティの重要な性質である「プライバシ」を，形式手法を用いて自動検証する技術を確立することで，安全・安心なICT社会の構築に貢献することを目指している．本年度は，電子投票プロトコルのプライバシに関する性質として知られる「無証拠性」を題材に，計算機を用いた検証実験を行った．具体的には，予備研究の段階から進めてきた電子投票プロトコル（Leeらの電子投票プロトコル）の検討をもとに，電子投票プロトコルの動作仕様をI/O-オートマトンを用いて形式化し，一階述語論理式に変換した．さらに，定理証明ソフトウェアを用いて匿名性を証明することで，電子投票プロトコルの無証拠性を半自動的に検証した．この証明には，研究代表者らの先行研究の手法（匿名シミュレーション法）を利用しているが，この手法は無限状態システムや有限非有界システムに対しても適用可能である．そのため，本研究のプライバシ検証の結果は，有限の限られた投票者数の場合のみならず，多数（数千万人・数億人単位）の投票者を考慮する場合においても成立する． また，無証拠性はプライバシの一種であるが，投票者が攻撃者に情報を漏らす（ただし，真の情報を漏らすとは限らない）という条件下での匿名性と考えられる．これに関連して，本研究では，投票者の情報漏洩の仕方に関する条件を明らかにすることができた．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
プライバシに属する様々な性質（無証拠性，耐買収性，狭義のプライバシなど）は匿名性の一種とみなせることから，本研究では，既存の匿名性検証手法（研究代表者らは，システムの実行ステップ数に関する帰納法で匿名性を検証する手法を提案している）をプライバシの検証に適用することを目指している． 平成23年度の計画では，電子投票プロトコルを題材にして無証拠性を形式化し，さらに計算機で（半）自動検証できるようにすることを目指した．実際にLeeらの電子投票プロトコルを題材とした形式化および検証実験を実施し，その検証実験を通じて無証拠性の「前提条件」を明らかにすることができた． 上記の状況から，研究はおおむね順調に進展したものと考える．
|
| Strategy for Future Research Activity |
今後は，他のセキュリティプロトコル（Crowdsなどの匿名通信路やネットオークションプロトコルなど）を題材としたプライバシ検証実験をすすめるとともに，これらの検証実験を通じて，プライバシを匿名性検証技術で扱うための各種の前提条件を明らかにしたい．また，プライバシの検証方式について，初年度は定理証明ソフトウェアを利用したが，他のツール（モデル検査ツールやSMTソルバなど）を利用した実験も検討したい． なお，当初の研究計画では，まずネットオークションプロトコルを題材にすることを計画していたが，現時点では，匿名通信路に対する検証実験を先行して行う予定である．実際に，本報告の執筆時点においては，Crowdsおよびその拡張に対する形式化をすすめている．ただし，その他のセキュリティプロトコルに対しても，適宜，形式化と検証をすすめてゆく予定である．
|
| Expenditure Plans for the Next FY Research Funding |
次年度では，研究費は研究成果の発表等を行うための旅費（国内・国外）・学会参加費・準備（論文の英文添削など）に使用する計画である．さらに，データ処理用計算機（UNIX OSが動作する計算機のなかから検討する）および実験に必要な基本ソフトウェア（VMWare Fusionなど）の購入を計画している．
|
