Abstract Transport Layer Cryptography Protocol (TLCP) is a secure communication protocol developed in China, featuring a dual-certificate architecture and incorporating ShangMi cryptographic algorithms. It has been widely deployed in security-critical domains such as finance, government, and energy. Despite its practical significance, TLCP did not undergo comprehensive formal analysis during its standardization process, leaving potential design-level vulnerabilities insufficiently explored. Moreover, the advent of quantum computing poses fundamental challenges to the classical cryptographic primitives employed by TLCP, motivating the need for both systematic security evaluation and post-quantum enhancements. To address these gaps, we first construct the comprehensive formal model of TLCP, covering certificate-based and identity-based cipher suites as well as its distinctive dual-certificate mechanism, under a realistic threat model and security assumptions that capture both classical and quantum adversaries. Based on this model, we conduct an automated security analysis using ProVerif, identifying nine potential attack vectors and deriving five concrete mitigation recommendations. Finally, motivated by the analysis results and the limitations of incremental fixes against quantum threats, we propose KEMTLCP, a post-quantum secure variant of TLCP that leverages key encapsulation mechanisms (KEMs) for both key exchange and authentication while preserving TLCP’s architectural principles through a novel explicit authentication mechanism. We further provide a security proof for the core authentication mechanism, show that KEMTLCP effectively mitigates the majority of identified vulnerabilities through formal analysis, and evaluate its practical performance.

Abstract The semi-classical One-Way to Hiding (SC-O2H) lemma given by Ambainis et al. (CRYPTO 2019) is a crucial technique to solve the reprogramming problem in the quantum random oracle model (QROM), which can lead to quadratically better bounds for many cases involving guessing games. To achieve tighter bounds, Bindel et al. (TCC, 2019) introduced the double-sided One-Way to Hiding (DS-O2H) lemma, which avoids the loss of query times suffered by the SC-O2H lemma. However, the potential of the DS-O2H lemma to provide better bounds for guessing games has not been considered by far. In this paper, a new double-sided O2H lemma is proposed. By using it, we for the first time give fully tight bounds for several cases involving guessing games. In summary, we show the following results in the QROM: (i) The hardness of inverting a random oracle with the leakage of a one-way injective function can be tightly reduced to the hardness of inverting the involved one-way injective function. (ii) Duman et al. (PKC 2023) introduced the randomness recoverability and defined two transformations $$\textsf {ACWC}_0$$ ACWC 0 and $$\textsf {ACWC}$$ ACWC relative to random oracles. For $$\textsf {ACWC}_0$$ ACWC 0 , we prove that its security can be tightly reduced to the security of the underlying public key encryption (PKE) scheme with the randomness recoverability. For $$\textsf {ACWC}$$ ACWC , we design a variant $$\textsf {ACWC}_1$$ ACWC 1 , and prove that its security can be tightly reduced to the security of the underlying PKE scheme with the unique randomness recoverability (a property slightly stronger than randomness recoverability). (iii) The security of the modular Fujisaki-Okamoto () transformation introduced by Hofheinz et al. (TCC 2017), can be tightly reduced to the security of the underlying PKE scheme with the unique randomness recoverability. Additionally, assuming the underlying PKE scheme is unique randomness recoverable, we prove the security of -like transformations "Image missing" (TCC, 2017) in the QROM, and as far as we know, our proof is tighter than the currently best proof.