OKlibrary  0.2.1.6
SmallScaleSboxCNF.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/SboxAnalysis.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/data/SboxCNF.mac")$
00024 
00025 
00026 /*********************************************************
00027  * Smallest known number of clauses                      *
00028  *********************************************************
00029 */
00030 
00031 /* Takes the exponent and the element in the field to multiply with */
00032 ss_sbox_cnfs : sm2hm({})$
00033 
00034 set_hm(ss_sbox_cnfs, 4, [[1,2,3,4,5,6,7,8],
00035   [{-4,-3,-2,5},{-6,-5,-3,-2},{-6,-1,5},{-6,-2,3,5},{-7,-3,1,2},{-7,-5,3,4},
00036    {-7,-6,-4,2},{-7,-4,-2,3,6},{-5,1,7},{-5,-3,4,7},{-8,-2,1,3},{-8,-4,-3},
00037    {-8,-5,-2},{-8,2,3,5},{-8,-6,3,4},{-8,-3,6},{-8,-5,-4,-1,6},{-8,-2,4,7},
00038    {-3,1,4,8},{2,6,8},{-7,-1,8},{3,7,8}]])$
00039 
00040 /* Generated by
00041 
00042 maxima> output_rijnsbox_fullcnf_stdname();
00043 shell> QuineMcCluskeySubsumptionHypergraph-n16-O3-DNDEBUG AES_Sbox_full.cnf > AES_Sbox_shg.cnf
00044 shell> cat AES_Sbox_shg.cnf | MinOnes2WeightedMaxSAT-O3-DNDEBUG > AES_Sbox_shg.wcnf
00045 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;
00046 shell> cat  AES_Sbox_full.cnf_primes | FilterDimacs AES_Sbox_s294.ass > AES_Sbox_s294.cnf
00047 maxima> SboxMinCNF : read_fcl_f("AES_Sbox_s294.cnf");
00048 
00049 Statistics : [16,294,1939,8,6]
00050 
00051 */
00052 set_hm(ss_sbox_cnfs, 8, SboxMinCNF)$
00053 
00054 
00055 /*********************************************************
00056  * r_1-bases with smallest known number of clauses       *
00057  *********************************************************
00058 */
00059 
00060 ss_sbox_rbase_cnfs : sm2hm({})$
00061 
00062 /* Generated by
00063 
00064 maxima> output_ss_sbox_fullcnf_stdname(2,4,ss_polynomial_2_4);
00065 shell>  QuineMcCluskey-n8-O3-DNDEBUG AES_sbox_2_4_full.cnf > primes_sbox.cnf
00066 shell>  cat primes_sbox.cnf | SortByClauseLength-O3-DNDEBUG > primes_sbox_sorted.cnf
00067 shell>  RUcpGen-O3-DNDEBUG primes_sbox_sorted.cnf | RUcpBase-O3-DNDEBUG > sbox_base.cnf
00068 
00069 Statistics: [8,27,96,4,3]
00070 
00071 It is not known if this is the minimum.
00072 
00073 */
00074 set_hm(ss_sbox_rbase_cnfs, 4, [[1,2,3,4,5,6,7,8],
00075   [{-1,2,5},{-6,-2,-1},{-7,-4,5},{-2,1,7},{1,3,7},{-8,-4,-3},{-8,-5,-2},{-8,-3,6},{-1,3,8},{-5,4,8},{2,6,8},{-7,-1,8},{-4,-3,-1,5},{-6,-4,-3,-2},{-6,-1,3,4},{-6,-2,3,4},{-6,-5,1,2},{-4,-1,2,6},{-5,-2,3,6},{-7,-3,1,2},{-7,-1,2,3},{-2,3,4,7},{-5,-3,4,7},{-8,1,3,4},{-8,-6,3,5},{-3,1,4,8},{-6,4,7,8}]])$
00076