OKlibrary  0.2.1.6
10_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 
00219 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}}]$
00220 set_hm(ss_field_cnfs,[8,2], FieldMul2CNF));
00221 /* Multiplication by 03: */
00222 maxima> FieldMul3CNF :
00223  [[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16],
00224   [{-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},
00225    {-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}]]$
00226 set_hm(ss_field_cnfs,[8,2], FieldMul3CNF));
00227 /* Sbox: */
00228 maxima> output_rijnsbox_fullcnf_stdname();
00229 shell> QuineMcCluskeySubsumptionHypergraph-n16-O3-DNDEBUG AES_Sbox_full.cnf > AES_Sbox_shg.cnf
00230 shell> cat AES_Sbox_shg.cnf | MinOnes2WeightedMaxSAT-O3-DNDEBUG > AES_Sbox_shg.wcnf
00231 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;
00232 shell> cat  AES_Sbox_full.cnf_primes | FilterDimacs AES_Sbox_s294.ass > AES_Sbox_s294.cnf
00233 maxima> SboxMinCNF : read_fcl_f("AES_Sbox_s294.cnf");
00234 maxima> set_hm(ss_sbox_cnfs,8, SboxMinCNF));
00235    \endverbatim
00236    </li>
00237    <li> Generating small scale AES for 10 + 1/3 rounds:
00238    \verbatim
00239 rounds : 10$
00240 num_rows : 2$
00241 num_columns : 1$
00242 exp : 8$
00243 final_round_b : false$
00244 box_tran : aes_small_box$
00245 seed : 1$
00246 mc_tran : aes_mc_bidirectional$
00247 output_ss_fcl_std(rounds, num_columns, num_rows, exp, final_round_b, box_tran, mc_tran)$
00248 
00249 shell> cat ssaes_r10_c1_rw2_e8_f0.cnf | ExtendedDimacsFullStatistics-O3-DNDEBUG n
00250  n non_taut_c red_l taut_c orig_l comment_count finished_bool
00251 1488 16384 91592 0 91592 1489 1
00252  length count
00253 1 80
00254 2 320
00255 3 3584
00256 4 640
00257 6 5720
00258 7 5080
00259 8 960
00260    \endverbatim
00261    </li>
00262    <li> In this translation, we have:
00263     <ul>
00264      <li> 10 full rounds (Key Addition, SubBytes, and MixColumns operation).
00265      </li>
00266      <li> 40 Sboxes:
00267       <ul>
00268        <li> 20 from SubBytes = 2 byte * 10 rounds; </li>
00269        <li> 20 from key schedule = 2 row * 1 byte * 10 rounds. </li>
00270       </ul>
00271      </li>
00272      <li> 40 multiplications by 02: 2 rows * 1 multiplication * 1 columns *
00273      10 round * 2 directions (forward + inverse). </li>
00274      <li> 40 multiplications by 03: 2 rows * 1 multiplication * 1 columns *
00275      10 round * 2 directions (forward + inverse). </li>
00276      <li> 576 additions of arity 2:
00277       <ul>
00278        <li> 160 from key additions = 16 bits * 10 round; </li>
00279        <li> 16 from final key addition = 16 bits; </li>
00280        <li> 80 from the key schedule = 1 rows * 8 bits * 10 round. </li>
00281        <li> 160 from forward MixColumns = 2 rows * 1 column * 8 bits *
00282        10 rounds; </li>
00283        <li> 160 from inverse MixColumns = 2 rows * 1 column * 8 bits * 10
00284        rounds. </li>
00285       </ul>
00286      </li>
00287      <li> 80 bits for the constant in the key schedule = 8 bits * 10 rounds.
00288      </li>
00289     </ul>
00290    </li>
00291    <li> Note that as this variant has only one column, the key schedule
00292    applies Sbox(K_i) + C rather than Sbox(K_i) + K_j + C where K_i and
00293    K_j are key words from the previous round key. </li>
00294    <li> The Sboxes and multiplications use the "minimum" translations,
00295    which have the following number of clauses of each length:
00296    \verbatim
00297 maxima> ncl_list_fcs(ev_hm(ss_sbox_cnfs,8));
00298 [[6,143],[7,127],[8,24]]
00299 maxima> ncl_list_fcs(ev_hm(ss_field_cnfs,[8,2]))
00300 [[2,8],[3,12]]
00301 maxima> ncl_list_fcs(ev_hm(ss_field_cnfs,[8,3]))
00302 [[3,20],[4,16]]
00303    \endverbatim
00304    </li>
00305    <li> This instance has the following number of clauses of length:
00306     <ul>
00307      <li> 1 : 80 = key schedule constant * 1; </li>
00308      <li> 2 : 320 = 40 multiplications by 02 * 8; </li>
00309      <li> 3 : 3584 = 40 multiplications by 02 * 12 + 40 multiplications by 03
00310      * 20 + 576 additions (arity 2) * 4; </li>
00311      <li> 4 : 640 = 40 multiplications by 04 * 16; </li>
00312      <li> 6 : 5720 = 40 S-boxes * 143; </li>
00313      <li> 7 : 5080 = 40 S-boxes * 127; </li>
00314      <li> 8 : 960 = 40 S-boxes * 24. </li>
00315     </ul>
00316    </li>
00317    <li> Generate random assignments for the plaintext and ciphertext, leaving
00318    the key unknown:
00319    \verbatim
00320 maxima> output_ss_random_pc_pair(seed,rounds,num_columns,num_rows,exp,final_round_b);
00321    \endverbatim
00322    Merge the assignments with the translations:
00323    \verbatim
00324 shell> AppendDimacs-O3-DNDEBUG ssaes_r10_c1_rw2_e4_f0.cnf ssaes_pkpair_r10_c1_rw2_e4_f0_s1.cnf > r10_keyfind.cnf; done
00325    \endverbatim
00326    </li>
00327    <li> Solver runs:
00328     <ul>
00329      <li> glucose:
00330      \verbatim
00331 shell> glucose r10_keyfind.cnf
00332 <snip>
00333 c restarts              : 400
00334 c conflicts             : 1442056        (2328 /sec)
00335 c decisions             : 1739229        (1.71 % random) (2808 /sec)
00336 c propagations          : 98283796       (158678 /sec)
00337 c CPU time              : 619.39 s
00338      \endverbatim
00339      </li>
00340      <li> cryptominisat:
00341      \verbatim
00342 shell> cryptominisat r10_keyfind.cnf
00343 c num threads              : 1
00344 c restarts                 : 8796
00345 c conflicts                : 1804584     (1843.24   / sec)
00346 c decisions                : 3052078     (1.15      % random)
00347 c bogo-props               : 79603311024 (81308347.06 / sec)
00348 c CPU time                 : 979.03      s
00349      \endverbatim
00350      </li>
00351      <li> precosat236
00352      \verbatim
00353 shell> precosat236 r10_keyfind.cnf
00354 c 8665518 conflicts, 9957497 decisions, 2 random
00355 c 0 iterations, 4 restarts, 14174 skipped
00356 c prps: 689660107 propagations, 0.12 megaprops
00357 c 5974.9 seconds, 66 MB max, 933 MB recycled
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 r10_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 */