日本応用数理学会 (JSIAM)
「数理的技法による情報セキュリティ」研究部会 (FAIS)

日本応用数理学会2010年春の研究部会連合発表会

           日本応用数理学会2010年春の研究部会連合発表会
      「数理的技法による情報セキュリティ」(FAIS)セッション


表記の研究集会を下記のとおり開催しますので, ご案内申し上げます. 

【日時】

  2010年3月8日(月) 13:30--16:00

  なお, 研究部会連合発表会の全体の開催期間は
  2010年3月8日(月)〜9日(火) となっております. 

【会場】

  筑波大学 筑波キャンパス (茨城県つくば市天王台 1-1-1)
  計算科学研究センター, 総合研究棟 B

【参加費】

  学生会員   ¥0,     一般会員   ¥1,000
  学生非会員 ¥0,     一般非会員 ¥2,000

  ジョブフェア開催に伴い, 学生は会員・非会員にかかわらず参加
  費は無料としました. 

【詳細情報】

  2010年春の研究部会連合発表会ホームページ: 
  http://www.cs.tsukuba.ac.jp/~sakurai/jsiam/spring-meeting2010.html

【講演申込】

  締め切りました. 
  参考: 講演募集のご案内 
        http://fais.jsiam.org/2010-spring-jsiam-cfp.html

【プログラム】(○: 登壇者)

  3月8日(月)

  [セッション１]
  座長: アフェルト レナルド (産業技術総合研究所 情報セキュリティ研究センター)

  13:30--14:00
  確率様相論理による秘匿性の証明 (30分)
  ○竹内 泉 (産業技術総合研究所)
    真野 健 (NTT コミュニケーション科学基礎研究所)
    講演資料

  14:00--14:30
  サイドチャネル攻撃に対する安全性の確率的ホーア論理を用いた形式的検証 (30分)
  ○久保田 貴大 (東京大学 大学院情報理工学系研究科)
    萩谷 昌己   (東京大学 大学院情報理工学系研究科)
    講演資料

  14:30--14:50
  休憩

  [セッション２]
  座長: 竹内 泉 (産業技術総合研究所)

  14:50--15:20
  強識別不可能性理論への非逐次的スケジューリングの適用 (30分)
  ○米山 一樹 (NTT 情報流通プラットフォーム研究所)
    講演資料

  15:20--15:50
  SSReflectによる符号理論の形式化に関する一考察 (30分)
  ○アフェルト レナルド (産業技術総合研究所 情報セキュリティ研究センター)
    講演資料

  15:50--16:00
  クロージング

【備考】

  プログラムは随時更新します. 
  最新情報は下記のホームページに掲載いたします. 

  FAIS ホームページ: 
  http://fais.jsiam.org/

【問い合わせ先】

    塚田恭章 (NTTコミュニケーション科学基礎研究所)
    tsukada(at)theory.brl.ntt.co.jp

【講演概要】

  -------------------------------------------------------

  確率様相論理による秘匿性の証明 (30分)
  ○竹内 泉 (産業技術総合研究所)
    真野 健 (NTT コミュニケーション科学基礎研究所)

  [講演概要] 
  　情報を秘匿するプロトコルの中には、確率変数によって秘匿性が
  保証されるものがある。そのようなプロトコルに対して、公理的体
  系の中で情報の秘匿性を証明することを目的とする。そのための、
  確率変数を扱うことの出来る公理的な論理体系を設計することを目
  標とする。本発表で提案する論理体系は命題変数と二階量化と確率
  様相が登場する量化様相命題論理である。意味論は可能世界意味論
  で与え、その意味論に対し健全な公理系を与える。その公理系は完
  全かどうかは分からない。公理系は完全であることが望ましいが、
  健全であって必要な定理が証明出来る程度に強力なものであれば有
  用である。本発表では例題として暗号学者の食事問題を採り上げ、
  そのプロトコルの情報の秘匿をこの論理体系によって証明する。

  -------------------------------------------------------

  サイドチャネル攻撃に対する安全性の確率的ホーア論理を用いた形式的検証 (30分)
  ○久保田 貴大 (東京大学大学院情報理工学系研究科)
    萩谷 昌己   (東京大学大学院情報理工学系研究科)

  [講演概要] 
  暗号スキームには、計算量理論に基づく安全性証明が必要であるが、
  安全性の指標となる攻撃ゲームにおいて、攻撃者はさまざまなオラ
  クルにアクセスできるため、安全性の証明は複雑になりやすく、検
  証が難しい。確率的ホーア論理は、安全性証明の中でも比較的単純
  なものの形式化に用いられているが、サイドチャネル攻撃を考慮し
  たより複雑な証明に対する有効性は明らかではない。そこで、本研
  究では確率的ホーア論理を用いてサイドチャネル攻撃を考慮した安
  全性証明の形式化を行うことによって、確率的ホーア論理の検証能
  力を調べる。

  -------------------------------------------------------

  強識別不可能性理論への非逐次的スケジューリングの適用 (30分)
  ○米山 一樹 (NTT 情報流通プラットフォーム研究所)

  [講演概要] 
  攻撃者に秘密資源へのアクセスを認めることにより従来の識別不可
  能性よりも強い安全性（置き換え可能性）を保証できる枠組みとし
  て，強識別不可能性理論が様々な暗号プリミティブの解析に用いら
  れている．しかし，枠組みのモデル化は逐次的なスケジューリング
  しか考慮されておらず，非逐次的なスケジューリングモデルに拡張
  した際にも同様の安全性を保証できるかどうかは未知である．本発
  表では，Task-PIOAフレームワークを強識別不可能性理論に適用す
  ることによって，非逐次的スケジューリングモデルも置き換え可能
  性を保証できることを示す．また，逐次的スケジューリングモデル
  と非逐次的スケジューリングモデルが互いに独立していることを示す．

  -------------------------------------------------------

  SSReflectによる符号理論の形式化に関する一考察 (30分)
  ○アフェルト レナルド (産業技術総合研究所 情報セキュリティ研究センター)

  [講演概要] 
  定理証明支援系は、近年暗号スキームや疑似乱数生成器などの暗号
  プリミティブの仕様同一性や安全性を形式検証するための有効な方
  法として評価されている。しかし形式化された数学のファクトのラ
  イブラリは未整備であり、今のところ整数論に基づく暗号プリミティ
  ブしか扱えない。昨年有限群を扱うための定理証明支援系Coqの拡
  張であるSSReflectを利用して、符号理論に基づく暗号スキームの
  形式化を始めた。本発表では、SSReflectのライブラリのサーベイ
  とそれに用いた符号理論の形式化、それに基づく暗号技術の検証へ
  の予備実験について報告する。

  -------------------------------------------------------