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 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.
Transport Layer Security (TLS) protocols are essential for ensuring the confidentiality, integrity, and authentication of data communications. Mutual authentication between client and server is crucial in high-security scenarios such as finance and government. However, existing TLS protocols typically rely on certificate-based public key infrastructures (PKI) for client authentication, which increases deployment complexity and introduces risks associated with third-party trust. In contrast, password-authenticated TLS protocols use memorable passwords for client authentication, offering advantages in simplicity and usability. Nonetheless, such protocols remain vulnerable to server compromise and fail to provide sufficient security against quantum adversaries.To address these challenges, we propose a novel TLS protocol based on asymmetric password-authenticated key exchange (PAKE). The protocol employs an asymmetric PAKE mechanism wherein only password-derived information is stored on the server, while the client derives its private key from the password. This design effectively mitigates the risk of server leakage attacks. The protocol further integrates two types of post-quantum secure key encapsulation mechanisms (KEMs): an OW-ChCCA (One-Way Checkable against Chosen-Ciphertext Attacks) secure KEM for server key exchange and authentication, and an OW-PCA (One-Way Plaintext-Checkable Attacks) secure KEM for binding the client’s password-derived private key to enable client authentication. Both KEMs support multi-user, multi-challenge settings and admit tight, post-quantum secure instantiations.Furthermore, this paper provides a formal security analysis of the proposed protocol within an optimized multi-stage key exchange model. By combining the random oracle and ideal cipher models with a game-based proof methodology, we demonstrate that the protocol achieves mutual authentication and forward secrecy, while also providing tight security bounds and post-quantum resilience. This work thus presents a promising solution for constructing post-quantum password-authenticated TLS protocols.
Secure Shell (SSH) is a widely used cryptographic protocol that establishes secure and encrypted communication over potentially untrusted networks, primarily supporting remote login and command-line execution. The SSH Transport Layer Protocol relies on the classical Elliptic Curve Diffie-Hellman (ECDH) key exchange mechanism, which derives its security from the computational hardness of the Elliptic Curve Discrete Logarithm Problem (ECDLP). However, with the emergence of quantum computing, the ECDLP can be solved efficiently, making traditional SSH protocols vulnerable to quantum attacks. To mitigate this threat, several approaches combining classical and post-quantum cryptographic techniques have been proposed; however, security analyses have revealed vulnerabilities to critical attacks. In response, we propose a post-quantum key exchange protocol for SSH, utilising the Split-Key Encapsulation Mechanism (KEM). The key generated through this protocol can then be used for subsequent communication tasks, such as authentication. The security of the proposed protocol is formally validated using the Real-Or-Random (ROR) model and the Scyther tool. Furthermore, we perform a comparative evaluation in terms of computational and communication costs to assess execution time and conduct a testbed analysis, demonstrating that the proposed scheme can be efficiently implemented in real-world applications. The comparative analysis reveals that the designed post-quantum secure protocol reduces computational cost by up to 98% compared to its competitors.
The emergence of quantum computing presents a fundamental challenge to the security of current Internet communication systems. Transport Layer Security (TLS), which forms the backbone of secure web communication, predominantly relies on classical public-key cryptographic algorithms such as RSA and elliptic curve cryptography (ECC), both of which are susceptible to quantum attacks. This paper conducts a large scale empirical evaluation of post-quantum readiness across 32,011 domains, with a primary focus on real-world TLS deployments across diverse sectors by analysing negotiated TLS parameters, including protocol versions, cipher suites, key exchange mechanisms, and certificates. The results indicate that while modern protocols like TLS 1.3 and QUIC are gaining adoption, 15.70% of domains especially in critical sectors such as banking and government still rely on TLS 1.2. Furthermore, 49.3% of domains support hybrid post-quantum key exchange mechanisms (e.g., MLKEM768 with X25519), whereas 50.7% continue to use classical key exchange, reflecting partial transition. Notably, 0% adoption of hybrid post-quantum certificates was observed, leaving the authentication layer vulnerable to quantum-enabled attacks such as certificate forgery. The findings reveal uneven adoption of post-quantum mechanisms across sectors, where technology driven platforms are advancing more rapidly than legacy-dependent infrastructures. Overall, the study highlights that achieving complete quantum resilience requires a coordinated transition not only in key exchange mechanisms but also in certificate infrastructures. Without such comprehensive migration, Internet communication systems remain vulnerable to long-term threats, including Harvest-Now-Decrypt-Later (HNDL) attacks.
[EN] With the arrival of quantum computing, ensuring the security of communications protocol has become even more crucial. This study explores the formal verification of a Transport Layer Security protocol designed to withstand quantum menaces. While traditional cryptographic methods are effective against classical computing adversaries, they are susceptible to attacks empowered by quantum computation. Hence, there is a real need to transition to Post-Quantum cryptography, which offers resilience against future threats. This research focuses on formally veryfiying the Hybrid Post-Quantum TLS protocol to provide mathematical assurance of its security properties. Formal verification offers a rigorous method for analyzing the correctness and robustness of cryptographic protocols, reducing the risk of undetected vulnerabilities. By employing formal methods, we scrutinize the protocol s design, implementation, and cryptographic primitives to identify a potential weaknesses and ensure compliance with security standards. The formal verification of the Hybrid Post-Quantum TLS protocol not only enhances our understanding of its security assurances but also underscores the significance of rigorous validation in cryptographic design.
The emergence of quantum computing presents a significant threat to classical cryptographic primitives, particularly those employed in securing internet communications via widely used protocols such as Transport Layer Security (TLS). As conventional key exchange mechanisms will become increasingly vulnerable in the post-quantum era, the integration of post-quantum cryptographic (PQC) algorithms into existing security protocols is of utmost importance. This study investigates the impact of incorporating PQC key encapsulation mechanisms—specifically, the recent standards CRYSTALS-Kyber and HQC, in conjunction with the candidate standard BIKE—into the TLS 1.3 handshake. A comprehensive experimental evaluation was conducted to measure handshake latency under emulated network conditions with varying packet loss probabilities. The findings offer useful insights into the performance trade-offs introduced by PQC integration and further highlight the necessity of a timely transition to post-quantum cryptographic standards.
With the rapid advancement of quantum computing, classical cryptographic protocols face an increasing risk of being broken. The Post-Quantum OpenPGP (PQ OpenPGP) protocol is an extension of the OpenPGP standard that incorporates hybrid cryptography by combining a classical key exchange and a post-quantum key encapsulation mechanism. This design aims to provide long-term security even in the presence of adversaries equipped with quantum computational capabilities and ensures backward compatibility while transitioning safely to the quantum era. This article presents a formal specification and verification of the PQ OpenPGP protocol using the algebraic specification language CafeOBJ. Our specification captures key aspects of the protocol, including hybrid key encapsulation using post-quantum Module-Lattice Key Encapsulation Mechanism (ML-KEM) and classical Elliptic Curve Diffie–Hellman (ECDH)-KEM, dual digital signatures using post-quantum Module-Lattice Digital Signature Algorithm (ML-DSA) and classical Edwards-curve Digital Signature Algorithm (EdDSA). To model adversarial behavior, we extend the standard Dolev-Yao intruder model, widely used in the analysis of security protocols, by incorporating quantum-enabled capabilities. Under our threat model, the intruder not only has full control over the network, as in the traditional Dolev-Yao setting, but is also capable of breaking classical public-key cryptographic primitives and compromising sensitive information, reflecting the realistic power of large-scale quantum computers. We successfully verify that the PQ OpenPGP protocol satisfies three essential security properties: secrecy of the session key, forward secrecy, and authenticity. The proofs are supported by ten auxiliary lemmas. Given the formal specification, security properties, and conjecture lemmas, the Invariant Proof Score Generator (IPSG) tool automatically generates proof scores to facilitate verification. This work contributes to the growing research on formal verification in post-quantum cryptographic protocols.