OKlibrary  0.2.1.6
3_13.hpp File Reference

Investigations into small-scale AES key discovery for 3+1/3 round AES with a 2x4 plaintext matrix and 4-bit field elements. More...

Go to the source code of this file.

Detailed Description

Investigations into small-scale AES key discovery for 3+1/3 round AES with a 2x4 plaintext matrix and 4-bit field elements.

Todo:
Problem specification
Todo:
Using the canonical box translation
• Translation of aes(3,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 self-inverse).
• We treat S-boxes, field multiplications and additions as boxes.
• The S-box 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 bit-wise as (k+1)-bit to 1-bit boolean functions; translated using their prime implicates.
• Generating small-scale AES for 1 + 1/3 round:
```num_rounds : 3\$
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_r3_c4_rw2_e4_f0.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
n non_taut_c red_l taut_c orig_l comment_count finished_bool
2916 19994 57660 0 57660 2917 1
length count
1 12
2 16128
3 1616
4 96
9 2016
16 126
```
• In this translation, we have:
• 3 full rounds (Key Addition, SubBytes, and MixColumns operation).
• 30 Sboxes:
• 24 from SubBytes = 8 byte * 3 rounds;
• 6 from key schedule = 2 row * 1 word * 3 rounds.
• 48 multiplications by 02: 2 rows * 1 multiplication * 4 columns * 3 rounds * 2 directions (forward + inverse).
• 48 multiplications by 03: 2 rows * 1 multiplication * 4 columns * 3 rounds * 2 directions (forward + inverse).
• 404 additions of arity 2:
• 96 from key additions = 32 bits * 3 rounds;
• 32 from final key addition = 32 bits;
• 84 from the key schedule = (32 bits - 4 bits) * 3 rounds.
• 96 from forward MixColumns = 2 rows * 4 column * 4 bits * 3 rounds;
• 96 from inverse MixColumns = 2 rows * 4 column * 4 bits * 3 rounds.
• 12 additions of arity 3:
• 12 from the key schedule = 4 bits * 3 rounds.
• 12 bits for the constant in the key schedule = 4 bits * 3 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]]
```
• This instance has 126 boxes = 30 S-boxes + 96 multiplications.
• This instance has the following number of clauses of length:
• 1 : 12 = key schedule constant * 1;
• 2 : 16128 = 42 boxes * 128;
• 3 : 1616 = 404 additions (arity 2) * 4;
• 4 : 96 = 12 additions (arity 3) * 8;
• 9 : 2016 = 126 boxes * 16;
• 16 : 126 = 126 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> AppendDimacs-O3-DNDEBUG ssaes_r1_c4_rw2_e4_f0.cnf ssaes_pkpair_r1_c4_rw2_e4_f0_s1.cnf > r1_keyfind.cnf
```
• minisat-2.2.0 solves it in 65s:
```shell> minisat-2.2.0 experiment_r3_k1.cnf
restarts              : 36632
conflicts             : 26578774       (406788 /sec)
decisions             : 28721930       (0.00 % random) (439590 /sec)
propagations          : 12638199080    (193427808 /sec)
conflict literals     : 690572739      (62.54 % deleted)
Memory used           : 63.00 MB
CPU time              : 65.3381 s
```
• cryptominisat solves it in 61.4s:
```shell> cryptominisat experiment_r3_k1.cnf
<snip>
c restarts                 : 105
c conflicts                : 5370243     (87472.26  / sec)
c decisions                : 5741789     (0.26      % random)
c CPU time                 : 61.39       s
```
• glucose solves it in 65s:
```shell> glucose experiment_r3_k1.cnf
<snip>
c restarts              : 50
c nb ReduceDB           : 164
c conflicts             : 14316868       (219560 /sec)
c decisions             : 15063464       (1.57 % random) (231010 /sec)
c propagations          : 4612945014     (70743001 /sec)
c CPU time              : 65.2071 s
```
• precosat236 solves it in 1246s:
```shell> precosat236 experiment_r3_k1.cnf
<snip>
c 5597931 conflicts, 6207027 decisions, 1 random
c 0 iterations, 58 restarts, 8769 skipped
c 47 simplifications, 2 reductions
c prps: 1627135948 propagations, 1.31 megaprops
c 1246.0 seconds, 22 MB max, 635 MB recycled
```

Definition in file 3_13.hpp.