OKlibrary  0.2.1.6
ConstraintTemplateSmallScaleRewriteRules.hpp File Reference

Plans for the small-scale AES constraint rewrite rules. More...

Go to the source code of this file.


Detailed Description

Plans for the small-scale AES constraint rewrite rules.

Todo:
Move AES box translations into separate file
Todo:
Update specifications
Todo:
Remove hard-coding of multiplication by 01 in small-scale MixColumn
  • In the current of the small-scale MixColumn rewrite function, if the mixcolumns matrix contains a 1 in any position, then this is hard-coded 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 small-scale 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 equalivalence-constraints 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:
    1. The Sboxes affine constant addition becomes a separate operation giving:
      1. Sbox: M . s^(-1)
      2. MixColumns is the same as standard.
      3. Affine constant operation: + [M3 . Ac + M2 . Ac + Ac + Ac, ..., M3 . Ac + M2 . Ac + Ac + Ac] performed after MixColumns and AddRoundKey.
    2. The Sboxes affine constant addition becomes a separate operation and the linear matrix multiplication joins with the MixColumn:
      1. Sbox: s^(-1)
      2. 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]
             
      3. 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 S-box 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.