Formal specification and security verification of post-quantum OpenPGP in CafeOBJ

Abstract

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.