ANF-Based Satisfiability for Weil-Descent Cryptographic Attacks

In recent years, SAT solvers have been increasingly used in cryptanalysis, for performing attacks both on symmetric and asymmetric schemes. More specifically, they are employed whenever one needs to compute a valid assignment for a logical formula when running the attack. Most often, these formulae are initially represented in Algebraic Normal Form (ANF). Solvers dedicated to solving such instances translate the input formulae into a conjunction of CNF and XOR clauses and use different techniques such as XOR recovery and manipulation and Gaussian elimination. In this paper, we aim to build a solver able to reason directly on ANF formulae derived from attacks using Weil descent on Semaev polynomials of elliptic curves, while integrating dedicated lazy structures inspired from SAT solvers.