Investigations into smallscale AES key discovery for 2 + 1/3 round AES with a 4x2 plaintext matrix and 4bit field elements.
More...
Investigations into smallscale AES key discovery for 2 + 1/3 round AES with a 4x2 plaintext matrix and 4bit field elements.
 Todo:
 Problem specification

We investigate the 2 + 1/3 round smallscale AES with 4 row, 2 column, using the 4bit field size.

We denote this AES instance by aes(2,4,2,4).

aes(2,4,2,4) takes a 32bit plaintext and 32bit key and outputs a 32bit ciphertext.

For the full specification of this AES instance, see "Problem specification" in Cryptography/AdvancedEncryptionStandard/plans/KeyDiscovery/032/4_2_4/general.hpp.

Note that we consider the canonical CNF translation, as this is an example of the "hardest" representation without new variables. See "Hardness of boolean function representations" in Experimentation/Investigations/BooleanFunctions/plans/general.hpp.
 Todo:
 Using the canonical box translation <u>l Translation of aes(2,4,2,4):

The MixColumns operation is decomposed into its field multiplications (02 and 03) and addition operations.

The MixColumns operation is translated by translating both the MixColumns operation and its inverse.

We treat Sboxes, field multiplications and additions as boxes.

The Sbox and field multiplications are considered as a 8x1 boolean functions, translated using the canonical translation; see dualts_fcl in ComputerAlgebra/Satisfiability/Lisp/FiniteFunctions/TseitinTranslation.mac.

Additions of arity k are considered bitwise as (k+1)bit to 1bit boolean functions; translated using their prime implicates.
Generating smallscale AES for 2 + 1/3 round:
num_rounds : 2$
num_rows : 4$
num_columns : 2$
exp : 4$
final_round_b : false$
box_tran : aes_ts_box$
seed : 1$
mc_tran : aes_mc_bidirectional$
output_ss_fcl_std(num_rounds, num_columns, num_rows, exp, final_round_b, box_tran, mc_tran)$
shell> cat ssaes_r2_c2_rw4_e4_f0.cnf  ExtendedDimacsFullStatisticsO3DNDEBUG n
n non_taut_c red_l taut_c orig_l comment_count finished_bool
2696 20128 62248 0 62248 2697 1
length count
1 8
2 15360
3 608
4 64
5 2048
9 1920
16 120
In this translation, we have:

Two full rounds (Key Addition, SubBytes, and MixColumns operation).

24 Sboxes:

16 from SubBytes = 8 byte * 2 rounds;

8 from key schedule = 4 row * 1 word * 2 rounds.

16 multiplications by 02 = 4 rows * 1 multiplication * 2 columns * 2 round * 1 direction (forward).

16 multiplications by 03 = 4 rows * 1 multiplication * 2 columns * 2 round * 1 directions (forward).

16 multiplications by 09 = 4 rows * 1 multiplication * 2 columns * 2 round * 1 directions (inverse).

16 multiplications by 11 = 4 rows * 1 multiplication * 2 columns * 2 round * 1 directions (inverse).

16 multiplications by 13 = 4 rows * 1 multiplication * 2 columns * 2 round * 1 directions (inverse).

16 multiplications by 14 = 4 rows * 1 multiplication * 2 columns * 2 round * 1 directions (inverse).

288 additions:

152 additions of arity 2:

64 from key additions = 32 bits * 2 round;

32 from final key addition = 32 bits;

56 from the key schedule = (32 bits  4 bits) * 2 round.

8 additions of arity 3:

8 from the key schedule = 4 bits * 2 rounds.

128 additions of arity 4:

64 from forward MixColumns = 4 rows * 2 column * 4 bits * 2 rounds;

64 from inverse MixColumns = 4 rows * 2 column * 4 bits * 2 rounds.

8 bits for the constant in the key schedule = 4 bits * 2 rounds.
The number of clauses of each length in the canonical translation:
maxima> ncl_list_full_dualts(8,16);
[[2,128],[9,16],[16,1]]
This instance has 120 boxes = 24 Sboxes + 96 multiplications. This instance has the following number of clauses of length:

1 : 8 = key schedule constant * 1;

2 : 15360 = 120 boxes * 128;

3 : 608 = 152 additions (arity 2) * 4;

4 : 64 = 8 additions (arity 3) * 8;

5 : 2048 = 128 additions (arity 4) * 16;

9 : 1920 = 120 boxes * 16;

16 : 120 = 120 boxes * 1.
Then we can generate a random assignment with the plaintext and ciphertext, leaving the key unknown:
maxima> output_ss_random_pc_pair(seed,num_rounds,num_columns,num_rows,exp,final_round_b);
and the merging the assignment with the translation:
shell> AppendDimacsO3DNDEBUG ssaes_r2_c2_rw4_e4_f0.cnf ssaes_pkpair_r2_c2_rw4_e4_f0_s1.cnf > r2_keyfind.cnf
minisat2.2.0 solves it in just over 45 minutes:
shell> minisat2.2.0 r2_keyfind.cnf
<snip>
restarts : 32761
conflicts : 21348407 (7855 /sec)
decisions : 23781237 (0.00 % random) (8751 /sec)
propagations : 9574903606 (3523177 /sec)
CPU time : 2717.69 s
Definition in file 2_13.hpp.