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 4x2 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 4x2 plaintext matrix and 4-bit field elements.

Todo:
Problem specification
Todo:
Using the canonical box translation
• Translation of aes(1,4,2,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.
• 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 : 4\$
num_columns : 2\$
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_c2_rw4_e4_f0.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
n non_taut_c red_l taut_c orig_l comment_count finished_bool
1396 10128 31316 0 31316 1397 1
length count
1 4
2 7680
3 368
4 32
5 1024
9 960
16 60
```
• In this translation, we have:
• 1 full round (Key Addition, SubBytes, and MixColumns operation).
• 12 S-boxes:
• 8 from SubBytes = 8 byte * 1 rounds;
• 4 from key schedule = 4 row * 1 word * 1 rounds.
• 8 multiplications by 02 = 4 rows * 1 multiplication * 2 columns * 1 round * 1 direction (forward).
• 8 multiplications by 03 = 4 rows * 1 multiplication * 2 columns * 1 round * 1 directions (forward).
• 8 multiplications by 09 = 4 rows * 1 multiplication * 2 columns * 1 round * 1 directions (inverse).
• 8 multiplications by 11 = 4 rows * 1 multiplication * 2 columns * 1 round * 1 directions (inverse).
• 8 multiplications by 13 = 4 rows * 1 multiplication * 2 columns * 1 round * 1 directions (inverse).
• 8 multiplications by 14 = 4 rows * 1 multiplication * 2 columns * 1 round * 1 directions (inverse).
• 92 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.
• 4 additions of arity 3:
• 4 from the key schedule = 4 bits * 1 rounds.
• 64 additions of arity 4:
• 32 from forward MixColumns = 4 rows * 2 column * 4 bits * 1 rounds;
• 32 from inverse MixColumns = 4 rows * 2 column * 4 bits * 1 rounds.
• 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]]
```
• This instance has 60 boxes = 12 S-boxes + 48 multiplications.
• This instance has the following number of clauses of length:
• 1 : 4 = key schedule constant * 1;
• 2 : 7680 = 60 boxes * 128;
• 3 : 368 = 92 additions (arity 2) * 4;
• 4 : 32 = 4 additions (arity 3) * 8;
• 5 : 1024 = 64 additions (arity 4) * 16;
• 9 : 960 = 60 boxes * 16;
• 16 : 60 = 60 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_c2_rw4_e4_f0.cnf ssaes_pkpair_r1_c2_rw4_e4_f0_s1.cnf > r1_keyfind.cnf
```
• OKsolver_2002:
```shell> OKsolver_2002-O3-DNDEBUG r1_keyfind.cnf
c running_time(sec)                     42.8
c number_of_nodes                       2915
c number_of_2-reductions                25478
```
• minisat-2.2.0 and glucose:
```shell> minisat-2.2.0 r1_keyfind.cnf
restarts              : 126
conflicts             : 38174          (11967 /sec)
decisions             : 41318          (0.00 % random) (12952 /sec)
propagations          : 15523483       (4866296 /sec)
CPU time              : 3.19 s

shell> minisat2 r1_keyfind.cnf
<snip>
restarts              : 14
conflicts             : 43604          (1401 /sec)
decisions             : 47364          (1.34 % random) (1522 /sec)
propagations          : 17037471       (547477 /sec)
CPU time              : 31.12 s
shell> glucose r1_keyfind.cnf
<snip>
c restarts              : 8
c conflicts             : 16554          (13035 /sec)
c decisions             : 21834          (1.56 % random) (17192 /sec)
c propagations          : 3407020        (2682693 /sec)
c CPU time              : 1.27 s
```
• We can check we get the right result with:
```shell> OKsolver_2002-O3-DNDEBUG -O r1_keyfind.cnf | grep "^v" | \$OKlib/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/validate_aes_assignment 1 2 4 4 0 && echo "VALID"
VALID
```

Definition in file 1_13.hpp.