How to convert a system of non-linear XOR equations to CNF

Question

I'm trying to analyse phase shift fault analysis in trivium and came across a system of non-linear equations to solve. I read about sat-solvers and Gaussian elimination but unfortunately, none of the articles I found on the internet shows how to tackle a non-linear system of equations with a large number of variables (here trivium gives 288 variables). So I'm pretty much stuck now on how to solve for these variables.

Answer 1

You could express your problem as a network of Boolean gates - a netlist - and use bc2cnf to translate it to CNF. You can instruct bc2cnf to output XOR clauses in XCNF format, an extended CNF format with "x" clauses denoting XOR clauses.

SAT solvers like cryptominisat are capable of reading XCNF and/or detecting the contained XOR gates and performing Gaussian elimination. Cryptominisat reportedly has been used several times to attack the Trivium stream cipher.

Answer 2

I'd recommend taking a look at an SMT solver, e.g. Z3. With SMT you can express Boolean equations and inequalities in a natural way instead of bit-blasting everything down to a SAT instance. There's plenty of documentation online to get you started.