AES experiments related to the SAT 2012 paper.
We consider experiments investigating the AES and smallscale translations to CNF, as well as the translations of the associated AES boxes such as the Sbox, field multiplication, field inversion and so on.
For information on the scope of the AES and small scale translations, see "Investigation dimensions" below. For an idea of the open problems, please see "Open problems".
 Todo:
 Links
 Todo:
 Investigating dimensions

The translation is available at ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/Translations.mac.

The translation system (irrespective of the AES) has three conceptual levels:

Variant: which AES function we consider (smallscale parameters etc). This level defines the whole boolean function we consider.

Decomposition: how to decompose the large boolean function into smaller functions.

Representation: how to represent the small boolean functions.

Discussion of each of the possible dimensions of the translations should become a separate todo.

A separate todo is needed on the decomposition of the AES.

Further discussion is needed on the decompositions of the key schedule.

Variants (AES parameters):

Number of rounds (10 options): 1,...,10.

Size of field (8 options) : 1,...,8.

Number of columns in AES block (4 options): 1,...,4.

Number of rows in AES block (4 options): 1,...,4.

Inclusion of special final round or not (2 options):

Final round is the same as every other (in line with smallscale).

Final round doesn't include the MixColumns operation.

Box replacements (3 options):

Original Sbox, field multiplication etc. are used.

Random permutations are used.

The identity is used.

See "Explain how to replace various AES boxes with identity or
random" in AdvancedEncryptionStandard/plans/general.hpp; this aspects needs better explanations.

Decomposition:

We consider the AES function as:

Rounds, which have:

Subbytes operation which is the Sbox applied to each consecutive 8bits of the input.

MixColumn operation applied to each column. This operation is a matrix multiplication applied to the vector of 8bit words in the column.

Key schedule, which has:

The Sbox applied to each 8bit word in the first column of the previous round key.

Additions of the Sbox result, a round constant and certain 8bit words from the previous round key.

So far, the decompositions we consider revolve around the Sboxes and MixColumn operation.

Sbox decompositions:

Movement of the Sbox linear map into MixColumns (2 options):

Sbox linear map is left in the Sbox.

Sbox linear map is moved through the ShiftRows operation. It is then combined with the MixColumn multiplication components.

Sbox affine constant (2 options):

Sbox affine constant addition remains in Sbox.

Sbox affine constant addition moved through ShiftRows and MixColumns. It is then added to the end of the round.

MixColumn decomposition:

MixColumns direction (3 options):

Translation of the MixColumn component using both the encryption and decryption components.

Translation using only the encryption direction.

Translation using only the decryption direction.

Function decomposition (3 options):

Multiplication function decomposition (default):

Representing the MixColumns using individual multiplication functions as well as addition constraints.

Bitmatrix representation:

Representing the MixColumns as a bitmatrix multiplication.

Representing the multiplication of each row in the bit matrix using addition constraints.

Whole function representation:

Taking the MixColumn as a single boolean function.

Key schedule decomposition (2 option):

Shared subexpression translation (default):

Translates the Sbox operations as individual functions.

