Conversion of equations to cnf, for using sat solvers

Question

So I've to convert some equations which has been devised by a colleague of mine into the cnf file format, to use with some open source sat solvers.

The equations are:

S-boxes:

y1= 1+x1+x2+x4+x1x2

y2= 1+x1+x2+x3+x3x2

y3= 1+x1+x4+x1x2+x1x3+x2x3+x3x4+x1x2x3

y4= x1+x2+x3+x1x3+x1x4+x2x4+x3x4+x1x2x3+x2x3x4

Mix-columns:

Y1= 2.X1+3.X2+1.X3+1.X4

Y2= 1.X1+2.X2+3.X3+1.X4

Y3= 1.X1+1.X2+2.X3+3.X4

Y4= 3.X1+1.X2+1.X3+2.X4

. denotes multiplication in GF(2^4) with x^4+x+1 being the irreducible polynomial.

For the attack,

Z= z1|z2|...|z16, 1<= i<=16

Then, ui= (1+z(4i-3)) ^ (1+ z(4i-2)) ^ (1+z(4i-1)) ^ (1+ z(4i)), 1<=i<=4

Then, (1+u1) V (1+u2) V (1+u3) V (1+u4) =1; ui + uj=1, i<=i<=j<=4

I'd appreciate any information on how to convert these to cnf file format, including any reference links. Some help regarding specifying constraints like the above in cnf file format would also be appreciated.

im trying to do a similar thing.i would be happy to hear a few good answers.. — Dchris, May 16 '13 at 13:46

score 2 · Answer 1 · edited Oct 31 '15 at 12:14

Here is one suggestion:

Encode the mathematical operations (addition, multiplication in GF(16) and so forth) as circuits. If you have done a course in digital logic design, you will know how to do this. If not, it'll be a little hard. If you need more information, tell me what your background is and I'll try to make specific suggestions.
Use the Tseitin transformation to convert the circuit into CNF.

PS. It seems like you're trying to do crypto using a SAT solver. AFAIK this doesn't work that well with standard solvers like MiniSat. Not sure if CryptoMiniSat will be better, but it might be good to keep in mind that these types of problems have traditionally been hard for SAT solvers.

Conversion of equations to cnf, for using sat solvers

1 Answers1