Design and Analysis of NTRU-based Cryptosystems Using Formal Methods 

This project is a joint research project funded by TÜBİTAK and SRGNSF for 24 months.

In this project, we modify NTRU-based cryptographic protocols and then analyze them in a formalism, which combines the power of conditional rewriting with logic programming. We analyze NTRU-based cryptosystems to verify in formal way properties. Our aim is to provide new ideas for NTRU-based cryptosystems which are formally verified and modify NTRU-based cryptosystems. Then, we extend ρLog (and, correspondingly, PρLog) to develop an automated tool to formally analyze NTRU-based cryptosystems. We also compare the formal verification tools with algebraic properties to test NTRU-based cryptosystems. Furthermore, we experiment with a use case scenario.

The project is aimed for the formal analysis of post-quantum cryptographic protocols and there is no known formal analysis tool for these protocols. Moreover, it’s known that formal analysis of NTRU-based cryptosystems has not been studied deeply. It’s important to explore formal verification properties of modular operations over finite rings. 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 NTRU-based cryptosystems in extended ρLog calculus.