OKlibrary  0.2.1.6
Translations.hpp
Go to the documentation of this file.
00001 // Matthew Gwynne, 5.9.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 
00223 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}}]$
00224 set_hm(ss_field_cnfs,[8,2], FieldMul2CNF));
00225 /* Multiplication by 03: */
00226 maxima> FieldMul3CNF :
00227  [[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16],
00228   [{-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},
00229    {-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}]]$
00230 set_hm(ss_field_cnfs,[8,2], FieldMul3CNF));
00231 /* Sbox: */
00232 maxima> output_rijnsbox_fullcnf_stdname();
00233 shell> QuineMcCluskeySubsumptionHypergraph-n16-O3-DNDEBUG AES_Sbox_full.cnf > AES_Sbox_shg.cnf
00234 shell> cat AES_Sbox_shg.cnf | MinOnes2WeightedMaxSAT-O3-DNDEBUG > AES_Sbox_shg.wcnf
00235 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;
00236 shell> cat  AES_Sbox_full.cnf_primes | FilterDimacs AES_Sbox_s294.ass > AES_Sbox_s294.cnf
00237 maxima> SboxMinCNF : read_fcl_f("AES_Sbox_s294.cnf");
00238 maxima> set_hm(ss_sbox_cnfs,8, SboxMinCNF));
00239    \endverbatim
00240    </li>
00241    <li> The Sboxes and multiplications use the "minimum" translations,
00242    which have the following number of clauses of each length:
00243    \verbatim
00244 maxima> ncl_list_fcs(ev_hm(ss_sbox_cnfs,8));
00245 [[6,143],[7,127],[8,24]]
00246 maxima> ncl_list_fcs(ev_hm(ss_field_cnfs,[8,2]))
00247 [[2,8],[3,12]]
00248 maxima> ncl_list_fcs(ev_hm(ss_field_cnfs,[8,3]))
00249 [[3,20],[4,16]]
00250    \endverbatim
00251    </li>
00252    <li> This instance has the following number of clauses of length:
00253     <ul>
00254      <li> 1 : 8*r = key schedule constant * 1; </li>
00255      <li> 2 : 32*r = 4*r multiplications by 02 * 8; </li>
00256      <li> 3 : 352*r + 64 = 4*r multiplications by 02 * 12 + 4*r
00257      multiplications by 03 * 20 + 56*r+16 additions (arity 2) * 4; </li>
00258      <li> 4 : 64*r = 4*r multiplications by 04 * 16; </li>
00259      <li> 6 : 572*r = 4*r S-boxes * 143; </li>
00260      <li> 7 : 508*r = 4*r S-boxes * 127; </li>
00261      <li> 8 : 96*r = 4*r S-boxes * 24. </li>
00262     </ul>
00263    </li>
00264   </ul>
00265 
00266 */