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

第二回研究集会

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

           http://fais.jsiam.org/

                       第二回研究集会のご案内

暗号研究者と数理的技法(フォーマルメソッド)研究者の交流を目的として, 
日本応用数理学会「数理的技法による情報セキュリティ」研究部会が本年
5月に発足しました. 詳しくは上記ホームページに記載の設立趣旨をご覧く
ださい. 

その第二回研究集会を次のように開催しますので, ご案内申し上げます. 
本研究集会は「第7回代数幾何・数論及び符号・暗号研究集会」
(12/20(水)〜12/22(金), プログラム(PDF))に協賛するという形で行います. 

暗号理論と数理的技法の境界領域をテーマに, その全体像が分かるような
プログラム構成を目指しました. 是非, 多くの皆様のご参加と活発なご討
論をお願いいたします. 

なお, 研究集会の後, 周辺での懇親会を予定しております. こちらにも奮っ
てご参加ください.

【日時】

  12月22日(金) 10:00〜17:00

【会場】

  東京大学 大学院 数理科学研究科 大講義室 
    京王井の頭線 駒場東大前駅 下車 徒歩5分.
    渋谷寄り踏切から東大構内に入ると研究科棟はすぐ右手にあります. 
    大講義室は渋谷寄りの一番奥にあります. 
    http://www.ms.u-tokyo.ac.jp/access/index.html
    http://www.u-tokyo.ac.jp/campusmap/map02_02_j.html
    http://www.u-tokyo.ac.jp/campusmap/cam02_01_27_j.html

  参加無料. 事前申込不要. 参加は応用数理学会の会員でなくても可. 

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

  オーガナイザー
    岡本龍明(日本電信電話(株) 情報流通プラットフォーム研究所)

  10:00〜11:00
  数理的技法による情報セキュリティについて
  ◎萩谷昌己(東京大学 大学院情報理工学系研究科 コンピュータ科学専攻)
    岡本龍明(日本電信電話(株) 情報流通プラットフォーム研究所)
  講演資料

  11:10〜12:10
  spi計算における暗号プロトコルの形式的検証について  
  ◎住井英二郎(東北大学 大学院情報科学研究科)
  講演資料

  13:30〜14:30
  Abadi-Rogawayによる暗号メッセージの解析手法とその健全性・完全性について
  ◎萩原茂樹(東京工業大学 大学院情報理工学研究科 計算工学専攻)
    米崎直樹(東京工業大学 大学院情報理工学研究科 計算工学専攻)
  講演資料

  14:45〜15:45
  ゲーム列による安全性証明の形式化と自動化
  ◎真野　健(日本電信電話(株) コミュニケーション科学基礎研究所)
    櫻田英樹(日本電信電話(株) コミュニケーション科学基礎研究所)
    河辺義信(日本電信電話(株) コミュニケーション科学基礎研究所)
    塚田恭章(日本電信電話(株) コミュニケーション科学基礎研究所)
  講演資料

  16:00〜17:00
  BAN 論理から Protocol Composition Logic へ
  〜セキュリティ・プロトコルの論理的分析法
  ◎長谷部浩二(産業技術総合研究所 システム検証研究センター)
    岡田光弘(慶應義塾大学 文学部哲学科)
  講演資料

  17:30〜19:00 懇親会

  講演の概要については下記をご覧下さい. 
  プログラムは随時更新します. 最新情報はFAISホームページに掲載いたします. 

【問い合わせ先】

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

