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

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

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


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

【日時】

  2012年3月8日(木) 13:30--16:40

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

【会場】

  九州大学 伊都キャンパス数理IMI棟
  〒819-0395 福岡市西区元岡744
  （交通）「JR博多駅」→（地下鉄空港線）→「姪浜駅」
  （JR筑肥線へ乗換）→「九大学研都市駅」→昭和バス→九大工学部
  ※博多駅からのバスは, 渋滞等に巻き込まれる可能性があります. 

【参加費】

  会員 学生¥1000/一般¥2000; 非会員 学生¥2000/一般¥4000

【詳細情報】

  2012年春の研究部会連合発表会ホームページ: 
  http://www.comfos.org/jp/Y2011/JSIAM-AG/

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

  3月8日(木)

  [セッション１]
  座長: 花谷 嘉一 ((株)東芝 研究開発センター)

  13:30--14:00
  盗聴下通信のための符号について (30分)
  ○濱田 充 (玉川大学 量子情報科学研究所 量子情報科学研究センター)

  14:00--14:20
  形式化数学記述言語Mizarによる共通鍵暗号AESの形式化 (20分)
  ○今村 充志 (信州大学 大学院工学系研究科)
    岡崎 裕之 (信州大学 大学院工学系研究科)
    師玉 康成 (信州大学 工学部)
    講演資料

  14:20--14:50
  量子鍵配送の安全性証明の量子プロセス計算を用いた形式的検証 (30分)
  ○久保田 貴大 (東京大学大学院情報理工学系研究科)
    角谷 良彦   (東京大学大学院情報理工学系研究科)
    加藤 豪     (NTT コミュニケーション科学基礎研究所)
    河野 泰人   (NTT コミュニケーション科学基礎研究所)
    櫻田 英樹   (NTT コミュニケーション科学基礎研究所)
    講演資料

  14:50--15:10
  休憩

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

  15:10--15:40
  シャノンの定理の形式化 (30分)
  ○アフェルト レナルド (産業技術総合研究所 情報セキュリティ研究センター)
    萩原 学             (産業技術総合研究所 情報セキュリティ研究センター/
                         University of Hawaii, Department of Mathematics)

  15:40--16:10
  計算論的に健全な一階述語論理による暗号プロトコルの分析 (30分) [講演者体調不良のため発表キャンセル]
  ○バナ・ゲルゲイ (INRIA-Microsoft Research Parc Orsay Universite & ENS Paris)
    長谷部 浩二    (筑波大学 コンピュータサイエンス専攻)
    岡田 光弘      (慶応義塾大学 文学部哲学科)

  16:10--16:40
  確率論の為の論理体系 (30分)
  ○竹内 泉 (産業技術総合研究所)

【備考】

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

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

