| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2026-03-03 10:20 TamarinによるSFrameプロトコルの形式検証 ○橋場慧志・田中 篤・五十部孝典（阪大）  ICSS2025-87 |
|
| 抄録 | （和） | SFrameは主にWeb会議における通信で、RTP/SRTPの上で動作して参加者同士のE2EE通信を実現するプロトコルである。SFrameのセキュリティに関して、Isobeらによって手動で暗号学的な評価がすでになされている一方、形式検証や包括的な検証は行われていない。 本研究では形式検証ツールであるTamarin Proverを用いてSFrameのプロトコルを形式化し、一般的なセキュリティ要件について形式的な検証を行った。 これによりなりすまされたパケットを認識できないことや、複数パケットの順序を一致させることができないなど、RFC 9605で指摘のある点も含めていくつかのセキュリティ要件を満たさないことを示した。 |
| （英） | SFrame is a protocol primarily used for web conference communications, running on top of RTP/SRTP to enable E2EE communication between participants. While a manual cryptographic evaluation of SFrame's security has already been performed by Isobe et al., formal or comprehensive verification has not yet been conducted. In this study, we formalized the SFrame protocol using the formal verification tool Tamarin Prover and performed formal verification of its general security requirements. We showed that it does not meet several security requirements, including those pointed out in RFC 9605, such as the inability to recognize spoofed packets and the inability to match the order of multiple packets. |
|
| キーワード | （和） | SFrame / Tamarin Prover / 形式検証 / RFC 9605 / / / / |
| （英） | SFrame / Tamarin Prover / Formal verification / RFC 9605 / / / / | |
| 文献情報 | 信学技報, vol. 125, no. 381, ICSS2025-87, pp. 9-16, 2026年3月. | |
| 資料番号 | ICSS2025-87 | |
| 発行日 | 2026-02-24 (ICSS) | |
| ISSN | Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | ICSS2025-87 |
|
| 研究会情報 | |
| 研究会 | ICSS IPSJ-SPT |
| 開催期間 | 2026-03-03 - 2026-03-04 |
| 開催地（和） | 沖縄県立美術館・博物館 |
| 開催地（英） | Okinawa Prefectural Museum & Art Museum |
| テーマ（和） | セキュリティ，トラスト，一般 |
| テーマ（英） | Security, Trust, etc. |
| 講演論文情報の詳細 | |
| 申込み研究会 | ICSS |
| 会議コード | 2026-03-ICSS-SPT |
| 本文の言語 | 英語（日本語タイトルあり） |
| タイトル（和） | TamarinによるSFrameプロトコルの形式検証 |
| サブタイトル（和） | |
| タイトル（英） | Formal verification of SFrame with Tamarin |
| サブタイトル（英） | |
| キーワード(1)（和/英） | SFrame / SFrame |
| キーワード(2)（和/英） | Tamarin Prover / Tamarin Prover |
| キーワード(3)（和/英） | 形式検証 / Formal verification |
| キーワード(4)（和/英） | RFC 9605 / RFC 9605 |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 橋場 慧志 / Keishi Hashiba / ハシバ ケイシ |
| 第1著者 所属（和/英） | 大阪大学 (略称： 阪大) The University of Osaka (略称： U Osaka) |
| 第2著者 氏名（和/英/ヨミ） | 田中 篤 / Atsushi Tanaka / |
| 第2著者 所属（和/英） | 大阪大学 (略称： 阪大) The University of Osaka (略称： U Osaka) |
| 第3著者 氏名（和/英/ヨミ） | 五十部 孝典 / Takanori Isobe / |
| 第3著者 所属（和/英） | 大阪大学 (略称： 阪大) The University of Osaka (略称： U Osaka) |
| 講演者 | 第1著者 |
| 発表日時 | 2026-03-03 10:20:00 |
| 発表時間 | 20分 |
| 申込先研究会 | ICSS |
| 資料番号 | ICSS2025-87 |
| 巻番号（vol） | vol.125 |
| 号番号（no） | no.381 |
| ページ範囲 | pp.9-16 |
| ページ数 | 8 |
| 発行日 | 2026-02-24 (ICSS) |
[研究会発表申込システムのトップページに戻る]