電子投票プロトコルに対する無証拠性の定理証明
スポンサーリンク
概要
- 論文の詳細を見る
電子投票プロトコルの満たすべき性質に,無証拠性があげられる.これは匿名性の拡張で,「プロトコルを観測して得られる情報に加えて,別の付加的な情報を投票者が外部に与えたとしても,ある投票パターンと別の(結果が同じとなる)投票パターンが区別できない」という性質である.本稿では,Leeらの電子投票プロトコルを題材とし,その無証拠性を定理証明器で形式的に検証する.
- 2011-09-15
著者
-
真野 健
NTTコミュニケーション科学基礎研究所
-
河辺 義信
日本電信電話株式会社nttコミュニケーション科学基礎研究所
-
櫻田 英樹
Nttコミュニケーション科学基礎研究所
-
櫻田 英樹
日本電信電話株式会社nttコミュニケーション科学基礎研究所
-
真野 健
日本電信電話株式会社NTTコミュニケーション科学基礎研究所
-
塚田 恭章
日本電信電話株式会社NTTコミュニケーション科学基礎研究所
-
塚田 恭章
日本電信電話(株)nttコミュニケーション科学基礎研究所
-
河辺 義信
愛知工業大学情報科学部情報科学科
-
河辺 義信
愛知工業大学 情報科学部 情報科学科
関連論文
- 確率様相論理による秘匿性の証明 (代数と言語のアルゴリズムと計算理論)
- モデル検査を用いたタグVLANの設定検査(ネットワークサービス基礎)
- タグスイッチネットワークのモデル検査による漏曳検査(セッション3)
- 確率様相論理による秘匿性の証明
- コンピュータサイエンスシリーズ 15 離散数学, 牛島和夫(編著), 相利民, 朝廣雄一(著), コロナ社(2006-09), A5判, 定価(本体3,000円+税)
- ニコニ・コモンズとクリエイティブ・コモンズの比較及びそれらの形式意味論(セッション5(EIP))
- クリエイティブ・コモンズ利用許諾の形式意味論
- SET支払いプロトコルの秘匿性検証(セキュリティプロトコル・電子公証)(新たな脅威に立ち向かうコンピュータセキュリティ技術)
- π計算に基づくプログラミング言語NepiのためのGUI機能
- 高階書換え系の単一正規形性
- 高階書き換え系の単一正規形性
- Nepi : π計算に基づくネットワーク・プログラミング言語
- ゲーム列による安全性証明の形式化と自動化(数理的技法による情報セキュリティ)
- 匿名性とプライバシ保護の数理的技法 (特集 コミュニケーション環境の未来に向けた研究最前線)
- ETAPS 2006参加報告(会議レポート)
- Nepiネットワークプログラミングシステムの形式的検証(ソフトウェア工学の基礎)
- π-計算の名前制限の名前生成による実装の正しさ
- プロセス代数に基づくネットワークプログラム言語 (特集論文1 情報科学研究の最前線--より安全で快適な情報処理技術を目指して) -- (快適にコンピュータを使えるために)
- π-計算に基づくモバイルエージェントの形式化
- アクタモデルのπ計算に基づく意味づけ : エージェントの形式化に向けて
- 関数部分知識と匿名性検証(理論,数理的技法による情報セキュリティ,平成19年研究部会連合発表会)
- 攻撃者を考慮した匿名性検証法 (第20回 回路とシステム軽井沢ワークショップ論文集) -- (形式的手法)
- プロセス代数を用いたセキュリティ・プロトコル記述
- 文脈計算の環境計算による解釈
- 編集にあたって(フォーマルメソッドの新潮流)
- 「数理的技法による情報セキュリティ」研究部会の紹介(研究部会だより)
- 対話型安全性証明つきプログラム配信方式における証明の秘匿とその応用(セキュリティ基盤技術)
- チャネルに基づく選択付き通信のための分散プロトコル
- Nepi^2: π計算に基づくネットワーク・プログラミングのための2レベル計算体系
- 電子投票プロトコルに対する無証拠性の定理証明
- 2006年読者モニタについて
- 安全なモバイルプログラム方式の理論 (特集論文1 情報科学研究の最前線--より安全で快適な情報処理技術を目指して) -- (安心して暮らせるネットワーク社会のために)
- フォーマルメソッドによるセキュリティ&プライバシ (特集 20周年を迎えたコミュニケーション科学)
- 「情報処理学会論文誌 : プログラミング」の編集について
- 匿名性・プライバシーの工学的定式化とその学際的応用
- CoSyProofs 2009参加報告(会議レポート)
- 認知変数連結論 : 認知心理学を見つめ直す, 中島義明(著), コロナ社(2007-11), B6判, 定価(本体2,600円+税)
- 6. 匿名性とプライバシのためのフォーマルメソッド(Part III:新領域の開拓,フォーマルメソッドの新潮流)
- 順序ソート項書換え系における合流性のモジュラ性
- 確率様相論理による秘匿性の証明
- 電子投票プロトコルに対する無証拠性の定理証明 (特集 人と共存するコンピュータセキュリティ技術)
- コンシェルジュサーバを持つ電話システムの形式的検証
- AT-1-2 Larch Proverによる論理パズルの解法(AT-1.システム数理における様々なツールの紹介,チュートリアルセッション,ソサイエティ企画)
- 素性構造に基づいたアクセス制御モデルの提案
- コンシェルジュサーバを持つ電話システムの形式的検証