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

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

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


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

【日時】

  2011年3月7日(月) 14:00--17:10 

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

【会場】

  電気通信大学 (〒812-8585 調布市調布ヶ丘 1-5-1)
  西キャンパス (西4号館, 西9号館)

【参加費】

  参加費: 会員 学生¥0/一般¥1000; 非会員 学生¥1000/一般¥2000

【詳細情報】

  2011年春の研究部会連合発表会ホームページ: 
  http://www.jsiam.org/modules/eguide01/event.php?eid=74

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

  3月7日(月)

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

  14:00--14:30
  匿名性とプライバシの合成可能性について (30分)
  ○塚田 恭章 (NTT コミュニケーション科学基礎研究所)
    櫻田 英樹 (NTT コミュニケーション科学基礎研究所)
    真野 健   (NTT コミュニケーション科学基礎研究所)
    真鍋 義文 (NTT コミュニケーション科学基礎研究所)
    講演資料

  14:30--15:00
  秘密分散法に於ける確率論的秘匿 (30分)
  ○竹内 泉   (産業技術総合研究所)
    足立 智子 (東邦大学)
    講演資料

  15:00--15:30
  Confidentiality-preserving Proof Theories for Distributed Proof Systems (30分)
  ○南 和宏 (国立情報学研究所)
    Nikita Borisov (University of Illinois)
    Marianne Winslett (University of Illinois)
    Adam Lee (University of Pittsburgh)
    講演資料

  15:30--15:50
  休憩

  [セッション２]
  座長: 山本 光晴 (千葉大学大学院理学研究科基盤理学専攻)

  15:50--16:10
  Specification-based verification and testing of Internet protocols (20分)
  ○David Nowak (産業技術総合研究所 情報セキュリティ研究センター)
    大岩 寛     (産業技術総合研究所 情報セキュリティ研究センター)
    講演資料

  16:10--16:40
  投票プロトコルの匿名性の自動検証 (30分)
  ○櫻田 英樹 (NTT コミュニケーション科学基礎研究所)
    講演資料

  16:40--17:10
  量子暗号プロトコルの形式的検証のための Applied Pi-Calculus (30分)
  ○久保田 貴大 (東京大学大学院情報理工学系研究科, M2)
    角谷 良彦   (東京大学大学院情報理工学系研究科)
    講演資料

【備考】

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

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

【講演概要】

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

  匿名性とプライバシの合成可能性について (30分)
  ○塚田 恭章 (NTT コミュニケーション科学基礎研究所)
    櫻田 英樹 (NTT コミュニケーション科学基礎研究所)
    真野 健   (NTT コミュニケーション科学基礎研究所)
    真鍋 義文 (NTT コミュニケーション科学基礎研究所)

  [講演概要] 
  部分システムの性質から全体システムの性質を導くモジュラーなアプローチはシス
  テム検証においても有用であると期待される. 本発表では, 知識論理の枠組みを利
  用し, 匿名性・プライバシ・顕名性・アイデンティティといった個人情報の秘匿・
  開示に関する性質が, 逐次的もしくは並列的な合成によって保存されるための条件
  について議論する.

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

  秘密分散法に於ける確率論的秘匿 (30分)
  ○竹内 泉  (産業技術総合研究所)
    足立智子 (東邦大学)

  [講演概要] 
  秘密分散法はシャミア (Adi Shamir) によって発明された秘密を分散して保持する
  方法である。この方法では乱数が用いられるが、乱数を確率変数と見做した場合に
  は、秘密は確率論的に秘匿される。この確率論的秘匿を証明する形式的論理体系を
  提案する。この論理体系では確率は様相記号によって表される。

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

  Confidentiality-preserving Proof Theories for Distributed Proof Systems (30分)
  ○南 和宏 (国立情報学研究所)
    Nikita Borisov (University of Illinois)
    Marianne Winslett (University of Illinois)
    Adam Lee (University of Pittsburgh)

  [講演概要] 
  本発表では、複数の知識ベースから構成される分散環境の証明システムにおいて、
  各知識ベースの情報の機密性に考慮した推論規則 (inference rules) について考察
  する。システムは Datalog を分散環境に拡張した言語をサポートし、複数の知識ベー
  スの論理ステートメント (facts) から証明を構成する。ただし各論理ステートメン
  トは任意アクセス制御 (DAC) のポリシーで定義された機密性の要件を満たす必要が
  あり、我々はシステムの安全性を nondeducibility の概念に基づき厳密に定義し、
  複数の異なる推論規則の安全性の分析を行った。

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

  Specification-based verification and testing of Internet protocols (20分)
  ○David Nowak (産業技術総合研究所 情報セキュリティ研究センター)
    大岩 寛     (産業技術総合研究所 情報セキュリティ研究センター)

  [講演概要] 
  We will develop a new methodology for verifying and testing implementations
  of Internet protocols.  More precisely, we will: (1) investigate the
  formalization in the proof assistant Coq of informal specifications found
  in RFCs; (2) verify critical pieces of code in the implementation of a
  protocol with respect to our formalization of its RFC; (3) generate test
  cases for black box testing of full implementations.  As a case study we
  will apply our methodology to the protocol Transport Layer Security (TLS)
  which adds a cryptographic layer on top of other Internet protocols.

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

  投票プロトコルの匿名性の自動検証 (30分)
  ○櫻田 英樹 (NTT コミュニケーション科学基礎研究所)

  [講演概要] 
  通信プロトコルの安全性を自動的に検証するツールとしてProverifやAVISPAなどが
  知られている。これらのツールを用いて認証プロトコルの安全性などを検証するこ
  とが可能であるが、匿名性を検証することができなかった。実際、KremerとRyanは、
  藤岡らによる投票プロトコルFOO(AUSCRYPT'92)の安全性を検証した(ESOP'05)が、匿
  名性以外の性質はProverifを用いて自動的に行っている一方、匿名性については手
  で安全性証明を記述して検証している。本研究では、匿名性を自動的に検証する方
  法を提案し、FOOの匿名性の検証に適用する。

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

  量子暗号プロトコルの形式的検証のための Applied Pi-Calculus (30分)
  ○久保田 貴大 (東京大学大学院情報理工学系研究科, M2)
    角谷 良彦   (東京大学大学院情報理工学系研究科)

  [講演概要] 
  量子暗号プロトコルは, 量子力学の法則によって古典暗号プロトコルにない強い安
  全性を満たすが, その証明は複雑であり検証が難しい. 応用π計算は, 古典暗号プ
  ロトコルの検証に成果を挙げており, その量子版もいくつか提案されているが, 量
  子鍵配送プロトコルの無条件安全性証明の形式的検証を可能にしているものはな
  い. そこで我々は, 量子暗号プロトコルの形式的検証のための新しい応用π計算を
  提案し, プロセスの観測同値性を定義した. ShorとPreskillのBB84量子鍵配送プロ
  トコルの安全性証明では, 等価なプロトコル同士を書き換えていくという手法が用
  いられるが, その等価性はプロセスの観測同値性として表せる.

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

【問い合わせ先】

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