【講演概要】

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

  数理的技法による情報セキュリティについて
    萩谷昌己(東京大学 大学院情報理工学系研究科 コンピュータ科学専攻)
    岡本龍明(日本電信電話(株) 情報流通プラットフォーム研究所)
  [講演概要] 
    　暗号プロトコルに対する計算論的アプローチと記号論的ア
    プローチを融合しようとする試みが盛んに行われている。前
    者は根底にある暗号の脆弱性も考慮に入れつつ、主として確
    率的多項式時間チューリング機械の枠組みを用いて解析を行
    う。後者は、いわゆるDolev-Yaoモデルに代表されるように、
    根底にある暗号は絶対に破られないという仮定のもとで、通
    信路に流れるメッセージを記号（から作られる木構造）に理
    想化してプロトコルの検証を行う。
    　両アプローチを融合する方法は大きく二つに分類される。一
    つは計算論的な解析を形式体系の中で定式化した上で記号論
    的アプローチに基づく自動検証技術を導入するもの（いわゆ
    る直接的方法）。もう一つは記号論的な推論に計算論的な解
    釈を与えるもの（いわゆる間接的方法）である。
    　本講演では、二つのアプローチを融合する試みについて概観
    し、その問題点や将来の方向性について議論したい。

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

  spi計算における暗号プロトコルの形式的検証について
    住井英二郎(東北大学 大学院情報科学研究科)
  [講演概要] 
    AbadiとGordonのspi計算は、並行・分散計算モデルの一種である
    π計算を、共通鍵暗号プリミティブで拡張した形式的体系である。
    本講演では、spi計算における暗号プロトコルの表現と秘密性の
    検証について、一般的な概論だけでなく具体的な詳細までふみこ
    んで、実例により紹介する。実例としては、Abadi とGordonの論
    文で議論されているWide Mouthed Frog Protocolを使用するが、
    原論文が採用している秘密性の定義(may testing equivalence)
    の問題点と、より適切な定義(barbed equivalence)についても紹
    介する。秘密性の検証にはBorgstromとNestmannのhedged
    bisimulationを使用する。BorgstromとNestmannの論文では、
    hedged bisimulationはbarbed equivalenceに対し健全かつ完全
    であると述べられているが、完全性は一般のプロセスについては
    証明されていないことを紹介する。

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

  Abadi-Rogawayによる暗号メッセージの解析手法とその健全性・完全性について
    萩原茂樹(東京工業大学 大学院情報理工学研究科 計算工学専攻)
    米崎直樹(東京工業大学 大学院情報理工学研究科 計算工学専攻)
  [講演概要] 
    暗号プロトコルの解析は、確率的多項式時間チューリング機械を
    用いる計算論的手法と、Dolev-Yaoモデルに基づいた記号論的手
    法がそれぞれ独立に研究されてきた。記号論による解析は、抽象
    レベルの解析とみなせ簡潔で分かりやすい一方、記号論による解
    析結果と計算論による解析結果の対応が明らかでなかった。この
    問題に対してAbadiとRogaway は、完全な対称鍵暗号方式を前提
    としてメッセージの見た目の等価性を記号論的に定義し、メッセー
    ジが等価ならばそれらは計算論的に識別不可能であること、すな
    わち記号論によるメッセージの識別不可能性の、計算論的意味に
    対する健全性を示した。さらに、MicciancioとWarinschiはその
    完全性を示している。本講演では、これら内容を中心に関連する
    研究を含め紹介を行う。

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

  ゲーム列による安全性証明の形式化と自動化
    真野　健(日本電信電話(株) コミュニケーション科学基礎研究所)
    櫻田英樹(日本電信電話(株) コミュニケーション科学基礎研究所)
    河辺義信(日本電信電話(株) コミュニケーション科学基礎研究所)
    塚田恭章(日本電信電話(株) コミュニケーション科学基礎研究所)
  [講演概要] 
    セキュリティプロトコルの安全性の形式検証のために，ゲーム列
    による安全性証明を形式化する手法の研究が盛んになりつつある．
    本手法は，従来攻撃者の能力を形式化する標準的方法であった 
    Dolev-Yao モデルを用いず，暗号研究者が安全性証明において行
    う議論を直接的に形式化するという意味で，直接的方法と呼ばれ
    る．本講演では，直接的方法にもとづく三つの研究例（Corinと
    Hartog:2006，BlanchetとPointcheval:2006，Canettiら:2006）
    をとりあげ，それらのもとになる形式的体系や，確率，計算が困
    難な問題，ランダム性等の取り扱い，および自動化への見通しな
    どを概説する．

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

  BAN 論理から Protocol Composition Logic へ
  〜セキュリティ・プロトコルの論理的分析法
    長谷部浩二(産業技術総合研究所 システム検証研究センター)
    岡田光弘(慶應義塾大学 文学部哲学科)
  [講演概要] 
    1989年にBurrows-Abadi-NeedhamによりBAN論理が提案されて以降、
    セキュリティ・プロトコルの形式的・論理的技法による安全性検
    証法の研究は飛躍的な発展を遂げてきた。この講演では、これま
    でに提起されてきた様々な安全性検証法の中でも、とりわけ論理
    推論を基にした方法のいくつかを取り上げて紹介する。特にここ
    では、BAN論理及びその後継の論理と、John C. Mitchell らのグ
    ループによるProtocol Composition Logic（PCL）及びそれに関
    連した研究（講演者らによるBasic Protocol Logic等）を中心に、
    それぞれの方法論の特徴や長所・短所などについて私観を交えな
    がら概説する。また、計算量的証明手法と形式的・論理的技法と
    の相互関係を明らかにする試みが、近年PCLの研究においても行
    われており、こうした最近の研究の動向についても紹介する。

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