Investigations into smallscale AES key discovery for 5+1/3 round AES with a 2x4 plaintext matrix and 4bit field elements.
More...
Go to the source code of this file.
Detailed Description
Investigations into smallscale AES key discovery for 5+1/3 round AES with a 2x4 plaintext matrix and 4bit field elements.
 Todo:
 Problem specification

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

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

aes(5,2,4,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/2_4_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 1base box translation

Translation of aes(5,2,4,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 (it is selfinverse).

We treat Sboxes, field additions and additions as boxes.

The Sbox and field multiplications are considered as a 8x1 boolean function, translated using 1bases; see ss_sbox_rbase_cnfs in ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/data/SmallScaleSboxCNF.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 5 + 1/3 round:
num_rounds : 5$
num_rows : 2$
num_columns : 4$
exp : 4$
final_round_b : false$
box_tran : aes_rbase_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_r5_c4_rw2_e4_f0.cnf  ExtendedDimacsFullStatisticsO3DNDEBUG n
n non_taut_c red_l taut_c orig_l comment_count finished_bool
1436 6858 21604 0 21604 1437 1
length count
1 20
2 480
3 4808
4 1550

In this translation, we have:

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

50 Sboxes:

40 from SubBytes = 8 byte * 5 rounds;

10 from key schedule = 2 row * 1 word * 5 rounds.

80 multiplications by 02: 2 rows * 1 multiplication * 4 columns * 5 rounds * 2 directions (forward + inverse).

80 multiplications by 03: 2 rows * 1 multiplication * 4 columns * 5 rounds * 2 directions (forward + inverse).

652 additions:

652 additions of arity 2:

160 from key additions = 32 bits * 5 rounds;

32 from final key addition = 32 bits;

140 from the key schedule = (32 bits  4 bits) * 5 rounds.

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

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

20 additions of arity 3:

20 from the key schedule = 4 bits * 5 round.

20 bits for the constant in the key schedule = 4 bits * 5 rounds.

The number of clauses of each length in the translation, computed by:
maxima> ncl_list_fcs(ev_hm(ss_sbox_rbase_cnfs,4));
[[3,12],[4,15]]
maxima> ncl_list_fcs(ev_hm(ss_field_rbase_cnfs,[4,2]));
[[2,6],[3,4]]
maxima> ncl_list_fcs(ev_hm(ss_field_rbase_cnfs,[4,3]));
[[3,16],[4,8]]

This instance has the following number of clauses of length:

1 : 20 = key schedule constant * 1;

2 : 480 = 80 multiplications by 02 * 6;

3 : 4808 = 50 Sboxes * 12 + 80 multiplications by 02 * 4 + 80 multiplications by 03 * 16 + 652 additions (arity 2) * 4;

4 : 1550 = 50 Sboxes * 15 + 80 multiplications by 03 * 8 + 20 additions (arity 3) * 8.

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_r5_c4_rw2_e4_f0.cnf ssaes_pkpair_r5_c4_rw2_e4_f0_s1.cnf > r5_keyfind.cnf

Picosat solves it in ~15 minutes:
c 0 restarts
c 4596920 conflicts
c 4789770 decisions
c 2809104667 propagations
c 903.5 seconds total run time

All other solvers run in the experiment were unable to solve the instance within 10 hours (cryptominisat, precosat236, precosat570.1, minisat2.2.0).
Definition in file 5_13.hpp.