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.
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.
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.
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.
The proliferation of Internet of Things (IoT) devices that use the Message Queuing Telemetry Transport (MQTT) protocol poses significant security challenges in the emerging quantum computing era. Current Transport Layer Security (TLS) implementations rely on classical cryptographic algorithms vulnerable to Shor's algorithm. This paper proposes PQ-MQTT, a hybrid post-quantum secure communication protocol that integrates ML-KEM-768 with X25519 for key encapsulation and a lightweight session-key derivation mechanism optimized for resource-constrained IoT publishers. We present a formal security analysis under the Quantum Random Oracle Model (QROM), demonstrating resilience against store-now-decryptlater attacks. Experimental evaluation on the Raspberry Pi 4, ESP32, and Arduino Nano 33 platforms shows that PQ-MQTT achieves handshake latencies of127.3ms,412.7ms, and1,847.2ms, respectively, with 18.2 KB of additional memory overhead. A comparative analysis of pure post-quantum and classical TLS implementations shows energy reductions of23.5%−40.5%relative to pure PQC, achieved through our hybrid optimization approach, while maintaining 94.2 % throughput efficiency.
The Signal Messenger recently introduced a new asynchronous key agreement protocol called PQXDH (Post-Quantum Extended Diffie-Hellman) that seeks to provide post-quantum forward secrecy, in addition to the authentication and confidentiality guarantees already provided by the previous X3DH (Extended Diffie-Hellman) protocol.More precisely, PQXDH seeks to protect the confidentiality of messages against harvest-now-decrypt-later attacks.In this work, we formally specify the PQXDH protocol and analyze its security using two formal verification tools, PROVERIF and CRYPTOVERIF.In particular, we ask whether PQXDH preserves the guarantees of X3DH, whether it provides post-quantum forward secrecy, and whether it can be securely deployed alongside X3DH.Our analysis identifies several flaws and potential vulnerabilities in the PQXDH specification, although these vulnerabilities are not exploitable in the Signal application, thanks to specific implementation choices which we describe in this paper.To prove the security of the current implementation, our analysis notably highlighted the need for an additional binding property of the KEM, which we formally define and prove for Kyber.We collaborated with the protocol designers to develop an updated protocol specification based on our findings, where each change was formally verified and validated with a security proof.This work identifies some pitfalls that the community should be aware of when upgrading protocols to be post-quantum secure.It also demonstrates the utility of using formal verification hand-in-hand with protocol design.
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.