概要
インターネット上で投票やショッピングなどのサービスを安心して利用するためには、安全性の十分な確保が不可欠です。特に、利用者の匿名性やプライバシー保護は、情報システム設計における重要課題です。私たちは、匿名性・プライバシーを、行為者と行為内容の結びつきに関する情報の隠ぺいととらえ、フォーマルに定式化し検証する手法を考案しました。このようなとらえ方では、匿名性とプライバシーは互いに対称な性質（数学では双対と呼ばれる）となります。この対称性は、検証要件の定式化に明快なパースペクティブを与えるとともに、検証作業の効率化にも役立つことがわかりました。
特徴
- 匿名性とプライバシーを数理的な手法でフォーマルに定式化し厳密に検証
- 知識論理によって、システムが満たすべき性質を柔軟に記述可能
- 匿名性とプライバシーの対称性（双対性）を利用して、効率的に検証
- インターネット電子投票プロトコルFOOの匿名性とプライバシーの検証に成功
利用シーン
- 電子商取引、電子政府など高い安全性を求められる情報システムの高信頼化
- 個々のシステムに固有の匿名性・プライバシー要件を、知識論理でフレキシブルに記述
- ISO情報技術セキュリティ評価基準のクリア
- 高い評価保証レベル（EAL5以上）のクリアには、フォーマルメソッドが必要
- プライバシー権侵害にかかわる、法的要請と技術的要請の対応を明確化
- 論理的表現を介して、法的な議論と技術的な議論を橋渡し
