日本応用数理学会2013年春の研究部会連合発表会
「数理的技法による情報セキュリティ」(FAIS)セッション
表記の研究集会を下記のとおり開催しますので, ご案内申し上げます.
【日時】
2013年3月15日(金) 13:10--15:40
なお, 研究部会連合発表会の全体の開催期間は
2013年3月14日(木)〜15日(金) となっております.
【会場】
東洋大学白山キャンパス 6号館2階
http://www.toyo.ac.jp/access/access_j.html
【参加費】
会員 学生¥1000/一般¥2000; 非会員 学生¥2000/一般¥4000
【詳細情報】
2013年春の研究部会連合発表会ホームページ:
http://www.jsiam.org/modules/eguide01/event.php?eid=127
【プログラム】(○: 登壇者)
3月15日(金)
[セッション１]
座長: 米山一樹（NTT）
13:10--13:30
ProVerifによるBluetooth のセキュアシンプルペアリングに対する形式的な安全性検証(20分)
○井上博之（東京理科大学大学院理工学研究科），
荒井研一（東京理科大学），金子敏信（東京理科大学）
13:30--14:00
量子暗号のためのプロトコル等価性検証ツール(30分)
○久保田貴大（東京大学大学院情報理工学系研究科），
角谷良彦（東京大学大学院情報理工学系研究科），加藤豪（NTT），
河野泰人（NTT），櫻田英樹（NTT）
14:00--14:30
暗号プリミティブに基づく機密データフロー解析
○林良太郎（株式会社東芝研究開発センター），
中西福友（株式会社東芝研究開発センター），
橋本幹生（株式会社東芝研究開発センター）
14:30--14:40
休憩
[セッション２]
座長: 櫻田英樹 (NTT)
14:40--15:10
確定的，またはヘッジ暗号における強識別不可能ハッシュ関数の適用について（30分）
内藤祐介（三菱電機），
○米山一樹（NTT）
15:10--15:40
形式化手法を利用した暗号プロトコル評価の適用拡大に向けて(30分)
松尾真一郎(NICT)，宮崎邦彦(日立製作所)，
○大塚玲(産業技術総合研究所)，手塚悟(東京工科大学)
【備考】
プログラムは随時更新します. 最新情報は下記のホームページに掲載いたします.
FAIS ホームページ:
http://fais.jsiam.org/
【講演概要】
ProVerifによるBluetoothのセキュアシンプルペアリングに対する形式的な
安全性検証(20分)
○井上博之（東京理科大学大学院理工学研究科），
荒井研一（東京理科大学），金子敏信（東京理科大学）
概要:
Proverifは，Blanchetらが開発した形式モデルでの自動検証ツールであり，形
式的検証の分野で幅広く利用されている．Proverifは，暗号プロトコルで要求
される秘匿や認証などの安全性を検証でき，さまざまな暗号プロトコルの検証
が可能である．一方，Bluetoothのセキュアシンプルペアリング（SSP）には４
つのモードがある．Changらにより，１つのモードはProVerifにより検証されて
いるが，その他のモードについては検証されていない．本稿では，Bluetoothの
SSPについてProverifを用いて形式的に記述し，安全性の検証を行う．
--------------------------------------------------------------------------
量子暗号のためのプロトコル等価性検証ツール(30分)
○久保田貴大（東京大学大学院情報理工学系研究科），
角谷良彦（東京大学大学院情報理工学系研究科），加藤豪（NTT），
河野泰人（NTT），櫻田英樹（NTT）
[講演概要]
量子プロトコルの安全性証明や，実装が仕様を満たすことの証明において，プ
ロトコルの等価性がしばしば議論される．量子プロセス計算qCCSにおいては，
プロトコルの等価性は，それらを形式化したプロセスの双模倣関係として表さ
れる．ところが，特にプロセスの状態遷移木が大きいとき，人手で双模倣関係
を検査することが困難になることがある．本研究では，qCCSの双模倣関係を自
動的に検査するツールを実装し，ShorとPreskillによるBB84鍵配送プロトコル
の安全性証明に適用した．
--------------------------------------------------------------------------
暗号プリミティブに基づく機密データフロー解析(30分)
○林良太郎（株式会社東芝研究開発センター），
中西福友（株式会社東芝研究開発センター），
橋本幹生（株式会社東芝研究開発センター）
[講演概要]
我々は，ソフトウェアのデータフローを解析し，保護が必要なデータを洗い出
す技術DFITSを提案している．データは，暗号プリミティブの入出力保護要件を
制約条件とした解析により，秘密鍵のように機密性保証が必要なconfidential
データ，秘密鍵の派生値のようにconfidentialデータの機密性を保証するため
に保護が必要なhiddenデータ，暗号文のように公開すべきexposedデータの3種
類に分類される．本発表では，DFITS の解析手法の概要とその妥当性を示す．
すなわち，任意のデータフローとDFITSの解析結果について，exposedデータを
観測してもconfidentialデータを予測できないことを示す．
--------------------------------------------------------------------------
確定的，またはヘッジ暗号における強識別不可能ハッシュ関数の適用について(30分)
内藤祐介（三菱電機），○米山一樹（NTT）
[講演概要]
強識別不可能性（Indifferentiability）はハッシュ関数の安全性の1つであり，
プロトコル内で用いた理想的関数（ランダムオラクル）を強識別不可能関数で
置き換えることができる結合可能性と呼ばれる性質を保証するが，Ristenpart
らによって確定的暗号などの安全性ゲームが複数攻撃者にまたがるプロトコル
ではSpongeなどの重要なハッシュ関数が結合可能性を持たないことが明らかに
なった．本研究では，置き換えるランダムオラクルを弱めることによってそれ
らのハッシュ関数が結合可能性を保つことを示す．また，効率的な確定的暗号
やヘッジ暗号が，弱めたランダムオラクルで構成可能であることを示す．
--------------------------------------------------------------------------
形式化手法を利用した暗号プロトコル評価の適用拡大に向けて(30分)
松尾真一郎(NICT)，宮崎邦彦(日立製作所)，
○大塚玲(産業技術総合研究所)，手塚悟(東京工科大学)
[講演概要]
形式化手法を用いた暗号プロトコルの評価は、これまでに様々な理論とツール
が提案され、具体的なプロトコルの脆弱性の指摘と修正が行われている。さら
に、暗号プロトコルの評価フレームワークについて、ISO/IEC JTC1において
2011年に標準化が完了し、実適用に向けた環境が整備されつつある。本発表で
は、ISO/IECやIETFなどで既存の標準化された暗号プロトコルを対象に、
ISO/IEC 29128をベースとした暗号プロトコル評価の適用のための、対象プロト
コルの分類と評価に必要な環境や条件について整理し、今後の適用拡大への指
針を示す。
--------------------------------------------------------------------------
【問い合わせ先】
櫻田英樹 (NTTコミュニケーション科学基礎研究所)
sakurada.hideki(at)lab.ntt.co.jp
最終更新: 2013.3.11