日本応用数理学会2025年度年会
「数理的技法による情報セキュリティ」(FAIS)
オーガナイズド・セッション
日本応用数理学会2025年度年会が2025年9月2日(火)～2025年9月4日(木)に
東京理科大学 神楽坂キャンパスにて開催されます：
＊年会webページ＊
「数理的技法による情報セキュリティ」(FAIS)研究部会も, 下記の日程で
オーガナイズド・セッション(OS)を開催いたします:
【日時】
9月4日(木) 13:20-14:40 および 15:00-16:20
【会場】
東京理科大学 神楽坂キャンパス C会場 (223教室)
【参加方法】
年会webページをご覧ください.
【プログラム】(○:登壇者)
下記の2セッションを予定しています.
研究部会OS: 数理的技法による情報セキュリティ(1) ［9月4日：13:20-14:40］
座長: 米山 一樹（茨城大学）
[企画講演] 自動運転システムの形式検証手法の確立に向けて
○冨田 尭（北陸先端科学技術大学院大学）
数理的技法による情報セキュリティの2024年度後半＆2025年度前半の研究動向
荒井 研一（長崎大学）, 鈴木 幸太郎（豊橋技術科学大学）, 中林 美郷（NTT 社会情報研究所）,
花谷 嘉一（株式会社東芝）, ○三重野 武彦（EPSON AVASYS株式会社）,
山本 光晴（千葉大学）, 吉田 真紀（国立情報通信研究機構）, 米山 一樹（茨城大学）
研究部会OS: 数理的技法による情報セキュリティ(2) ［9月4日：15:00-16:20］
座長: 櫻田 英樹（ZEN大学）
LWE問題とケーリー・ハミルトンの定理
○白勢 政明（公立はこだて未来大学）
ProVerifによるBGPセキュリティ機構の形式的安全性検証
○神谷 海登（信州大学）, 三重野 武彦（EPSON AVASYS, 信州大学）, 岡崎 裕之（信州大学）,
鈴木 彦文（NII）, 荒井 研一（長崎大学）, 布田 裕一（東京工科大学）
ProVerifによる線形秘密分散の形式化とSPDZの検証への応用
○渡部 翔（茨城大学）, 三田 翔平（茨城大学）, 米山 一樹（茨城大学）
An Approach to Formalize Information-theoretic Security of Multiparty Computation Protocols
○Weng Cheng Hui（名古屋大学）, Affeldt Reynald（產業技術綜合研究所）,
Garrigue Jacques （名古屋大学）, 才川 隆文（名古屋大学）
【講演概要】
[企画講演] 自動運転システムの形式検証手法の確立に向けて
○冨田 尭（北陸先端科学技術大学院大学）
[概要]
近年，自動運転システムの実用化に向けた研究開発や実証実験が活発に行わ
れている．安全安心なモビリティ社会の実現のためには，自動運転を構成す
る認識，判断・経路計画，制御などすべての要素を包括した合理的かつ実行
可能な仕様・シナリオ記述方法や検証・テスト方法が必須である．
本講演では，自動運転システムの安全性・信頼性を保証するための形式手法
及び検証ツールの開発に向けた取り組みについて紹介する．
--------------------------------------------------------------------------
数理的技法による情報セキュリティの2024年度後半＆2025年度前半の研究動向
荒井 研一（長崎大学）, 鈴木 幸太郎（豊橋技術科学大学）, 中林 美郷（NTT 社会情報研究所）,
花谷 嘉一（株式会社東芝）, ○三重野 武彦（EPSON AVASYS株式会社）,
山本 光晴（千葉大学）, 吉田 真紀（国立情報通信研究機構）, 米山 一樹（茨城大学）
[概要]
数理的技法は暗号プロトコルやシステムの安全性検証など，情報セキュリティ
の様々な分野で応用されている．
本発表では，数理的技法による情報セキュリティに関する2024年後半と2025
年度前半の研究動向として，2024年9月から2025年8月までに開催されたトッ
プ会議における関連論文の発表件数や特色，概要について紹介する．さらに，
全体を通したトレンドや特に注目されている分野と論文を紹介する．
--------------------------------------------------------------------------
LWE問題とケーリー・ハミルトンの定理
○白勢 政明（公立はこだて未来大学）
[概要]
b=sA+eという関係のある探索LWE問題(A,b)に対して、
線形代数学のケーリー・ハミルトンの定理を適用することで、
ノイズベクトルeの一部に関する線形関係式が得られる場合があることを示す。
--------------------------------------------------------------------------
ProVerifによるBGPセキュリティ機構の形式的安全性検証
○神谷 海登（信州大学）, 三重野 武彦（EPSON AVASYS, 信州大学）, 岡崎 裕之（信州大学）,
鈴木 彦文（NII）, 荒井 研一（長崎大学）, 布田 裕一（東京工科大学）
[概要]
BGPは、インターネットの基幹ルーティングプロトコルであるが、セキュリ
ティについて考慮されておらず経路ハイジャック攻撃等の脅威に晒されてい
る。そこでROVやASPAなどの防御機構が提案されているが、従来の評価手法
は主にシミュレーションベースであり、攻撃パターンの網羅性や防御効果の
理論的保証に限界があった。本研究では、形式検証ツールProVerifを用いて、
BGP防御機構適用時の安全性のモデル検査を試みる。具体的には、BGPを拡張
π計算でモデル化し、ROV単体、ASPA単体、および両者の組み合わせ時にお
ける経路真正性をProVerifで検証し、各防御機構の有効性を評価する。さら
に、網羅的な攻撃探索により従来手法では発見困難な新たな攻撃シナリオの
発見を目指す。本研究により、既存防御機構の安全性保証レベルの明確化、
未知攻撃パターンの発見、および防御機構の組み合わせ戦略に向けた理論的
指針の提供を目指す。
--------------------------------------------------------------------------
ProVerifによる線形秘密分散の形式化とSPDZの検証への応用
○渡部 翔（茨城大学）, 三田 翔平（茨城大学）, 米山 一樹（茨城大学）
[概要]
秘密分散法に基づく秘密計算の安全性について，ProVerifを用いた形式検証
の事例はこれまでに知られていない．本研究では，ProVerifによるShamirの
(n-out-of-n)秘密分散法と加法型秘密分散法のそれぞれの形式化手法を提案
する．本講演では特に，シェアおよび定数による演算の線形性の形式化と，
SPDZの出力フェーズにおける不正検知の検証について論じる．
--------------------------------------------------------------------------
An Approach to Formalize Information-theoretic Security of Multiparty Computation Protocols
○Weng Cheng Hui（名古屋大学）, Affeldt Reynald（產業技術綜合研究所）,
Garrigue Jacques （名古屋大学）, 才川 隆文（名古屋大学）
[概要]
Secure multiparty computation (hereafter, SMC) refers to
cryptographic protocols that allow multiple parties to jointly
compute a function over their inputs while keeping them private. The
main security property of SMC protocols is information leakage
freedom, whose proofs can be found in the scientific literature for
idealized models. But how does one guarantee that information
leakage freedom still holds once SMC is implemented as a concrete
piece of software? As a step toward solving this problem, we use
the proof assistant Rocq to formalize the security claims of an SMC
stack. We develop a method based on an interpreter for a subset of
the 𝜋-calculus in which protocols can be modeled as programs and
then input traces verified for correctness and information leakage
freedom. Thanks to this approach, the properties of SMC can be
established in a clearly defined trusted base that can be reused to
verify other SMC stacks.
【問い合わせ先】
FAIS幹事団 fais-kanji@ml.jsiam.org (下記幹事団に届きます)
代表：
吉田 真紀（情報通信研究機構）
幹事（五十音順）：
櫻田 英樹（ZEN大学 知能情報社会学部 知能情報社会学科）
花谷 嘉一（(株)東芝 研究開発センター）
山本 光晴（千葉大学 大学院理学研究院）
米山 一樹（茨城大学 工学部 情報工学科）