Plans on translating AES into active clauses.
More...
Go to the source code of this file.
Detailed Description
Plans on translating AES into active clauses.
 Todo:
 Links

Links must be added to other references to active clauses in the library.
 Todo:
 Partitioning into active clauses

This todo has to be updated according to ComputerAlgebra/Satisfiability/Lisp/plans/SatisfactionProblems.hpp.

An overview on the possibilities of anatomising the AESprocess into active clauses has to be gained.

The roughest subdivision presents just the inputoutput relation (this should not be considered as an active clause).

At the finest level we have represented the whole of AES as a boolean CNF.

Inbetween there are many possibilities to handle the roundcomputations.
 Todo:
 Active clauses for field operations

Likely the two best first candidates for active clauses are the Sbox (as map GF(2^8) > GF(2^8)) and multiplication with some constant a in GF(2^8)^* (again, as map GF(2^8) > GF(2^8)).

Both types of functions yield boolean functions in 16 variables.

As bijections, they all have trivial DNF representations (with 256 satisfying assignments).

For CNF representations see "Generate good CNF clausesets for the AES
Sbox" in Cryptology/Lisp/Cryptanalysis/Rijndael/plans/SboxAnalysis.hpp (obviously all the algorithmic techniques can be generalised to any function given by truth tables.

Obviously also of interest are OBDD representations of these boolean functions.

One should come pretty close to finding an optimal variable ordering.

These allow efficient handling of all basic tasks for active clauses (see ComputerAlgebra/Satisfiability/Lisp/plans/SatisfactionProblems.hpp).

Of course, special algorithms should be investigated.

It seems, that actually the DNF representation we have, which actually is a full DNF, and just having 256 clauses, yields an unbeatable active clause:

Given any DNF representation D of a boolean function F, satisfiability of phi * F is just checked by testing whether phi * D is not the empty clauseset.

In general, for a clauseset F, considered as CNF or DNF, the opposite representation is just obtained by the transversal hypergraph, from which nonclauses are eliminated, and which then is complemented.

So forced literals for phi * D are literals which occur in every clause. This can be checked by just checking the literal degrees.

And the number of satisfying assignments for a hitting D can be computed by the standard counting arguments. The given case is even simpler, since we have a full clauseset (where full clausesets are stable under application of partial assignments), and so we just need to count the remaining clauses.

Nevertheless we need to compute the primeimplicate representation, since the minimal size of a prime implicate tells us how many variables have to be set until we may obtain a contradiction  this is important information for the analysis, and furthermore for the active clause it can be used as threshold which triggers some action (before, we are just lazy and don't do anything (w.r.t. updating the counters)).

All these generalisations are very general, and should go to supermodule Satisfiability/ProblemInstances.
Using these active clauses should give us a good advantage over any CNF translation!

We should aim at "high integration":

The more active clauses can manage the better.

So we should have the full Sbox an active clause, and not dividing it further.

Perhaps in combination with the various permutations we can combine several "microsteps" into one. Perhaps the ShiftRows step doesn't need to be made explicit at all. And also MixColumns operates on the bytes.

Perhaps we create "generic active clauses" for these cases, and instantiate them appropriately (so that many variations of the same basic active clause appear).

Identifying transformations of GF(2^8) seems most promising, since this yield active clauses with 16 bits, which can be thoroughly analysed. 32 bits likely is too much (since we won't have much exploitable structure(?)).

We have also the field addition, which can be broken down into binary xor, and perhaps a dedicated active clause(set) handles all these equations over GF(2) (via Gaussian elimination).

The main underlying theoretical question is whether the conditions "x * y = 1" and "a * x = y" are active clauses (for arbitrary GF(2^n).

This depends on the choice of literals (i.e., which partial assignments are allowed).

A coarse choice is to use bytevalued variables (x, y here are just elements of the bytefield) and standard literals: Here we have active clauses, since the field operations as well as inversions can be performed in polynomial time.

The next level (perhaps our preferred level) is the boolean level (now the bits of x and y can be queried). Using the natural representation of elements of GF(2^n) as vectors in the canonical base, we obtain one quadratic equation in both cases. If quadratic equations in GF(2^n) can be solved in polynomial time, then we are done, if not then we have to investigate whether the special form of equations we have matters or not.

A fine level considers again bytevalued variables, but signed literals. It seems rather unlikely that this can be solved in polynomial time. However for n=8 perhaps we can perform heavy preprocessing?
Definition in file ActiveClauses.hpp.