IEICE TRANSACTIONS on Information
Verification of LINE Encryption Version 1.0 Using ProVerif
Summary :
LINE is currently the most popular messaging service in Japan. Communications using LINE are protected by the original encryption scheme, called LINE Encryption, and specifications of the client-to-server transport encryption protocol and the client-to-client message end-to-end encryption protocol are published by the Technical Whitepaper. Though a spoofing attack (i.e., a malicious client makes another client misunderstand the identity of the peer) and a reply attack (i.e., a message in a session is sent again in another session by a man-in-the-middle adversary, and the receiver accepts these messages) to the end-to-end protocol have been shown, no formal security analysis of these protocols is known. In this paper, we show a formal verification result of secrecy of application data and authenticity for protocols of LINE Encryption (Version 1.0) by using the automated security verification tool ProVerif. Especially, since it is claimed that the transport protocol satisfies forward secrecy (i.e., even if the static private key is leaked, security of application data is guaranteed), we verify forward secrecy for client's data and for server's data of the transport protocol, and we find an attack to break secrecy of client's application data. Moreover, we find the spoofing attack and the reply attack, which are reported in previous papers.
- Publication
- IEICE TRANSACTIONS on Information Vol.E102-D No.8 pp.1439-1448
- Publication Date
- 2019/08/01
- Publicized
- 2019/04/24
- Online ISSN
- 1745-1361
- DOI
- 10.1587/transinf.2018FOP0001
- Type of Manuscript
- Special Section PAPER (Special Section on Formal Approaches)
- Category
Authors
Cheng SHI
Ibaraki University
Kazuki YONEYAMA
Ibaraki University
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Cheng SHI, Kazuki YONEYAMA, "Verification of LINE Encryption Version 1.0 Using ProVerif" in IEICE TRANSACTIONS on Information,
vol. E102-D, no. 8, pp. 1439-1448, August 2019, doi: 10.1587/transinf.2018FOP0001.
Abstract: LINE is currently the most popular messaging service in Japan. Communications using LINE are protected by the original encryption scheme, called LINE Encryption, and specifications of the client-to-server transport encryption protocol and the client-to-client message end-to-end encryption protocol are published by the Technical Whitepaper. Though a spoofing attack (i.e., a malicious client makes another client misunderstand the identity of the peer) and a reply attack (i.e., a message in a session is sent again in another session by a man-in-the-middle adversary, and the receiver accepts these messages) to the end-to-end protocol have been shown, no formal security analysis of these protocols is known. In this paper, we show a formal verification result of secrecy of application data and authenticity for protocols of LINE Encryption (Version 1.0) by using the automated security verification tool ProVerif. Especially, since it is claimed that the transport protocol satisfies forward secrecy (i.e., even if the static private key is leaked, security of application data is guaranteed), we verify forward secrecy for client's data and for server's data of the transport protocol, and we find an attack to break secrecy of client's application data. Moreover, we find the spoofing attack and the reply attack, which are reported in previous papers.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.2018FOP0001/_p
Copy
@ARTICLE{e102-d_8_1439,
author={Cheng SHI, Kazuki YONEYAMA, },
journal={IEICE TRANSACTIONS on Information},
title={Verification of LINE Encryption Version 1.0 Using ProVerif},
year={2019},
volume={E102-D},
number={8},
pages={1439-1448},
abstract={LINE is currently the most popular messaging service in Japan. Communications using LINE are protected by the original encryption scheme, called LINE Encryption, and specifications of the client-to-server transport encryption protocol and the client-to-client message end-to-end encryption protocol are published by the Technical Whitepaper. Though a spoofing attack (i.e., a malicious client makes another client misunderstand the identity of the peer) and a reply attack (i.e., a message in a session is sent again in another session by a man-in-the-middle adversary, and the receiver accepts these messages) to the end-to-end protocol have been shown, no formal security analysis of these protocols is known. In this paper, we show a formal verification result of secrecy of application data and authenticity for protocols of LINE Encryption (Version 1.0) by using the automated security verification tool ProVerif. Especially, since it is claimed that the transport protocol satisfies forward secrecy (i.e., even if the static private key is leaked, security of application data is guaranteed), we verify forward secrecy for client's data and for server's data of the transport protocol, and we find an attack to break secrecy of client's application data. Moreover, we find the spoofing attack and the reply attack, which are reported in previous papers.},
keywords={},
doi={10.1587/transinf.2018FOP0001},
ISSN={1745-1361},
month={August},}
Copy
TY - JOUR
TI - Verification of LINE Encryption Version 1.0 Using ProVerif
T2 - IEICE TRANSACTIONS on Information
SP - 1439
EP - 1448
AU - Cheng SHI
AU - Kazuki YONEYAMA
PY - 2019
DO - 10.1587/transinf.2018FOP0001
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E102-D
IS - 8
JA - IEICE TRANSACTIONS on Information
Y1 - August 2019
AB - LINE is currently the most popular messaging service in Japan. Communications using LINE are protected by the original encryption scheme, called LINE Encryption, and specifications of the client-to-server transport encryption protocol and the client-to-client message end-to-end encryption protocol are published by the Technical Whitepaper. Though a spoofing attack (i.e., a malicious client makes another client misunderstand the identity of the peer) and a reply attack (i.e., a message in a session is sent again in another session by a man-in-the-middle adversary, and the receiver accepts these messages) to the end-to-end protocol have been shown, no formal security analysis of these protocols is known. In this paper, we show a formal verification result of secrecy of application data and authenticity for protocols of LINE Encryption (Version 1.0) by using the automated security verification tool ProVerif. Especially, since it is claimed that the transport protocol satisfies forward secrecy (i.e., even if the static private key is leaked, security of application data is guaranteed), we verify forward secrecy for client's data and for server's data of the transport protocol, and we find an attack to break secrecy of client's application data. Moreover, we find the spoofing attack and the reply attack, which are reported in previous papers.
ER -
English
