Project summary

In this project we aim to develop new verification techniques of post-quantum cryptographic primitives. Quantum computers will be a real threat to public-key cryptography which is used to secure all digital communication in today’s world. The security of these cryptographic primitives is provided by their complex security proofs which are prone to errors. In the case of post-quantum security, the security proofs are even more complex than in the classical setting. Therefore, to ensure a high guarantee of post-quantum cryptographic security, simple security proofs performed by humans are not sufficient to provide confidence in those primitives. Formal verification methods which are performed by software are highly required. In this project we will investigate and develop new formal verification methods.

Project description

Rational: Current research in post-quantum cryptography and its formal verification is timely and relevant as never before. Even if the first fully-fledged quantum computer seems to be years away from being available to the public use, cryptographers must prepare for this future now. Integration of quantum-safe crypto systems will require years of challenging work and tests. All the existing security proofs of post-quantum cryptographic primitives are performed by a human and therefore error prone, because small mistakes in a proof can be easily overlooked. Even though the modern proof methods of security are well-structured, which makes it possible to reduce the number of errors, it is still extremely hard to achieve a 100% guarantee that the proof is correct. Therefore, it is significant to have verification methods which can be performed by software and so enhance confidence in security proof. While this is a widespread practice for many classical, i.e., pre-quantum cryptographic primitives, in the case of post-quantum crypto schemes the problem of formal verification is still unsolved. Since the development and deployment of post-quantum cryptographic primitives can yet take several years, we need to analyze and verify the developed post-quantum algorithms already today. The national institute for standardization and technology (NIST) has already initiated the standardization procedure of new post-quantum encryption and digital signature schemes.

Methodology: The common approach for presenting security proofs for cryptographic schemes is given by a sequence of games, which is also well suited for formal verification. There are several frameworks which use this approach and have been developed for verifying classical cryptographic primitives. Unfortunately, these frameworks cannot be used for verifying post-quantum cryptography, since the soundness of these primitives is proven in relation to classical semantics of the protocol and the adversary. A novel approach is needed to cover post-quantum cryptography. This can be achieved by introducing a new relational logic that would enable us to verify the correctness of proofs in the post-quantum setting.

Innovation: Currently, there exists only one tool that allows us to prove relational statements about quantum programs. However, no cryptographic schemes have been verified yet using this tool. This tool is a generalization of probabilistic relational Hoare logic to the quantum setting. In this project we will investigate the functionality of the above-mentioned verification tool and apply it to several post-quantum encryption and signature schemes. We will also explore any modifications/adaptations of this verification tool to enable a more universal verification approach of post-quantum cryptography.


View publications

Partner organization(s)

Data61 logo

Project members

Lead investigators:

Dr Naipeng Dong

School of Information Technology and Electrical Engineering

Dr Veronika Kuchta

Honorary Research Fellow
School of Mathematics and Physics

Associate Professor Guangdong Bai

Associate Professor Software Engine
School of Information Technology and Electrical Engineering