第19回日本応用数理学会研究部会連合発表会
「数理的技法による情報セキュリティ」(FAIS)
オーガナイズド・セッション
日本応用数理学会研究部会連合発表会は2023年3月8日（水）〜10日（金）に岡山理科大学
岡山キャンパスを会場に現地とオンラインのハイブリッド形式で開催されます：
【日時】
3月10日(金) 9:20-10:40 および 11:10-12:30 (各80分)
【会場】
岡山理科大学岡山キャンパス
〒700-0005 岡山県岡山市北区理大町1-1
および
オンライン
【参加方法】
研究部会連合発表会webページをご覧ください.
★今回は森岡澄夫様(インターステラテクノロジズ)に
「商用宇宙ロケット開発における形式検証の必要性と基盤研究への期待」
と題しまして企画講演をお願いしております!★
【プログラム】(○:登壇者)
研究部会 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 ホームページ＊
最終更新: 2023.2.25