日本応用数理学会2015年研究部会連合発表会
「数理的技法による情報セキュリティ」(FAIS)セッション
表記の研究集会を下記のとおり開催しますので, ご案内申し上げます.
【日時】
2015年3月7日(土) 9:40--10:50
なお, 研究部会連合発表会の全体の開催期間は
2015年3月6日(金)〜7日(土) となっております.
【会場】
明治大学 中野キャンパス
http://www.meiji.ac.jp/nakano/access/index.html
【参加費】
会員 学生¥1000/一般¥2000; 非会員 学生¥2000/一般¥4000
【詳細情報】
2015年研究部会連合発表会ホームページ:
http://union2015.jsiam.org/
【プログラム】(○: 登壇者)
3月7日(土)
[セッション１]
座長: 櫻田英樹（NTT）
9:40--10:00
Tamarin Proverによる投票プロトコルの安全性検証 (20分)
○櫻田 英樹 (日本電信電話株式会社)
10:00--10:20
Mizarによるnegligible function の形式定義について (20分)
○岡崎 裕之 (信州大学), 布田 裕一 (北陸先端技術大学院大学)
10:20--10:50
無視し得る確率を表現する論理体系 (30分)
○竹内 泉 (産業技術総合研究所)
【備考】
プログラムは随時更新します. 最新情報は下記のホームページに掲載いたします.
FAIS ホームページ:
http://fais.jsiam.org/
【講演概要】
Tamarin Proverによる投票プロトコルの安全性検証 (20分)
○櫻田 英樹 (日本電信電話株式会社)
概要:
KremerとRyanは藤岡らの提案した投票プロトコルFOOおよびその様々
な安全性を応用π計算の枠組みで記述し、ProVerifツールを用いて
検証した。しかし、二重投票ができないという性質は検証していない。
その原因として、二重投票不能性をProVerifツールで記述・検証
できないことが挙げられる。また、彼らがFOOの記述で用いたブラ
インド署名の形式化は、形式化の計算論的健全性がブラインド署名
の基本的な安全性（偽造不能性およびブラインド性）からは導けない
という問題がある。例えば、FDH-RSAブラインド署名を用いる場合、
彼らの形式化でカバーできない攻撃がある。櫻田はこれにかわる
新しい形式化を提案し、計算論的健全性を証明したが、検証ツール
上でこれを利用した例は無い。本発表では、MeierとSchmidtらに
よって開発されたプロトコル検証ツールTamarin Prover上で櫻田の
ブラインド署名の形式化を記述し、FOOプロトコルの二重投票不能性を
検証する取り組みについて述べる。
--------------------------------------------------------------------------
Mizarによるnegligible function の形式定義について (20分）
○岡崎 裕之(信州大学), 布田 裕一 (北陸先端技術大学院大学)
概要:
発表等は定理証明システムを用いた安全性証明検証システムの開発
を進めている． 暗号理論において，必要不可欠であるnegligible
functionの形式化定義を行った． 本発表では形式化記述言語Mizar
でのnegligible functionの定義と関連する諸定義の形式化について
報告する．
--------------------------------------------------------------------------
無視し得る確率を表現する論理体系 (30分）
○竹内 泉 (産業技術総合研究所)
概要:
暗号理論では〈確率の差が無視し得る位小さい〉という概念が頻繁
に登場する。本発表では、この〈無視し得る位小さい確率〉を表現
することの出来る形式的論理体系を提案する。この論理体系の有用
性を示す為に、暗号函数の弁別不能性から投票プロトコルの匿名性
を導き出す証明をこの体系の中で行なう。
--------------------------------------------------------------------------
【問い合わせ先】
櫻田英樹 (NTTコミュニケーション科学基礎研究所)
sakurada.hideki(at)lab.ntt.co.jp
最終更新: 2015.8.7