匿名性・プライバシ保護の数理的技法

高度情報ネットワーク社会の到来により，私たちの個人情報（氏名・ID・パスワード・生体認証情報・位置情報・アクセス履歴情報など）は際限なくネットワークに吸収され続けています．個人情報が適切に利用される仕組みを実現するためには，法制度の検討や社会科学的考察を含む総合的なアプローチが必要ですが，私たちはこの課題に技術的側面から取り組んでいます．

匿名性を確保する方法やプライバシを保護する方法には多くの研究成果があり，それらに基づいて設計された通信システムも多数存在します．数理的技法（Formal Methods，形式手法とも訳されます）は，数理論理学に基づいて厳密にモデル化・分析・検証する手法であり [1]，これまで直観的に「匿名性・プライバシを保護している」と思われてきたそれら既存の方法やシステムを見つめ直し，その安全性を強固にするのに役立ちます [2, 3]．

電子投票プロトコルを例題として

私たちは，通信システムの匿名性を，ある通信者の特定の動作が他の任意の通信者も行いうることとして定義し，これを定理証明器上で帰納法によって証明する方法を考案しました [4, 5]．従来法と異なり，通信参加者の総数に上限を置くことなく検証可能であるという特徴があります．この方法をさらに発展させ，藤岡・岡本・太田の電子投票プロトコル（FOOプロトコル）の匿名性を検証しました [6, 7, 8, 9]．また，この検証手法を能動的な攻撃者が存在する場合に拡張する [10] ことを通じて，電子投票プロトコルの無証拠性を検証する方法についても検討を進めています [11, 12, 13]．

匿名性・プライバシの双対性

私たちはさらに，匿名性・プライバシについての理解を深めるため，知識論理の枠組みでこれらを考察しました．まず，プライバシを匿名性の双対概念として定式化し，両者が役割交換可能性という別の基本概念から双対性を通じて導かれることを明らかにしました．さらに役割交換可能性の証明方法を考案し，これを適用することにより，藤岡・岡本・太田の電子投票プロトコル（FOOプロトコル）の匿名性・プライバシを示しました [14, 15]．

匿名性・プライバシから顕名性・アイデンティティへ

これらの考察をさらに発展させ，匿名性・プライバシおよび（それらの反対概念と位置付けられる）顕名性・アイデンティティを包括的に含むフォーマルな概念マップを，知識論理に基づき作成することにも取り組んでいます [16, 17, 18, 19]．これらの研究を通じ，PfitzmannとHansenによる標準用語集 [20] を理論的な視点から整備することを目指しています．

参考文献

[1] 塚田恭章 (編), 特集 フォーマルメソッドの新潮流, 情報処理, Vol. 49, No. 5 (May 2008) 491-543. [Online Magazine]

[2] 塚田恭章, 真野健, 河辺義信, 櫻田英樹, 匿名性とプライバシ保護の数理的技法, NTT技術ジャーナル, Vol. 19, No. 6 (June 2007) 38-40. [Abstract]

[3] 塚田恭章, 真野健, 櫻田英樹, フォーマルメソッドによるセキュリティ＆プライバシ, NTT技術ジャーナル, Vol. 23, No. 9 (September 2011) 22-25. [Abstract]

[4] 河辺義信, 真野健, 櫻田英樹, 塚田恭章, 無限状態システムの匿名性検証, 第18回 回路とシステム軽井沢ワークショップ (電子情報通信学会 基礎・境界ソサイエティ, April 2005) pp. 293-298.

[5] Yoshinobu Kawabe, Ken Mano, Hideki Sakurada, and Yasuyuki Tsukada, Theorem-proving anonymity of infinite-state systems, Information Processing Letters, Vol. 101, Issue 1 (January 2007) 46-51. [Abstract]

[6] 河辺義信, 真野健, 櫻田英樹, 塚田恭章, バックワード匿名シミュレーションを用いた匿名性の検証, 日本ソフトウェア科学会第22回大会講演論文集 (日本ソフトウェア科学会, September 2005) CD-ROM Publication (ISSN 1348-0901) 7B-2.

[7] 河辺義信, 真野健, 櫻田英樹, 塚田恭章, シミュレーション技法によるセキュリティプロトコルの匿名性検証法, コンピュータセキュリティシンポジウム 2005, 情報処理学会シンポジウムシリーズ, Vol. 2005, No. 13 (情報処理学会, October 2005) pp. 43-48. [優秀論文賞 受賞]

