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

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

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

日本応用数理学会2024年度年会が2024年9月14日(土)～2024年9月16日(月)に
京都大学にて開催されます：

     ＊年会webページ＊
       https://jsiam.org/annual2024/

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

【日時】

  9月15日(日) 9:30-10:30 および 10:50-12:10

【会場】

  京都大学 大学院理学研究科 201教室

【参加方法】

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

【プログラム】

  下記の2セッションを予定しています.

  研究部会OS: 数理的技法による情報セキュリティ(1) ［9月15日：9:30-10:30］
  座長: 山本 光晴 (千葉大学)

  [企画講演] Isabelle/HOLを用いた差分プライバシーの形式的検証
  ○佐藤 哲也 (東京工業大学)


  研究部会OS: 数理的技法による情報セキュリティ(2) ［9月15日：10:50-12:10］
  座長: 花谷 嘉一 (株式会社 東芝)

  数理的技法による情報セキュリティに関する2024年度前半の研究動向
  荒井 研一 (長崎大学), 鈴木 幸太郎 (豊橋技術科学大学), 中林 美郷 (NTT 社会情報研究所),
  花谷 嘉一 (株式会社 東芝), 三重野 武彦 (EPSON AVASYS 株式会社), 山本 光晴 (千葉大学),
  ○吉田 真紀 (情報通信研究機構), 米山 一樹 (茨城大学)

  LWE暗号の弱鍵について
  ○白勢 政明 (公立はこだて未来大学)

  Tamarin proverの Heuristic Oracleを利用した CPA Modelの安全性検証
  ○三重野 武彦 (EPSON AVASYS 株式会社, 信州大学), 岡崎 裕之(信州大学),
  荒井 研一(長崎大学), 布田 裕一(東京工科大学)

  カードベース暗号の形式検証の再考
  ○藤田 和弘 (茨城大学), 米山 一樹 (茨城大学), 品川 和雅 (茨城大学 / 産業技術総合研究所)

【講演概要】

  [企画講演] Isabelle/HOLを用いた差分プライバシーの形式的検証
  ○佐藤 哲也 (東京工業大学)
  [概要]
  差分プライバシーは、ノイズ付加で匿名化したデータベースのプライバシー
  基準で、出力から内部データが漏れないことを数学的に保証する。プライバ
  シーを保証したままノイズを小さくするなどの課題を解決するため、差分プ
  ライバシーには厳密な検証が必要とされる。定理証明支援系は、数学の定理
  証明を支援するソフトウェアで、数学における定義や命題を形式的に表現し、
  推論の各ステップで誤りがない定理証明を可能とする。本講演では、定理証
  明支援系 Isabelle/HOL 上での差分プライバシーの形式検証の途中経過を紹
  介する。

  --------------------------------------------------------------------------
  数理的技法による情報セキュリティに関する2024年度前半の研究動向
  荒井 研一 (長崎大学), 鈴木 幸太郎 (豊橋技術科学大学), 中林 美郷 (NTT 社会情報研究所),
  花谷 嘉一 (株式会社 東芝), 三重野 武彦 (EPSON AVASYS 株式会社), 山本 光晴 (千葉大学),
  ○吉田 真紀 (情報通信研究機構), 米山 一樹 (茨城大学)
  [概要]
  数理的技法による情報セキュリティに関する2024年度前半の研究動向として，
  調査した国際会議の一覧，各会議ごとの特色，FAISに関係する講演の件数，
  分野の内訳を紹介する．さらに，全体を通したトレンドや特に注目されてい
  る分野と論文を紹介する．

  --------------------------------------------------------------------------
  LWE暗号の弱鍵について
  ○白勢 政明 (公立はこだて未来大学)
  [概要]
  有限体Fp成分の(n,m)行列Aとn次ベクトルs、m次ベクトルe、
  及びb=sA+eで計算されるm次ベクトルbに対して、
  (A,b)からsを求める問題をLWE問題という。
  但し、AとsはFp上一様ランダムに選ばれ、eは離散正規分布に従って選ばれる。
  LWE暗号は、(A,b)を公開鍵、sを秘密鍵とする耐量子計算機暗号である。

  m=2nを仮定して、A=(A0 A1)とし、W=A0^(-1) A1とすると、
  Wが対角行列ならばLWE問題(A,b)を短時間で解くことができることを実証した。
  このことからLWE暗号の弱鍵を生成できる可能性がある。

  --------------------------------------------------------------------------
  Tamarin proverの Heuristic Oracleを利用した CPA Modelの安全性検証
  ○三重野 武彦 (EPSON AVASYS 株式会社, 信州大学), 岡崎 裕之(信州大学),
  荒井 研一(長崎大学), 布田 裕一(東京工科大学)
  [概要]
  Chosen Plaintext Attack(CPA)は, 攻撃者が選択した平文に対して, 暗号文
  を取得できることを前提とした暗号解読の攻撃モデルである. これは, 攻撃
  者がブラックボックスとみなした暗号化Oracleと対話できるようにすること
  で形式化される. 本稿では, Dolev–Yaoモデルのプロトコル検証ツールであ
  る Tamarin proverを用い, 幅優先探索(BFS)と組み合わせることができる
  Heuristic Oracleを使用して, CPAモデルの安全性検証を実施した.
  Tamarin proverの正式な扱いは, Schmitらによって与えられているが,
  Heuristic Oracleを使用する検証は, Tamarin proverがデフォルトで実行す
  る標準的な攻撃発見手法(完全自動モード) に比べて, 証明探索の選択肢を
  カスタムで記述できる. 目的の証明に繋がるHeuristic Oracleを導入するこ
  とで, 効率的に証明したいlemmaを検証することができることを示す.

  --------------------------------------------------------------------------
  カードベース暗号の形式検証の再考
  ○藤田 和弘 (茨城大学), 米山 一樹 (茨城大学), 品川 和雅 (茨城大学 / 産業技術総合研究所)
  [概要]
  近年、物理的に実行可能な秘密計算プロトコルとしてカードベース暗号が盛
  んに研究されている。Kochらはカードベース暗号におけるカード枚数やステッ
  プ数の下界の形式手法に基づく検証手法を提案した。本稿では、Kochらの手
  法におけるプロトコルの安全性条件の記述の問題点を具体的な反例を用いて
  指摘するとともに、その修正方法を示す。


【問い合わせ先】

  FAIS幹事団 fais-kanji@ml.jsiam.org (下記幹事団に届きます)

       代表：
         吉田 真紀（情報通信研究機構）
       幹事（五十音順）：
         櫻田 英樹（日本電信電話(株) NTTコミュニケーション科学基礎研究所）
         花谷 嘉一（(株)東芝 研究開発センター）
         山本 光晴（千葉大学 大学院理学研究院）
         米山 一樹（茨城大学 工学部 情報工学科）
FAISホームページにもどる.