Experimental Algebraic Cryptanalysis of Block Ciphers

Benchmarking Algebraic,
Logical and Constraint Solvers
and Study of Selected Hard Problems

Main objective: Study the hardness of randomly generated dense or sparse MQ problems, and SAT problems. We concentrate on systems which are generated at random in such a way that they have a solution (or a small number of solutions). Interesting systems are systems which are sparse, overdefined, or both.

Generating standard instances of hard problems used to benchmark different solving algorithms such as generic Gröbner basis algorithms, ElimLin, SAT solvers, constraint satisfaction algorithms, specialized or advanced methods such as (geometric) T' methods, etc.

Our Program Tool

We have a ready program axel.exe to generate as a file on a hard drive, various systems of equations and hard problems to benchmark various solvers against each other.

It also includes a number of embedded solvers which can be activated through command line options. We will give here a short legend on how to use it with some embedded solvers, the list of command line switches in terms of solvers given here is not exhaustive, and in general there are some extra options available, which will be very similar as many options which exist for another program, XL0.exe , which are documented here at tools.html.

Remark: if axel.exe does not work on your computer try to install Visual Studio 6 (or just some some missing dlls) on your PC. The file XL0.exe and for certain options even more extra files must be found in the same directory. These extra files can be downladed from tools.html.

Copyright: The exe files (closed-source code programs) provided here can be used freely if the user acknowledges that they use tools developed by Nicolas T. Courtois AND links to this page. Source code is not available.

Random Dense and Sparse MQ Systems of Equations

In order to generate a random dense system of multivariate quadratic equations with m equations and n variables, we type:

axel.exe 78 n m 2 0.5 0.5 1.0 [1= homogenous only] [solver options....] [/quiet]. Legend:

2 is the degree, 3 would give cubic equations but less things will work. Degree 4 is the maximum supported for most solvers, though with certain options such as "axel 78 n m D 0.05 0.5 0.1 /bard /sat" we can try to solve a system of equations of any degree.
if no option for the solver is specified, the program will apply the ElimLin algorithm which may reduce the number of variables in the system and will write on the disk a modified system. To avoid this (really apply no solver at all) it is necessary to use the option /genonly.
Examples of dense MQ problems generated by this program can be seen here: few MQ challenges to solve. They have no trapdoor and no hidden structure. We encourage the researchers to solve these systems by their favourite method (one solution is enough, it is not demanded to find all of them). We will post their timings on this page.
no option but with switch /up3 will expand the equations to the degree 3 as in the XL algorithm, and then apply the ElimLin algorithm as one possible final step. It can be seen as a powerful version of the XL algorithm, neiher the best, nor the worst.
the option /xsl will apply a version of the XSL algorithm, not a very good algorithm, and expands systems of equations a lot at degree 2+2=4. There are also special variants of XSL such as the option /xsm and /xsn.
the option /sat will apply a built-in ANF-to-CNF conversion algorithm and a SAT solver. By default it uses MiniSat2.exe which needs to be present in the current directory. To download another SAT solver or for better conversion options, see tools.html.

axel.exe 78 n m 2 beta lbeta gamma [1=homogenous only] [solver options....][/genonly] [/quiet].
This allows more generally, to generate sparse systems.
Sparsity is expressed by three parameters:
- beta is the probability that a randomly selected quadratic coefficient is 1. It can be called 'local sparsity'.
- lbeta is the probability that a randomly selected linear coefficient is 1.
- gamma is a GLOBAL sort of sparsity. Basically, for all the m equations, out of n*n/2 possible quadratic monomials like x_i*x_j, a proportion of gamma is active, and will be at 1 with probability beta for each equation independently. However a proportion of 1-gamma of these monomials will never ever be used, in any out of m equations. They are 'globally' absent.
- the last parameter exists for compatibility reasons and should not be used. It can be absent, or put at 1, to indicate that equations must be homogenous quadratic, which also is obtained by setting lbeta=0 and therefore this option is simply not needed.

Again, all systems are generated in such a way that they have 1 solution, and may have more solutions which will occur by accident. To do this we generate a random system as above, generate a random solution, and adjust the constants in the system so that this solution satisifies all the equations. Moreover, for smaller n up to n=24 systems actually will have a unique solution, this is checked by brute force. For larger systems it is impossible to guarantee that the system have no extra solutions, but it is easy to see that on average the number of extra solutions will be small, like 0,1 or 2 extra solutions.

SAT Solving Challenges

This generator is a beta. In order to generate a random k-SAT system m clauses and n variables, we type:

