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

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

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

日本応用数理学会2007年度年会が, 2007年9月15(土)から9月17日(月)にかけて, 
北海道大学にて開催されます. 「数理的技法による情報セキュリティ」(FAIS)
研究部会も, 下記の日程でオーガナイズドセッションを開催いたします. 
奮ってご参加下さいますようお願い申し上げます. 

[年会ホームページ]
    http://www.jsiam.org/annualmeeting/2007/

[FAIS 研究部会ホームページ]
    http://fais.jsiam.org/

【日時】

    2007年9月15日(土) 14:10〜17:20

【会場】

    北海道大学 工学部 (札幌市北区北13条西8丁目)

【参加方法】

    年会ホームページをご覧ください. 
    参加の事前登録受付は8月17日(金)までです. 

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

    座長: 赤間 陽二 (東北大学大学院理学研究科)

    14:10--14:50 (40分) 
    [FAIS 特別講演] 暗号プロトコルの安全性　
      −セキュリティの世界に形式的検証から入った研究者の立場から−
    ○藤原 融 (大阪大学大学院情報科学研究科)

    講演資料

    14:50--15:10 (20分) 
    ブラインド署名を扱うことが可能な計算論的に健全なプロトコル検証法
    ○櫻田 英樹 (NTT コミュニケーション科学基礎研究所)
      萩谷 昌己 (東京大学大学院情報理工学系研究科
                 /NTT コミュニケーション科学基礎研究所)

    15:10--15:30 (20分)
    証明可能安全性の形式的証明：定理証明ツールによるゲームの手法
      Reynald Affeldt (産業技術総合研究所 情報セキュリティ研究センター)
    ○田中 三貴 (情報通信研究機構 情報通信セキュリティ研究センター)
      Nicolas Marti (東京大学)

    講演資料

    15:30--15:40 (10分) 
    休憩

    15:40--16:00 (20分) 
    CryptoVerif のための MAC の安全性の定式化に関する考察
    ○荒井 研一 (信州大学大学院総合工学系研究科)
      岡崎 裕之 (信州大学大学院工学系研究科)
      不破 泰 (信州大学大学院工学系研究科)

    講演資料

    16:00--16:20 (20分)
    task-PIOAフレームワークとBlanchetのフレームワークの証明能力に関する一考察
    ○花谷 嘉一 ((株)東芝 研究開発センター)
      米山 一樹 (電気通信大学)
      國分 雄一 (電気通信大学)
      太田 和夫 (電気通信大学)

    講演資料

    16:20--16:40 (20分)
    タスク PIOA の統計的 Simulation 関係に関する考察
    ○古田 憲一郎 ((株)東芝 研究開発センター)
      村谷 博文 ((株)東芝 研究開発センター)
      花谷 嘉一 ((株)東芝 研究開発センター)

    講演資料

    16:40--17:00 (20分)
    CSF'07, FCC'07 参加報告
    ○櫟 粛之 (NTT コミュニケーション科学基礎研究所)

    17:00--17:20 (20分)
    FCS-ARSPA'07 参加報告
    ○米山 一樹 (電気通信大学)
      太田 和夫 (電気通信大学)

    講演資料


    講演の概要については下記をご覧下さい. 

    都合によりプログラムが変更になる可能性があります. 
    最新情報は FAIS 研究部会のホームページでご確認ください. 

【問い合わせ先】

    塚田 恭章
    NTTコミュニケーション科学基礎研究所
    tsukada(at)theory.brl.ntt.co.jp
    (「数理的技法による情報セキュリティ」セッション オーガナイザ)

