日本応用数理学会2026年度年会
「数理的技法による情報セキュリティ」(FAIS)
オーガナイズド・セッション
日本応用数理学会2026年度年会が2026年9月15日(火)～2026年9月17日(木)に
福岡国際会議場にて開催されます：
＊年会webページ＊
「数理的技法による情報セキュリティ」(FAIS)研究部会も, 下記の日程で
オーガナイズド・セッション(OS)を開催いたします:
【日時】
9月16日(水) 9:00～10:20 および 10:40～12:00
【会場】
福岡国際会議場 402室
【参加方法】
年会webページをご覧ください.
【プログラム】(○:登壇者)
下記の2セッションを予定しています.
研究部会OS: 数理的技法による情報セキュリティ(1) ［9月16日：9:00～10:20］
座長: 吉田 真紀（情報通信研究機構）
[企画講演] 製品開発における暗号プロトコル形式検証の実践
○三重野 武彦（EPSON AVASYS 株式会社）
数理的技法による情報セキュリティの2025年度後半＆2026年度前半の研究動向
○荒井 研一（長崎大学）, 鈴木 幸太郎（豊橋技術科学大学）,
田中 篤（大阪大学）, 中林 美郷（NTT社会情報研究所）,
花谷 嘉一（株式会社 東芝）, 三重野 武彦（EPSON AVASYS 株式会社）,
山本 光晴（千葉大学）, 吉田 真紀（情報通信研究機構）, 米山 一樹（茨城大学）
研究部会OS: 数理的技法による情報セキュリティ(2) ［9月16日：10:40～12:00］
座長: 山本 光晴（千葉大学）
An Application of Kleene's Second Recursion Theorem to Mutual Attestation
(Kleeneの第二再帰定理の相互アテステーションへの応用)
○今村 拓万（株式会社Acompany）
TPM主導Composite AttestationのProVerifによる形式的安全性検証
○渡邉 健斗（信州大学）, 三重野 武彦（EPSON AVASYS 株式会社）,
岡崎 裕之（信州大学）, 布田 裕一（東京工科大学）
ProVerifを用いたワンタイムパスワード認証方式の安全性検証
○末永 和也（長崎大学大学院総合生産科学研究科）,
荒井 研一（長崎大学大学院総合生産科学研究科）
秘密分散最適化のための解析・設計・検証基盤の基礎検討
○吉田 真紀（情報通信研究機構）
【講演概要】
[企画講演] 製品開発における暗号プロトコル形式検証の実践
○三重野 武彦（EPSON AVASYS 株式会社）
[概要]
欧米やイスラエルでは、暗号ライブラリ、スマートコントラクト、安全クリティ
カルソフトウェアに形式検証を組み込み、仕様記述から証明、継続的インテグ
レーション、規制対応までを開発工程として接続する動きが進んでいる。一方、
日本の製品開発では、暗号プロトコルが求める秘匿性、完全性、認証性などの
安全性保証が、担当者ごとのレビュー、暗黙知、後工程の試験に依存しやすく、
設計判断の根拠を再現可能な形で残すことが難しい。
本講演では、事務機等のセキュリティ基準、業界が直面する課題、実機内部プ
ロトコルの検証経験を踏まえ、形式検証を業界共通のエンジニアリング資産と
して活用する道筋を示す。鍵管理、ファームウェア更新、アテステーション、
クラウド連携を題材に、ProVerifやTamarin Proverが保証できる範囲とその
限界を具体的に整理する。さらに、企業単独の取り組みにとどめず、共通脅威
モデル、検証パターン、証跡テンプレートを整備する意義を論じ、暗号プロト
コルの形式検証を製品開発工程に組み込むための実践的な方向性を提示する。
--------------------------------------------------------------------------
数理的技法による情報セキュリティの2025年度後半＆2026年度前半の研究動向
○荒井 研一（長崎大学）, 鈴木 幸太郎（豊橋技術科学大学）,
田中 篤（大阪大学）, 中林 美郷（NTT社会情報研究所）,
花谷 嘉一（株式会社 東芝）, 三重野 武彦（EPSON AVASYS 株式会社）,
山本 光晴（千葉大学）, 吉田 真紀（情報通信研究機構）, 米山 一樹（茨城大学）
[概要]
数理的技法は暗号プロトコルやシステムの安全性検証など，情報セキュリティの
様々な分野で応用されている．本発表では，数理的技法による情報セキュリティ
に関する2025年度後半&2026年度前半の研究動向として，2025年9月から2026年8
月までに開催されたトップ会議における関連論文の発表件数や特色，概要につい
て紹介する．さらに，全体を通したトレンドや特に注目されている分野と論文を
紹介する．
--------------------------------------------------------------------------
An Application of Kleene's Second Recursion Theorem to Mutual Attestation
(Kleeneの第二再帰定理の相互アテステーションへの応用)
○今村 拓万（株式会社Acompany）
[概要]
複数のアテスタブルなノードからなる分散型アーキテクチャでは，ノード間の相
互アテステーションのために互いのリファレンス測定値の共有が必要である．し
かしながら，リファレンス値を相互にハードコーディングするという素朴な方法
は無限後退に陥るため，実現不可能である．既存の解決策は，Trusted Third
Party（TTP）にリファレンス値配送を委託するものと，アーキテクチャ依存の特
殊なデータ領域を用いるものとに分類できる．本研究は，Kleeneの第二再帰定理
（自己反映計算）に基づき，TTP非依存かつアーキテクチャ非依存な相互アテス
テーションを実現する．自己反映計算トランスパイラPyReflect及びTPMにおける
相互アテステーションのPoC実装を与える．
--------------------------------------------------------------------------
TPM主導Composite AttestationのProVerifによる形式的安全性検証
○渡邉 健斗（信州大学）, 三重野 武彦（EPSON AVASYS 株式会社）,
岡崎 裕之（信州大学）, 布田 裕一（東京工科大学）
[概要]
仮想化環境やクラウド環境では、利用者が直接確認できない実行環境や基盤ソ
フトウェアの信頼性を、外部から確認する仕組みが重要である。特にTEEは実
行環境の保護に有用であり、TPMはプラットフォーム状態の証明に用いられる
が、それぞれを個別に検証するだけでは、両者が同一環境に正しく結び付いて
いることを十分に示せない可能性がある。本発表ではTEEとTPMを組み合わせた
複合アテステーションに着目し、CCxTrustのTPM主導方式をProVerifで形式モ
デル化する。レポートの生成から検証までの流れを整理し、検証者が受理する
レポートが意図した生成過程に対応しているかを確認することで、想定される
攻撃に対する安全性を考察する。
--------------------------------------------------------------------------
ProVerifを用いたワンタイムパスワード認証方式の安全性検証
○末永 和也（長崎大学大学院総合生産科学研究科）,
荒井 研一（長崎大学大学院総合生産科学研究科）
[概要]
ProVerifは，Blanchetらが開発した形式モデル（いわゆる，Dolev-Yaoモデル）
での暗号プロトコルの自動検証ツールであり，暗号プロトコルに要求される秘匿，
認証などの安全性要件を自動で検証することができる．一方，SAS-L1およびSAS-
L2は，清水らによって提案されたワンタイムパスワード認証方式であり，SAS-L1
は認証側，SAS-L2は被認証側で擬似乱数と一方向性変換関数を適用しないため処
理能力が限定された機器に対しても適用可能な方式となっている．本稿では，
ProVerifを用いてSAS-L1およびSAS-L2を形式的に記述し，安全性検証を行った結
果を報告する．
--------------------------------------------------------------------------
秘密分散最適化のための解析・設計・検証基盤の基礎検討
○吉田 真紀（情報通信研究機構）
[概要]
秘密分散方式の最適化では，アクセス構造に対するシェアサイズ下界の解析，構
成法の設計，および方式の機密性・正当性の検証を反復しながら検討を進める必
要がある．しかし，これらの作業は個別に行われることが多く，最適方式の探索
には多大な試行錯誤を要する．本研究では，秘密分散最適化のための解析・設計・
検証を一貫して支援する基盤の実現を目指す．
本稿では，その実現に向けた基礎検討として，まず統合基盤の構成と設計方針を
示す．提案基盤は，(1) 解析：シャノンエントロピー不等式に基づくシェアサイ
ズ下界の自動導出，(2) 設計：自明な構成法から得られる上界と導出した下界に
基づく探索範囲の限定による秘密分散方式の自動構成，(3) 検証：秘密分散方式
に対する正当性・機密性の形式検証，の三つの機能から構成される．そして，各
機能を実装し，非自明なシェアサイズ下界が初めて導出されたCapocelliらのア
クセス構造への適用例を通じて，提案基盤の有用性を考察するとともに，今後の
課題について述べる．
【問い合わせ先】
FAIS幹事団 fais-kanji@ml.jsiam.org (下記幹事団に届きます)
代表：
吉田 真紀（情報通信研究機構）
幹事（五十音順）：
櫻田 英樹（ZEN大学 知能情報社会学部 知能情報社会学科）
花谷 嘉一（(株)東芝 研究開発センター）
山本 光晴（千葉大学 情報戦略機構）
米山 一樹（茨城大学 工学部 情報工学科）
＊JSIAM-FAIS ホームページ＊