Formal specification and security verification of post-quantum OpenPGP in CafeOBJ
This article presents a formal specification and verification of the PQ OpenPGP protocol using the algebraic specification language CafeOBJ and successfully verify that the PQ OpenPGP protocol satisfies three essential security properties: secrecy of the session key, forward secrecy, and authenticity.