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.
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.