Formal Analysis and Verification of Post-Quantum Cryptographic Protocols

In FAVPQC project, we develop/modify post-quantum cryptographic protocols and analyse 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 postquantum 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.

This project is directly related with the call in the scope of “Cyber security, including the prevention of and recovery from cyberattacks, also taking into account the postquantum era”.