JSIAM-FAIS Home Page: JSIAM 2023 Spring FAIS Session

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

第19回日本応用数理学会研究部会連合発表会「数理的技法による情報セキュリティ」(FAIS) オーガナイズド・セッション日本応用数理学会研究部会連合発表会は2023年3月8日（水）〜10日（金）に岡山理科大学岡山キャンパスを会場に現地とオンラインのハイブリッド形式で開催されます： https://jsiam.org/union2023/ 【日時】 3月10日(金) 9:20-10:40 および 11:10-12:30 (各80分) 【会場】岡山理科大学岡山キャンパス〒700-0005 岡山県岡山市北区理大町1-1 　および　オンライン【参加方法】研究部会連合発表会webページをご覧ください. https://jsiam.org/union2023/

★今回は森岡澄夫様(インターステラテクノロジズ)に「商用宇宙ロケット開発における形式検証の必要性と基盤研究への期待」と題しまして企画講演をお願いしております!★

【プログラム】(○:登壇者) 研究部会 OS: 数理的技法による情報セキュリティ(1) ［3月10日：09:20-10:40］座長: 吉田真紀 09:20-10:20 ★企画講演★ 商用宇宙ロケット開発における形式検証の必要性と基盤研究への期待 (60分) ○森岡澄夫（インターステラテクノロジズ株式会社）講演資料 10:20-10:40 数理的技法による情報セキュリティの最近の研究動向 (20分) ○中林美郷（NTT社会情報研究所）, 吉田真紀（国立研究開発法人情報通信研究機構）, 花谷嘉一（（株)東芝）, 山本光晴（千葉大学）, 米山一樹（茨城大学）講演資料研究部会 OS: 数理的技法による情報セキュリティ(2) ［3月10日：11:10-12:30］座長: 山本光晴 11:10-11:30 FIDO2の形式化の再考と複数モードの検証への拡張 (20分) ○佐藤瑞己（茨城大学）, 米山一樹（茨城大学）講演資料 11:30-11:50 Revisiting the security analysis against 2F method (20分) ○池松泰彦（九州大学マス・フォア・インダストリ研究所）, Duong Dung（University of Wollongong）, 安田貴徳（岡山理科大学） 11:50-12:10 ProVerifによるトークン型電子現金プロトコルの形式検証 (20分) 山本輪（長崎大学）, ○江島奨悟（長崎大学）, 奥田哲矢（NTT社会情報研究所）, 荒井研一（長崎大学）講演資料 12:10-12:30 ProVerifとTamarin-proverの観測等価性の違い (20分) ○三重野武彦（エプソンアヴァシス株式会社, 信州大学）, 岡崎裕之（信州大学）, 荒井研一（長崎大学）, 布田裕一（東京工科大学）講演資料【講演概要】 ★企画講演★ 商用宇宙ロケット開発における形式検証の必要性と基盤研究への期待 (60分) ○森岡澄夫（インターステラテクノロジズ株式会社） [概要] 宇宙ロケット搭載コンピュータのソフトウェアは飛行誘導や機械制御，安全性判断など　クリティカルな処理を多数実行しており，網羅的検証が必要である．しかし商用宇宙機では開発　コストに強い制限があり，検証工数を無尽蔵に投入できないため，形式検証の効果的導入が望ましい．　いっぽう形式検証は万能ではなく，適用対象や検証可能規模に依然として制約がある．　本発表では弊社のロケットMOMO, ZEROを具体事例とし，重要な検証項目や，今後の発展を期待　する形式検証技法などについて述べる． -------------------------------------------------------------------------- 数理的技法による情報セキュリティの最近の研究動向 (20分) ○中林美郷（NTT社会情報研究所）, 吉田真紀（国立研究開発法人情報通信研究機構）, 花谷嘉一（（株)東芝）, 山本光晴（千葉大学）, 米山一樹（茨城大学） [概要] 数理的技法による情報セキュリティに関する2022年の研究動向として、調査した国際会議の一覧、　各会議ごとの特色、FAISに関係する講演の件数、分野の内訳を紹介する。さらに、全体を通した　トレンドや特に注目されている分野と論文を紹介する。 -------------------------------------------------------------------------- FIDO2の形式化の再考と複数モードの検証への拡張 (20分) ○佐藤瑞己（茨城大学）, 米山一樹（茨城大学） [概要] FIDO2はトークンなどを用いたパスワードレス認証の実現を目的として標準化されているプロトコルである。　ESORICS 2022において、GuanらはFIDO2に対するProverifを用いた安全性の形式検証を行った。　彼らは、FIDO2をサブプロトコルであるWebAuthn2とCTAP2の仕様に沿って形式化し、秘密情報の漏えいなどを考慮した安全性を検証している。　我々は、まずGuanらの形式化の証明書の取り扱いに関する軽微なミスを指摘し、修正する。　次に、Guanらが形式化していなかったWebAuthn2のいくつかのモードとCTAPの異なる仕様の組み合わせについて形式化と検証を行う。　結果として、WebAuthn2におけるユーザ-クライアント間の認証性について、より弱めた攻撃者の下で、異なる攻撃が存在することを示す。 -------------------------------------------------------------------------- Revisiting the security analysis against 2F method (20分) ○池松泰彦（九州大学マス・フォア・インダストリ研究所）, Duong Dung（University of Wollongong）, 安田貴徳（岡山理科大学） [概要] 　モジュラススイッチはNTRUをはじめ多くの格子暗号で使われるメソッドである。　PQC2022でSmith-Toneによって、　モジュラススイッチを使い既存の多変数多項式暗号の安全性を強化する2Fメソッドが提案された。　その中では格子簡約アルゴリズムを使った攻撃が考えられており、　多変数多項式暗号の直接攻撃よりも非効率であることが述べられている。　今回の発表では、格子サイズをカットする格子攻撃の改良を考え、　2Fメソッドで得られる128ビット安全性パラメータをもつ暗号方式に対して、　標準的なPCで1時間以内で2Fメソッドを無力化できることを報告する。 -------------------------------------------------------------------------- ProVerifによるトークン型電子現金プロトコルの形式検証 (20分) 山本輪（長崎大学）, ○江島奨悟（長崎大学）, 奥田哲矢（NTT社会情報研究所）, 荒井研一（長崎大学） [概要] ProVerifはBlanchetらが開発した形式モデル（Dolev-Yaoモデル）での暗号プロトコルの自動検証ツールであり，　暗号プロトコルに要求される秘匿や認証などの安全性要件を自動で検証することができる．本発表では，　第99回CSEC研究会（トークン型電子現金方式の形式検証手法に関する初期検討）において述べられている，　利用者の間でオフラインで流通可能な電子現金プロトコルを対象として，ProVerifを用いて形式的に記述し，　安全性検証を行った際の工夫点や形式化のテクニックについて報告する． -------------------------------------------------------------------------- ProVerifとTamarin-proverの観測等価性の違い (20分) ○三重野武彦（エプソンアヴァシス株式会社, 信州大学）, 岡崎裕之（信州大学）, 荒井研一（長崎大学）, 布田裕一（東京工科大学） [概要] 暗号学のセキュリティの特性は,トレース特性と観測等価特性の2種類に分けられる. トレース特性は, モデル化したプロトコルの検証トレースに対して後方探索などの探索手法を用いて攻撃出来る網羅性を探索する. 一方観測等価性は, 攻撃者が2つの状況を区別できないことを表し, 秘匿性や強秘匿性を検証するために用いられる. 安全性の自動検証ツール ProVerifと, Tamarin-proverのトレース特性や, 観測等価性にはどのような違いがあるかを調査している. 特に本講演では, DDHプロトコルを形式化し, 両ツールにおける観測等価性の違いを調査し考察する. 【問い合わせ先】 FAIS幹事団 fais-kanji@ml.jsiam.org (下記幹事団に届きます) 代表：吉田真紀（情報通信研究機構）幹事（五十音順）：櫻田英樹（日本電信電話(株) NTTコミュニケーション科学基礎研究所）花谷嘉一（(株)東芝研究開発センター）山本光晴（千葉大学大学院理学研究院）米山一樹（茨城大学工学部情報工学科）＊JSIAM-FAIS ホームページ＊ http://fais.jsiam.org/

FAISホームページ

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

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

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