| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2026-03-03 10:00 LINEグループ通信に対するTamarin-Proverを用いた安全性自動検証 ○松本岳大・田中 篤・山下恭佑・伊藤竜馬・五十部孝典（阪大）  ICSS2025-86 |
|
| 抄録 | （和） | 本稿では，LINEにおけるグループ通信プロトコルLetter Sealing Version1およびVersion2に対し，形式的検証ツールTamarin Proverを用いた安全性検証を行った． LINEのE2EE通信は日本の社会基盤として広く普及しているが，グループ通信における形式的検証はこれまで行われていなかった． 本研究では，悪意のあるサーバーおよび悪意のあるグループメンバーの2種類の脅威モデルを定義し， 秘匿性，認証性，完全性，リプレイ攻撃耐性などの主要なセキュリティ性質を検証した． 検証の結果，Version2ではAES-GCMの導入により悪意のあるサーバーに対する認証性が大きく改善された一方， 依然として内部攻撃者に対する脆弱性や前方秘匿性の欠如といった課題が残存することを明らかにした． |
| （英） | In this paper, we conduct a formal security verification of LINE’s group communication protocols, Letter Sealing Version 1 and Version 2, using the Tamarin Prover. While LINE’s end-to-end encrypted (E2EE) communication has become an essential component of Japan’s social infrastructure, formal verification of its group communication protocol had not been previously explored. This study defines two threat models: a malicious server (E2E adversary) and a malicious group member. Based on these models, we verify critical security properties, including confidentiality, authenticity, integrity, and resistance to replay attacks. Our verification results demonstrate that Version 2 provides enhanced authenticity against malicious servers through the adoption of AES-GCM. However, the analysis also reveals persistent vulnerabilities, specifically regarding internal attackers and the inherent lack of forward secrecy. |
|
| キーワード | （和） | LINE Letter Sealing / エンドツーエンド暗号化 / 形式検証 / Tamarin Prover / / / / |
| （英） | LINE Letter Sealing / End-to-End Encryption / Formal Verification / Tamarin Prover / / / / | |
| 文献情報 | 信学技報, vol. 125, no. 381, ICSS2025-86, pp. 1-8, 2026年3月. | |
| 資料番号 | ICSS2025-86 | |
| 発行日 | 2026-02-24 (ICSS) | |
| ISSN | Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | ICSS2025-86 |
|
| 研究会情報 | |
| 研究会 | ICSS IPSJ-SPT |
| 開催期間 | 2026-03-03 - 2026-03-04 |
| 開催地（和） | 沖縄県立美術館・博物館 |
| 開催地（英） | Okinawa Prefectural Museum & Art Museum |
| テーマ（和） | セキュリティ，トラスト，一般 |
| テーマ（英） | Security, Trust, etc. |
| 講演論文情報の詳細 | |
| 申込み研究会 | ICSS |
| 会議コード | 2026-03-ICSS-SPT |
| 本文の言語 | 日本語 |
| タイトル（和） | LINEグループ通信に対するTamarin-Proverを用いた安全性自動検証 |
| サブタイトル（和） | |
| タイトル（英） | Automated Security Verification of LINE Group Communication Using Tamarin-Prover |
| サブタイトル（英） | |
| キーワード(1)（和/英） | LINE Letter Sealing / LINE Letter Sealing |
| キーワード(2)（和/英） | エンドツーエンド暗号化 / End-to-End Encryption |
| キーワード(3)（和/英） | 形式検証 / Formal Verification |
| キーワード(4)（和/英） | Tamarin Prover / Tamarin Prover |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 松本 岳大 / Takehiro Matsumoto / マツモト タケヒロ |
| 第1著者 所属（和/英） | 大阪大学大学院 (略称： 阪大) The University of Osaka, Japan (略称： The University of Osaka, Japan) |
| 第2著者 氏名（和/英/ヨミ） | 田中 篤 / Atsushi Tanaka / アツシ タナカ |
| 第2著者 所属（和/英） | 大阪大学大学院 (略称： 阪大) The University of Osaka, Japan (略称： The University of Osaka, Japan) |
| 第3著者 氏名（和/英/ヨミ） | 山下 恭佑 / Kyosuke Yamashita / ヤマシタ キョウスケ |
| 第3著者 所属（和/英） | 大阪大学大学院 (略称： 阪大) The University of Osaka, Japan (略称： The University of Osaka, Japan) |
| 第4著者 氏名（和/英/ヨミ） | 伊藤 竜馬 / Ryoma Ito / イトウ リョウマ |
| 第4著者 所属（和/英） | 大阪大学大学院 (略称： 阪大) The University of Osaka, Japan (略称： The University of Osaka, Japan) |
| 第5著者 氏名（和/英/ヨミ） | 五十部 孝典 / Takanori Isobe / |
| 第5著者 所属（和/英） | 大阪大学大学院 (略称： 阪大) The University of Osaka, Japan (略称： The University of Osaka, Japan) |
| 講演者 | 第1著者 |
| 発表日時 | 2026-03-03 10:00:00 |
| 発表時間 | 20分 |
| 申込先研究会 | ICSS |
| 資料番号 | ICSS2025-86 |
| 巻番号（vol） | vol.125 |
| 号番号（no） | no.381 |
| ページ範囲 | pp.1-8 |
| ページ数 | 8 |
| 発行日 | 2026-02-24 (ICSS) |
[研究会発表申込システムのトップページに戻る]