Investigations into smallscale AES key discovery with 1 row, 1 column and 4bit field elements for 1 round AES (1+1/3)
More...
Go to the source code of this file.
Detailed Description
Investigations into smallscale AES key discovery with 1 row, 1 column and 4bit field elements for 1 round AES (1+1/3)
 Todo:
 Overview

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

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

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

For the full specification of this AES instance, see "Problem specification" in Cryptography/AdvancedEncryptionStandard/plans/KeyDiscovery/004/1_1_4/general.hpp.

For a full list of the possible translations, see "Investigating dimensions" in Cryptography/AdvancedEncryptionStandard/plans/Experimentation.hpp.

In this file we consider:

"Using the canonical box translation".
 Todo:
 Using the canonical box translation

Translation of aes(1,1,1,4):

Generating simplest smallscale AES for 1 round
num_rounds : 1$
num_rows : 1$
num_columns : 1$
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_c1_rw1_e4_f0.cnf  ExtendedDimacsFullStatisticsO3DNDEBUG n
n non_taut_c red_l taut_c orig_l comment_count finished_bool
68 358 1012 0 1012 69 1
length count
1 4
2 272
3 48
9 32
16 2

In this translation, we have:

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

2 Sboxes:

1 from SubBytes = 1 byte * 1 round;

1 from key schedule = 1 row * 1 byte * 1 round.

20 additions:

8 additions of arity 1:

4 from forward MixColumns = 4 bits * 1 round;

4 from inverse MixColumns = 4 bits * 1 rounds.

12 additions of arity 2:

4 from key additions = 4 bits * 1 round;

4 from final key addition = 4 bits;

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

4 bits for the constant in the key schedule.

The additions are translated by their prime implicates, containing 2^a clauses where a is the arity of the addition constraint.

The Sbox is translated by the canonicaltranslation:
> ncl_list_fcl(dualts_fcl(ss_sbox_fulldnf_fcl(2,4,ss_polynomial_2_4)));
[[2,128],[9,16],[16,1]]

This instance has the following number of clauses of length:

1 : 4 = key schedule constant * 1;

2 : 272 = 2 Sboxes * 128 + 8 "additions" (arity 1) * 2;

3 : 48 = 12 additions (arity 2) * 4;

9 : 32 = 2 Sboxes * 16;

16 : 2 = 2 Sboxes * 1.

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_c1_rw1_e4_f0.cnf ssaes_pcpair_r1_c1_rw1_e4_f0_s1.cnf > r1_keyfind.cnf

OKsolver solves this with no decisions:
shell> OKsolver_2002O3DNDEBUG r1_keyfind.cnf
c running_time(sec) 0.0
c number_of_nodes 1
c number_of_2reductions 19
c number_of_autarkies 1
c file_name r1_keyfind.cnf

However, minisat2.2.0 and glucose need to branch:
shell> minisat2.2.0 r1_keyfind.cnf
<snip>
restarts : 1
conflicts : 7 (inf /sec)
decisions : 14 (0.00 % random) (inf /sec)
propagations : 198 (inf /sec)
CPU time : 0 s
shell> minisat2 r1_keyfind.cnf
<snip>
restarts : 1
conflicts : 13 (inf /sec)
decisions : 21 (0.00 % random) (inf /sec)
propagations : 286 (inf /sec)
CPU time : 0 s
shell> glucose r1_keyfind.cnf
<snip>
c restarts : 1
c conflicts : 12 (inf /sec)
c decisions : 32 (0.00 % random) (inf /sec)
c propagations : 215 (inf /sec)
c CPU time : 0 s

It seems OKsolver is propagating purely by r_2. Perhaps the OKsolver is able to take advantage of the r_1basedness of the canonical translation due to its use of r_2 reductions?

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