日本応用数理学会2010年度年会
「数理的技法による情報セキュリティ」(FAIS)
オーガナイズド・セッション
日本応用数理学会2010年度年会が 2010.9.6(月)〜2010.9.9(木) に明治大学
駿河台キャンパスにて開催されます. 「数理的技法による情報セキュリティ」
(FAIS)研究部会も, 下記の日程でオーガナイズド・セッション(OS)を開催いた
します. 奮ってご参加下さいますようお願い申し上げます.
[年会 ホームページ]
http://www.jsiam.org/annualmeeting/2010
[JSIAM-FAIS ホームページ]
http://fais.jsiam.org/
【日時】
2010年9月6日(月) (年会初日) 14:10--15:30 + 15:40--16:40
【会場】
明治大学 駿河台キャンパス
【参加方法】
年会ホームページをご覧ください.
【プログラム】(○: 登壇者)
[セッション1]
座長: アフェルト レナルド (産業技術総合研究所 情報セキュリティ研究センター)
14:10--14:30 (20分)
CryptoVerifを用いたRFID向け相互認証プロトコルの安全性証明の検討
○花谷 嘉一 (電気通信大学 大学院情報理工学研究科
/ (株)東芝 研究開発センター)
大久保 美也子 (情報通信研究機構)
松尾 真一郎 (情報通信研究機構)
太田 和夫 (電気通信大学 大学院情報理工学研究科 総合情報学専攻)
崎山 一男 (電気通信大学 大学院情報理工学研究科 総合情報学専攻)
14:30--15:10 (40分)
A calculus for game-based security proofs
○David NOWAK (産業技術総合研究所 情報セキュリティ研究センター)
Yu ZHANG (Institute of Software, Chinese Academy of Sciences)
15:10--15:30 (20分)
量子鍵配送プロトコルの無条件安全性証明の自動化に向けて
○久保田 貴大 (東京大学 大学院情報理工学系研究科 コンピュータ科学専攻)
角谷 良彦 (東京大学 大学院情報理工学系研究科 コンピュータ科学専攻)
加藤 豪 (日本電信電話株式会社 NTT コミュニケーション科学基礎研究所)
河野 泰人 (日本電信電話株式会社 NTT コミュニケーション科学基礎研究所)
15:30--15:40 (10分) 休憩
[セッション2]
座長: 竹内 泉 (産業技術総合研究所)
15:40--16:00 (20分)
能動的攻撃者の下でのXORの記号モデルとその計算論的健全性
○櫻田 英樹 (日本電信電話株式会社 NTT コミュニケーション科学基礎研究所)
川本 裕輔 (日本学術振興会特別研究員 / ENS Cachan)
萩谷 昌己 (東京大学 大学院情報理工学系研究科)
16:00--16:20 (20分)
Computationally Sound Symbolic Analysis for EUC Security of Key Exchange
○鈴木 斎輝 (大阪大学 大学院情報科学研究科)
吉田 真紀 (大阪大学 大学院情報科学研究科)
藤原 融 (大阪大学 大学院情報科学研究科)
16:20--16:40 (20分)
CosyProofs 2010 参加報告
○真野 健 (日本電信電話株式会社 NTT コミュニケーション科学基礎研究所)
17:30--19:30 懇親会
セッション終了後に懇親会を予定しています. 詳細は追ってご連絡いたします.
講演の概要については下記をご覧下さい.
都合によりプログラムが変更になる可能性があります.
最新情報は FAIS 研究部会のホームページでご確認ください.
【備考】
FAIS OS での発表論文には, 電子ジャーナル JSIAM Letters 誌への投稿
機会が与えられます. ただし, 投稿資格は会員に限ります.
詳しくは JSIAM Letters 誌のホームページをご参照ください.
[JSIAM Letters ホームページ]
http://jsiam.amp.i.kyoto-u.ac.jp/letters/
【重要な日程】
2010年6月23日(水) 講演申込締切
2010年6月28日(月) FAISオーガナイズド・セッション 暫定プログラム決定
2010年7月 2日(金) 年会 Web からの正式な講演申込締切
2010年8月 3日(火) 講演予稿提出締切 (予稿は2ページです)
2010年8月 6日(金) 参加費事前支払い(割引適用)締切
2010年9月 6日(月) 年会
〜2010年9月 9日(木)
【講演概要】
--------------------------------------------------------------------
CryptoVerifを用いたRFID向け相互認証プロトコルの安全性証明の検討
○花谷 嘉一 (電気通信大学 大学院情報理工学研究科
/ (株)東芝 研究開発センター)
大久保 美也子 (情報通信研究機構)
松尾 真一郎 (情報通信研究機構)
太田 和夫 (電気通信大学 大学院情報理工学研究科 総合情報学専攻)
崎山 一男 (電気通信大学 大学院情報理工学研究科 総合情報学専攻)
[講演概要]
SCIS2008で松尾らが提案したRFID向け軽量相互認証プロトコルの改良方式の
安全性検証に CryptoVerif の適用を検討した．
松尾らの相互認証プロトコルは，非力なデバイスでも実行できるよう，ハッ
シュ関数のみで構成された方式で，人手による証明ではランダムオラクルモデ
ルにおいて相互認証性，追跡不能性などの安全性が証明できる．
今回の検討では，CryptoVerif では松尾らのプロトコルの攻撃モデルを表現
することができなかった．そこで，簡易化した攻撃モデルでの安全性を
CryptoVerifで検証し，その検証結果を利用して人手による検証で安全性を示
す方法を検討した．
--------------------------------------------------------------------
A calculus for game-based security proofs
○David NOWAK (産業技術総合研究所 情報セキュリティ研究センター)
Yu ZHANG (Institute of Software, Chinese Academy of Sciences)
[講演概要]
The game-based approach to security proofs in cryptography is a
widely-used methodology for writing proofs rigorously. However a
unifying language for writing games is still missing. In this
presentation we show how CSLR, a probabilistic lambda-calculus with a
type system that guarantees that computations are probabilistic
polynomial time, can be equipped with a notion of game
indistinguishability. This allows us to define cryptographic
constructions, effective adversaries, security notions, computational
assumptions, game transformations, and game-based security proofs in
the unified framework provided by CSLR. Our code for cryptographic
constructions is close to implementation in the sense that we do not
assume arbitrary uniform distributions but use a realistic algorithm
to approximate them. We illustrate our calculus on cryptographic
constructions for public-key encryption and pseudorandom bit
generation.
--------------------------------------------------------------------
量子鍵配送プロトコルの無条件安全性証明の自動化に向けて
○久保田 貴大 (東京大学 大学院情報理工学系研究科 コンピュータ科学専攻)
角谷 良彦 (東京大学 大学院情報理工学系研究科 コンピュータ科学専攻)
加藤 豪 (日本電信電話株式会社 NTT コミュニケーション科学基礎研究所)
河野 泰人 (日本電信電話株式会社 NTT コミュニケーション科学基礎研究所)
[講演概要]
ShorとPreskillによるBB84の無条件安全性証明を自動化する手法を提案する。
彼らの証明において、BB84の安全性は、エンタングルメント蒸留プロトコル
(EDP)に基づいたある量子鍵配送プロトコル(QKD)の安全性に帰着される。後者
の安全性の方が前者の安全性よりも証明をシンプルに行うことができる。我々
は、攻撃者の存在のもとでのBB84の実行をひとつのプログラミング言語を用い
て形式化し、プログラムの等価性を書き換え規則として形式化した。これらの
書き換え規則を用いることで、BB84は、EDPに基づいたQKDに自動的に簡約され
る。さらに、書き換えの順序について項書き換えの見地から考察を行った。
--------------------------------------------------------------------
能動的攻撃者の下でのXORの記号モデルとその計算論的健全性
○櫻田 英樹 (日本電信電話株式会社 NTT コミュニケーション科学基礎研究所)
川本 裕輔 (日本学術振興会特別研究員 / ENS Cachan)
萩谷 昌己 (東京大学 大学院情報理工学系研究科)
[講演概要]
通信プロトコルには、メッセージを構成する際にビットごとの排他的論理和
(XOR)を用いるものがある。また、このようなプロトコルを記号モデルを用い
て検証する方法も提案されている。しかし、このような記号モデルが計算論的
に健全であるかは知られていなかった。本発表では、XORを用いるプロトコル
の記号を与え、その計算論的健全性を示す。
--------------------------------------------------------------------
Computationally Sound Symbolic Analysis for EUC Security of Key Exchange
○鈴木 斎輝 (大阪大学 大学院情報科学研究科)
吉田 真紀 (大阪大学 大学院情報科学研究科)
藤原 融 (大阪大学 大学院情報科学研究科)
[講演概要]
Canetti et al. presented a symbolic analysis framework for universally
composable (UC) security of key exchange protocols where adaptive
party corruptions are handled. We extend their framework to
externalized UC (EUC) security. EUC security is more preferable for
protocols that use trusted information such as certified public
keys. The EUC framework introduces functionalities to share trusted
information. Thus, we symbolically model these functionalities and
prove a mapping lemma. We then show that the previous symbolic
criterion for key exchange is computationally sound in our extended
framework.
--------------------------------------------------------------------
CosyProofs 2010 参加報告
○真野 健 (日本電信電話株式会社 NTT コミュニケーション科学基礎研究所)
[講演概要]
2010年4月12日から4月16日にフランス・バルビゾンで開催された 2010 Spring
School and French-Japanese Collaboration Workshop on Computational and
Symbolic Proofs of Security (CosyProofs 2010)の参加報告を行う.
--------------------------------------------------------------------
【問い合わせ先】
塚田 恭章 (NTTコミュニケーション科学基礎研究所)
tsukada(at)theory.brl.ntt.co.jp
最終更新: 2010.9.15