Recently, researchers from the Japan Advanced Institute of Science and Technology (JAIST) on formal analysis and verification of post-quantum cryptographic protocols. Led by Researcher Duong Dinh Tran and Professor Kazuhiro Ogata from JAIST, who is also an adjunct Full Professor Santiago Escobar from VRAIN, Universitat Politecnica de Valencia (Spain), the Professor Sedat Akleylek from Ondokuz Mayis University(Turkey) and Professor Ayoub Otmani from University of Rouen Normandie(France). Their study was published online on 28 December, 2023 in IEEE Access.

Research Outline: The emerging quantum computing technology has brought danger to public-key encryption systems widely used today as quantum-based algorithms like Shor's can solve the presumedly hard problems on which those public-key encryption systems are based. With massive investments from big companies and governments, the National Institute of Standards and Technology (NIST) predicts a 50% chance of a quantum computer capable of breaking RSA-2048 being developed by 2031. Besides, attackers can record the encrypted long-lived data from now and later decrypt it when large-scale quantum computers become available, which is known as the harvest now and decrypt later attack. These are strong motivations for the early construction of cryptographic algorithms and protocols that are resistant to quantum attackers, the so-called post-quantum cryptographic algorithms and protocols.
In our study, we present a security analysis of version 01 of the Post-Quantum Secure Shell (SSH) Transport Layer protocol being standardized by an Internet Engineering Task Force (IETF) Working Group. SSH provides us with a secure way to access remote computers over an unsecured network. The most well-known application of SSH is to allow users, particularly system administrators, to securely log in to a server and execute commands through the command line environment. SSH consists of three sub-protocols, among which, the SSH Transport Layer protocol is in charge of key negotiation in order to establish symmetric keys, which are then used by the other protocols to securely exchange information between two participants. The Post-Quantum SSH Transport Layer protocol (PQ SSH), which was proposed as a countermeasure against the quantum attack threat, bases its security on the so-called post-quantum hybrid key exchange method that uses a classical key exchange algorithm and a quantum-resistant Key Encapsulation Mechanism (KEM) in parallel.
Unlike traditional pen-and-paper security analysis, our analysis is conducted by using two formal method tools CafeOBJ and IPSG. CafeOBJ is an advanced algebraic language for writing formal specifications of a wide variety of systems, supporting order-sorted equational logic with various equational theory attributes such as associative, commutativity, identity, and idempotency. We construct a symbolic model of the protocol and specify it in CafeOBJ as a formal specification, faithfully capturing what is described in the Internet-Draft of the protocol. We use an extended version of the standard Dolev-Yao intruder model to specify a threat model in which the attacker has the capabilities of fully controlling the network, breaking classical key exchange schemes under the assumption that they have access to large-scale quantum computers, and compromising secrets. Once the formal specification is completed, we formally verify that the protocol enjoys three desired security properties stated in the Internet-Draft including (1) session key secrecy, (2) forward secrecy, and (3) session identifier uniqueness. The verification process, outlined in Figure 1, is automated using the tool IPSG to generate the executable proof scores. The proofs of the three properties are achieved with respect to an unbounded number of protocol participants and session executions.
The analysis found a weakness of the protocol related to the authentication process, that is, the protocol does not meet the claimed authentication property. Although the found weakness does not affect the confidentiality of session keys shared by honest participants, we propose to fix the weakness and improve the protocol by including the identifiers of the client and the server in the exchange hash. We revise the CafeOBJ formal specification accordingly so that we can formally verify that the improved protocol enjoys the authentication property as well as (1), (2), and (3).

Figure 1: Analysis and Verification flow with IPSG and CafeOBJ.

Future Prospects: At the end of 2023, after six years of the Post-Quantum Cryptography Standardization project, NIST released three draft standards for post-quantum key exchange and digital signature algorithms. Using these primitives as building blocks, more and more variants of cryptographic protocols will be introduced shortly after due to the urgent of the quantum attack threat. These post-quantum cryptographic protocols, such as PQ SSH, are typically complex and may exhibit design flaws that are hard to detect even by security experts. Given their novelty and recent emergence, formal verification of this class of protocols has been lacking. Therefore, it is highly imperative to guarantee the correctness and reliability of them in preparing for the quantum era. As demonstrated through the study, our verification technique is capable of verifying large and complex post-quantum cryptographic protocols with high automation.

DOI: 10.1109/ACCESS.2023.3347914

May 24, 2024