【講演概要】

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

  盗聴下通信のための符号について (30分)
  ○濱田 充 (玉川大学 量子情報科学研究所 量子情報科学研究センター)

  [講演概要] 
  情報理論において盗聴通信路 (Wiretap channel) というモデルが注目を集めている。
  このモデルにおいて、漸近的に最適な符号で明示的なもの、すなわち多項式時間構
  成可能な符号が最近著者によって見出された。この際、用いた安全性の基準は盗聴
  通信路モデルの提案時の標準的なものであったが、知られている、これを強化した
  基準 (Csiszar 1996) や更に強めた基準のもとでもやはり、やはり最適符号が多項
  式時間構成可能であることを示す。安全性基準はいずれも情報理論における相互情
  報量を用いたものである。また、提案する符号は線型符号の自然な一般化である。

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

  形式化数学記述言語Mizarによる共通鍵暗号AESの形式化 (20分)
  ○今村 充志 (信州大学 大学院工学系研究科)
    岡崎 裕之 (信州大学 大学院工学系研究科)
    師玉 康成 (信州大学 工学部)

  [講演概要] 
  本発表では，形式化数学記述言語Mizarを用いた共通鍵暗号AESの形式化記述につい
  て述べる．Mizarシステムとは，数学証明の正しさを機械的に検証しようとするプルー
  フチェッカと呼ばれるシステムの一種である．本発表ではAESのアルゴリズムの
  Mizar言語での形式化の方針および証明された結果について報告する。

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

  量子鍵配送の安全性証明の量子プロセス計算を用いた形式的検証 (30分)
  ○久保田 貴大 (東京大学大学院情報理工学系研究科)
    角谷 良彦   (東京大学大学院情報理工学系研究科)
    加藤 豪     (NTT コミュニケーション科学基礎研究所)
    河野 泰人   (NTT コミュニケーション科学基礎研究所)
    櫻田 英樹   (NTT コミュニケーション科学基礎研究所)

  [講演概要] 
  量子暗号プロトコルは, 量子力学の法則によって古典暗号プロトコルにない強い安
  全性を満たすが, その証明は一般に複雑であり検証が難しい.  Fengらは検証系とし
  て量子プロセス計算qCCSを提案し, プロセスの双模倣関係が文脈の構成で閉じるこ
  とを示した. これは形式検証において有用な性質である.  彼らは, qCCSを比較的単
  純なプロトコルの検証に適用したが, 量子暗号ような複雑な対象に対する適用はし
  ていない.そこで, 我々は, BB84のShor-Preskillによる安全性証明を, qCCSを用い
  て形式検証し,量子プロセス計算の安全性証明に対する適用への有効性と課題につい
  て考察した.

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

  シャノンの定理の形式化 (30分)
  ○アフェルト レナルド (産業技術総合研究所 情報セキュリティ研究センター)
    萩原 学             (産業技術総合研究所 情報セキュリティ研究センター/
                         University of Hawaii, Department of Mathematics)

  [講演概要] 
  通信の特性は情報の理論で記述されるが、その最も基本的な結果がシャノンの定理
  である。シャノンの定理の証明は単純ではなく、証明の詳細は入門書でもあまり述
  べられない。これは好ましくない状況である。なぜなら、コンピュータセキュリティ
  の重要な結果は情報理論を安全性根拠（無条件安全性など）としているからである。
  本発表では、証明支援系 Coq上での情報理論の形式定義や補題のライブラリの構成
  に関して報告する。今回構成するライブラリの有用性を示す結果として、圧縮と誤
  り訂正に関するシャノンの定理の形式的証明を（我々の知る限り）世界で最初に提
  供する。

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

  計算論的に健全な一階述語論理による暗号プロトコルの分析 (30分)
  ○バナ・ゲルゲイ (INRIA-Microsoft Research Parc Orsay Universite & ENS Paris)
    長谷部 浩二    (筑波大学 コンピュータサイエンス専攻)
    岡田 光弘      (慶応義塾大学 文学部哲学科)

  [講演概要] 
  計算論的に健全な一階述語論理による暗号プロトコルの安全性検証法を提案する．
  我々の検証法は，まず秘匿性やプロトコル参加者の動作を表現するための述語記号
  とその計算論的な意味論を導入する．また，計算論的に成り立つ基本的な性質のう
  ち，攻撃者の振る舞いや特定のプロトコルのパターンに依存しない一般的なものを
  論理公理として仮定する．以上で定式化された論理体系により，秘匿性や認証成立
  などといった安全性に関する種々の性質を証明することができる．この論理体系の
  有用性は，Needham-Schroeder-Loweプロトコルなどの安全性証明によって示される．

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

  確率論の為の論理体系 (30分)
  ○竹内 泉 (産業技術総合研究所)

  [講演概要] 
  暗号の理論では「確率が無視出来る位小さい」という概念が登場する。これは通常、
  解析的手法により議論されるが、この議論を抽象化して記号的な推論が出来るよう
  な論理体系があれば、安全性の証明等が容易になる。本発表では、このような論理
  体系を設計することを目指した研究の現状を報告し、参加者の助言を仰ぐ。

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

【問い合わせ先】

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