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

日本応用数理学会2014年会FAISオーガナイズド・セッション

                   日本応用数理学会2014年会
             「数理的技法による情報セキュリティ」(FAIS)
                    オーガナイズド・セッション


日本応用数理学会2014年会が 2014.9.3(水)〜2013.9.5(金) に
政策研究大学院大学にて開催されます:

  [年会 ホームページ]
  http://jsiam2014.jsiam.org/

「数理的技法による情報セキュリティ」(FAIS)研究部会も, 下記の日程で
オーガナイズド・セッション(OS)を開催いたします.

今回はFAIS研究会 初の試みとしてチュートリアル講演も企画しました.
プロトコルの結合可能安全性やツールを使った自動検証などの基本的な内容に
加え、最近盛んになっている両者の融合研究(Dahl & Damgard, Eurocrypt2014)
についても解説します。

奮ってご参加下さいますようお願い申し上げます.

【日時】

  9月5日(金) 9:30-10:50

【会場】

  政策研究大学院大学 (東京都港区六本木)

【参加方法】

  年会ホームページをご覧ください.

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

  研究部会OS：数理的技法による情報セキュリティ ［9月5日：09:30-10:50：D会場］
  座長: 花谷 嘉一 （(株)東芝 研究開発センター）

  9:30-9:50
  可変長情報源符号化順定理の形式化
  ○小尾 良介 (千葉大学大学院理学研究科)
  講演資料
  [概要]
  現代数学における証明は膨大な長さになりつつあり、証明の信頼性の問題が発
  生している。定理証明支援系を用いた形式的検証は、これらの証明の正当性を
  保証するための解決策として近年現れた。長い証明を形式的に検証する前に、
  形式的な定義、定理の確立されたライブラリを構築する必要がある。我々は既
  存のライブラリに「可変長情報源符号化順定理」を加えることによってどう情
  報理論の形式化に貢献したのかを説明する。

  9:50-10:10
  チュートリアル：暗号プロトコルの結合可能安全性とその形式検証
  ○米山 一樹 (NTTセキュアプラットフォーム研究所)
  講演資料
  [概要]
  高機能なシステムを実現するためには、複数の暗号プロトコルを組み合わせる
  必要があるが、一般に個別には安全なプロトコルであっても、組み合わせたシ
  ステムが安全とは限らない。組み合わせても安全性が損なわれない性質を、結
  合可能安全性 と呼ぶ。しかし、結合可能安全性の証明は一般に複雑であるた
  め、証明を形式検証で行う技術が提案されている。本発表では、結合可能安全性
  とその形式検証技術についての過去の研究を紹介する。

  10:10-10:30
  チュートリアル：結合可能安全性の形式検証における最近の研究動向
  ○吉田 真紀 (情報通信研究機構)
  講演資料
  [概要]
  結合可能安全性の形式検証の提案以降、様々な拡張が試みられている。最近、
  Eurocrypt2014で、形式検証の枠組みが整備され、結合可能安全性の定式化に近
  い形で検証対象を定義可能となった。さらに検証 対象が拡張され、新たに準同
  型暗号などを用いたプロトコルが検証可能となり、紛失通信プロトコルに適用
  されている。本発表では、上記成果を解説し、今後の研究の展望について紹介
  する。

  10:30-10:50
  チュートリアル：ProVerifによる結合可能安全性の形式検証
  ○櫻田 英樹 (NTT コミュニケーション科学基礎研究所)
  講演資料
  ProVerifスクリプト(zipアーカイブ)
  [概要]
  セキュリティ・プロトコルの安全性を自動的に検証するツールとして広く用い
  られているProVerifについて解説する。プロトコルの記述のしかたや安全性の
  記述のしかた、検証結果の読みかたに加え、検証において注意すべき点などに
  ついても述べる。ProVerifは認証や秘匿性などを含むいくつかの種類の安全性
  を検証できるが、ここでは特に、結合可能安全性の自動検証に用いられた観測
  等価性の検証について述べる。


  最新情報は年会のホームページでご確認ください.

【問い合わせ先】

  櫻田 英樹 (NTTコミュニケーション科学基礎研究所)
  sakurada.hideki(at)lab.ntt.co.jp