ここでは，展示「フォーマルメソッドの新潮流」でご説明した内容について，さらに深く知りたいという方に対し，技術資料や論文等をご紹介致します．
フォーマルメソッドについて知りたい方
【解説資料】 塚田恭章, 真野健, 河辺義信, 櫻田英樹: 匿名性とプライバシ保護の数理的技法. NTT技術ジャーナル, Vol.19, No.6, pp.38-40 (2007).
フォーマルメソッド（本資料内では「数理的技法」と呼んでいます）に関する基本的な説明が書かれています．また，本展示の話題1「匿名性・プライバシのフォーマル検証」についても解説しています．
【解説資料】 塚田恭章（編）: 特集 フォーマルメソッドの新潮流. 情報処理, Vol.49, No.5 (2008).
フォーマルメソッドの歴史から現在に至る流れについて説明されています．また，フォーマルメソッドの最新動向として，産業界への応用事例や，新しい適用分野（社会，匿名性・プライバシ，暗号）について紹介されています．
【解説資料】 特集 数理的技法による情報セキュリティ. 応用数理, Vol.17, No.4, pp.6-58 (2007).
暗号へのフォーマルメソッドの応用について，さらに詳しく知りたい方向けの解説論文集です．
話題1「匿名性・プライバシのフォーマル検証」に興味をもたれた方
【動画】 匿名性・プライバシのフォーマルメソッド
話題1について分かりやすく説明したビデオです．展示会場で上映していたのと同じものです．
 |
- 日本語 [ ブロードバンド / ナローバンド ]
- English [ ブロードバンド / ナローバンド ]
※ビデオをご覧になるには、Windows Media Player™が必要です。 |
【論文】 K. Mano, Y. Kawabe, H. Sakurada, Y. Tsukada: Role Interchangeability and Verification of Electronic Voting, 2006年暗号と情報セキュリティシンポジウム (2006).
暗号通信プロトコルにおいて，利用者の匿名性・プライバシを検証する方法を提案しています．匿名性と並ぶ重要な性質であるプライバシを，匿名性の双対概念として一般的な枠組で定式化したことが特長です．
【解説資料】 真野健: 匿名性とプライバシのためのフォーマルメソッド，情報処理, Vol.49, No.5 (2008). （
※利用上の注意事項）
匿名性とプライバシのためのフォーマルメソッド研究の最新動向を紹介しています．特に匿名性・プライバシのフォーマルな定式化の方法に焦点をあて，それらの法的な定式化との比較検討もおこなっています．
【論文】 H. Sakurada, M. Hagiya: Computationally Sound Symbolic Blind Signature, 3rd Franco-Japanese Security Symposium (2008).
ブラインド署名を使ったプロトコルの安全性を記号的に検証する方法を提案しています．また，この検証法によって安全であると判断されたならば，暗号学的（確率的・計算量的）にも安全であるという性質（健全性）を示しています．
話題2「デジタル著作権記述／管理をロジカルに」に興味をもたれた方
【論文】 藤田邦彦, 塚田恭章: クリエイティブ・コモンズ利用許諾の定式化, コンピュータセキュリティシンポジウム2007, 情報処理学会シンポジウムシリーズ, Vol.2007, No.10, pp.235-240 (2007). （
※利用上の注意事項）
クリエイティブ・コモンズのライセンス付与の条件について記述された利用許諾を対象に，多種論理を用いて定式化を行い，厳密な形式意味論を与えた結果について書かれています．
1分17秒
