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

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

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

aes(4,2,2,4) takes a 16bit plaintext and 16bit key and outputs a 16bit ciphertext.

For the full specification of this AES instance, see "Problem specification" in Cryptography/AdvancedEncryptionStandard/plans/KeyDiscovery/016/2_2_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(4,2,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 (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 4 + 1/3 rounds:
rounds : 4$
num_rows : 2$
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(rounds, num_columns, num_rows, exp, final_round_b, box_tran, mc_tran)$
shell> cat ssaes_r4_c2_rw2_e4_f0.cnf  ExtendedDimacsFullStatisticsO3DNDEBUG n
n non_taut_c red_l taut_c orig_l comment_count finished_bool
2016 13928 40208 0 40208 2017 1
length count
1 16
2 11264
3 1024
4 128
9 1408
16 88

In this translation, we have:

4 full rounds (Key Addition, SubBytes, and MixColumns operation).

24 Sboxes:

16 from SubBytes = 4 byte * 4 rounds;

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

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

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

144 additions:

256 additions of arity 2:

64 from key additions = 16 bits * 4 rounds;

16 from final key addition = 16 bits;

48 from the key schedule = (16 bits  4 bits) * 4 rounds.

64 from forward MixColumns = 2 rows * 2 column * 4 bits * 4 rounds;

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

16 additions of arity 3:

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

16 bits for the constant in the key schedule = 4 bits * 4 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 instances has 88 boxes = 24 Sboxes + 64 multiplications.

This instance has the following number of clauses of length:

1 : 16 = key schedule constant * 1;

2 : 11264 = 88 boxes * 128;

3 : 1024 = 256 additions (arity 2) * 4;

4 : 128 = 16 additions (arity 3) * 8;

9 : 1408 = 88 boxes * 16;

16 : 88 = 88 boxes * 1.

Then we can generate random assignments with the plaintext and ciphertext, leaving the key unknown:
maxima> output_ss_random_pc_pair(seed,rounds,num_columns,num_rows,exp,final_round_b);
and the merging the assignments with the translations: shell> AppendDimacsO3DNDEBUG ssaes_r4_c2_rw2_e4_f0.cnf ssaes_pkpair_r4_c2_rw2_e4_f0_s1.cnf > r4_keyfind.cnf

OKsolver solves this with very few decisions:
shell> OKsolver_2002O3DNDEBUG r4_keyfind.cnf
s SATISFIABLE
c sat_status 1
c initial_maximal_clause_length 16
c initial_number_of_variables 2016
c initial_number_of_clauses 13960
c initial_number_of_literal_occurrences 40240
c number_of_initial_uniteliminations 48
c reddiff_maximal_clause_length 0
c reddiff_number_of_variables 48
c reddiff_number_of_clauses 176
c reddiff_number_of_literal_occurrences 624
c number_of_2clauses_after_reduction 11328
c running_time(sec) 20.9
c number_of_nodes 1246
c number_of_single_nodes 0
c number_of_quasi_single_nodes 0
c number_of_2reductions 44291
c number_of_pure_literals 0
c number_of_autarkies 0
c number_of_missed_single_nodes 0
c max_tree_depth 17
c number_of_table_enlargements 0
c number_of_1autarkies 0
c number_of_new_2clauses 0
c maximal_number_of_added_2clauses 0
c file_name r4_keyfind.cnf

However, minisat2 and glucose need to branch a lot more:
shell> minisat2 r4_keyfind.cnf
<snip>
Verified 13576 original clauses.
Verified 976 eliminated clauses.
restarts : 12
conflicts : 18318 (1104 /sec)
decisions : 20892 (1.78 % random) (1259 /sec)
propagations : 14693302 (885672 /sec)
conflict literals : 514079 (63.22 % deleted)
Memory used : 18.46 MB
CPU time : 16.59 s
shell> minisat2.2.0 r4_keyfind.cnf
<snip>
restarts : 127
conflicts : 40470 (7125 /sec)
decisions : 45214 (0.00 % random) (7960 /sec)
propagations : 36303086 (6391388 /sec)
conflict literals : 1250043 (71.04 % deleted)
Memory used : 20.00 MB
CPU time : 5.68 s
shell> glucose r4_keyfind.cnf
<snip>
c restarts : 2
c nb ReduceDB : 1
c nb learnts DL2 : 55
c nb learnts size 2 : 1
c nb learnts size 1 : 0
c conflicts : 6731 (8742 /sec)
c decisions : 7756 (1.77 % random) (10073 /sec)
c propagations : 2519893 (3272588 /sec)
c conflict literals : 286835 (44.78 % deleted)
c Memory used : 3.98 MB
c CPU time : 0.77 s

The number of decision nodes used by the OKsolver has jumped drastically here! What has changed?

Also note that minisat2.2.0 does a lot better here than minisat2.

We can check we get the right result with:
shell> OKsolver_2002O3DNDEBUG O r4_keyfind.cnf  grep "^v"  $OKlib/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/validate_aes_assignment 4 2 2 4 0 && echo "VALID"
VALID
Definition in file 4_13.hpp.