The first column of a new round key is computed by K_1 + Sbox(K_p') + C. K_p is a column of certain key words from the previous round key. K_1 is the first column of the previous round key and C is a constant.

Column i+1 in the new round key is computed by K_(i1) + K_p''. K_(i1) is the previous column of the new round key. K_pi is ith column from the previous round key.

Larger arity addition computation (not implemented):

Translates the Sbox operations as individual functions.

Column i of the new round key is computed by SBox(K_p) + C + sum(K_1,...,K_i). K_i is the ith column of the previous round key. K_p is a column of certain key words from the previous round key.

The point here is that later columns of the *new* round key are defined using earlier columns of the *new* round key.

In this translation, instead of using earlier columns of the new round key, we expand the computation out. Each new round key is specified using only columns from the previous round key (no reusing results).

Representation:

Box representation (4 options):

Canonical translation.

Canonical+ translation.

0based representation.

1based representation.

Minimum representation (i.e., var(F)based representation).

This todo needs to be moved to docus in Cryptology/Lisp/Cryptanalysis/Rijndael/docus/.

Note that addition constraints are always represented using their prime implicates.

In each case, the first option is considered the default.

We need instructions on how to generate each translation. These should occur here (in this plans file).

See "Separate keyschedule and blockcipher" in AdvancedEncryptionStandard/plans/general.hpp; this aspects needs better explanations.

For more information, see Cryptology/Lisp/Cryptanalysis/Rijndael/plans/Translations.hpp.
 Todo:
 Open problems

For a description of the investigation, please see Cryptography/AdvancedEncryptionStandard/plans/general.hpp.

Here is a list of experiments which still need to be run, or questions for which we still do not know the answer.

We need to find out which solvers and local search algorithms perform best on different minimisation problems, see AdvancedEncryptionStandard/plans/Representations/general.hpp.

We need basic data on the prime implicates and subsumption hypergraphs for the following:

We need to find minimum CNF representations for the following functions:

Investigations into the prime implicates, subsumption hypergraphs and minimum representations of:

Random permutations (see "First considerations of random permutation" in Experimentation/Investigations/BooleanFunctions/plans/Permutations.hpp).

Random linear maps (see "Affine bijections over ZZ_2" in Experimentation/Investigations/BooleanFunctions/plans/Permutations.hpp).

Random boolean functions (see Experimentation/Investigations/BooleanFunctions/plans/general.hpp).
 Todo:
 Update experiment script

First experimentrunning script:

Using three steps: experimentcreation, experimentrunning, experimentevaluation.

An experiment is representing via a directory with a good descriptive name, where inside all information is found for reproduction and restarting.

The problems are created by computing the key by the Maxima randomnumber generator, encrypting the all0 plaintext, and then taking the problem of guessing the key from given plain and ciphertext.

The major problem here is running Maxima in parallel:

See "Improve locality" in Buildsystem/MasterScript/SpecialProcessing/plans/Call_Maxima.hpp, especially point "No interference of different invocations".

Until now it was not a major issue, however now running, say, 30 experiments in parallel won't work out without a solution.

For what is Maxima needed?

Creation of the templateSATproblems should be possible in advance.

If a key is computed, we should check whether this key is correct.

At least for the smallscale system the could be done using Sage; hopefully Sage is more amenable to scriptusage.

DONE It seems best to have first a script which takes as parameters the generalised AESparameters plus optionally a seed (default=1), so that these parameters fully specify a sequence of generalised AES problems, and then all combinations of SAT solvers and translations are executed.

Experiment creation:

See Cryptography/AdvancedEncryptionStandard/generate_aes_experiment.

The current experiment creation script allows one to specify the number of rounds, number of random plaintextciphertextpairs to generate and the parameters specifying the AES instance and translation (see output_ss_fcl_std in ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/Translations.mac).

This generator generates several AES instances (one for each round) at once.

The generator should be split up into two scripts, one generating a single AES instance, another generating random plaintextciphertextpairs.

The script should output the parameters for the computation to a file "instance_parameters" in the experiment directory; the directory might be renamed.

The script badly needs documentation.

Experiment running:

See Cryptography/AdvancedEncryptionStandard/run_aes_experiment.

The AES experiment script should be split up into persolver scripts:

We need a "run_aes_experiment_oksolver", "run_aes_experiment_minisat2.2.0" and so on.

Each solverspecific experiment script can then handle outputting solver output to the correct directory.

Each script should examine "instance_parameters" to determine how many AES rounds and number of plaintextciphertextpairs to run the experiment on.

The script should then create the AES key discovery instances from the AES instances and plaintextciphertextpairs.

Finally it should run the selected solver on the instance and record the output into a file "r${r}_s${i}.cnf" where

r is the number of rounds for the AES key discovery instance the solver is being run on;

s is the seed for the plaintextciphertextpair used to instantiate the AES key discovery instance.

Documentation is badly needed for the script.

Experiment monitoring:

All directories created should have the datetime included in the name.

Each script should have the option to continue generating, running or monitoring from where it left off. This should be a case of rerunning the last experiment, and perhaps outputting a special file to indicate the experiment has been finished.

This todo should be split into todos for scripts for generating, running and monitoring.

For a list of other experiment scripts see "Experiment scripts" in Experimentation/Investigations/plans/general.hpp.

See "Update scripts" and "Just an unstructured morass of scripts" in Cryptography/AdvancedEncryptionStandard/plans/general.hpp.
 Todo:
 Move experiment data to investigationreports

All data, especially that generated for LCC and CP 2011 must be transferred to Annotations.

For LCC and CP there must be docus page with links to the relevant experiment plans, and summaries of the results.

Consolidation is needed of summary todos such as "Boundaries" in Cryptography/AdvancedEncryptionStandard/plans/KeyDiscovery/general.hpp; we must be able to *see* results.
 Todo:
 Solvers to be used for experimentation

We need a list of the solvers we will use for all experiments.

As time goes on, some solvers might not be used for later experiments based on earlier results, and this can be recorded here.

Solvers to be used:

ArgoSAT

OKsolver_2002

minisat2.2.0

glucose

ubcsat (120)

picosat913

precosat236

precosat570

(p)lingeling

Satz215

Grasp

sp

march_pl

Is it possible in the time constraints to run ALL of these solvers for every experiment?

Any solvers to be used which are not currently in the library, need to be added to ExternalSources (see also "Add todos for SATRace 2010 SAT
solvers" in BuildSystem/ExternalSources/SpecialBuilds/plans/SAT.hpp).

This data needs to be moved to docus.

DONE (moved to Buildsystem/ExternalSources/SpecialBuilds/plans/SAT.hpp) The following solvers (from the SAT 2010 race) are not in the library, but should be added to the library (see BuildSystem/ExternalSources/plans/SAT.hpp):

Barcelogic

borgsat

CircleSAT

CirCUs

CryptoMiniSAT

glucose

glucoER

kw

lingeling

LySAT

oprailleur

riss

rcl

SApperloT

SATPower

SATHYS
 Todo:
 DONE (individual issues moved to separate todos) Prepare experiments for the SAT 2012 paper

DONE (moved to "Move experiment data to investigationreports") A full update of the existing investigationsreports is needed.

DONE (moved to "Update experiment script") First experimentrunning script:

Using three steps: experimentcreation, experimentrunning, experimentevaluation.

An experiment is representing via a directory with a good descriptive name, where inside all information is found for reproduction and restarting.

The problems are created by computing the key by the Maxima randomnumber generator, encrypting the all0 plaintext, and then taking the problem of guessing the key from given plain and ciphertext.

The major problem here is running Maxima in parallel:

See "Improve locality" in Buildsystem/MasterScript/SpecialProcessing/plans/Call_Maxima.hpp, especially point "No interference of different invocations".

Until now it was not a major issue, however now running, say, 30 experiments in parallel won't work out without a solution.

For what is Maxima needed?

Creation of the templateSATproblems should be possible in advance.

If a key is computed, we should check whether this key is correct.

At least for the smallscale system the could be done using Sage; hopefully Sage is more amenable to scriptusage.

DONE It seems best to have first a script which takes as parameters the generalised AESparameters plus optionally a seed (default=1), so that these parameters fully specify a sequence of generalised AES problems, and then all combinations of SAT solvers and translations are executed.

DONE (moved to "Explain how to replace various AES boxes with identity
or random boxes" in /AdvancedEncryptionStandard/plans/Experimentation.hpp) Systematic variations on the various boxes:

In order to find out about the effects of boxtranslations, a good method should be to "turn off" all other boxes, i.e., making them the identity.

This could perhaps distinguish between the various occurrences of the box under consideration.

For this to be welltested, we should have reasonable possibilities to create also the corresponding cryptosystem, so that we can check encryption/decryption.

The translation system shouldn't have any variables regarding the identities created by those identityboxes.

Perhaps for version 1.0 of the Maxima module Cryptology we plan to have a fully integrated system, which from a very general specification creates the cryptosystems as well as the various SAT or CSP translations.

DONE Milestones are needed.
Definition in file Experimentation.hpp.