How to fake an RSA signature by encoding modular root finding as a SAT problem

Logical cryptanalysis has been introduced by Massacci and Marraro as a general framework for encoding properties of crypto-algorithms into SAT problems, with the aim of generating SAT benchmarks that are controllable and that share the properties of real-world problems and randomly generated problems. In this paper, spurred by the proposal of Cook and Mitchell to encode the factorization of large integers as a SAT problem, we propose the SAT encoding of another aspect of RSA, namely finding (i.e. faking) an RSA signature for a given message without factoring the modulus. Given a small public exponent e, a modulus n and a message m, we can generate a SAT formula whose models correspond to the eth roots of m modulo n, without encoding the factorization of n or other functions that can be used to factor n. Our encoding can be used to either generate solved instances for SAT or both satisfiable and unsatisfiable instances. We report the experimental results of three solvers, HeerHugo by Gr...