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

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

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

aes(1,4,4,4) takes a 64bit plaintext and 64bit key and outputs a 64bit 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,4,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 round:
num_rounds : 1$
num_rows : 4$
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_rw4_e4_f0.cnf  ExtendedDimacsFullStatisticsO3DNDEBUG n
n non_taut_c red_l taut_c orig_l comment_count finished_bool
2708 19656 60884 0 60884 2709 1
length count
1 4
2 14848
3 752
4 32
5 2048
9 1856
16 116

In this translation, we have:

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

20 Sboxes:

16 from SubBytes = 16 byte * 1 rounds;

4 from key schedule = 1 row * 1 byte * 1 rounds.

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

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

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

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

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

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

1088 additions:

188 additions of arity 2:

64 from key additions = 64 bits * 1 round;

64 from final key addition = 64 bits;

60 from the key schedule = (64 bits  4 bits) * 1 round.

4 additions of arity 3:

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

128 additions of arity 4:

64 from forward MixColumns = 4 rows * 4 columns * 4 bits * 1 round;

64 from inverse MixColumns = 4 rows * 4 columns * 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 translation, computed by:
maxima> ncl_list_full_dualts(8,16);
[[2,128],[9,16],[16,1]]

There are 116 boxes = 20 Sboxes + 96 multiplications.

This instance has the following number of clauses of length:

1 : 4 = key schedule constant * 1;

2 : 14848 = 116 boxes * 128;

3 : 752 = 188 additions (arity 2) * 4;

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

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

9 : 1856 = 116 boxes * 16;

16 : 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_e4_f0.cnf ssaes_pkpair_r1_c4_rw4_e4_f0_s1.cnf > experiment_r1_k1.cnf
??? This todo is obviously too long  the solvers etc. must go into another todo ???

minisat2.2.0 takes only 20s:
restarts : 435
conflicts : 159689 (7684 /sec)
decisions : 191056 (0.00 % random) (9193 /sec)
propagations : 80837387 (3889809 /sec)
conflict literals : 7597323 (51.64 % deleted)
Memory used : 18.00 MB
CPU time : 20.7818 s
This has been verified by hand.

Other solvers such as cryptominisat take longer (but still only a few minutes):
shell> cryptominisat experiment_r1_k1.cnf
c restarts : 569
c conflicts : 22042524 (350318.21 / sec)
c decisions : 24091000 (0.14 % random)
c CPU time : 62.92 s

precosat236 takes a very long time (comparatively):
shell> precosat236 experiment_r1_k1.cnf
c 12017467 conflicts, 13372168 decisions, 1 random
c 0 iterations, 2 restarts, 17488 skipped
c 95 simplifications, 10 reductions
c prps: 3155560431 propagations, 0.70 megaprops
c 4505.6 seconds, 56 MB max, 1732 MB recycled

glucose takes over 3 hours:
shell> time glucose experiment_r1_k1.cnf
c restarts : 566
c conflicts : 12127207 (1021 /sec)
c decisions : 12923545 (1.40 % random) (1088 /sec)
c propagations : 5248749924 (441984 /sec)
c CPU time : 11875.4 s
real 198m9.532s
user 197m55.440s
sys 0m1.020s

DONE (reran experiment; see above) glucose (apparently) solves this in a fraction of a second:
shell> glucose experiment_r1_k1.cnf
c restarts : 566
c conflicts : 12127207 (92588235 /sec)
c decisions : 12923545 (1.40 % random) (98668079 /sec)
c propagations : 5248749924 (40072911315 /sec)
c CPU time : 0.13098 s
however, rerunning glucose does not yield the same behaviour, and there are a very large number of restarts in just 0.13s. Does glucose have a bug in its timing code? Perhaps there is a bug in the experiment run script? ??? where are 2 rounds etc.? where is the general plansfile ???
Definition in file 1_13.hpp.