LINE is the most widely used messaging application worldwide, with 196 million monthly active users as of March 2025. Given its broad adoption, ensuring the security of its communication protocol is of significant importance. However, its end-to-end encryption protocol, Letter Sealing, has not undergone comprehensive formal verification. Although Letter Sealing Version 2—introduced after vulnerabilities were identified in Version 1—is now widely deployed, its security guarantees remain insufficiently scrutinized. In this work, we formally model the one-to-one communication protocol in both Letter Sealing versions using the symbolic verification tool Tamarin-Prover and analyze key security properties, including confidentiality, authentication, and integrity. For Letter Sealing Version 1, we reproduce previously reported vulnerabilities, such as impersonation and replay attacks, and additionally conduct an exhaustive verification of a broad range of security properties. For Letter Sealing Version 2, we represent the first comprehensive formal analysis. We confirm that several vulnerabilities have been mitigated through changes in cryptographic algorithms; however, our analysis also reveals several previously unidentified weaknesses that persist in the protocol. This work provides a foundational step toward a rigorous evaluation of the security guarantees offered by LINE’s encryption mechanisms and underscores the ongoing need for formal verification in widely deployed communication systems.