This article presents a security formal analysis of the hybrid post-quantum Transport Layer Security (TLS) protocol, a quantum-resistant version of the TLS protocol proposed by Amazon Web Services as a precaution in dealing with future attacks from quantum computers. In addition to a classical key exchange algorithm, the proposed protocol uses a post-quantum key encapsulation mechanism, which is believed invulnerable under quantum computers, so the protocol's key negotiation is called the hybrid key exchange scheme. One of our assumptions about the intruder's capabilities is that the intruder is able to break the security of the classical key exchange algorithm by utilizing the power of large quantum computers. For the formal analysis, we use Maude-NPA and a parallel version of Maude-NPA (called Par-Maude-NPA) to conduct experiments. The security properties under analysis are (1) the secrecy property of the shared secret key established between two honest principals with the classical key exchange algorithm, (2) a similar secrecy property but with the post-quantum key encapsulation mechanism, and (3) the authentication property. Given the time limit T = 1,722 h (72 days), Par-Maude-NPA found a counterexample of (1) at depth 12 in T, while Maude-NPA did not find it in T. At the same time T, Par-Maude-NPA did not find any counterexamples of (2) and (3) up to depths 12 and 18, respectively, and neither did Maude-NPA. Therefore, the protocol does not enjoy (1), while it enjoys (2) and (3) up to depths 12 and 18, respectively. Subsequently, the secrecy property of the master secret holds for the protocol up to depth 12.
This article presents a security formal analysis of the hybrid post-quantum Transport Layer Security (TLS) protocol, a quantum-resistant version of the TLS protocol proposed by Amazon Web Services as a precaution in dealing with future attacks from quantum computers. In addition to a classical key exchange algorithm, the proposed protocol uses a post-quantum key encapsulation mechanism, which is believed invulnerable under quantum computers, so the protocol's key negotiation is called the hybrid key exchange scheme. One of our assumptions about the intruder's capabilities is that the intruder is able to break the security of the classical key exchange algorithm by utilizing the power of large quantum computers. For the formal analysis, we use Maude-NPA and a parallel version of Maude-NPA (called Par-Maude-NPA) to conduct experiments. The security properties under analysis are (1) the secrecy property of the shared secret key established between two honest principals with the classical key exchange algorithm, (2) a similar secrecy property but with the post-quantum key encapsulation mechanism, and (3) the authentication property. Given the time limit T = 1,722 h (72 days), Par-Maude-NPA found a counterexample of (1) at depth 12 in T, while Maude-NPA did not find it in T. At the same time T, Par-Maude-NPA did not find any counterexamples of (2) and (3) up to depths 12 and 18, respectively, and neither did Maude-NPA. Therefore, the protocol does not enjoy (1), while it enjoys (2) and (3) up to depths 12 and 18, respectively. Subsequently, the secrecy property of the master secret holds for the protocol up to depth 12.
Transport Layer Security (TLS) is a fundamental protocol for securing communications over untrusted networks. With the rising threat of quantum computing, Amazon Web Services (AWS) proposed Hybrid Post-Quantum (PQ) TLS, an extended version of TLS 1.2 designed to resist quantum attacks. In this paper, we present a formal symbolic analysis of the AWS protocol proposal using the CafeOBJ algebraic specification language and the Invariant Proof Score Generator (IPSG) tool. Our analysis formally evaluates the protocol’s resilience under two attacker models: one where classical primitives fail (by quantum adversaries), and one where PQ primitives are compromised (as they are relatively new). We verify key security properties, including the confidentiality of session keys, confidentiality of ephemeral secret keys, and forward secrecy, against both classical and quantum adversaries, confirming the security claims of the proposal. All proofs are executable within the CafeOBJ system and hold for an unbounded number of protocol participants and sessions. Although authentication is beyond the scope of the AWS protocol, we propose an improved version that incorporates hybrid digital signatures to restore quantum-safe authentication.
Facing the quantum attack threat, a quantum-resistant version of the SSH Transport Layer protocol has been proposed and been standardized by an IETF working group. This standardization process has been motivated by the fact that if practical quantum computers become available, classical key exchange algorithms used today will no longer be safe because their security can be efficiently broken by Shor’s algorithm running on a quantum computer. In this paper, we construct a symbolic model of the proposed protocol, specify it in the specification language CafeOBJ, and conduct a formal analysis of the claimed security properties with the employment of a formal method tool called Invariant Proof Score Generator (IPSG). Three security properties are formally verified with respect to an unbounded number of protocol participants and protocol executions by employing IPSG to produce their formal proofs, the so-calledproof scoresin CafeOBJ. With another property, namelyauthentication, we find a counterexample against it, and then we propose to slightly revise the protocol. With the improved version, we formally verify that theauthenticationproperty is enjoyed, while the three properties remain secure. To model the presence of malicious participants, we extend the Dolev-Yao intruder, which is the standard intruder model used in security protocol analysis/verification, because the availability assumption of large-scale quantum computers gives the attacker some new capabilities. Under our threat model, the intruder is given capabilities of fully controlling the network as the Dolev-Yao intruder, and additionally breaking ECDH’s security as well as compromising secrets.
Hybrid authenticated key exchange combines cryptography key material from different sources (classical, quantum and post-quantum cryptography) to build protocols that are resilient to catastrophic failures, technology advances and future cryptanalytic attacks. In this work, we propose and implement a triple-hybrid version of the transport layer security network protocol TLS 1.3, combining classical and post-quantum cryptography, and quantum key distribution. We evaluate the performance of this triple-hybrid TLS in an experimental network scenario and our analysis shows that the quantum-resistant feature comes at an increased communication cost of approximately 68 % over the total time of the composite handshakes. In exchange, our solution is an enhancement to the TLS 1.3 protocol by adding quantum-resistant cryptography schemes.
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.
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.
Quantum computers pose a long-term threat to many currently used cryptographic schemes as they are able to efficiently solve the computational problems those schemes are based on. This threat has lead to research into quantum-resistant cryptographic schemes to eventually replace those currently used, as well as research into how to ease the transition from classical schemes to quantum-resistant ones. One approach to address these issues is to use a combiner that creates hybrid schemes, that is schemes which are classically and quantum-resistant, to protect against quantum attacks and maintain current security guarantees. Such combiners are used as a way to provide trust from different schemes and their differing computational difficulty assumptions rather than a single scheme. which may later become vulnerable. An important type of scheme that must be secure against both classical and quantum attacks are key encapsulation mechanisms (KEMs), as they are commonly used for constructing public-key encryption and key exchange protocols. We first define new security notions for KEMs modeling attackers of various levels of quantum power ranging from fully classical to fully quantum. We then construct a combiner that creates hybrid schemes for key encapsulation mechanisms which is secure against adversaries with varying levels of quantum power over time and can be implemented efficiently. Our construction provides an efficient method to combine KEMs using an additional scheme. This construction is also general enough that it can be implemented in settings such as key exchange protocols, like those used in the Transport Layer Security (TLS) protocol for web browsers, without affecting existing structure meaningfully.