日本応用数理学会 (JSIAM)
「数理的技法による情報セキュリティ」研究部会 (FAIS)
日本応用数理学会2008年春の研究部会連合発表会
日本応用数理学会2008年春の研究部会連合発表会
「数理的技法による情報セキュリティ」(FAIS)セッション
表記の研究集会を下記のとおり開催しますので, ご案内申し上げます.
【日時】
2008年3月8日(土) 15:00--18:00
なお, 研究部会連合発表会の全体の開催期間は
2008年3月8日(土)〜9日(日) 9:00--18:00 となっております.
【会場】
首都大学東京 南大沢キャンパス 12号館 (東京都八王子市南大沢)
アクセス: http://www.tmu.ac.jp/access.html#access_minamiosawa
【参加費】(予定)
学生会員 ¥0, 一般会員 ¥1,000
学生非会員 ¥1,000, 一般非会員 ¥2,000
【講演申込】
締め切りました.
参考: 講演募集のご案内
http://fais.jsiam.org/2008-spring-jsiam-cfp.html
【プログラム】(○: 登壇者)
3月8日(土)
座長: Reynald Affeldt (産業技術総合研究所 情報セキュリティ研究センター)
15:00--15:50
[FAIS 特別講演] Computational soundness of observational equivalence
○Hubert Comon-Lundh (Ecole Normale Superieure de Cachan/
産業技術総合研究所 情報セキュリティ研究センター)
講演資料
15:50--16:00
休憩
16:00--16:20
計算論的に健全な形式的再暗号化
○川本 裕輔 (東京大学大学院情報理工学系研究科)
櫻田 英樹 (NTT コミュニケーション科学基礎研究所)
萩谷 昌己 (東京大学大学院情報理工学系研究科/
NTT コミュニケーション科学基礎研究所)
講演資料
16:20--16:40
ブラインド署名の計算論的に健全な形式化
○櫻田 英樹 (NTT コミュニケーション科学基礎研究所)
萩谷 昌己 (東京大学大学院情報理工学系研究科/
NTT コミュニケーション科学基礎研究所)
講演資料
16:40--17:00
CryptoVerif のための Authenticated Encryption の
安全性の定式化に関する考察
○荒井 研一 (信州大学大学院総合工学系研究科システム開発専攻)
岡崎 裕之 (信州大学大学院工学系研究科情報工学専攻)
不破 泰 (信州大学大学院工学系研究科情報工学専攻)
講演資料
17:00--17:20
Blanchet フレームワークにおけるＣＤＨ仮定の定式化方針について
○花谷 嘉一 ((株)東芝 研究開発センター)
國分 雄一 (電気通信大学)
米山 一樹 (電気通信大学)
太田 和夫 (電気通信大学)
講演資料
17:20--17:40
CryptoVerifによるブロック暗号の安全性自動証明
○大熊 建司 ((株)東芝 研究開発センター)
村谷 博文 ((株)東芝 研究開発センター)
花谷 嘉一 ((株)東芝 研究開発センター)
古田 憲一郎 ((株)東芝 研究開発センター)
講演資料
17:40--18:00
Task-PIOA: 電子署名に対する能動的攻撃者の扱いについて
○米山 一樹 (電気通信大学)
講演資料
【備考】
1. 3月8日(土) 13:40--14:40には, 栗田太郎氏(フェリカネットワークス株式会社)
による研究部会連合発表会 総合講演
「携帯電話組込み用'モバイル FeliCa IC チップ'開発における数理的技法
の適用」が予定されています.
2. また, 同日 9:00--12:00には「数論アルゴリズムとその応用」(JANT)研究部会
のセッションがございます.
3. プログラムは随時更新します.
最新情報は下記のホームページに掲載いたします.
FAIS ホームページ:
http://fais.jsiam.org/
2008年春の研究部会連合発表会ホームページ(準備中):
http://www.jsiam.org/modules/eguide01/event.php?eid=36
【問い合わせ先】
塚田恭章
NTTコミュニケーション科学基礎研究所
tsukada(at)theory.brl.ntt.co.jp
【講演概要】
-------------------------------------------------------
Computational soundness of observational equivalence
○Hubert Comon-Lundh (Ecole Normale Superieure de Cachan/
産業技術総合研究所 情報セキュリティ研究センター)
[講演概要]
Security properties are often defined as computational
indistinguishability: an attacker cannot make any
difference between an ideal functionality and the actual
implementation. A typical example is confidentiality:
replacing the secret data by a random number, an
attacker should not be able to tell if he is interacting
with the protocol using the secret or with the one using
the random number. A popular property, universal
composability, is typically an indistinguishability
property. There is a similar notion in the area of
process algebras, which is called observational
equivalence: two processes are observationally
equivalent if, in any context, they can equally output a
signal on a designated channel. We show that these two
notions are related: observational equivalence implies
indistinguishability, under some standard security
assumptions. This means that proving security can be
performed at the process algebra level, for which there
are some automatic verification tools.
-------------------------------------------------------
計算論的に健全な形式的再暗号化
川本 裕輔 (東京大学大学院情報理工学系研究科)
櫻田 英樹 (NTT コミュニケーション科学基礎研究所)
萩谷 昌己 (東京大学大学院情報理工学系研究科/
NTT コミュニケーション科学基礎研究所)
[講演概要]
再暗号化可能な暗号方式を用いたプロトコルを解析するため
の形式的手法を提案する。具体的には、Abadi-Rogaway 流の形
式化において乱数の合成を扱う新しい方法を導入し、この方法
を用いて再暗号化可能な暗号方式を形式化する。さらに、
IND-RCCA 安全性と乱数合成の安全性を用いて、我々の形式化
が計算論的に健全であることを示す。
-------------------------------------------------------
ブラインド署名の計算論的に健全な形式化
櫻田 英樹 (NTT コミュニケーション科学基礎研究所)
萩谷 昌己 (東京大学大学院情報理工学系研究科/
NTT コミュニケーション科学基礎研究所)
[講演概要]
ブラインド署名は電子投票や電子現金などのプロトコルにお
けるプライバシ保護に重要な役割を果たしており、ブラインド
署名を用いたプロトコルを記号的モデルで解析する研究も行わ
れている。しかし、記号的モデルにおけるブラインド署名の定
式化の妥当性（健全性）についてはこれまで明らかにされてこ
なかった。本発表では、ブラインド署名を扱うことのできる記
号モデルを提案し、その計算論的健全性について述べる。
-------------------------------------------------------
CryptoVerif のための Authenticated Encryption の
安全性の定式化に関する考察
荒井 研一 (信州大学大学院総合工学系研究科システム開発専攻)
岡崎 裕之 (信州大学大学院工学系研究科情報工学専攻)
不破 泰 (信州大学大学院工学系研究科情報工学専攻)
[講演概要]
Blanchet らは，計算論的モデルにおいて，ゲームを用いて安
全性を証明する手法を記号論的モデルに適応し，計算論的安全
性を数学的技法で自動証明することに成功した．Blanchet ら
は，提案手法を実装したプログラムである CryptoVerif を公
開している．
一方，Authenticated Encryption とは，メッセージ秘匿と
メッセージ認証の機能を併せ持つ共通鍵暗号方式である．
本発表では，CryptoVerif における Authenticated
Encryption の安全性の定式化に関する考察を行う．
-------------------------------------------------------
Blanchet フレームワークにおけるＣＤＨ仮定の定式化方針について
花谷 嘉一 ((株)東芝 研究開発センター)
國分 雄一 (電気通信大学)
米山 一樹 (電気通信大学)
太田 和夫 (電気通信大学)
[講演概要]
暗号プロトコルの安全性を形式的に検証する手法の一種であ
るBlanchet のフレームワークにおいて，計算量的仮定の定式
化は，証明結果の正当性に影響を与える重要な作業である．し
かし，定式化の際には，人間が記述の作成，評価を行う必要が
あるため，手間がかかるだけでなく，ミスを犯す可能性がある．
もし，計算量的仮定の定式化を行う回数を最小限に抑えるこ
とができれば上記の問題を改善することができるが，そのよう
な手法は明確に議論されていなかった．
本発表では，主要な計算量的仮定の1つであるＣＤＨ仮定を
例に，様々な安全性の検証に使いまわすことができる定式化の
方針を探り，定式化の際の問題の改善を試みる．
-------------------------------------------------------
CryptoVerifによるブロック暗号の安全性自動証明
大熊 建司 ((株)東芝 研究開発センター)
村谷 博文 ((株)東芝 研究開発センター)
花谷 嘉一 ((株)東芝 研究開発センター)
古田 憲一郎 ((株)東芝 研究開発センター)
[講演概要]
暗号プロトコルの安全性証明を自動的に生成する手法として
Blanchet-Pointcheval 法が提案されており、Blanchet はこの
手法を実現するソフトウェア CryptoVerif を公開している。
このソフトウェアを用いて、Bellare-Rogaway による公開鍵暗
号や Full-Domain-Hash 署名に対して安全性証明が生成されて
いる。我々は、同手法がブロック暗号に対しても有効であるこ
とを示すため、CryptoVerif による Luby-Rackoff の擬ランダ
ム置換に対する安全性証明の生成を確認する。同手法は、近年
提案されている Tweakable ブロック暗号の構成に対しても有
効である。
-------------------------------------------------------
Task-PIOA: 電子署名に対する能動的攻撃者の扱いについて
米山 一樹 (電気通信大学)
[講演概要]
これまでの事例研究では能動的攻撃者に対する安全性を解析
した例が存在しないため，task-PIOA フレームワークにおける
能動的攻撃者の扱い方には不明な点が多い．ここでいう能動的
攻撃者とは，パブリックに得られる情報以外の情報を何らかの
手段で利用して攻撃を行う攻撃者を指す．本研究では，電子署
名に対する能動的攻撃者の一種である選択文書攻撃を行う署名
偽造者の task-PIOA としての定式化を提案する．また，実際
に FDH 署名の安全性証明への適用を考察する．そのための準
備として，必要な計算量的仮定（一方向性）の task-PIOA フ
レームワークでの定式化を示す．
-------------------------------------------------------
最終更新: 2008.3.31
FAISホームページにもどる．