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.
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.
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.
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 Post-quantum OpenPGP (PQ OpenPGP) protocol extends OpenPGP with hybrid cryptography, combining classical and post-quantum algorithms.It aims to ensure longterm security against attacks by quantum-capable adversaries.This paper 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 ML-KEM and classical ECDH-KEM, dual digital signatures from post-quantum ML-DSA and classical EdDSA, and a quantumcapable Dolev-Yao attacker model.We then focus on verifying the secrecy of the session key property under this attacker model.To facilitate the verification process, we employ the IPSG tool, which automatically generates formal proofs for desired properties based on a formal specification and auxiliary lemmas.
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.
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.
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.