Plans for the smallscale AES constraint rewrite rules.
More...
Go to the source code of this file.
Detailed Description
Plans for the smallscale AES constraint rewrite rules.
 Todo:
 Move AES box translations into separate file
 Todo:
 Update specifications
 Todo:
 Remove hardcoding of multiplication by 01 in smallscale MixColumn

In the current of the smallscale MixColumn rewrite function, if the mixcolumns matrix contains a 1 in any position, then this is hardcoded in the rewrite function to be translated to an "eq_cst" constraint, which will then be removed by the global propagation stage later.

A better way of handling this is to convert it to a multiplication constraint, and then simply have the multiplication constraint rewrite rule convert it to the "eq_cst" constraint.

At the same time, one needs to handle multiplication by 0, which doesn't occur in any current AES or smallscale MixColumns matrices but will occur in later versions.

Equalivalence constraints for trivial instances:

When an AES instance has only 1 row, then the MixColumns matrix is the identity matrix.

In this instance, the multiplication is replaced by an equalivalence constraint which results in the variables being renamed.

However, the additions that are part of the matrix computation are then arity 1 additions, i.e., equalivalence constraints, but these are not currently handled specially as equalivalenceconstraints in the system.

Therefore, when translating AES instances with 1 row, there are still some binary clauses in the translation representing equivalence of variables.

These clauses need to be removed!

There should be a simple check within the MixColumns constraint translation, which checks for "identity cases" and then rewrites the MixColumns constraint to a large equivalence constraint.

See also "Remove linear diffusion from translation" in Investigations/Cryptography/AdvancedEncryptionStandard/plans/KeyDiscovery/004/1_1_4/20_13.hpp.
 Todo:
 Rearranging linear components of Sbox and MixColumns

Due to the linearity of the Sboxes affine transform and the MixColumns operation, as well as the fact that the Shiftrows only permutes bytes, the linear/affine aspects of the Sbox can be moved out and combined with the MixColumns.

The Sbox is essentially an operation (M . (s^(1)) + Ac) where M is a bit matrix, A a bit vector and s^(1) is inversion within the byte field.

For each column [A,B,C,D] in the matrix, the MixColumns (for AES) is [M3 . A + M2 . B + C + D, A + M3 . B + M2 . C + D, A + B + M3 . C + M2 . D, M2 . A + B + C + M3 . D], where M3 and M2 are the bit matrices representing multiplication by 03 (x^2+1) and 02 (x) in the byte field respectively.

We therefore have two additional possibilities other than the default AES translation:

The Sboxes affine constant addition becomes a separate operation giving:

Sbox: M . s^(1)

MixColumns is the same as standard.

Affine constant operation: + [M3 . Ac + M2 . Ac + Ac + Ac, ..., M3 . Ac + M2 . Ac + Ac + Ac] performed after MixColumns and AddRoundKey.

The Sboxes affine constant addition becomes a separate operation and the linear matrix multiplication joins with the MixColumn:

Sbox: s^(1)

MixColumns: Each column becomes:
[(M. M3) . A + (M . M2) . B + M . C + M . D,
M . A + (M . M3) . B + (M . M2) . C + M . D,
M . A + M . B + (M . M3) . C + (M . M2) . D,
(M . M2) . A + M . B + M . C + (M . M3) . D]

Affine constant operation (same as without moving the linear matrix) : + [M3 . Ac + M2 . Ac + Ac + Ac, ..., M3 . Ac + M2 . Ac + Ac + Ac] performed after MixColumns and AddRoundKey (all values are just constants).

Such rearrangements mean there need to be several additional functions written:

Each of the new boxes need minimum representations and generation functions, including (see SboxAnalysis.mac, FieldOperationsAnalysis.mac):

The combination of linear maps (i.e. M . M3, M . M2 etc for AES and small scale, including the multiplications for the inverse mixcolumns).

The inverse map (i.e. s^(1)).

The inverse map with the linear matrix multiplication (i.e. M . s^(1)).

Additional rewrite functions for the AES round which includes the affine constant addition as a separate constraint.

Rewrite functions for the constraint denoting the affine constant addition.
 Bug:
 DONE (Tests weren't updated when a new smaller Sbox was found) Test failure with okltest_ss_sbox_pi_cst_cl

okltest_ss_sbox_pi_cst_cl(ss_sbox_pi_cst_cl)
ASSERT: Expression " {10,9,7,6,5,3,4} = {16,15,14,13,4,11,12} " does not evaluate to true.
Definition in file ConstraintTemplateSmallScaleRewriteRules.hpp.