Investigations into representations for components of the AES related to the SAT 2011 paper.
More...
Go to the source code of this file.
Detailed Description
Investigations into representations for components of the AES related to the SAT 2011 paper.
 Todo:
 Connections
 Todo:
 Considering output bits on their own

For better comparison with the DESpaper (see Cryptography/AdvancedEncryptionStandard/plans/general.hpp), we also need to consider the treatment of the boxes as 8 boolean functions (one for each output bit).

In this way at least encryption by just UCP is ensured.

We need to compare it with our standard approach, considering the whole boolean function.

This needs to be done for all approaches (minimum, canonical, and bases).
 Todo:
 Overview

One needs to systematically explore CNF representations, with and without new variables.

We consider methods for computing the following representations for the AES boxes:

the prime implicates.

minimum CNF representations.

small (minimal) CNF representations (in cases where minimum representations are infeasible).
These are described in Cryptography/AdvancedEncryptionStandard/plans/Representations/Methods.hpp .

There are currently open investigations in the following files:

For kbased representations see "kbased representations".
 Todo:
 Combining linear components

A full description of all of the possibilities for recombining AES and small scale linear components (from the Sbox and MixColumns) needs to be provided.

The idea here is that, due to the linearity of the Sbox's affine transformation, and the MixColumns operations, as well as the fact the Shiftrows simply permutes bytes, the linear aspects of the Sbox can be moved out, and seperated (in the case of the affine addition), or merged into the boxes for the MixColumn.

For the Sbox, we have 3 possibilities:

Full Sbox (M . s^(1) + A) .

Sbox minus addition of the affine constant (M . s^(1)).

Sbox minus affine transform entirely (s^(1)).

For the MixColumn multiplications, we have 2 possibilities:

Standard bytefield multiplications.

Sbox linear component (M) and Standard bytefield multiplications together.

A description of how to generate such translation is needed.

See also "Rearranging linear components of Sbox and MixColumns" in ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/plans/Translations.hpp.
 Todo:
 Scripts for generating statistics on random boxes

We currently wish to investigate various types of random boxes to see how they compare with the standard AES components.

Therefore, we need scripts to generate and almalgamate this data.

We can generate the various random boxes using:

We also need scripts to investigate the small scale multiplications, as well as the multiplications combined with the Sbox linear map (see ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/FieldOperationsAnalysis.mac).
 Todo:
 Find "best" solver(s) and local search algorithms for minimisation

There are currently a considerable number of problems in our investigation which require the solving of minimisation problems and finding transversals of subsumption hypergraphs when looking for minimum CNF representations (see Cryptography/AdvancedEncryptionStandard/plans/Representations/Methods.hpp)

We need a survey of the various solvers and local search algorithms that we can use with these problems, along with their performance on small instances, so that we can apply the best methods we have given limited resources.
 Todo:
 Standard naming scheme for experiment files

We need to think of a naming scheme for the AES boxes so we can create the hpp files discussing them in this directory.

We have the following boxes to investigate:

Sboxes with the following variants and parameters:

Sboxes with exponent / number of bits ranging from 18.

Sboxes without and without the affine constant addition and linear multiplication (see "Combining linear components").

random permutations for the Sbox.

random linear maps inside and outside the Sbox.
At the simplest level we vary the exponent (as in the [Small Scale Variants of the AES; Cid, Murphy, Robshaw]) and keep the rest as defaults.

Multiplication within the field with following variants:

the field element to multiply by.

the exponent / number of bits ranging from 18.

multiplications with and without the combination of the Sbox linear map (see "Combining linear components").

For now, we name:

the small scale Sboxes: Sbox_${e}.cnf , where ${e} is the field of the Sbox is a GF(2^e) finite field.

the small scale multiplications by element "a", in the default field with exponent e: Mul_${a}_${e}.cnf .
 Todo:
 kbased representations

We consider kbases for k in {1,2,...}? (see rand_rbase_cs(F,r) in ComputerAlgebra/Satisfiability/Lisp/Reductions/RBases.mac.)

One could consider certain prime implicates more important than others; for example ensuring that at least given a full input and/or a full output to one permutation the output resp. input can be inferred.

Can one formulate (relatively efficiently) the minimisation target that these inferences are "easily" available while otherwise using the smallest representation?

We could generalise the notion of rbase w.r.t. specific clauses which have to be deducible via r, while all (other) removed clauses just need to follow logically, or perhaps using some stronger reduction.

When investigations begin fully in this area, this todo should be moved to a new file, and most likely a new submodule.

We need to bring together here all information on currently known on 1bases for the AES boxes.

We also need to synchronise the notions in Annotations, here in this todo and in ComputerAlgebra/Satisfiability/Lisp/Reductions/plans/RBases.hpp.
 Todo:
 The square of the Sbox

As a start into the consideration of mergers within the AES"circuit" we consider the square of the sbox.

As a Maxima booleanfunction this is obtained by
s2 : square_bf(rijn_sbox_bf);

The full CNF representation is then obtained by
F2 : bf2relation_fullcnf_fcs(s2,8)$

A DIMACS file is created via
output_fcs(
sconcat("The squared AES Sbox in full CNF representation."),
F2,
"AES_Sbox2_full.cnf")$
\verbatim
</li>
<li> Prime clauses:
\verbatim
> QuineMcCluskeyn16O3DNDEBUG AES_Sbox2_full.cnf > AES_PK2.cnf
> cat AES_PK2.cnf  ExtendedDimacsFullStatisticsO3DNDEBUG
n non_taut_c red_l taut_c orig_l comment_count finished_bool
16 137185 1007214 0 1007214 1 1
length count
5 5
6 3898
7 83267
8 49203
9 812

This doesn't look much different from the Sbox itself; one needs to consider further properties.
 Todo:
 Understanding prime implicates after any partial assignment

To consider the AES boxes as an "active clause", we want to first be able, given a partial assignment, to infer as many forced assignments as possible. This can be done simply with the DNF representation.

However, secondly one needs, given a partial assignment, to be able to determine various measures for heuristics.

Therefore, investigating several statistics (most notably the number of clauses for a given variable) of the prime implicates of the clauseset, formed after taking the Sbox and applying each partial assignment, is necessary to try and discern a pattern.

If such patterns can be deduced for particular clauseset measures, then the active clause can use this pattern, given a partial assignment, to return reasonable values for these measures which can be used for statistics.

A C++ implementation of such a system whereby the set of prime implicates is taken as input, and each partial assignment along with the relevant statistics is returned is necessary.

Such a C++ implementation would need to be able to apply a partial assignment to a clauseset and then compute various statistics on the result. This would need to be done for every partial assignment.

After applying the partial assignment, to gain the prime implicates of the new boolean function, one must simply apply subsumption elimination to the new clauseset (which is just result of applying a partial assignment to the prime implicates of the original function). This can be done using functionality already in the library (MG: Where?).
Definition in file general.hpp.