[8] Yoshinobu Kawabe, Ken Mano, Hideki Sakurada, and Yasuyuki Tsukada, Backward simulations for anonymity, in: D. Gollmann and J. Jürjens, editors, Sixth IFIP WG 1.7, GI FoMSESS Workshop on Issues in the Theory of Security (WITS '06) (March 2006) pp. 206-220. [Abstract]

[9] Yoshinobu Kawabe, Ken Mano, Hideki Sakurada, and Yasuyuki Tsukada, On backward-style anonymity verification, IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, Vol. E91-A, No. 9 (September 2008) 2597-2606. [Abstract]

[10] 河辺義信, 真野健, 櫻田英樹, 塚田恭章, 能動的な攻撃者が存在するシステムに対する匿名性の検証について, 2008年暗号と情報セキュリティシンポジウム (電子情報通信学会情報セキュリティ研究専門委員会, January 2008) CD-ROM Publication 2F2-5.

[11] 河辺義信, 真野健, 櫻田英樹, 塚田恭章, I/O-オートマトンによる無証拠性の形式化について, 2009年暗号と情報セキュリティシンポジウム (電子情報通信学会情報セキュリティ研究専門委員会, January 2009) CD-ROM Publication 4C2-5.

[12] 河辺義信, 真野健, 櫻田英樹, 塚田恭章, 電子投票プロトコルに対する無証拠性の定理証明, コンピュータセキュリティシンポジウム 2010, 情報処理学会シンポジウムシリーズ, Vol. 2010, No. 9 (情報処理学会, October 2010) pp. 573-578.

[13] 河辺義信, 真野健, 櫻田英樹, 塚田恭章, 電子投票プロトコルに対する無証拠性の定理証明, 情報処理学会論文誌, Vol. 52, No. 9 (September 2011) 2549-2561. [Abstract]

[14] Ken Mano, Yoshinobu Kawabe, Hideki Sakurada, and Yasuyuki Tsukada, Role interchangeability and verification of electronic voting, 2006年暗号と情報セキュリティシンポジウム (電子情報通信学会情報セキュリティ研究専門委員会, January 2006) CD-ROM Publication 4D2-1.

[15] Ken Mano, Yoshinobu Kawabe, Hideki Sakurada, and Yasuyuki Tsukada, Role interchange for anonymity and privacy of voting, Journal of Logic and Computation, Vol. 20, Issue 6 (December 2010) 1251-1288. [Abstract]

[16] 塚田恭章, 真野健, 櫻田英樹, 河辺義信, 匿名性・プライバシ・顕名性・アイデンティティへの知識論理的アプローチ, コンピュータセキュリティシンポジウム 2008, 情報処理学会シンポジウムシリーズ, Vol. 2008, No. 8 (情報処理学会, October 2008) pp. 599-604.

[17] Yasuyuki Tsukada, Ken Mano, Hideki Sakurada, and Yoshinobu Kawabe, Anonymity, privacy, onymity, and identity: A modal logic approach, in: Proceedings of the 2009 IEEE International Conference on Privacy, Security, Risk and Trust (PASSAT-09) (IEEE Computer Society Press, August 2009) pp. 42-51. [Abstract] [Slides (PDF)]

[18] Yasuyuki Tsukada, Ken Mano, Hideki Sakurada, and Yoshinobu Kawabe, Anonymity, privacy, onymity, and identity: A modal logic approach, Transactions on Data Privacy, Vol. 3, Issue 3 (December 2010) 177-198. [Abstract]

[19] 塚田恭章, 櫻田英樹, 真野健, 真鍋義文, 匿名性とプライバシの合成可能性について, 日本応用数理学会 2011年春の研究部会連合発表会 (March 2011).

[20] Akiko Orita, Ken Mano, and Yasuyuki Tsukada, Translation of essential terms to Japanese, in: A. Pfitzmann and M. Hansen, A terminology for talking about privacy by data minimization: Anonymity, Unlinkability, Undetectability, Unobservability, Pseudonymity, and Identity Management, Version v0.34 (August 2010) pp. 74-78. [Anon Terminology Website]