3

I've been trying to use Cryptominisat (something similar will do) to formulate an attack on Piccolo, a lightweight block cipher, similar to AES.

The equations are something like this:

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 need some help regarding my next step. I have the CNF equations for the attack and the decryption ready, I really need help on how to use that with the sat solver and put it in a CNF file format. I've been looking all over the internet but there's no clear method given anywhere. Any help would be appreciated. If any more information is needed, please feel free to ask. I need to put the above equations in a cnf file.

Since the equations involved are quite complex(there are more), some references or examples for cnf files and their working would be awesome.

Rishav Mishra
  • 51
  • 4

1 Answers1

2

This specification of the CNF format might help you:

http://people.sc.fsu.edu/~jburkardt/pdf/dimacs_cnf.pdf

There are sample files linked on this page:

http://people.sc.fsu.edu/~jburkardt/data/cnf/cnf.html

Tilo
  • 3,255
  • 26
  • 31
  • Thanks for the references. Since I'm working on Piccolo which is really similar to AES, an example CNF file used for solving a related Block cipher would help a ton. I need a better idea of how to put down complex and cascading equations in this format. Thanks! – Rishav Mishra Apr 30 '13 at 18:42
  • The problem will probably be that you have operators in your equations that are not directly supported by SAT solvers - I would guess XORs for example? You might have to write a program to transform the equations for you, but maybe someone knows of a SAT solver that has been adjusted to the needs of crypto analysis... – Tilo Apr 30 '13 at 18:54
  • No, the equations are all in cnf format. However, I've to represent the faults and decryption as equations. For example, the equations for the fault are: Z= z1|z2|...|z16, 1<= i<=16 Then, ui= (1+z(4i-3)) ^ (!+ z(4i-2)) ^ (1+z(4i-1)) ^ (!+ z(4i)), 1<=i<=4 and the last equation which i described in the question. Hope I've explained myself better now. – Rishav Mishra Apr 30 '13 at 19:07
  • This might be the same file: http://elis.dvo.ru/~lab_11/glpk-doc/cnfsat.pdf (link working as of 12/9/2013) – Tilo Dec 09 '13 at 17:40
  • @RishavMishra you will be able to help me with this questions please http://crypto.stackexchange.com/questions/18514/algebraic-normal-form-piccolo – Juan Aug 07 '14 at 20:57
  • Here is an archive url of the CNF file format pdf: https://web.archive.org/web/20121224005200/https://people.sc.fsu.edu/~jburkardt/pdf/dimacs_cnf.pdf – Rashi Abramson Dec 11 '21 at 23:29