OKlibrary  0.2.1.6
general.hpp File Reference

Investigations into small-scale AES key discovery for AES with a 2x4 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 2x4 plaintext matrix and 4-bit field elements.

Todo:
Problem specification
  • We consider the small-scale AES with 2 row, 4 column, using the 4-bit field size for rounds 1 to 20.
  • We denote this AES instance by aes(r,2,4,4) for r in 1,...,20.
  • We investigate translations of the key discovery problem for aes(r,2,4,4) into SAT.
  • aes(r,2,4,4) takes a 32-bit plaintext and 32-bit key and outputs a 32-bit ciphertext.
  • aes(r,2,4,4) applies the following operations:
    1. Key schedule which takes the key and generates r+1 32-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,4)) + C_i + sum(K_(i-1,j,l),l,1,j)
    K_(i,2,k) := S-box(K_(i-1,1,4)) + sum(K_(i-1,j,l),l,1,j)
       
    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 2x2 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)
    MixColumns(I_2) := Mul03(I_1) + Mul02(I_2)
    MixColumns(I_3) := Mul02(I_3) + Mul03(I_4)
    MixColumns(I_4) := Mul03(I_3) + Mul02(I_4)
       
    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 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.