general.hpp File Reference

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.

Considering output bits on their own
  • For better comparison with the DES-paper (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).
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 byte-field multiplications.
    • Sbox linear component (M) and Standard byte-field 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.
Scripts for generating statistics on random boxes
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.
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 1-8.
      • 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 1-8.
      • 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 .
k-based representations
  • We consider k-bases 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.
    1. Can one formulate (relatively efficiently) the minimisation target that these inferences are "easily" available while otherwise using the smallest representation?
    2. We could generalise the notion of r-base 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 sub-module.
  • We need to bring together here all information on currently known on 1-bases 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.
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 boolean-function 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
        sconcat("The squared AES Sbox in full CNF representation."),
       <li> Prime clauses:
    > QuineMcCluskey-n16-O3-DNDEBUG AES_Sbox2_full.cnf > AES_PK2.cnf
    > cat AES_PK2.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG
     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.
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 clause-set, 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 clause-set 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 clause-set 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 clause-set (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.