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.

Abstract A perfect matroid design (PMD) is a matroid whose flats of the same rank all have the same size. In this paper we introduce the q -analogue of a PMD and its properties. In order to do so, we first establish a new cryptomorphic definition for q -matroids. We show that q -Steiner systems are examples of q -PMD’s and we use this q -matroid structure to construct subspace designs from q -Steiner systems. We apply this construction to the only known q -Steiner system, which has parameters S (2, 3, 13; 2), and hence establish the existence of a new subspace design with parameters 2-(13, 4, 5115; 2).