【講演概要】

  --------------------------------------------------------------------
    
    暗号プロトコルの安全性　
      −セキュリティの世界に形式的検証から入った研究者の立場から−
      藤原 融 (大阪大学)
    [講演概要]
      講演者は、Dolev-Yao Model の提案と同時期から暗号プロトコル
      の形式的検証を行ってきた。本講演では、講演者が行ってきた暗
      号プロトコルの形式的検証やその周辺について紹介する。また、
      今後のプロトコル安全性検証についても話題提供できればと考え
      ている。

  --------------------------------------------------------------------
    
    ブラインド署名を扱うことが可能な計算論的に健全なプロトコル検証法
      櫻田 英樹 (NTT), 萩谷 昌己 (東京大学/NTT)
    [講演概要]
      本講演ではセキュリティ・プロトコルを記号的に検証する方法を
      提案する．提案方法は，ブラインド署名を用いるプロトコルを扱
      うことができ，検証されたプロトコルが計算論的な意味において
      も安全である初めての方法である．ブラインド署名は文書の内容
      を署名者に知らせずに署名させることが可能な電子署名の一種で
      あり，電子投票などのプロトコルで匿名性を保証するために用い
      られる．提案方法では，署名者へ送られるブラインド化されたメッ
      セージを，記号的にはノンス（乱数）として扱うことで，計算論
      的に健全な検証を可能にした．

  --------------------------------------------------------------------
    
    証明可能安全性の形式的証明：定理証明ツールによるゲームの手法
      Reynald Affeldt (産業技術総合研究所), 田中 三貴 (情報通信研究機構), 
      Nicolas Marti (東京大学)
    [講演概要]
      ゲーム列による証明手法は，証明し易い安全性証明を構成するた
      めの方法である．安全性性質や計算量的問題はプログラムとして
      記述され，リダクションによる証明はプログラム書換の列として
      表現される．その明らかなプログラム言語的指向性からコンパイ
      ラの構成手法の適用が想定されるが，その場合健全性の証明が問
      題となってくる．本発表では，安全性証明の構成ツールとして定
      理証明支援系 Coq 上でのゲーム手法の形式化を提案する．確率
      的プログラミング言語を形式的に定義し，安全性証明に必要な性
      質を全て Coq 上で表現・証明することで健全性が保証できる．
      具体的には，Bellare と Rogaway によるゲーム手法の枠組みを
      形式化し，Fundamental lemma 等の各補題，応用例として 
      PRP/PRF Switching Lemma の証明を紹介する．

  --------------------------------------------------------------------
    
    CryptoVerif のための MAC の安全性の定式化に関する考察
      荒井 研一 (信州大学), 岡崎 裕之 (信州大学), 不破 泰 (信州大学)
    [講演概要]
      Blanchet らは，計算論的アプローチにおいて，ゲーム列で安全
      性を証明する手法を数理的アプローチに適応し，計算論的安全性
      を数学的技法で自動証明することに成功した．彼らは，提案手法
      を実装したプログラムである CryptoVerif を公開し，既に FDH 
      署名方式の UF-CMA を自動検証することに成功している．
      本講演では，MAC (Message Authentication Code) の安全性の定
      式化に関する考察を行う．

  --------------------------------------------------------------------
    
    task-PIOAフレームワークとBlanchetのフレームワークの証明能力に関する一考察
      花谷 嘉一 (東芝), 米山 一樹 (電気通信大学), 國分 雄一 (電気通信大学), 
      太田 和夫 (電気通信大学)
    [講演概要]
      task-PIOA フレームワークは，二つのシステムを task-PIOA の
      形式で表現し，その間にある対応関係が成立するか評価すること
      で安全性を検証するフレームワークである．
      一方，Blanchet のフレームワークは，システムへの攻撃 Game 
      とその書き換えルールを Blanchet のプロセス計算の形式で表現
      し，書き換えルールを用いて安全性が成立する Game に書き換え
      可能か検証するフレームワークである．
      この二つのフレームワークの証明能力の差について考察を行う．

  --------------------------------------------------------------------
    
    タスク PIOA の統計的 Simulation 関係に関する考察
      古田 憲一郎 (東芝), 村谷 博文 (東芝), 花谷 嘉一 (東芝)
    [講演概要]
      タスク PIOA を用いた安全性証明の枠組みでは、現実プロトコル
      から理想プロトコルへの Implementation 関係を示すことで安全
      性が示される。プロトコル間において、Simulation 関係が成り
      立つならば Implementation 関係が成り立つ。本稿では、
      Simulation 関係を拡張し統計的 Simulation 関係を提案する。
      これは、確率変数族間の統計的識別不可能性とのアナロジーによ
      り、上述の2つの関係の間にある関係として定義される。プロト
      コル間の Simulation 関係が示せない場合でも、統計的 
      Simulation 関係が示せれば安全性が証明される。

  --------------------------------------------------------------------
    
    CSF'07, FCC'07 参加報告
      櫟 粛之 (NTT)
    [講演概要]
      セキュリティの形式的基礎理論に関する代表的会議である CSF,
      FCC の参加報告を行う。

  --------------------------------------------------------------------
    
    FCS-ARSPA'07 参加報告
      米山 一樹 (電気通信大学), 太田 和夫 (電気通信大学)
    [講演概要]
      7/8にポーランド（ブロツワフ）にて行われた国際会議 
      FCS-ARSPA'07 の参加報告を行う．FCS-ARSPA ではセキュリティ
      プロトコルの自動証明を専門に扱っており，FAIS 研究会とも関
      連の深い会議である．本発表では，それぞれの講演内容について
      簡単な紹介を行う予定である．

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