Investigations into smallscale AES key discovery for 1+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 1+1/3 round AES with a 2x4 plaintext matrix and 4bit field elements.
 Todo:
 Problem specification

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

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

aes(1,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 canonical box translation

Translation of aes(1,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 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 1 + 1/3 round:
num_rounds : 1$
num_rows : 2$
num_columns : 4$
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_r1_c4_rw2_e4_f0.cnf  ExtendedDimacsFullStatisticsO3DNDEBUG n
n non_taut_c red_l taut_c orig_l comment_count finished_bool
1036 6750 19476 0 19476 1037 1
length count
1 4
2 5376
3 624
4 32
9 672
16 42

In this translation, we have:

1 full round (Key Addition, SubBytes, and MixColumns operation).

10 Sboxes:

8 from SubBytes = 8 byte * 1 rounds;

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

16 multiplications by 02: 2 rows * 1 multiplication * 4 columns * 1 round * 2 directions (forward + inverse).

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

160 additions:

156 additions of arity 2:

32 from key additions = 32 bits * 1 round;

32 from final key addition = 32 bits;

28 from the key schedule = (32 bits  4 bits) * 1 round.

32 from forward MixColumns = 2 rows * 4 column * 4 bits * 1 round;

32 from inverse MixColumns = 2 rows * 4 column * 4 bits * 1 round.

4 additions of arity 3:

4 from the key schedule = 4 bits * 1 round.

4 bits for the constant in the key schedule = 4 bits * 1 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 42 boxes = 10 Sboxes + 32 multiplications.

This instance has the following number of clauses of length:

1 : 4 = key schedule constant * 1;

2 : 5376 = 42 boxes * 128;

3 : 624 = 156 additions (arity 2) * 4;

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

9 : 672 = 42 boxes * 16;

16 : 42 = 42 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_rw2_e4_f0.cnf ssaes_pkpair_r1_c4_rw2_e4_f0_s1.cnf > r1_keyfind.cnf

minisat2.2.0 solves it in 0.03s:
restarts : 11
conflicts : 1654 (55133 /sec)
decisions : 2581 (0.00 % random) (86033 /sec)
propagations : 211137 (7037900 /sec)
conflict literals : 36509 (24.97 % deleted)
Memory used : 19.00 MB
CPU time : 0.03 s

cryptominisat solves it in 0.03s:
c restarts : 3
c conflicts : 362 (12066.67 / sec)
c decisions : 581 (0.00 % random)
c CPU time : 0.03 s
??? what does "Verified 1017 clauses." mean here ???

OKsolver solves it in 0.9s:
c running_time(sec) 0.9
c number_of_nodes 103
c number_of_2reductions 3705
Definition in file 1_13.hpp.