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

第20回日本応用数理学会研究部会連合発表会

              第20回日本応用数理学会研究部会連合発表会
             「数理的技法による情報セキュリティ」(FAIS)
                    オーガナイズド・セッション

日本応用数理学会研究部会連合発表会が2024年3月4日(月)〜6日(水)に
長岡技術科学大学で開催されます：

      ＊研究部会連合発表会webページ＊
        https://jsiam.org/union2024/

【日時】

  3月4日(月) 9:40-10:40 および 11:10-12:10 (各60分)

【会場】

  長岡技術科学大学
  〒940-2188 新潟県長岡市上富岡町1603-1

【参加方法】

  研究部会連合発表会webページをご覧ください. 
  https://jsiam.org/union2024/




★今回は竹内勇貴様（日本電信電話（株））に
「量子コンピュータの基礎と検証」
と題しまして企画講演をお願いしております!★




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

  研究部会 OS: 数理的技法による情報セキュリティ(1) ［3月4日：09:40-10:40］
  座長: 米山 一樹（茨城大学）

  09:40-10:40
  ★企画講演★ 量子コンピュータの基礎と検証 (60分)
  ○竹内 勇貴（日本電信電話（株））
  講演資料

  研究部会 OS: 数理的技法による情報セキュリティ(2) ［3月4日：11:10-12:10］
  座長: 吉田 真紀（情報通信研究機構）

  11:10-11:30
  FIDO2における中間者攻撃の影響のProVerifを用いた検証 (20分)
  ○西 総一朗（豊橋技術科学大学）, 中井 雄士（豊橋技術科学大学）, 鈴木 幸太郎（豊橋技術科学大学）
  講演資料

  11:30-11:50
  ProVerifとTamarin-proverを開発支援プロセスへ導入するための考察その2 (20分)
  ○三重野 武彦（エプソンアヴァシス株式会社, 信州大学）, 岡崎 裕之（信州大学）, 荒井 研一（長崎大学）, 布田 裕一（東京工科大学）
  講演資料

  11:50-12:10
  数理的技法による情報セキュリティに関する2023年の研究動向 (20分)
  ○中林 美郷（NTT社会情報研究所）, 鈴木 幸太郎（豊橋技科大学）, 花谷 嘉一（（株)東芝）, 山本 光晴（千葉大学）, 吉田 真紀（情報通信研究機構）, 米山 一樹（茨城大学）
  講演資料

【講演概要】

  ★企画講演★ 量子コンピュータの基礎と検証
  ○竹内 勇貴（日本電信電話（株）） (60分)
  [概要]
  近年、従来のコンピュータ(古典コンピュータ)よりも高い計算能力を有する
  と期待されている量子コンピュータの開発が世界中で盛んになっている。特
  に、量子コンピュータは個人で所有するのが困難なため、現在のスーパーコ
  ンピュータと同様、クラウド方式での運用が有望視されている。本発表では、
  まず初めに、量子コンピュータの基礎や現状を紹介する。その後、クラウド
  量子コンピュータの実現に重要な「量子コンピュータの検証」という技術を、
  自身の研究成果を交えつつ紹介する。

--------------------------------------------------------------------------
  FIDO2における中間者攻撃の影響のProVerifを用いた検証 (20分)
  ○西 総一朗（豊橋技術科学大学）, 中井 雄士（豊橋技術科学大学）, 鈴木 幸太郎（豊橋技術科学大学）
  [概要]
  FIDO2は認証器を用いたパスワードレス認証フレームワークであり,
  WebAuthnとCTAPの2つのサブプロトコルにより構成される.

  Barbosaら (CRYPTO 2021)はFIDO2の安全性解析を行い, CTAP2の内部で使用
  される鍵交換プロトコルにおいて中間者攻撃を指摘した. 2023年12月時点に
  おいて当該脆弱性に関する修正は確認されていない. 本研究では, CTAP2に
  おける中間者攻撃がFIDO2の安全性にどのような影響を及ぼすかの検証を行っ
  た. 複数の認証器が存在するモデルを提案し, 攻撃者が認証器をすり替えて
  登録できるか否かをProVerifで形式的に検証した. 結果として, 攻撃者が正
  規ユーザの認証器登録プロセスに介入し中間者攻撃を行うことで, 正規ユー
  ザに自身の認証器が登録されたと誤認させつつ, 実際には攻撃者の認証器が
  登録される攻撃を発見した.

--------------------------------------------------------------------------
  ProVerifとTamarin-proverを開発支援プロセスへ導入するための考察その2 (20分)
  ○三重野 武彦（エプソンアヴァシス株式会社, 信州大学）, 岡崎 裕之（信州大学）, 荒井 研一（長崎大学）, 布田 裕一（東京工科大学）
  [概要]
  ProVerifは, モデルによって“cannot be proved”, すなわち, ProVerif
  では検証結果が判断できないので, 検証者に攻撃導出手順の判断を委ねるこ
  とがある.
  この場合にTamarin prover を用い, 同じモデルを検証することで, 厳密に
  セキュリティ特性や弱点を判断することができる可能性があるため, 両ツー
  ルの検証結果の違いを検証し, 開発支援プロセスへ導入するための考察を行っ
  ている.
  SCIS2024では, ProVerif が観測等価性の同値性が成立しない場合:
  “Observational equivalence cannot be proved.” を出力するモデルの検
  証を実施したが, Tamarin proverを用いて検証結果を補填できるまでには至
  らなかった. そのため, 本講演はその継続検証と考察を報告する.

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

【問い合わせ先】

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

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

＊JSIAM-FAIS ホームページ＊
     http://fais.jsiam.org/
最終更新: 2024.3.21
FAISホームページにもどる.