OKlibrary  0.2.1.6
10_13.hpp File Reference

Investigations into small-scale AES key discovery with 1 row, 1 column and 4-bit field elements for 10 rounds AES with MixColumns. More...

Go to the source code of this file.


Detailed Description

Investigations into small-scale AES key discovery with 1 row, 1 column and 4-bit field elements for 10 rounds AES with MixColumns.

Todo:
Overview
Todo:
Using the canonical translation
  • Translation of aes(10,1,1,4):
  • Generating simplest small-scale AES for 10 rounds:
    num_rounds : 10$
    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_r10_c1_rw1_e4_f0.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
     n non_taut_c red_l taut_c orig_l comment_count finished_bool
    572 3436 9688 0 9688 573 1
     length count
    1 40
    2 2720
    3 336
    9 320
    16 20
       
  • In this translation, we have:
    • 10 full rounds (Key Addition, SubBytes, and MixColumns operation).
    • 20 Sboxes:
      • 10 from SubBytes = 1 byte * 10 rounds;
      • 10 from key schedule = 1 row * 1 byte * 10 rounds.
    • 164 additions:
      • 80 additions of arity 1:
        • 40 from forward MixColumns = 4 bits * 10 rounds;
        • 40 from inverse MixColumns = 4 bits * 10 rounds.
      • 84 additions of arity 2:
        • 40 from key additions = 4 bits * 10 rounds;
        • 4 from final key addition = 4 bits;
        • 40 from the key schedule = 4 bits * 10 rounds.
    • 40 bits for the constant in the key schedule = 4 bits * 10 rounds.
  • The additions are translated by their prime implicates, containing 2^a clauses where a is the arity of the addition constraint.
  • Sbox canonical-translation statistics:
    > 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 : 40 = key schedule constant * 1;
    • 2 : 2720 = 20 S-boxes * 128 + 80 "additions" (arity 1) * 2;
    • 3 : 336 = 84 additions (arity 2) * 4;
    • 9 : 320 = 20 S-boxes * 16;
    • 16 : 20 = 20 S-boxes * 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> AppendDimacs-O3-DNDEBUG ssaes_r10_c1_rw1_e4_f0.cnf ssaes_pkpair_r10_c1_rw1_e4_f0_s1.cnf > r10_keyfind.cnf
       
  • OKsolver solves this with no decisions:
    shell> OKsolver_2002-O3-DNDEBUG r10_keyfind.cnf
    c running_time(sec)                     0.0
    c number_of_nodes                       1
    c number_of_2-reductions                148
    c number_of_autarkies                   1
       
  • However, minisat-2.2.0 and glucose need to branch:
    shell> minisat-2.2.0 r10_keyfind.cnf
    <snip>
    restarts              : 1
    conflicts             : 22             (inf /sec)
    decisions             : 41             (0.00 % random) (inf /sec)
    propagations          : 6095           (inf /sec)
    CPU time              : 0 s
    
    shell> minisat2 r10_keyfind.cnf
    <snip>
    restarts              : 1
    conflicts             : 29             (1450 /sec)
    decisions             : 67             (0.00 % random) (3350 /sec)
    propagations          : 5397           (269850 /sec)
    CPU time              : 0.02 s
    shell> glucose r10_keyfind.cnf
    c restarts              : 1
    c conflicts             : 48             (inf /sec)
    c decisions             : 168            (2.38 % random) (inf /sec)
    c propagations          : 5738           (inf /sec)
    c CPU time              : 0 s
       
  • We can check we get the right result with:
    shell> OKsolver_2002-O3-DNDEBUG -O r10_keyfind.cnf | grep "^v" | $OKlib/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/validate_aes_assignment 10 1 1 4 0 && echo "VALID"
    VALID
       

Definition in file 10_13.hpp.