NeuroGIFT: Using a Machine Learning Based Sat Solver for Cryptanalysis

Abstract

A recent trend in machine learning is the implementation of machine learning based solvers, such as the sat solver NeuroSat. The main limitation of NeuroSat is its scaling to large problems. We conjecture that this lack of scaling is due to learning an all-purpose SAT solver, and that learning to solve specialized SAT problems instead should yield better results. In this article, we evaluate our hypothesis by training and testing NeuroSat on SAT problems for differential cryptanalysis on the block cipher GIFT, and present the resulting classifier NeuroGift. We show that on these highly structured problems, our models are able to perform orders of magnitude better than the original NeuroSat, potentially paving the way for the use of specialized solvers for cryptanalysis problems.