Investigations into AES key discovery for 1 round AES (1+1/3)
More...
Go to the source code of this file.
Detailed Description
Investigations into AES key discovery for 1 round AES (1+1/3)
 Todo:
 Problem specification

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

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

aes(1,4,4,8) takes a 128bit plaintext and 128bit key and outputs a 128bit ciphertext.

For the full specification of this AES instance, see "Problem specification" in Cryptography/AdvancedEncryptionStandard/plans/KeyDiscovery/128/4_4_8/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

Translation of aes(1,4,4,8):

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 multiplications and additions as boxes.

The Sbox and field multiplications are considered as a 16x1 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 AES for 1 + 1/3 round:
num_rounds : 1$
num_rows : 4$
num_columns : 4$
exp : 8$
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)$
???
Maxima encountered a Lisp error:
Memory limit reached. Please jump to an outer pointer, quit program and enlarge the
memory limits before executing the program again.
???
shell> cat ssaes_r1_c4_rw4_e8_f0.cnf  ExtendedDimacsFullStatistics n
n non_taut_c red_l taut_c orig_l comment_count finished_bool
31400 510620 1510056 0 1510056 31401 1
length count
1 8
2 475136
3 1504
4 64
5 4096
17 29696
256 116

In this translation, we have:

1 full round (Key addition, SubBytes and MixColumns).

20 Sboxes:

16 from SubBytes = 16 bytes * 1 round.

4 from key schedule = 1 column * 4 bytes * 1 round.

640 additions:

376 arity two additions:

128 from key additions = 128 bits * 1 round.

128 from final key addition = 128 bits.

120 from key schedule = (128  8) bits * 1 round.

8 arity three additions: 8 from key schedule = 8 bits * 1 round.

256 arity four additions: 256 from summation in MixColumns matrix multiplication = 4 additions * 4 columns * 16 bits * 1 round.

16 multiplications by 02: 4 rows * 1 multiplication * 4 columns 1 round.

16 multiplications by 03: 4 rows * 1 multiplication * 4 columns 1 round.

16 multiplications by 09: 4 rows * 1 multiplication * 4 columns 1 round.

16 multiplications by 11: 4 rows * 1 multiplication * 4 columns 1 round.

16 multiplications by 13: 4 rows * 1 multiplication * 4 columns 1 round.

16 multiplications by 14: 4 rows * 1 multiplication * 4 columns 1 round.

8 bits set for the constant in the key schedule.

The number of clauses of each length in the canonical box translations:
maxima> ncl_list_full_dualts(16,256);
[[2,4096],[17,256],[256,1]]

The instance has 20 Sboxes + 16 * 6 multiplications = 116 boxes (excluding additions).

The instance has the following number of clauses of the following size:

1 : 8 = key schedule constant * 1;

2 : 475136 = 116 boxes * 4096;

3 : 1504 = 376 additions (arity 2) * 4;

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

5 : 4096 = 256 additions (arity 4) * 16;

16 : 29696 = 116 boxes * 256 clauses;

256 : 116 = 116 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_r1_c4_rw4_e8_f0.cnf ssaes_pkpair_r1_c4_rw4_e8_f0_s1.cnf > ssaes_r1_c4_rw4_e8_f0_keyfind.cnf

MG is running experiments with various solvers, but all are ongoing (after a day).

The next thing to try is replacing the boxes with the r_1 bases we have.
Definition in file 1_13.hpp.