OKlibrary  0.2.1.6
general.hpp File Reference

Investigations into small-scale AES key discovery for AES with a 4x4 plaintext matrix and 4-bit field elements. More...

Go to the source code of this file.


Detailed Description

Investigations into small-scale AES key discovery for AES with a 4x4 plaintext matrix and 4-bit field elements.

Todo:
Problem specification
  • We consider the small-scale AES with 4 row, 4 column, using the 4-bit field size for rounds 1 to 20.
  • We denote this AES instance by aes(r,4,4,4) for r in 1,...,20.
  • We investigate translations of the key discovery problem for aes(r,4,4,4) into SAT.
  • aes(r,4,4,4) takes a 64-bit plaintext and 64-bit key and outputs a 64-bit ciphertext.
  • aes(r,4,4,4) applies the following operations:
    1. Key schedule which takes the key and generates r+1 64-bit round keys.
    2. Application of the following operation (the "round") r times:
      1. Addition of round key n-1.
      2. Application of Sbox operation to each byte.
      3. Application of the MixColumns operation.
    3. Addition of round key r+1.
    4. The result of the last round key addition is the ciphertext.
  • Round key 0 is the input key.
  • The key schedule computes the round key i from round key i-1 by:
    K_(i,1,k) := S-box(K_(i-1,2,2)) + C_i + sum(K_(i-1,1,l),l,1,4)
    K_(i,2,k) := S-box(K_(i-1,3,2)) + sum(K_(i-1,2,l),l,1,4)
    K_(i,3,k) := S-box(K_(i-1,4,2)) + sum(K_(i-1,3,l),l,1,4)
    K_(i,4,k) := S-box(K_(i-1,1,2)) + sum(K_(i-1,4,l),l,1,4)
       
    where
    • C_i is the round constant for round i;
    • K_(i,j,k) is the 4-bit word in the j-th row, k-th column of the i-th round-key considered as a 4x2 matrix.
  • The S-box is a permutation from {0,1}^4 to {0,1}^4 which we consider as either:
  • The MixColumns operation is a permutation from ({0,1}^4)^2 to ({0,1}^4)^2, which we consider to be defined as:
    MixColumns(I_1) := Mul02(I_1) + Mul03(I_2) + I_3 + I_4
    MixColumns(I_2) := I_1 + Mul02(I_2) + Mul03(I_3) + I_4
    MixColumns(I_3) := I_1 + I_2 + Mul02(I_3) + Mul03(I_4)
    MixColumns(I_4) := Mul03(I_1) + I_2 + I_3 + Mul02(I_4)
    
    MixColumns(I_5) := Mul02(I_5) + Mul03(I_6) + I_7 + I_8
    MixColumns(I_6) := I_5 + Mul02(I_6) + Mul03(I_7) + I_8
    MixColumns(I_7) := I_5 + I_6 + Mul02(I_7) + Mul03(I_8)
    MixColumns(I_8) := Mul03(I_5) + I_6 + I_7 + Mul02(I_8)
       
    where
    • I_i is the i-th 4-bit word in the input;
    • Mul02 is a permutation over {0,1}^4 representing multiplication by 02 in the Rijndael byte field;
    • Mul03 is a permutation over {0,1}^4 representing multiplication by 03 in the Rijndael byte field.
  • The inverse MixColumns operation is a permutation from ({0,1}^4)^2 to ({0,1}^4)^2, which we consider to be defined as:
    InvMixColumns(I_1) := Mul14(I_1) + Mul11(I_2) + Mul13(I_3) + Mul9(I_4)
    InvMixColumns(I_2) := Mul9(I_1) + Mul14(I_2) + Mul11(I_3) + Mul13(I_4)
    InvMixColumns(I_3) := Mul13(I_1) + Mul9(I_2) + Mul14(I_3) + Mul11(I_4)
    InvMixColumns(I_4) := Mul11(I_1) + Mul13(I_2) + Mul9(I_3) + Mul14(I_4)
    
    InvMixColumns(I_5) := Mul14(I_5) + Mul11(I_6) + Mul13(I_7) + Mul9(I_8)
    InvMixColumns(I_6) := Mul9(I_5) + Mul14(I_6) + Mul11(I_7) + Mul13(I_8)
    InvMixColumns(I_7) := Mul13(I_5) + Mul9(I_6) + Mul14(I_7) + Mul11(I_8)
    InvMixColumns(I_8) := Mul11(I_5) + Mul13(I_6) + Mul9(I_7) + Mul14(I_8)
       
    where
    • I_i is the i-th 4-bit word in the input;
    • MulX is a permutation over {0,1}^4 representing multiplication by X in the Rijndael byte field;
  • The decompositions and translations are listed in "Investigating dimensions" in Cryptography/AdvancedEncryptionStandard/plans/Experimentation.hpp.
  • The plaintext and ciphertext variables are then set, and the SAT SAT solver is run on this instance to deduce the key variables.

Definition in file general.hpp.