FWS2026では，FWS2025に引き続き，本分野に関する議論を促進するために下記の要領でライトニングトークを募集します．
- 内容：未発表・既発表問わず，形式検証とセキュリティに関するもの
- 例：こんな検証ツールを使ってみた，こんな研究テーマを考えている，などなど
- CSS2026で発表する内容を歓迎します！
- 日時：FWSセッション内
- 発表時間：最大2分（予定）
- 発表方法：プレゼンテーション形式（現地での発表のみ）
発表申込およびお問い合わせはこちらからお願いします．枠が埋まり次第募集を終了します．
注意- 発表内容についてはCSSのガイドラインを遵守してください．
- 発表にはCSS2026の参加登録が必要です．
- 発表タイトルおよび発表者のお名前を本ページで公開予定です．
- 他の発表と同様にオンラインで配信予定です．
- 発表スライドのWebページでの公開はありませんが，知財の取り扱いについてはご注意ください．
皆さまの発表申込をお待ちしております！
FWSについて
Formal method and security WorkShop（FWS）は形式検証とセキュリティ分野に関するワークショップです．
形式検証とは，システムやプロトコルなどの対象とその要件を形式言語を用いて記述し，対象がその要件を満たす/満たさないことを数理的な技法を用いて証明する技術です． 厳密性が必要なセキュリティ分野との相性がよく，暗号プロトコルやシステムの検証など，セキュリティの様々な分野で応用されています． 本ワークショップでは，形式検証とセキュリティの境界領域の研究および実用化の促進を目的とし，最新の研究動向や検証ツールを紹介します．
開催概要
開催期間
2026年10月20(火) 14:10-17:50 (CSS2026期間中)
CSS2026のプログラムはこちら
会場
アクトシティ浜松 & オンライン（ハイブリッド開催）
アクセス情報はこちら
参加登録
FWS2026への参加登録はCSS2026の参加登録と共通になっています．
手続きの詳細につきましてはCSS2026の参加登録および参加費のページをご参照ください．
運営委員会
櫻田 英樹（ZEN大学）
田久 健人（NTT社会情報研究所）
中林 美郷（NTT社会情報研究所）
花谷 嘉一（東芝）
米山 一樹（茨城大学）
プログラム
10/20(火) 14:10-15:50 FWS企画① チュートリアル・招待講演・ライトニングトークセッション
チュートリアル講演「入門者向けチュートリアル」 中林 美郷（NTT社会情報研究所）
形式検証×セキュリティの入門者に向けて，分野の概観やおすすめのツール，最新の研究動向について紹介します．
招待講演「証明の外側 — 仕様・証明・実装をつなぐヒューマンチェックをどう減らすか」 神波 真聖 様（Nyx Foundation）
「形式検証済み」という表示だけでは、仕様が意図を正しく表しているか、証明が実装のどこまで届いているか、何を仮定として残したかは分からない。本講演では、イーサリアムの仕様形式化を活用した脆弱性発見、Yosysを用いたハードウェア設計の検査、Lean 4を用いた静的解析などの実例を紹介する。これらを通じて、Lean 4などによる機械的な証明と、人間による意味・仮定・対象範囲の確認を分け、仕様・証明・実装の境界に残る確認事項を小さく、追跡可能にする実践を議論する。
ライトニングトークセッション
ライトニングトークを募集中です！詳しくは本ページの最上部をご覧ください．
プログラムは前日または当日に公開いたします
プログラムは前日または当日に公開いたします
10/20(火) 16:10-17:50 FWS企画② 招待講演・ハンズオン
招待講演「Tamarin Proverを用いた形式検証への参入」 田中 篤 様（大阪大学）
近年、暗号プロトコルの形式検証に対する需要は、学術界のみならず産業界においても高まりつつある。従来、形式検証は新たな攻撃やプロトコル上の脆弱性を発見するための研究手段として用いられることが多かった。一方、EUのCyber Resilience Act（CRA）に代表される近年のサイバーセキュリティ規制では、製品の安全性やセキュリティ要件への適合性を客観的に示すことがこれまで以上に重要となっており、そのための手段として形式検証を活用する動きも進みつつある。このように、形式検証は「未知の脆弱性を発見するためのツール」だけでなく、「システムが要求された安全性を満たすことを示すためのツール」としても、その重要性を増している。
本講演では、暗号プロトコルの形式検証ツールであるTamarin Proverに焦点を当てる。講演者はここ数年間、Tamarinを用いた暗号プロトコルの形式検証に取り組んできた。本講演では、形式検証の初学者として研究を始めた段階から、実際のプロトコルをモデル化し、安全性を検証する研究に取り組む現在に至るまで、どのようにTamarinを学び、どのような課題に直面しながら研究を進めてきたのかを、これまでの取り組みを交えて紹介する。
本講演では、暗号プロトコルの形式検証ツールであるTamarin Proverに焦点を当てる。講演者はここ数年間、Tamarinを用いた暗号プロトコルの形式検証に取り組んできた。本講演では、形式検証の初学者として研究を始めた段階から、実際のプロトコルをモデル化し、安全性を検証する研究に取り組む現在に至るまで、どのようにTamarinを学び、どのような課題に直面しながら研究を進めてきたのかを、これまでの取り組みを交えて紹介する。
ハンズオン「Tamarin Proverハンズオン」 花谷 嘉一（東芝）・米山 一樹（茨城大学）
暗号プロトコルの形式検証ツールであるTamarin Proverについて，初学者に向けてハンズオン形式で紹介します．
本ハンズオンのDocker環境を近日配布予定です
本ハンズオンのDocker環境を近日配布予定です
★ ぜひTamarin Proverの実行環境をご用意の上ご参加ください！
★ 会場には電源の用意がないためご注意ください．
プライバシーポリシー
FWS2026のプライバシーポリシーはCSS2026のプライバシーポリシーに準じます．