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.
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.
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.
This study reviews post-quantum cryptographic algorithms for secure communication, focusing on standardized lattice-based schemes and their practical deployment implications. Classical public-key systems such as RSA and elliptic curve cryptography remain central to secure communication, but their long-term security is threatened by quantum algorithms capable of solving factorization and discrete logarithm problems. The study adopts a hybrid approach combining literature-based review with dataset-driven performance analysis. The empirical evaluation compares ML-KEM and ML-DSA with RSA-4096 and ECDSA-P256 using CPU benchmarking and network simulation metrics. Results indicate that ML-KEM provides substantial computational advantages over RSA-4096, making it suitable for latency-sensitive key establishment. ML-DSA also demonstrates competitive performance, especially in verification, but introduces larger signature sizes than ECDSA-P256. The analysis shows that the main deployment challenge is not computational feasibility but increased communication overhead caused by larger keys, ciphertexts, and signatures. These findings suggest that post-quantum migration requires more than direct algorithm replacement. Effective deployment should involve protocol optimization, crypto-agility, hybrid transition strategies, and context-specific parameter selection. Although the dataset focuses mainly on lattice-based algorithms, the study confirms the practical relevance of standardized post-quantum schemes for future secure communication infrastructure and identifies directions for broader evaluation across additional PQC families, including code-based, hash-based, multivariate approaches, real-world networks, and implementation-level security testing in practice contexts.
Abstract—The advent of fault-tolerant Cryptanalytically Relevant Quantum Computers (CRQCs) presents an existential threat to modern information security. Shor's polynomial-time quantum algorithm renders widely deployed public-key cryptographic primitives—including RSA, Diffie-Hellman (DH), and Elliptic Curve Cryptography (ECDH/ECDSA)—completely vulnerable to private key derivation. Furthermore, 'Harvest Now, Decrypt Later' (HNDL) adversarial campaigns actively intercept and store encrypted enterprise telemetry today, anticipating future quantum decryption capabilities. In response, the National Institute of Standards and Technology (NIST) finalized its primary Post-Quantum Cryptography (PQC) standards in FIPS 203 (ML-KEM), FIPS 204 (ML-DSA), and FIPS 205 (SLH-DSA). However, transitioning complex enterprise IT ecosystems to quantum-resistant primitives introduces severe architectural and computational disruptions: public key and signature sizes increase by several orders of magnitude, cryptographic handshake latencies escalate, network packets experience Maximum Transmission Unit (MTU) fragmentation, and legacy Hardware Security Modules (HSMs) lack microarchitectural support for lattice-based polynomial arithmetic. This paper provides an exhaustive, mathematically grounded technical survey and architectural roadmap for enterprise PQC migration. We formalize the Module Learning with Errors (M-LWE) and Module Short Integer Solution (M-SIS) hardness foundations, evaluate hybrid classical/post-quantum cryptographic transition models across standard transport protocols (TLS 1.3, IKEv2/IPsec, SSH), and formulate an enterprise Crypto-Agility Maturity Model. Furthermore, we construct an empirical enterprise testbed measuring throughput, connection establishment latency, memory footprints, and packet fragmentation across legacy and quantum-resistant suites. Our results show that while ML-KEM-768 achieves microsecond-level encapsulation, its 1,088-byte ciphertext expands TLS ClientHello payloads into multiple TCP segments under constrained networks. Finally, we establish open research directions in post-quantum identity federations, stateful hash signature tracking, and hardware-accelerated polynomial arithmetic. Index Terms—Post-Quantum Cryptography (PQC), FIPS 203 (ML-KEM), FIPS 204 (ML-DSA), Crypto-Agility, TLS 1.3, Lattice-Based Cryptography, Harvest Now Decrypt Later, Hardware Security Modules (HSM), Enterprise Migration.
The rapid advancement of quantum computing introduces unprecedented security threats to modern cloud and edge computing infrastructures. Classical public-key cryptographic algorithms such as RSA, Diffie–Hellman, and Elliptic Curve Cryptography (ECC) are fundamentally vulnerable to quantum attacks enabled by Shor’s algorithm. As a result, the confidentiality, integrity, and authenticity of data stored and processed in distributed systems are at serious risk.Post-quantum cryptography (PQC) aims to develop cryptographic algorithms that are resistant to both classical and quantum adversaries. This paper presents a comprehensive quantum-resilient cryptographic framework designed specifically for post-quantum cloud and edge computing environments. The framework integrates post-quantum cryptographic primitives, hybrid cryptographic approaches, crypto-agile architectures, and secure key management mechanisms. The proposed framework addresses performance constraints, scalability requirements, and deployment challenges in heterogeneous environments. A detailed discussion of security threats, architectural components, performance considerations, and future research directions is provided. The proposed approach enables longterm security and supports a smooth transition toward quantum-safe distributed computing systems.