Attacking RSA moduli with SAT solvers

This thesis aimed to explore how sequential boolean satisability solvers can be used on the integer factorisation problem. The integer factorisation problem is believed to be hard and modern public key cryptography relies on that,note worthily SSL/TSL and SSH support the use of RSA. However, it is not proven that integer factorisation is hard and therefore it is of great importanceto explore dierent attack avenues. The modulus in RSA is a semiprime, e.g.an integer that is the product of two primes. Hence, in this thesis an empiricalstudy of the factorisation of semiprimes with a bit-length of up to 32 bits iscarried out. Randomly selected semiprimes are factorized through six dierent reductions using three dierent solvers (Glucose, Lingeling and PicoSAT) and the result are compared to that of MSieve, an open-source integer factorisationprogram. As seen in the comparison boolean satisability solvers cannot be used as a replacement of an integer factorisation solver. Additionally comparisons between the dierent reductions and boolean satisability solvers show that the combination of solver and reduction greatly aects performance. The implication is that further explorations of the integer factorisation problem with boolean satisability solvers can greatly benet from either avoiding a inadequate solver and reduction pair or from attempting to identify the outliers that signify a inadequate coupling