OKlibrary  0.2.1.6
SmallScaleFieldMulCNF.mac
Go to the documentation of this file.
00001 /* Matthew Gwynne, 16.12.2010 (Swansea) */
00002 /* Copyright 2010, 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 
00022 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/FieldOperationsAnalysis.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/data/FieldMul2CNF.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/data/FieldMul3CNF.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/data/FieldMul9CNF.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/data/FieldMul11CNF.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/data/FieldMul13CNF.mac")$
00028 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/data/FieldMul14CNF.mac")$
00029 
00030 
00031 /*********************************************************
00032  * Smallest known number of clauses                      *
00033  *********************************************************
00034 */
00035 
00036 /* Generated using
00037 
00038    $OKlib/Experimentation/Investigations/Cryptography/AdvancedEncryptionStandard/minimise_cnf_cryptominisat
00039 
00040    applied to output_ssmult_fullcnf_stdname(e,2,4,ss_polynomial_2_4) for each
00041    e in {2,...,15}. */
00042 
00043 /* Takes the exponent and the element in the field to multiply with */
00044 ss_field_cnfs : sm2hm({})$
00045 
00046 set_hm(ss_field_cnfs, [4,2],
00047   [[1,2,3,4,5,6,7,8],[{-5,2},{-2,5},{-6,3},{-3,6},{-7,-4,-1},{-1,4,7},{-8,1},
00048   {-7,4,8},{-4,7,8}]])$
00049 set_hm(ss_field_cnfs, [4,3],
00050   [[1,2,3,4,5,6,7,8],[{-5,1,2},{-1,2,5},{-6,-3,-2},{-6,-5,-1,3},{-6,1,3,5},
00051   {-2,3,6},{-5,-3,-1,6},{-3,1,5,6},{-8,-4,-1},{-8,1,4},{-8,-7,-3},{-8,3,7},
00052   {-4,1,8},{-1,4,8},{-7,3,8},{-3,7,8}]])$
00053 set_hm(ss_field_cnfs, [4,4],
00054   [[1,2,3,4,5,6,7,8],[{-5,3},{-3,5},{-6,-4,-1},{-6,1,4},{-4,1,6},{-1,4,6},
00055   {-7,-2,-1},{-2,1,7},{-8,2},{-7,1,8},{-1,7,8}]])$
00056 set_hm(ss_field_cnfs, [4,5],
00057   [[1,2,3,4,5,6,7,8],[{5,-3,-1},{-5,1,3},{-6,-4,-1,2},{-6,-2,-1,4},{-4,1,2,6},
00058   {-2,1,4,6},{-7,-3,-2,1},{-7,-2,-1,3},{-7,2,5},{-3,1,2,7},{-1,2,3,7},
00059   {-2,5,7},{-8,-4,-2},{-8,2,4},{-6,1,8},{-1,6,8}]])$
00060 set_hm(ss_field_cnfs, [4,6],
00061   [[1,2,3,4,5,6,7,8],[{-5,2,3},{-3,2,5},{-6,-4,-1,3},{-3,1,4,6},{-7,3,4,5},
00062   {-7,-5,-1,6},{-5,-4,-3,7},{-6,1,5,7},{-8,-2,-1},{-8,-6,-5,4},{-8,-7,-4,1},
00063   {-8,3,6,7},{-2,1,8},{-4,5,6,8},{-7,-6,-3,8},{-1,4,7,8}]])$
00064 set_hm(ss_field_cnfs, [4,7],
00065   [[1,2,3,4,5,6,7,8],[{-5,-3,-1,2},{-2,1,3,5},{-7,2,3,4},{-7,-4,-1,5},
00066   {-7,1,6},{-4,-3,-2,7},{-5,1,4,7},{-1,6,7},{-8,-2,-1,4},{-8,-5,-4,3},
00067   {-8,-6,-3},{-8,2,5,7},{-4,1,2,8},{-3,4,5,8},{-6,3,8},{-7,-5,-2,8}]])$
00068 set_hm(ss_field_cnfs, [4,8],
00069   [[1,2,3,4,5,6,7,8],[{-5,-4,-1},{-1,4,5},{-6,1,2},{-6,-5,-2,4},{-6,-4,-2,5},
00070   {-2,1,6},{-5,2,4,6},{-4,2,5,6},{-7,-3,-2},{-3,2,7},{-8,3},
00071   {-7,2,8},{-2,7,8}]])$
00072 set_hm(ss_field_cnfs, [4,9],
00073   [[1,2,3,4,5,6,7,8],[{-4,5},{-6,1},{-1,6},{-7,2},{-2,7},{-8,3,4},{-8,-5,-3},
00074   {-3,4,8},{-5,3,8}]])$
00075 set_hm(ss_field_cnfs, [4,10],
00076   [[1,2,3,4,5,6,7,8],[{-6,-3,-2,1},{-6,-2,-1,3},{-3,1,2,6},{-1,2,3,6},
00077   {-7,-5,-3},{-7,3,5},{-7,-6,-4},{-7,4,6},{-5,3,7},{-3,5,7},{-6,4,7},{-4,6,7},
00078   {-8,-3,-1},{-8,1,3},{-6,2,8},{-2,6,8}]])$
00079 set_hm(ss_field_cnfs, [4,11],
00080   [[1,2,3,4,5,6,7,8],[{-4,2,5},{-2,4,5},{-6,-3,-1},{-6,1,3},{-3,1,6},{-1,3,6},
00081   {-7,-4,-2,1},{-7,1,2,4},{-7,-5,-1},{-4,-2,-1,7},{-1,2,4,7},{-5,1,7},
00082   {-8,-6,-4},{-8,4,6},{-6,4,8},{-4,6,8}]])$
00083 set_hm(ss_field_cnfs, [4,12],
00084   [[1,2,3,4,5,6,7,8],[{-5,-3,-1,4},{-5,1,3,4},{-4,-3,-1,5},{-4,1,3,5},
00085   {-6,-4,-2},{-6,2,4},{-4,2,6},{-2,4,6},{-7,-5,-4},{-7,4,5},{-3,1,7},{-1,3,7},
00086   {-8,-3,-2},{-8,2,3},{-3,2,8},{-2,3,8}]])$
00087 set_hm(ss_field_cnfs, [4,13],
00088   [[1,2,3,4,5,6,7,8],[{-5,3,4},{-3,4,5},{-6,-5,-3},{-6,3,5},{-4,6},{-7,1},
00089   {-1,7},{-8,-5,-2},{-8,2,5},{-5,2,8},{-2,5,8}]])$
00090 set_hm(ss_field_cnfs, [4,14],
00091   [[1,2,3,4,5,6,7,8],[{-5,1,6},{-1,5,6},{-7,-4,-3},{-7,3,4},{-7,-5,-1,2},
00092   {-7,1,2,5},{-7,-6,-2},{-4,3,7},{-3,4,7},{-5,-2,-1,7},{-2,1,5,7},{-6,2,7},
00093   {-8,-5,-4},{-8,4,5},{-5,4,8},{-4,5,8}]])$
00094 set_hm(ss_field_cnfs, [4,15],
00095   [[1,2,3,4,5,6,7,8],[{-6,3,4},{-6,-5,-2},{-3,4,6},{-5,2,6},{-7,-6,-3},
00096   {-7,3,6},{-4,7},{-8,1,5},{-8,-6,-1,2},{-8,-2,-1,6},{-1,5,8},{-6,1,2,8},
00097   {-2,1,6,8}]])$
00098 set_hm(ss_field_cnfs, [8,2], FieldMul2CNF)$
00099 set_hm(ss_field_cnfs, [8,3], FieldMul3CNF)$
00100 set_hm(ss_field_cnfs, [8,9], FieldMul9CNF)$
00101 set_hm(ss_field_cnfs, [8,11], FieldMul11CNF)$
00102 set_hm(ss_field_cnfs, [8,13], FieldMul13CNF)$
00103 set_hm(ss_field_cnfs, [8,14], FieldMul14CNF)$
00104 /* ... */
00105 
00106 
00107 /*********************************************************
00108  * r_1-bases with smallest known number of clauses       *
00109  *********************************************************
00110 */
00111 
00112 ss_field_rbase_cnfs : sm2hm({})$
00113 
00114 /* For each field element small scale exponent e and field element a, the
00115    following CNFs have been generated by the following commands:
00116 
00117 maxima> e : 4$ a : 2$
00118 maxima> output_ssmult_fullcnf_stdname(a,2,e,ss_polynomial(2,e));
00119 shell>  e=4; a=2
00120 shell>  QuineMcCluskey-n8-O3-DNDEBUG ss_byte2_${e}_field_mul_full_${a}.cnf > primes_${e}_${a}.cnf
00121 shell>  cat primes_${e}_${a}.cnf | SortByClauseLength-O3-DNDEBUG > primes_${e}_${a}_sorted.cnf
00122 shell>  RUcpGen-O3-DNDEBUG primes_${e}_${a}_sorted.cnf | RUcpBase-O3-DNDEBUG > mul_${e}_${a}_base.cnf
00123 
00124 These are the smallest known r_1 bases, but it is not known if they are the
00125 the minimum size.
00126 
00127 */
00128 set_hm(ss_field_rbase_cnfs, [4,2], [[1,2,3,4,5,6,7,8],
00129   [{-5,2},{-2,5},{-6,3},{-3,6},{-8,1},{-1,8},{-7,-4,-1},{-7,1,4},{-4,1,7},
00130   {-1,4,7}]])$
00131 set_hm(ss_field_rbase_cnfs, [4,3], [[1,2,3,4,5,6,7,8],
00132   [{-5,-2,-1},{-5,1,2},{-2,1,5},{-1,2,5},{-6,-3,-2},{-6,2,3},{-3,2,6},
00133    {-2,3,6},{-8,-4,-1},{-8,1,4},{-8,-7,-3},{-8,3,7},{-4,1,8},{-1,4,8},
00134    {-7,3,8},{-3,7,8},{-7,-6,-5,4},{-7,-6,-4,5},{-7,-5,-4,6},{-7,4,5,6},
00135    {-6,-5,-4,7},{-6,4,5,7},{-5,4,6,7},{-4,5,6,7}]])$
00136 set_hm(ss_field_rbase_cnfs, [4,4], [[1,2,3,4,5,6,7,8],
00137   [{-5,3},{-3,5},{-8,2},{-2,8},{-6,-4,-1},{-6,1,4},{-4,1,6},{-1,4,6},
00138    {-7,-2,-1},{-7,1,2},{-2,1,7},{-1,2,7}]])$
00139 set_hm(ss_field_rbase_cnfs, [4,5], [[1,2,3,4,5,6,7,8],
00140   [{-5,-3,-1},{-5,1,3},{-3,1,5},{-1,3,5},{-7,-5,-2},{-7,2,5},{-5,2,7},
00141    {-2,5,7},{-8,-4,-2},{-8,2,4},{-8,-6,-1},{-8,1,6},{-4,2,8},{-2,4,8},
00142    {-6,1,8},{-1,6,8},{-7,-6,-4,3},{-7,-6,-3,4},{-7,-4,-3,6},{-7,3,4,6},
00143    {-6,-4,-3,7},{-6,3,4,7},{-4,3,6,7},{-3,4,6,7}]])$
00144 set_hm(ss_field_rbase_cnfs, [4,6], [[1,2,3,4,5,6,7,8],
00145   [{-5,-3,-2},{-5,2,3},{-3,2,5},{-2,3,5},{-7,-4,-2},{-7,2,4},{-4,2,7},
00146    {-2,4,7},{-8,-2,-1},{-8,1,2},{-2,1,8},{-1,2,8},{-6,-4,-3,1},{-6,-4,-1,3},
00147    {-6,-3,-1,4},{-6,1,3,4},{-4,-3,-1,6},{-4,1,3,6},{-3,1,4,6},{-1,3,4,6},
00148    {-7,-6,-5,1},{-7,-6,-1,5},{-7,-5,-1,6},{-7,1,5,6},{-6,-5,-1,7},{-6,1,5,7},
00149    {-5,1,6,7},{-1,5,6,7},{-8,-6,-5,4},{-8,-6,-4,5},{-8,-5,-4,6},{-8,4,5,6},
00150    {-8,-7,-6,3},{-8,-7,-3,6},{-8,-6,-3,7},{-8,3,6,7},{-6,-5,-4,8},{-6,4,5,8},
00151    {-5,4,6,8},{-4,5,6,8},{-7,-6,-3,8},{-7,3,6,8},{-6,3,7,8},{-3,6,7,8}]])$
00152 set_hm(ss_field_rbase_cnfs, [4,7], [[1,2,3,4,5,6,7,8],
00153   [{-6,-5,-4},{-6,4,5},{-5,4,6},{-4,5,6},{-7,-6,-1},{-7,1,6},{-6,1,7},
00154    {-1,6,7},{-8,-6,-3},{-8,3,6},{-6,3,8},{-3,6,8},{-5,-3,-2,1},{-5,-3,-1,2},
00155    {-5,-2,-1,3},{-5,1,2,3},{-3,-2,-1,5},{-3,1,2,5},{-2,1,3,5},{-1,2,3,5},
00156    {-7,-4,-3,2},{-7,-4,-2,3},{-7,-3,-2,4},{-7,2,3,4},{-4,-3,-2,7},{-4,2,3,7},
00157    {-3,2,4,7},{-2,3,4,7},{-8,-4,-2,1},{-8,-4,-1,2},{-8,-2,-1,4},{-8,1,2,4},
00158    {-8,-7,-5,2},{-8,-7,-2,5},{-8,-5,-2,7},{-8,2,5,7},{-4,-2,-1,8},{-4,1,2,8},
00159    {-2,1,4,8},{-1,2,4,8},{-7,-5,-2,8},{-7,2,5,8},{-5,2,7,8},{-2,5,7,8}]])$
00160 set_hm(ss_field_rbase_cnfs, [4,8], [[1,2,3,4,5,6,7,8],
00161   [{-8,3},{-3,8},{-5,-4,-1},{-5,1,4},{-4,1,5},{-1,4,5},{-6,-2,-1},{-6,1,2},
00162   {-2,1,6},{-1,2,6},{-7,-3,-2},{-7,2,3},{-3,2,7},{-2,3,7}]])$
00163 set_hm(ss_field_rbase_cnfs, [4,9], [[1,2,3,4,5,6,7,8],
00164   [{-5,4},{-4,5},{-6,1},{-1,6},{-7,2},{-2,7},{-8,-4,-3},{-8,3,4},{-4,3,8},
00165    {-3,4,8}]])$
00166 set_hm(ss_field_rbase_cnfs, [4,10], [[1,2,3,4,5,6,7,8],
00167   [{-7,-5,-3},{-7,3,5},{-7,-6,-4},{-7,4,6},{-5,3,7},{-3,5,7},{-6,4,7},
00168    {-4,6,7},{-8,-3,-1},{-8,1,3},{-8,-6,-2},{-8,2,6},{-3,1,8},{-1,3,8},
00169    {-6,2,8},{-2,6,8},{-5,-4,-2,1},{-5,-4,-1,2},{-5,-2,-1,4},{-5,1,2,4},
00170    {-4,-2,-1,5},{-4,1,2,5},{-2,1,4,5},{-1,2,4,5}]])$
00171 set_hm(ss_field_rbase_cnfs, [4,11], [[1,2,3,4,5,6,7,8],
00172   [{-5,-4,-2},{-5,2,4},{-4,2,5},{-2,4,5},{-6,-3,-1},{-6,1,3},{-3,1,6},
00173    {-1,3,6},{-7,-5,-1},{-7,1,5},{-5,1,7},{-1,5,7},{-8,-6,-4},{-8,4,6},
00174    {-6,4,8},{-4,6,8},{-8,-7,-3,2},{-8,-7,-2,3},{-8,-3,-2,7},{-8,2,3,7},
00175    {-7,-3,-2,8},{-7,2,3,8},{-3,2,7,8},{-2,3,7,8}]])$
00176 set_hm(ss_field_rbase_cnfs, [4,12], [[1,2,3,4,5,6,7,8],
00177   [{-6,-4,-2},{-6,2,4},{-4,2,6},{-2,4,6},{-7,-3,-1},{-7,1,3},{-7,-5,-4},
00178    {-7,4,5},{-3,1,7},{-1,3,7},{-5,4,7},{-4,5,7},{-8,-3,-2},{-8,2,3},{-3,2,8},
00179    {-2,3,8},{-8,-6,-5,1},{-8,-6,-1,5},{-8,-5,-1,6},{-8,1,5,6},{-6,-5,-1,8},
00180    {-6,1,5,8},{-5,1,6,8},{-1,5,6,8}]])$
00181 set_hm(ss_field_rbase_cnfs, [4,13], [[1,2,3,4,5,6,7,8],
00182   [{-6,4},{-4,6},{-7,1},{-1,7},{-5,-4,-3},{-5,3,4},{-4,3,5},{-3,4,5},
00183    {-8,-5,-2},{-8,2,5},{-5,2,8},{-2,5,8}]])$
00184 set_hm(ss_field_rbase_cnfs, [4,14], [[1,2,3,4,5,6,7,8],
00185   [{-6,-5,-1},{-6,1,5},{-5,1,6},{-1,5,6},{-7,-4,-3},{-7,3,4},{-7,-6,-2},
00186    {-7,2,6},{-4,3,7},{-3,4,7},{-6,2,7},{-2,6,7},{-8,-5,-4},{-8,4,5},{-5,4,8},
00187    {-4,5,8},{-8,-3,-2,1},{-8,-3,-1,2},{-8,-2,-1,3},{-8,1,2,3},{-3,-2,-1,8},
00188    {-3,1,2,8},{-2,1,3,8},{-1,2,3,8}]])$
00189 set_hm(ss_field_rbase_cnfs, [4,15], [[1,2,3,4,5,6,7,8],
00190   [{-7,4},{-4,7},{-6,-4,-3},{-6,3,4},{-6,-5,-2},{-6,2,5},{-4,3,6},{-3,4,6},
00191   {-5,2,6},{-2,5,6},{-8,-5,-1},{-8,1,5},{-5,1,8},{-1,5,8}]])$
00192 set_hm(ss_field_rbase_cnfs, [8,2],
00193   [[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16],
00194   [{-9,2},{-2,9},{-10,3},{-3,10},{-11,4},{-4,11},{-14,7},{-7,14},{-16,1},
00195   {-1,16},{-12,-5,-1},{-12,1,5},{-5,1,12},{-1,5,12},{-13,-6,-1},{-13,1,6},
00196   {-6,1,13},{-1,6,13},{-15,-8,-1},{-15,1,8},{-8,1,15},{-1,8,15}]])$
00197 set_hm(ss_field_rbase_cnfs, [8,3], [[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16],
00198   [{-9,-2,-1},{-9,1,2},{-2,1,9},{-1,2,9},{-10,-3,-2},{-10,2,3},{-3,2,10},
00199   {-2,3,10},{-11,-4,-3},{-11,3,4},{-4,3,11},{-3,4,11},{-14,-7,-6},{-14,6,7},
00200   {-7,6,14},{-6,7,14},{-16,-8,-1},{-16,1,8},{-16,-15,-7},{-16,7,15},{-8,1,16},
00201   {-1,8,16},{-15,7,16},{-7,15,16},{-12,-5,-4,1},{-12,-5,-1,4},{-12,-4,-1,5},
00202   {-12,1,4,5},{-5,-4,-1,12},{-5,1,4,12},{-4,1,5,12},{-1,4,5,12},{-13,-6,-5,1},
00203   {-13,-6,-1,5},{-13,-5,-1,6},{-13,1,5,6},{-13,-12,-6,4},{-13,-12,-4,6},
00204   {-13,-6,-4,12},{-13,4,6,12},{-6,-5,-1,13},{-6,1,5,13},{-5,1,6,13},
00205   {-1,5,6,13},{-12,-6,-4,13},{-12,4,6,13},{-6,4,12,13},{-4,6,12,13},
00206   {-12,-11,-10,-9,-5},{-12,-11,-10,5,9},{-12,-11,-9,5,10},{-12,-11,-5,9,10},
00207   {-12,-10,-9,5,11},{-12,-10,-5,9,11},{-12,-9,-5,10,11},{-12,5,9,10,11},
00208   {-11,-10,-9,5,12},{-11,-10,-5,9,12},{-11,-9,-5,10,12},{-11,5,9,10,12},
00209   {-10,-9,-5,11,12},{-10,5,9,11,12},{-9,5,10,11,12},{-5,9,10,11,12},
00210   {-15,-14,-13,-8,-5},{-15,-14,-13,5,8},{-15,-14,-8,5,13},{-15,-14,-5,8,13},
00211   {-15,-13,-8,5,14},{-15,-13,-5,8,14},{-15,-8,-5,13,14},{-15,5,8,13,14},
00212   {-14,-13,-8,5,15},{-14,-13,-5,8,15},{-14,-8,-5,13,15},{-14,5,8,13,15},
00213   {-13,-8,-5,14,15},{-13,5,8,14,15},{-8,5,13,14,15},{-5,8,13,14,15}]])$
00214 
00215 
00216