OKlibrary  0.2.1.6
14_13.hpp
Go to the documentation of this file.
00001 // Matthew Gwynne, 21.5.2011 (Swansea)
00002 /* Copyright 2011 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library; either version 3 of the
00006 License, or any later version. */
00007 
00229 maxima> FieldMul2CNF : [{1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16},{{-9,2},{-2,9},{-10,3},{-3,10},{-11,4},{-4,11},{-12,-5,-1},{-12,1,5},{-5,1,12},{-1,5,12},{-13,-6,-1},{-1,6,13},{-14,7},{-7,14},{-15,1,8},{-8,1,15},{-16,-15,-8},{-16,8,15},{-13,6,16},{-6,13,16}}]$
00230 set_hm(ss_field_cnfs,[8,2], FieldMul2CNF));
00231 /* Multiplication by 03: */
00232 maxima> FieldMul3CNF :
00233  [[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16],
00234   [{-9,-2,-1},{-2,1,9},{-10,2,3},{-10,-9,-3,1},{-10,-3,-1,9},{-3,2,10},{-9,1,3,10},{-1,3,9,10},{-11,-4,-3},{-11,3,4},{-4,3,11},{-3,4,11},{-12,-5,-4,1},{-12,-4,-1,5},{-5,1,4,12},{-1,4,5,12},{-13,-5,-1,6},{-13,1,5,6},{-13,-12,-6,4},{-13,-6,-4,12},{-6,-5,-1,13},{-6,1,5,13},
00235    {-12,4,6,13},{-4,6,12,13},{-14,-7,-6},{-14,6,7},{-7,6,14},{-6,7,14},{-16,-8,-1},{-16,1,8},{-16,-15,-7},{-16,7,15},{-8,1,16},{-1,8,16},{-15,7,16},{-7,15,16}]]$
00236 set_hm(ss_field_cnfs,[8,2], FieldMul3CNF));
00237 /* Sbox: */
00238 maxima> output_rijnsbox_fullcnf_stdname();
00239 shell> QuineMcCluskeySubsumptionHypergraph-n16-O3-DNDEBUG AES_Sbox_full.cnf > AES_Sbox_shg.cnf
00240 shell> cat AES_Sbox_shg.cnf | MinOnes2WeightedMaxSAT-O3-DNDEBUG > AES_Sbox_shg.wcnf
00241 shell> ubcsat-okl  -alg gsat -w -runs 100 -cutoff 40000000 -wtarget 294 -solve 1 -seed 3213901809 -i AES_Sbox_shg.wcnf -r model AES_Sbox_s294.ass;
00242 shell> cat  AES_Sbox_full.cnf_primes | FilterDimacs AES_Sbox_s294.ass > AES_Sbox_s294.cnf
00243 maxima> SboxMinCNF : read_fcl_f("AES_Sbox_s294.cnf");
00244 maxima> set_hm(ss_sbox_cnfs,8, SboxMinCNF));
00245    \endverbatim
00246    </li>
00247    <li> Generating small scale AES for 14 + 1/3 rounds:
00248    \verbatim
00249 rounds : 14$
00250 num_rows : 2$
00251 num_columns : 1$
00252 exp : 8$
00253 final_round_b : false$
00254 box_tran : aes_small_box$
00255 seed : 1$
00256 mc_tran : aes_mc_bidirectional$
00257 output_ss_fcl_std(rounds, num_columns, num_rows, exp, final_round_b, box_tran, mc_tran)$
00258 
00259 shell> cat ssaes_r14_c1_rw2_e8_f0.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
00260  n non_taut_c red_l taut_c orig_l comment_count finished_bool
00261 2064 22912 128152 0 128152 2065 1
00262  length count
00263 1 112
00264 2 448
00265 3 4992
00266 4 896
00267 6 8008
00268 7 7112
00269 8 1344
00270    \endverbatim
00271    </li>
00272    <li> In this translation, we have:
00273     <ul>
00274      <li> 14 full rounds (Key Addition, SubBytes, and MixColumns
00275      operation). </li>
00276      <li> 56 Sboxes:
00277       <ul>
00278        <li> 28 from SubBytes = 2 byte * 14 rounds; </li>
00279        <li> 28 from key schedule = 2 row * 1 byte * 14 rounds. </li>
00280       </ul>
00281      </li>
00282      <li> 56 multiplications by 02: 2 rows * 1 multiplication * 1 columns *
00283      14 rounds * 2 directions (forward + inverse). </li>
00284      <li> 56 multiplications by 03: 2 rows * 1 multiplication * 1 columns *
00285      14 rounds * 2 directions (forward + inverse). </li>
00286      <li> 800 additions of arity 2:
00287       <ul>
00288        <li> 224 from key additions = 16 bits * 14 rounds; </li>
00289        <li> 16 from final key addition = 16 bits; </li>
00290        <li> 112 from the key schedule = 1 rows * 8 bits * 14 rounds. </li>
00291        <li> 224 from forward MixColumns = 2 rows * 1 column * 8 bits *
00292        14 rounds; </li>
00293        <li> 224 from inverse MixColumns = 2 rows * 1 column * 8 bits * 14
00294        rounds. </li>
00295       </ul>
00296      </li>
00297      <li> 112 bits for the constant in the key schedule = 8 bits * 14 rounds.
00298      </li>
00299     </ul>
00300    </li>
00301    <li> Note that as this variant has only one column, the key schedule
00302    applies Sbox(K_i) + C rather than Sbox(K_i) + K_j + C where K_i and
00303    K_j are key words from the previous round key. </li>
00304    <li> The Sboxes and multiplications use the "minimum" translations,
00305    which have the following number of clauses of each length:
00306    \verbatim
00307 maxima> ncl_list_fcs(ev_hm(ss_sbox_cnfs,8));
00308 [[6,143],[7,127],[8,24]]
00309 maxima> ncl_list_fcs(ev_hm(ss_field_cnfs,[8,2]))
00310 [[2,8],[3,12]]
00311 maxima> ncl_list_fcs(ev_hm(ss_field_cnfs,[8,3]))
00312 [[3,20],[4,16]]
00313    \endverbatim
00314    </li>
00315    <li> This instance has the following number of clauses of length:
00316     <ul>
00317      <li> 1 : 112 = key schedule constant * 1; </li>
00318      <li> 2 : 448 = 56 multiplications by 02 * 8; </li>
00319      <li> 3 : 4992 = 56 multiplications by 02 * 12 + 56 multiplications by 03
00320      * 20 + 800 additions (arity 2) * 4; </li>
00321      <li> 4 : 896 = 56 multiplications by 04 * 16; </li>
00322      <li> 6 : 8008 = 56 S-boxes * 143; </li>
00323      <li> 7 : 7112 = 56 S-boxes * 127; </li>
00324      <li> 8 : 1344 = 56 S-boxes * 24. </li>
00325     </ul>
00326    </li>
00327    <li> Generate random assignments for the plaintext and ciphertext, leaving
00328    the key unknown:
00329    \verbatim
00330 maxima> output_ss_random_pc_pair(seed,rounds,num_columns,num_rows,exp,final_round_b);
00331    \endverbatim
00332    Merge the assignments with the translations:
00333    \verbatim
00334 shell> AppendDimacs-O3-DNDEBUG ssaes_r14_c1_rw2_e4_f0.cnf ssaes_pkpair_r14_c1_rw2_e4_f0_s1.cnf > r14_keyfind.cnf; done
00335    \endverbatim
00336    </li>
00337    <li> Solver runs:
00338     <ul>
00339      <li> cryptominisat:
00340      \verbatim
00341 shell> cryptominisat r14_keyfind.cnf
00342 <snip>
00343 c restarts                 : 9433
00344 c conflicts                : 2030565     (4696.47   / sec)
00345 c decisions                : 4350327     (1.04      % random)
00346 c CPU time                 : 432.36      s
00347      \endverbatim
00348      </li>
00349      <li> glucose:
00350      \verbatim
00351 shell> glucose r14_keyfind.cnf
00352 <snip>
00353 c restarts              : 918
00354 c conflicts             : 2226769        (2807 /sec)
00355 c decisions             : 2781657        (1.75 % random) (3507 /sec)
00356 c propagations          : 136974745      (172675 /sec)
00357 c CPU time              : 793.25 s
00358      \endverbatim
00359      </li>
00360     </ul>
00361    </li>
00362    <li> We can check we get the right result with:
00363    \verbatim
00364 shell> OKsolver_2002-O3-DNDEBUG -O r14_keyfind.cnf | grep "^v" | $OKlib/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/validate_aes_assignment 1 1 2 8 0 && echo "VALID"
00365 VALID
00366    \endverbatim
00367    </li>
00368   </ul>
00369 
00370 */