Formal Analysis and Verification of Post-Quantum Cryptographic Protocols (FAVPQC)

In this project, we develop/modify post-quantum cryptographic protocols and analyze them formally using software, called Maude-NPA. Maude-NPA is an analysis tool for cryptographic security protocols that takes into account the algebraic properties of the cryptosystem. Sometimes algebraic properties can uncover weaknesses of cryptosystems and, in other cases, they are part of the protocol security assumptions. Maude-NPA has a theoretical basis on rewriting logic, equational unification, and narrowing. It can be used to reason about a wide range of cryptographic properties, including cancellation of encryption and decryption, Diffie-Hellman exponentiation, exclusive-or, bilinear pairings, and some approximations of homomorphic encryption. The project is aimed for the formal analysis of post-quantum cryptographic protocols by focusing on lattice-based and code-based. In our knowledge, there is no known formal analysis tool for these protocols. Moreover, it’s known that formal analysis of post-quantum cryptosystems has not been studied deeply. In the scope of the project, we will use Maude-NPA for the analysis of post-quantum cryptographic protocols. The methods which will be used in the project are based on studying search and decision problems, and different interpretations of algebraic techniques. We will adopt these methodologies to encode and (semi)-automatically analyze post-quantum cryptosystems in extended Maude-NPA.