Modelling and verification of post-quantum key encapsulation mechanisms using Maude [Póster]

Abstract

The security of information systems relies on math ematical problems that are hard to solve. Quantum computing threatens the security of our systems and communications. Kyber, BIKE and Classic McEliece are three candidates in the Post-Quantum Cryptography project launched by the National Institute of Standards and Technologies. We propose a formal framework in Maude for the security analysis of post quantum key encapsulation mechanisms. With our framework, we construct a symbolic model for each candidate. Through reachability analysis, we find both a man-in-the-middle attack in each of them and a design vulnerability in BIKE. For both cases, we provide some possible solutions. Then, we use Maude’s Linear Temporal Logic model checker to extend the analysis of the symbolic system regarding security, liveness and fairness properties. Liveness and fairness properties hold but the security property does not due to the man-in-the-middle attack and the design vulnerability in BIKE.