[with patch, positive review] Add SBox -> CNF Conversion

[Martin Albrecht]

While not really complicated it is nice to have a direct conversion from S-Boxes to CNF since SAT-solves enjoy some attention right now in crypto.

[Martin Albrecht]

Minh, can I ask you to review this ticket?

[Minh Van Nguyen]

Replying to malb:

Minh, can I ask you to review this ticket?

Hi Martin. Sorry for my simple question: Is there a reference or paper that describes the algorithm you use for converting an S-box to CNF? I only know about the application of SAT to cryptanalysis by reading this ticket. I usually find it much easier to understand code if I can access a reference somewhere that describes the algorithm.

[Martin Albrecht]

Hi Minh,

the standard reference for SAT-solvers in block cipher cryptanalysis is:

​http://eprint.iacr.org/2007/024

I've implemented a converter along those lines at

​http://bitbucket.org/malb/algebraic_attacks/src/tip/anf2cnf.py

which isn't ready for inclusion yet. This ticket follows a different approach and converts the S-Box directly. The algorithm used is the standard algorithm for computing CNF from a truth table,

cf. sage.sage.logic.boolformula

[Martin Albrecht]

Hi Burcin, Ralf,

can I ask for this (hopefully) easy review?

[ylchapuy]

My 2 cents:

• the complexity is 'n * 2m' (instead of 'm * 2n'):

    for x in X:                        <-- 2^m
        for output_bit in output_bits: <-- n
  

• typos:
  • line 866: evaluate instead of evaulate
  • line 840: endianness instead of endianess

• maybe add an exception if xi or yi has wrong size

• maybe (but as you like) construct x's on the fly:

    for e in xrange(2**m):
        x = self.to_bits(e)
  

otherwise seems good to me.

[Martin Albrecht]

The attached updated patch addresses the reviewer's comments. Is that a positive review then?

[ylchapuy]

Yes it is. Positive review.