axel.exe 80 n m k [alpha] [/fixXX] [/sat and solver options....] [/quiet]. Legend:
In each clause there are k litterals which are variables or negations of variables.
If k is not an integer, for example k=3.8, then we get a biased mix of clauses of size randomly either s and s+1 where s=floor(k), and the average size being k.
alpha is optional, it is the the proportion of clauses of length 2 in the m clauses in the system generated.
/fix20 will fix the first 20 variables to their actual values (correct assignment) .
/wrong will fix these 20 variables to some values which are wrong, and the system will be UNSAT (incorrect assignment), unless we are very lucky and the system is still satisfiable, totallly by accident.
/genonly will not use any solver, but only generate equations, this is currently the default behaviour.
/CPU0 will only use the first CPU on your PC.
/below_normal and /idle allow one to run the process with a lower priority.
there is a trick to make the same thing run several times with different random coins, for this we add a numerical parameter like 1-100 after alpha. It will then run 100 times to see how much is the average and median running time.
solver options: one must specify at least one of these options for example /sat to run a SAT solver, and there is no conversion, but different SAT solvers can be tried, similar to the options of XL0.exe solver specified in tools.html. We recall here the main options:

option /elite uses a preprocessor, famous SatElite, this can be combined with any other SAT solver, but should not be needed with MiniSat because it is already kind of embedded inside(!). It requires the file SatElite2005.exe to be present in the current directory.
by default it uses MiniSat 2.0.6. compiled under cygwin but only if it is present under the fixed path c:\cygwin\sat\minisat20.exe exactly.

otherwise it will try to use MiniSat2.exe compiled under windows which needs to be present in the current directory.
option /minisat114 uses even an older version 1.14 if present under c:\cygwin\sat\MiniSat_v1.14_cygwin exactly.
/minisat206 and /minisat207 and /minisat220 will use a specific version like MiniSat206.exe or MiniSat207.exe or MiniSat220.exe exactly, and only if present.
/minisat64220 and /minisat64206 are two 64-bit versions of MiniSat to try. Requires Windows x64 and the right exe file: MiniSatx64v220.exe or MiniSatx64v206.exe to be present in the current directory.
/cryptominisat209 and /cryptominisat64209 are two recent versions (2011) of the famous CryptoMiniSat by Mate Soos. The second being 64-bit. Requires the corresponding compiled exe file and dll bundled here for convenience: CryptoMiniSat209_32-bit_Intel.zip or CryptoMiniSat209_64-bit_Intel.zip to be present in the current directory.

/pico will use PicoSat which needs picostat.exe to be in the same directory.
/goX /depY is a stochastic parallel SAT solver. Here we split the task through adding extra Y assumptions. /depY does NOT need to be specified, and will be decreased automatically.
/koX is the same but only variables starting with k_i are used for assumptions.
also /zooX is another major parallelization option which tries different solvers, it is very messy, requires XL0.exe and extra files, creates subdirectories with even more extra files.
/soos1 and /soos2 are two different versions of MiniSat with embedded Gauss, developed by Mate Soos, the file minisat_gauss.exe or this one minisat_gauss2.exe needs to be in the same directory.

an internal solver to find contradictions based on unit propagation (elimination of clauses of length 1) is also implemented, currently always active

another internal solver to find contradictions based the graph algorithm for 2-SAT is also implemented, currently always active

conversion of CNF to ANF and using algebraic solvers such as ElimLin, XL or Gröbner bases, is also implemented:

for now we can try the special option /tp, which does convert a 3-SAT problem to a system of cubic equations. Then it applied the ElimLin algorithm. Then it tries the (standard) T' method which is a very powerful solver able to generate new equations which would have been found by certain Gröbner bases algorithms at a higher degree and with much more memory. However it is quite slow and is far from being optimised (it kind of finds the same equations many times). Requires XL0.exe and Tp.exe.

Multiplicative Complexity Challenges - Linear Algebra

These are optimisation problems which minimize the number of multiplications in various circuits.
We need at least these four programs, axel.exe and mp.exe with XL0.exe and MiniSat206.exe.
With some options more programs are needed (similar options as elsewhere).

In order to find a method for multipying nxn matrices within m=23 multiplications we type:

mp.exe n m /xl0 /sat /likebard [/fixXX] [/minisat206 or other solver options....] [/quiet]. Legend:
/CPU0 will only use the first CPU on your PC.
/below_normal and /idle allow one to run the process with a lower priority.
solver options: one must specify at least one of these options for example /sat to run a SAT solver, different SAT solvers can be tried, similar to the options of XL0.exe solver specified in tools.html. We recall here the main options:
option /elite uses a preprocessor, famous SatElite, requires SatElite2005.exe to be present.
/minisat64206 is a 64-bit version of MiniSat to try. Requires Windows x64 and the right exe file MiniSatx64v206.exe to be present.
/goX is an experimental parallel SAT solver which will use X CPUs.
used alone, option /zooX is another major parallelization option.

With this program we have obtained results on problems which remained open for more than 30 years, like Laderman 3x3 matrix multiplication method. To be published soon.

Multiplicative Complexity Challenges - Sboxes

We dispose of ready software to optimize any S-box and PROVE the one cannot do better (optimality).
To be published soon...

This page is a subspace of the cryptosystem.net/aes/ page.

Maintained by Nicolas T. Courtois
Last updated on 18th of July 2007.