OKlibrary  0.2.1.6
1_13.hpp File Reference

Investigations into small-scale AES key discovery for 1+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 1+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(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 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 : 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 | ExtendedDimacsFullStatistics-O3-DNDEBUG 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).
• 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 S-boxes + 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> 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 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_2-reductions                3705
```

Definition in file 1_13.hpp.