オープンハウス×未来想論2008
トップページ
ごあいさつ
プログラム
アクセス
お問合わせ
個人情報の取り扱いについて
What's New
2008/6/18
ライブ配信でお送りした「所長講演」及び「未来想論」の映像を、ビデオアーカイブとして公開致しました。

2008/5/29
各テーマ展示ページを更新致しました。より一層充実した内容で、展示情報をお知らせしています。

2008/5/21
アクセスにバス時刻表を追加致しました。

各テーマ展示ページに展示紹介ムービーを追加致しました。
2008/5/19
ストリーミングLive配信のお知らせを公開致しました。
2008/4/14
ごあいさつプログラムどんな展示があるの?会場案内を公開致しました。

2008/3/17
オープンハウス×未来想論2008のホームページを開設致しました。

プログラム一覧 どんな展示があるの?
フォーマルメソッドの新潮流
展示会場地図
会場MAPへ
概要
情報システムが複雑になるにつれ、それが仕様通りに動作するかどうかの検証が非常に困難になります。ミッションクリティカルな情報システムの場合、生命や財産を脅かすことにもなりかねません。フォーマルメソッドは、厳密な検証手段として注目を浴びつつあります。

今回は、フォーマルメソッドを、匿名性・プライバシの検証(話題1)や、デジタル著作権記述/管理の検証(話題2)に適用した例を展示しています。
展示に関連する技術資料,研究論文など
ここでは,展示「フォーマルメソッドの新潮流」でご説明した内容について,さらに深く知りたいという方に対し,技術資料や論文等をご紹介致します.

フォーマルメソッドについて知りたい方

【解説資料】 塚田恭章, 真野健, 河辺義信, 櫻田英樹: 匿名性とプライバシ保護の数理的技法. 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について分かりやすく説明したビデオです.展示会場で上映していたのと同じものです.
匿名性・プライバシのフォーマルメソッド ※ビデオをご覧になるには、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秒


用語解説

  • 匿名性
    特定のアクションを,誰が実施したのか分からないという性質
  • プライバシ
    特定の人物が,何を実施したのか分からないという性質
  • クリエイティブ・コモンズ
    コンテンツを再利用しやすいライセンスの一種.また,その枠組みを提供するプロジェクトや非営利団体を指す.
  • 多種論理
    一階述語論理に,変数や定数の領域を設定できるよう拡張を施した論理体系.
  • 形式意味論
    対象とする概念に対し,その解釈を特定の論理体系で表現したもの.
藤田 邦彦
藤田 邦彦

人間情報研究部 情報基礎理論研究グループ