講演抄録/キーワード |
講演名 |
2024-03-14 15:30
トランスポートレイヤセキュリティプロトコルの形式検証の動向と課題 ○櫻田英樹(NTT/九大)・櫻井幸一(九大/ATR) IT2023-121 ISEC2023-120 WBS2023-109 RCC2023-103 |
抄録 |
(和) |
webサーバとクライアントの間の通信では、これを安全に行うためにTLSプロトコルを用いられており、安全性のために不可欠といえる。TLSは通信相手を認証し、鍵を共有し、その鍵でwebページなどの情報を暗号化して送受信することを可能にする。さらに、メッセージが正しい順序で受信され、消失などがおこっていないことも保証することができる。このようなプロトコルを、本稿ではトランスポートレイヤのセキュリティプロトコルと呼ぶ。そのようなプロトコルの代表的なものがTLSであり、その前身はNetscape社により提案されたSSLプロトコルである。また、TCPプロトコル上で動作するTLSの欠点を改良すべく、UDPプロトコル上で動作するQUICプロトコルも提案されている。本稿では、これらのプロトコルに対して、その安全性を形式的に厳密に検証する取り組みについて概観し、その動向と課題について議論する。 |
(英) |
The TLS protocol is used to secure communications between web servers and clients, and is essential for security: it allows the parties to authenticate, share keys and use those keys to encrypt information, such as web pages, before sending and receiving it. It also ensures that messages are received in the correct sequence and are not lost. Such protocols are referred to as transport layer security protocols in this paper. This paper provides an overview of efforts to verify the security of the transport layer security protocols SSL, TLS and QUIC using formal verification methods and discusses trends and challenges in this area. |
キーワード |
(和) |
フォーマルメソッド / TLS / SSL / QUIC / / / / |
(英) |
formal methods / TLS / SSL / QUIC / / / / |
文献情報 |
信学技報, vol. 123, no. 424, ISEC2023-120, pp. 287-293, 2024年3月. |
資料番号 |
ISEC2023-120 |
発行日 |
2024-03-06 (IT, ISEC, WBS, RCC) |
ISSN |
Online edition: ISSN 2432-6380 |
著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) |
PDFダウンロード |
IT2023-121 ISEC2023-120 WBS2023-109 RCC2023-103 |
研究会情報 |
研究会 |
RCC ISEC IT WBS |
開催期間 |
2024-03-13 - 2024-03-14 |
開催地(和) |
大阪大学吹田キャンパス |
開催地(英) |
Osaka Univ. (Suita Campus) |
テーマ(和) |
RCC・ISEC・IT・WBS合同研究会 |
テーマ(英) |
RCC, ISEC, IT, WBS |
講演論文情報の詳細 |
申込み研究会 |
ISEC |
会議コード |
2024-03-RCC-ISEC-IT-WBS |
本文の言語 |
日本語 |
タイトル(和) |
トランスポートレイヤセキュリティプロトコルの形式検証の動向と課題 |
サブタイトル(和) |
|
タイトル(英) |
Research Directions in Formal Verification of Transport Layer Security Protocols |
サブタイトル(英) |
|
キーワード(1)(和/英) |
フォーマルメソッド / formal methods |
キーワード(2)(和/英) |
TLS / TLS |
キーワード(3)(和/英) |
SSL / SSL |
キーワード(4)(和/英) |
QUIC / QUIC |
キーワード(5)(和/英) |
/ |
キーワード(6)(和/英) |
/ |
キーワード(7)(和/英) |
/ |
キーワード(8)(和/英) |
/ |
第1著者 氏名(和/英/ヨミ) |
櫻田 英樹 / Hideki Sakurada / サクラダ ヒデキ¥ |
第1著者 所属(和/英) |
日本電信電話株式会社/九州大学 (略称: NTT/九大)
Nippon Telephone and Telegraph Corporation/Kyushu University (略称: NTT/Kyushu Univ.) |
第2著者 氏名(和/英/ヨミ) |
櫻井 幸一 / Kouichi Sakurai / サクライ コウイチ |
第2著者 所属(和/英) |
九州大学/ATR (略称: 九大/ATR)
Kyushu University/ATR (略称: Kyushu Univ./ATR) |
第3著者 氏名(和/英/ヨミ) |
/ / |
第3著者 所属(和/英) |
(略称: )
(略称: ) |
第4著者 氏名(和/英/ヨミ) |
/ / |
第4著者 所属(和/英) |
(略称: )
(略称: ) |
第5著者 氏名(和/英/ヨミ) |
/ / |
第5著者 所属(和/英) |
(略称: )
(略称: ) |
第6著者 氏名(和/英/ヨミ) |
/ / |
第6著者 所属(和/英) |
(略称: )
(略称: ) |
第7著者 氏名(和/英/ヨミ) |
/ / |
第7著者 所属(和/英) |
(略称: )
(略称: ) |
第8著者 氏名(和/英/ヨミ) |
/ / |
第8著者 所属(和/英) |
(略称: )
(略称: ) |
第9著者 氏名(和/英/ヨミ) |
/ / |
第9著者 所属(和/英) |
(略称: )
(略称: ) |
第10著者 氏名(和/英/ヨミ) |
/ / |
第10著者 所属(和/英) |
(略称: )
(略称: ) |
第11著者 氏名(和/英/ヨミ) |
/ / |
第11著者 所属(和/英) |
(略称: )
(略称: ) |
第12著者 氏名(和/英/ヨミ) |
/ / |
第12著者 所属(和/英) |
(略称: )
(略称: ) |
第13著者 氏名(和/英/ヨミ) |
/ / |
第13著者 所属(和/英) |
(略称: )
(略称: ) |
第14著者 氏名(和/英/ヨミ) |
/ / |
第14著者 所属(和/英) |
(略称: )
(略称: ) |
第15著者 氏名(和/英/ヨミ) |
/ / |
第15著者 所属(和/英) |
(略称: )
(略称: ) |
第16著者 氏名(和/英/ヨミ) |
/ / |
第16著者 所属(和/英) |
(略称: )
(略称: ) |
第17著者 氏名(和/英/ヨミ) |
/ / |
第17著者 所属(和/英) |
(略称: )
(略称: ) |
第18著者 氏名(和/英/ヨミ) |
/ / |
第18著者 所属(和/英) |
(略称: )
(略称: ) |
第19著者 氏名(和/英/ヨミ) |
/ / |
第19著者 所属(和/英) |
(略称: )
(略称: ) |
第20著者 氏名(和/英/ヨミ) |
/ / |
第20著者 所属(和/英) |
(略称: )
(略称: ) |
講演者 |
第1著者 |
発表日時 |
2024-03-14 15:30:00 |
発表時間 |
25分 |
申込先研究会 |
ISEC |
資料番号 |
IT2023-121, ISEC2023-120, WBS2023-109, RCC2023-103 |
巻番号(vol) |
vol.123 |
号番号(no) |
no.423(IT), no.424(ISEC), no.425(WBS), no.426(RCC) |
ページ範囲 |
pp.287-293 |
ページ数 |
7 |
発行日 |
2024-03-06 (IT, ISEC, WBS, RCC) |
|