S-box optimization using SAT solvers
These tools are part of the paper "Optimizing S-box Implementations for Several Criteria using SAT Solvers" by Ko Stoffelen, published at FSE 2016, available here.
C', given an optimization goal, an S-box and a
k. It writes to
stdout. Adding another S-box can easily be done with 1 line of code.
$ ./getanf.py -h usage: getanf.py [-h] mode cipher k [width] positional arguments: mode Mode to operate in. One of: mc for multiplicative complexity bgc for bitslice gate complexity gc for gate complexity depth for depth complexity cipher Name of cipher of which the S-box should be used. One of: ascon, ctc2, icepole, joltik, joltik_inv, ketje, keyak, lac, minalpher, present, primate, primate_inv, prost, rectangle, rectangle_inv k Value to test for. E.g. number of nonlinear gates for mode=mc, circuit depth for mode=depth, etc. width Only applicable to mode=depth. Set width of circuit layer to test for. optional arguments: -h, --help show this help message and exit
In DIMACS CNF format, all variables are replaced by numbers.
cnfclaimtoclaim.py takes care of a preprocessing step to translate a solution found by the SAT solver (CNF claim file) back to the original variable names. It writes to
$ ./cnfclaimtoclaim.py -h usage: cnfclaimtoclaim.py [-h] claim [resolve] positional arguments: claim Name of the CNF claim file as provided by the SAT solver. resolve Name of the resolve file as provided by xl0.exe. If omitted, <claim>.eqs.cnf.resolve will be used optional arguments: -h, --help show this help message and exit
getsolution.py reconstructs the S-box implementation from the original ANF file and the file outputted by
cnfclaimtoclaim.py. It writes to
stdout. It is possible that some 'gates' are not actually being used. They can freely be removed from the implementation.
$ ./getsolution.py -h usage: getsolution.py [-h] [-m mode] [-c claim] file positional arguments: file Name of the anf file as generated by getanf.py optional arguments: -h, --help show this help message and exit -m mode Mode to operate in. One of: mc for multiplicative complexity bgc for bitslice gate complexity gc for gate complexity depth for depth complexity If omitted, the mode will be based on the filename -c claim Name of the claim file as generated by cnfclaimtoclaim.py. If omitted, <file>.claim.txt will be used
An implementation of Bard-Courtois-Jefferson for converting a sparse system of low-degree multivariate polynomials over GF(2) from ANF to CNF can be found here. It is also implemented in the xl0 tool, available here (documentation). Unfortunately it is only distributed as a Windows binary.
Optionally, if one wants to optimize linear parts separately, as done for the S-box used by the PRIMATE permutation in Section 4 of the paper, an implementation of Fuhs-Kamp by Thom Wiggers is available on GitHub. He also implemented Boyar-Matthews-Peralta, which can be found here.
A typical run will go like this. Assume we want to optimize the RECTANGLE S-box for gate complexity and we want to test if there exists a circuit implementing the S-box with 11 gates. Any SAT solver that reads DIMACS CNF files can be used.
$ ./getanf.py gc rectangle 11 > rectangle_gc11.eqs C:\> xl0.exe /deg3 /dontsat /bard rectangle_gc11.eqs $ nohup ./myfavouritesatsolver rectangle_gc11.eqs.cnf > rectangle_gc11.eqs.cnf.claim & $ ./cnfclaimtoclaim.py rectangle_gc11.eqs.cnf.claim > rectangle_gc11.eqs.claim.txt $ ./getsolution.py rectangle_gc11.eqs > rectangle_gc11.solution