OKlibrary  0.2.1.6
Experimentation.hpp File Reference

AES experiments related to the SAT 2012 paper. More...

Go to the source code of this file.


Detailed Description

AES experiments related to the SAT 2012 paper.

We consider experiments investigating the AES and small-scale 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 (small-scale 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):
      1. Final round is the same as every other (in line with small-scale).
      2. Final round doesn't include the MixColumns operation.
    • Box replacements (3 options):
      1. Original Sbox, field multiplication etc. are used.
      2. Random permutations are used.
      3. The identity is used.
      4. 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 8-bits of the input.
        • MixColumn operation applied to each column. This operation is a matrix multiplication applied to the vector of 8-bit words in the column.
      • Key schedule, which has:
        • The Sbox applied to each 8-bit word in the first column of the previous round key.
        • Additions of the Sbox result, a round constant and certain 8-bit 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):
        1. Sbox linear map is left in the Sbox.
        2. Sbox linear map is moved through the ShiftRows operation. It is then combined with the MixColumn multiplication components.
      • Sbox affine constant (2 options):
        1. Sbox affine constant addition remains in Sbox.
        2. 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):
        1. Translation of the MixColumn component using both the encryption and decryption components.
        2. Translation using only the encryption direction.
        3. Translation using only the decryption direction.
      • Function decomposition (3 options):
        1. Multiplication function decomposition (default):
          • Representing the MixColumns using individual multiplication functions as well as addition constraints.
        2. Bit-matrix representation:
          • Representing the MixColumns as a bit-matrix multiplication.
          • Representing the multiplication of each row in the bit matrix using addition constraints.
        3. Whole function representation:
          • Taking the MixColumn as a single boolean function.
    • Key schedule decomposition (2 option):
      • Shared sub-expression 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_(i-1) + K_p''. K_(i-1) is the previous column of the new round key. K_pi is i-th 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 i-th 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):
      1. Canonical translation.
      2. Canonical+ translation.
      3. 0-based representation.
      4. 1-based representation.
      5. 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 key-schedule and block-cipher" in AdvancedEncryptionStandard/plans/general.hpp; this aspects needs better explanations.
  • For more information, see Cryptology/Lisp/Cryptanalysis/Rijndael/plans/Translations.hpp.
Todo:
Open problems
Todo:
Update experiment script
  • First experiment-running script:
    1. Using three steps: experiment-creation, experiment-running, experiment-evaluation.
    2. An experiment is representing via a directory with a good descriptive name, where inside all information is found for reproduction and restarting.
    3. The problems are created by computing the key by the Maxima random-number generator, encrypting the all-0 plaintext, and then taking the problem of guessing the key from given plain- and ciphertext.
    4. The major problem here is running Maxima in parallel:
      1. See "Improve locality" in Buildsystem/MasterScript/SpecialProcessing/plans/Call_Maxima.hpp, especially point "No interference of different invocations".
      2. Until now it was not a major issue, however now running, say, 30 experiments in parallel won't work out without a solution.
      3. For what is Maxima needed?
        1. Creation of the template-SAT-problems should be possible in advance.
        2. If a key is computed, we should check whether this key is correct.
        3. At least for the small-scale system the could be done using Sage; hopefully Sage is more amenable to script-usage.
    5. DONE It seems best to have first a script which takes as parameters the generalised AES-parameters 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 plaintext-ciphertext-pairs 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 plaintext-ciphertext-pairs.
    • 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 per-solver scripts:
      • We need a "run_aes_experiment_oksolver", "run_aes_experiment_minisat-2.2.0" and so on.
      • Each solver-specific 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 plaintext-ciphertext-pairs to run the experiment on.
      • The script should then create the AES key discovery instances from the AES instances and plaintext-ciphertext-pairs.
      • 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 plaintext-ciphertext-pair 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 investigation-reports
  • 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
    • minisat-2.2.0
    • glucose
    • ubcsat (1-2-0)
    • 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 SAT-Race 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
    • borg-sat
    • CircleSAT
    • CirCUs
    • CryptoMiniSAT
    • glucose
    • glucoER
    • kw
    • lingeling
    • LySAT
    • oprailleur
    • riss
    • rcl
    • SApperloT
    • SAT-Power
    • SATHYS
Todo:
DONE (individual issues moved to separate todos) Prepare experiments for the SAT 2012 paper
  • DONE (moved to "Move experiment data to investigation-reports") A full update of the existing investigations-reports is needed.
  • DONE (moved to "Update experiment script") First experiment-running script:
    1. Using three steps: experiment-creation, experiment-running, experiment-evaluation.
    2. An experiment is representing via a directory with a good descriptive name, where inside all information is found for reproduction and restarting.
    3. The problems are created by computing the key by the Maxima random-number generator, encrypting the all-0 plaintext, and then taking the problem of guessing the key from given plain- and ciphertext.
    4. The major problem here is running Maxima in parallel:
      1. See "Improve locality" in Buildsystem/MasterScript/SpecialProcessing/plans/Call_Maxima.hpp, especially point "No interference of different invocations".
      2. Until now it was not a major issue, however now running, say, 30 experiments in parallel won't work out without a solution.
      3. For what is Maxima needed?
        1. Creation of the template-SAT-problems should be possible in advance.
        2. If a key is computed, we should check whether this key is correct.
        3. At least for the small-scale system the could be done using Sage; hopefully Sage is more amenable to script-usage.
    5. DONE It seems best to have first a script which takes as parameters the generalised AES-parameters 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:
    1. In order to find out about the effects of box-translations, a good method should be to "turn off" all other boxes, i.e., making them the identity.
    2. This could perhaps distinguish between the various occurrences of the box under consideration.
    3. For this to be well-tested, we should have reasonable possibilities to create also the corresponding crypto-system, so that we can check encryption/decryption.
    4. The translation system shouldn't have any variables regarding the identities created by those identity-boxes.
    5. 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.