OKlibrary  0.2.1.6
SboxAnalysis.mac
Go to the documentation of this file.
00001 /* Matthew Gwynne, 2.4.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 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/TestSystem/Lisp/Asserts.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/PartialAssignments.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Backtracking/DLL_solvers.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/CryptoSystems/Rijndael/SmallScaleWordFields")$
00027 
00028 kill(f)$
00029 
00030 
00031 /* ******************************************
00032    * Sbox Analysis                          *
00033    ******************************************
00034 */
00035 
00036 okltest_rijnsbox_fulldnf_fcs(f) := block([FF],
00037   FF : f(),
00038   assert(length(FF[2]) = 256),
00039   assert(length(FF[1]) = 16),
00040   assert(apply_pa_cs(setify(create_list(i,i,1,8)), FF[2])=
00041     {{-14,-13,-12,-9,10,11,15,16}}),
00042   assert(elementp({-11,-9,-8,-7,-5,-4,-3,-2,1,6,10,12,13,14,15,16},
00043     FF[2])),
00044   assert(elementp({-15,-14,-10,-6,-3,1,2,4,5,7,8,9,11,12,13,16},
00045     FF[2])),
00046   assert(apply_pa_cs(setify(create_list(-i,i,1,8)), FF[2])=
00047     {{-16,-13,-11,-10,-9,12,14,15}}),
00048   true)$
00049 
00050 okltest_rijnsbox_fullcnf_fcs(f) := block([FF],
00051   if oklib_test_level = 0 then return(true),
00052   FF : f(),
00053   assert(length(FF[2]) = 2^16 - 256),
00054   assert(length(FF[1]) = 16),
00055   assert(apply_pa_cs(union(setify(create_list(-i,i,1,8)),
00056     {-14,-13,-12,-9,10,11,15,16}), FF[2])= {}),
00057   assert(apply_pa_cs(union(setify(create_list(-i,i,1,8)),
00058     {-14,-13,-12,-9,10,-11,15,16}), FF[2])= {{}}),
00059   assert(apply_pa_cs(union(setify(create_list(i,i,1,8)),
00060     {-16,-13,-11,-10,-9,12,14,15}), FF[2]) = {}),
00061   assert(apply_pa_cs(union(setify(create_list(i,i,1,8)),
00062     {-16,-13,-11,-10,-9,12,14,-15}), FF[2]) = {{}}),
00063   true)$
00064 
00065 okltest_rijnsbox_cnfp(f) := block(
00066   if oklib_test_level = 0 then return(true),
00067   assert(f([{},{}]) = false),
00068   assert(f([{},{{}}]) = false),
00069   assert(f([{1},{{}}]) = false),
00070   assert(f([{1},{{1}}]) = false),
00071   assert(f([{1,2},{{1}}]) = false),
00072   assert(f([{1,2},{{1,2},{-1,2},{-2,1}}]) = false),
00073   assert(f(rijnsbox_fullcnf_fcs())),
00074   true)$
00075 
00076 /* ******************************************************
00077    * Small Scale Sbox Analysis                          *
00078    ******************************************************
00079 */
00080 
00081 okltest_ss_sbox_fulldnf_gen_fcl(f) := block(
00082   assert(f(2,4,ss_polynomial_2_4,ss_sbox_matrix(2,4),ss_affine_constant(2,4)) =
00083     [[1,2,3,4,5,6,7,8],
00084     [{-8,-5,-4,-3,-2,-1,6,7},{-6,-3,-2,-1,4,5,7,8},{-7,-5,-4,-2,-1,3,6,8},
00085     {-8,-7,-5,-2,-1,3,4,6},{-8,-6,-5,-4,-3,-1,2,7},{-8,-3,-1,2,4,5,6,7},
00086     {-5,-4,-1,2,3,6,7,8},{-8,-6,-1,2,3,4,5,7},{-7,-6,-4,-3,-2,1,5,8},
00087     {-7,-3,-2,1,4,5,6,8},{-4,-2,1,3,5,6,7,8},{-8,-7,-2,1,3,4,5,6},
00088     {-6,-5,-4,-3,1,2,7,8},{-7,-6,-5,-3,1,2,4,8},{-8,-7,-6,-5,-4,1,2,3},
00089     {-8,-7,-6,1,2,3,4,5}]]),
00090   if oklib_test_level = 0 then return(true),
00091   assert(f(2,8,ss_polynomial_2_8,ss_sbox_matrix(2,8),ss_affine_constant(2,8)) =
00092       rijnsbox_fulldnf_fcl()),
00093   true)$
00094 
00095 okltest_ss_sbox_fullcnf_gen_fcs(f) := block(
00096   assert(f(2,4,ss_polynomial_2_4,ss_sbox_matrix(2,4),ss_affine_constant(2,4))=
00097     [{1,2,3,4,5,6,7,8},
00098         {{-8,-7,-6,-5,-4,-3,-2,-1},{-8,-7,-6,-5,-4,-3,-2,1},
00099         {-8,-7,-6,-5,-4,-3,-1,2},{-8,-7,-6,-5,-4,-3,1,2},
00100         {-8,-7,-6,-5,-4,-2,-1,3},{-8,-7,-6,-5,-4,-2,1,3},
00101         {-8,-7,-6,-5,-4,-1,2,3},{-8,-7,-6,-5,-4,1,2,3},
00102         {-8,-7,-6,-5,-3,-2,-1,4},{-8,-7,-6,-5,-3,-2,1,4},
00103         {-8,-7,-6,-5,-3,1,2,4},{-8,-7,-6,-5,-2,-1,3,4},
00104         {-8,-7,-6,-5,-2,1,3,4},{-8,-7,-6,-5,-1,2,3,4},{-8,-7,-6,-5,1,2,3,4},
00105         {-8,-7,-6,-4,-3,-2,-1,5},{-8,-7,-6,-4,-3,-2,1,5},
00106         {-8,-7,-6,-4,-3,-1,2,5},{-8,-7,-6,-4,-3,1,2,5},{-8,-7,-6,-4,-2,-1,3,5},
00107         {-8,-7,-6,-4,-2,1,3,5},{-8,-7,-6,-4,-1,2,3,5},{-8,-7,-6,-4,1,2,3,5},
00108         {-8,-7,-6,-3,-2,-1,4,5},{-8,-7,-6,-3,-1,2,4,5},{-8,-7,-6,-3,1,2,4,5},
00109         {-8,-7,-6,-2,-1,3,4,5},{-8,-7,-6,-2,1,3,4,5},{-8,-7,-6,-1,2,3,4,5},
00110         {-8,-7,-6,1,2,3,4,5},{-8,-7,-5,-4,-3,-2,-1,6},{-8,-7,-5,-4,-3,-2,1,6},
00111         {-8,-7,-5,-4,-3,-1,2,6},{-8,-7,-5,-4,-3,1,2,6},{-8,-7,-5,-4,-2,-1,3,6},
00112         {-8,-7,-5,-4,-2,1,3,6},{-8,-7,-5,-4,-1,2,3,6},{-8,-7,-5,-3,-2,-1,4,6},
00113         {-8,-7,-5,-3,-2,1,4,6},{-8,-7,-5,-3,-1,2,4,6},{-8,-7,-5,-3,1,2,4,6},
00114         {-8,-7,-5,-2,-1,3,4,6},{-8,-7,-5,-2,1,3,4,6},{-8,-7,-5,-1,2,3,4,6},
00115         {-8,-7,-5,1,2,3,4,6},{-8,-7,-4,-3,-2,-1,5,6},{-8,-7,-4,-3,-2,1,5,6},
00116         {-8,-7,-4,-3,-1,2,5,6},{-8,-7,-4,-3,1,2,5,6},{-8,-7,-4,-2,-1,3,5,6},
00117         {-8,-7,-4,-2,1,3,5,6},{-8,-7,-4,-1,2,3,5,6},{-8,-7,-4,1,2,3,5,6},
00118         {-8,-7,-3,-2,-1,4,5,6},{-8,-7,-3,-2,1,4,5,6},{-8,-7,-3,-1,2,4,5,6},
00119         {-8,-7,-3,1,2,4,5,6},{-8,-7,-2,1,3,4,5,6},{-8,-7,-1,2,3,4,5,6},
00120         {-8,-7,1,2,3,4,5,6},{-8,-6,-5,-4,-3,-2,-1,7},{-8,-6,-5,-4,-3,-2,1,7},
00121         {-8,-6,-5,-4,-3,-1,2,7},{-8,-6,-5,-4,-3,1,2,7},{-8,-6,-5,-4,-2,-1,3,7},
00122         {-8,-6,-5,-4,-2,1,3,7},{-8,-6,-5,-4,1,2,3,7},{-8,-6,-5,-3,-2,-1,4,7},
00123         {-8,-6,-5,-3,-2,1,4,7},{-8,-6,-5,-3,-1,2,4,7},{-8,-6,-5,-3,1,2,4,7},
00124         {-8,-6,-5,-2,-1,3,4,7},{-8,-6,-5,-2,1,3,4,7},{-8,-6,-5,-1,2,3,4,7},
00125         {-8,-6,-5,1,2,3,4,7},{-8,-6,-4,-3,-2,-1,5,7},{-8,-6,-4,-3,-2,1,5,7},
00126         {-8,-6,-4,-3,-1,2,5,7},{-8,-6,-4,-3,1,2,5,7},{-8,-6,-4,-2,-1,3,5,7},
00127         {-8,-6,-4,-2,1,3,5,7},{-8,-6,-4,-1,2,3,5,7},{-8,-6,-4,1,2,3,5,7},
00128         {-8,-6,-3,-2,-1,4,5,7},{-8,-6,-3,-2,1,4,5,7},{-8,-6,-3,-1,2,4,5,7},
00129         {-8,-6,-2,-1,3,4,5,7},{-8,-6,-2,1,3,4,5,7},{-8,-6,-1,2,3,4,5,7},
00130         {-8,-6,1,2,3,4,5,7},{-8,-5,-4,-3,-2,-1,6,7},{-8,-5,-4,-3,-2,1,6,7},
00131         {-8,-5,-4,-3,-1,2,6,7},{-8,-5,-4,-3,1,2,6,7},{-8,-5,-4,-2,-1,3,6,7},
00132         {-8,-5,-4,-2,1,3,6,7},{-8,-5,-4,-1,2,3,6,7},{-8,-5,-4,1,2,3,6,7},
00133         {-8,-5,-3,-2,-1,4,6,7},{-8,-5,-3,-2,1,4,6,7},{-8,-5,-3,-1,2,4,6,7},
00134         {-8,-5,-3,1,2,4,6,7},{-8,-5,-2,-1,3,4,6,7},{-8,-5,-2,1,3,4,6,7},
00135         {-8,-5,1,2,3,4,6,7},{-8,-4,-3,-2,-1,5,6,7},{-8,-4,-3,-2,1,5,6,7},
00136         {-8,-4,-3,-1,2,5,6,7},{-8,-4,-3,1,2,5,6,7},{-8,-4,-2,1,3,5,6,7},
00137         {-8,-4,-1,2,3,5,6,7},{-8,-4,1,2,3,5,6,7},{-8,-3,-2,-1,4,5,6,7},
00138         {-8,-3,-2,1,4,5,6,7},{-8,-3,-1,2,4,5,6,7},{-8,-3,1,2,4,5,6,7},
00139         {-8,-2,-1,3,4,5,6,7},{-8,-2,1,3,4,5,6,7},{-8,-1,2,3,4,5,6,7},
00140         {-8,1,2,3,4,5,6,7},{-7,-6,-5,-4,-3,-2,-1,8},
00141         {-7,-6,-5,-4,-3,-2,1,8},{-7,-6,-5,-4,-3,-1,2,8},{-7,-6,-5,-4,-3,1,2,8},
00142         {-7,-6,-5,-4,-2,-1,3,8},{-7,-6,-5,-4,-1,2,3,8},{-7,-6,-5,-4,1,2,3,8},
00143         {-7,-6,-5,-3,-2,-1,4,8},{-7,-6,-5,-3,-2,1,4,8},{-7,-6,-5,-3,-1,2,4,8},
00144         {-7,-6,-5,-3,1,2,4,8},{-7,-6,-5,-2,-1,3,4,8},{-7,-6,-5,-2,1,3,4,8},
00145         {-7,-6,-5,-1,2,3,4,8},{-7,-6,-5,1,2,3,4,8},{-7,-6,-4,-3,-2,-1,5,8},
00146         {-7,-6,-4,-3,-2,1,5,8},{-7,-6,-4,-3,-1,2,5,8},{-7,-6,-4,-3,1,2,5,8},
00147         {-7,-6,-4,-2,-1,3,5,8},{-7,-6,-4,-2,1,3,5,8},{-7,-6,-4,-1,2,3,5,8},
00148         {-7,-6,-4,1,2,3,5,8},{-7,-6,-3,-2,-1,4,5,8},{-7,-6,-3,-2,1,4,5,8},
00149         {-7,-6,-3,-1,2,4,5,8},{-7,-6,-3,1,2,4,5,8},{-7,-6,-2,-1,3,4,5,8},
00150         {-7,-6,-2,1,3,4,5,8},{-7,-6,-1,2,3,4,5,8},{-7,-5,-4,-3,-2,-1,6,8},
00151         {-7,-5,-4,-3,-1,2,6,8},{-7,-5,-4,-3,1,2,6,8},{-7,-5,-4,-2,-1,3,6,8},
00152         {-7,-5,-4,-2,1,3,6,8},{-7,-5,-4,-1,2,3,6,8},{-7,-5,-4,1,2,3,6,8},
00153         {-7,-5,-3,-2,-1,4,6,8},{-7,-5,-3,-2,1,4,6,8},{-7,-5,-3,-1,2,4,6,8},
00154         {-7,-5,-3,1,2,4,6,8},{-7,-5,-2,-1,3,4,6,8},{-7,-5,-2,1,3,4,6,8},
00155         {-7,-5,-1,2,3,4,6,8},{-7,-5,1,2,3,4,6,8},{-7,-4,-3,-2,-1,5,6,8},
00156         {-7,-4,-3,-2,1,5,6,8},{-7,-4,-3,-1,2,5,6,8},{-7,-4,-3,1,2,5,6,8},
00157         {-7,-4,-2,-1,3,5,6,8},{-7,-4,-2,1,3,5,6,8},{-7,-4,-1,2,3,5,6,8},
00158         {-7,-4,1,2,3,5,6,8},{-7,-3,-2,-1,4,5,6,8},{-7,-3,-2,1,4,5,6,8},
00159         {-7,-3,-1,2,4,5,6,8},{-7,-3,1,2,4,5,6,8},{-7,-2,-1,3,4,5,6,8},
00160         {-7,-1,2,3,4,5,6,8},{-7,1,2,3,4,5,6,8},{-6,-5,-4,-3,-2,-1,7,8},
00161         {-6,-5,-4,-3,-2,1,7,8},{-6,-5,-4,-3,1,2,7,8},{-6,-5,-4,-2,-1,3,7,8},
00162         {-6,-5,-4,-2,1,3,7,8},{-6,-5,-4,-1,2,3,7,8},{-6,-5,-4,1,2,3,7,8},
00163         {-6,-5,-3,-2,-1,4,7,8},{-6,-5,-3,-2,1,4,7,8},{-6,-5,-3,-1,2,4,7,8},
00164         {-6,-5,-3,1,2,4,7,8},{-6,-5,-2,-1,3,4,7,8},{-6,-5,-2,1,3,4,7,8},
00165         {-6,-5,-1,2,3,4,7,8},{-6,-5,1,2,3,4,7,8},{-6,-4,-3,-2,-1,5,7,8},
00166         {-6,-4,-3,-2,1,5,7,8},{-6,-4,-3,-1,2,5,7,8},{-6,-4,-2,-1,3,5,7,8},
00167         {-6,-4,-2,1,3,5,7,8},{-6,-4,-1,2,3,5,7,8},{-6,-4,1,2,3,5,7,8},
00168         {-6,-3,-2,-1,4,5,7,8},{-6,-3,-2,1,4,5,7,8},{-6,-3,-1,2,4,5,7,8},
00169         {-6,-3,1,2,4,5,7,8},{-6,-2,-1,3,4,5,7,8},{-6,-2,1,3,4,5,7,8},
00170         {-6,-1,2,3,4,5,7,8},{-6,1,2,3,4,5,7,8},{-5,-4,-3,-2,1,6,7,8},
00171         {-5,-4,-3,-1,2,6,7,8},{-5,-4,-3,1,2,6,7,8},{-5,-4,-2,-1,3,6,7,8},
00172         {-5,-4,-2,1,3,6,7,8},{-5,-4,-1,2,3,6,7,8},{-5,-4,1,2,3,6,7,8},
00173         {-5,-3,-2,-1,4,6,7,8},{-5,-3,-2,1,4,6,7,8},{-5,-3,-1,2,4,6,7,8},
00174         {-5,-3,1,2,4,6,7,8},{-5,-2,-1,3,4,6,7,8},{-5,-2,1,3,4,6,7,8},
00175         {-5,-1,2,3,4,6,7,8},{-5,1,2,3,4,6,7,8},{-4,-3,-2,-1,5,6,7,8},
00176         {-4,-3,-2,1,5,6,7,8},{-4,-3,-1,2,5,6,7,8},{-4,-3,1,2,5,6,7,8},
00177         {-4,-2,-1,3,5,6,7,8},{-4,-2,1,3,5,6,7,8},{-4,-1,2,3,5,6,7,8},
00178         {-4,1,2,3,5,6,7,8},{-3,-2,1,4,5,6,7,8},{-3,-1,2,4,5,6,7,8},
00179         {-3,1,2,4,5,6,7,8},{-2,-1,3,4,5,6,7,8}, {-2,1,3,4,5,6,7,8},
00180         {-1,2,3,4,5,6,7,8},{1,2,3,4,5,6,7,8}}]),
00181   if oklib_test_level = 0 then return(true),
00182   assert(f(2,8,ss_polynomial_2_8,ss_sbox_matrix(2,8),ss_affine_constant(2,8)) =
00183       rijnsbox_fullcnf_fcs()),      
00184   true)$
00185 
00186 
00187 okltest_ss_sbox_gen_cnfp(f) := block(
00188   if oklib_test_level = 0 then return(true),
00189   assert(f(rijnsbox_fullcnf_fcs(),2,8,ss_polynomial_2_8,
00190       ss_sbox_matrix(2,8),ss_affine_constant(2,8))),
00191   true)$
00192 
00193 
00194 /* *****************************************************************
00195    * Small Scale Sbox linear map Analysis                          *
00196    *****************************************************************
00197 */
00198 
00199 okltest_ss_sbox_linmap_fulldnf_fcl(f) := block(
00200   assert(f(2,1,ss_polynomial_2_1) = [[1,2],[{-2,-1},{1,2}]]),
00201   assert(f(2,4,ss_polynomial_2_4) =
00202     [[1,2,3,4,5,6,7,8],
00203      [{-8,-7,-6,-5,-4,-3,-2,-1},{-7,-3,-2,-1,4,5,6,8},{-6,-4,-2,-1,3,5,7,8},
00204       {-8,-5,-2,-1,3,4,6,7},{-5,-4,-3,-1,2,6,7,8},{-8,-6,-3,-1,2,4,5,7},
00205       {-8,-7,-4,-1,2,3,5,6},{-7,-6,-5,-1,2,3,4,8},{-8,-4,-3,-2,1,5,6,7},
00206       {-6,-5,-3,-2,1,4,7,8},{-7,-5,-4,-2,1,3,6,8},{-8,-7,-6,-2,1,3,4,5},
00207       {-7,-6,-4,-3,1,2,5,8},{-8,-7,-5,-3,1,2,4,6},{-8,-6,-5,-4,1,2,3,7},
00208       {1,2,3,4,5,6,7,8}]]),
00209   true)$
00210 
00211 okltest_ss_sbox_linmap_fullcnf_fcs(f) := block(
00212   assert(f(2,1) = [{1,2},{{-2,1},{-1,2}}]),
00213   assert(elementp({-8,-7,-6,5,-4,-3,-2,-1}, f(2,4)[2])),
00214   true)$
00215 
00216 okltest_ss_matrix2str(f) := block(
00217   assert(f(ss_sbox_matrix_2_1) = "1"),
00218   assert(f(ss_sbox_matrix_2_4) = "1_0_1_1_1_1_0_1_1_1_1_0_0_1_1_1"),
00219   true)$
00220 
00221 okltest_ss_sbox_linmap_cnfp(f) := block(
00222   assert(f([{1,2},{{-2,1},{-1,2}}],2,1)),
00223   assert(not(f([{1,2},{{-2,1},{1,2}}],2,1))),
00224   true)$
00225 
00226 
00227 /* *****************************************************************
00228    * Small scale multiplication then Sbox linear map analysis      *
00229    *****************************************************************
00230 */
00231 
00232 okltest_ss_mul_w_sbox_linmap_fulldnf_fcl(f) := block(
00233   assert(f(1,2,1,ss_polynomial_2_1) = [[1,2],[{-2,-1},{1,2}]]),
00234   assert(f(1,2,4,ss_polynomial_2_4) =
00235     [[1,2,3,4,5,6,7,8],
00236      [{-8,-7,-6,-5,-4,-3,-2,-1},{-7,-3,-2,-1,4,5,6,8},{-6,-4,-2,-1,3,5,7,8},
00237       {-8,-5,-2,-1,3,4,6,7},{-5,-4,-3,-1,2,6,7,8},{-8,-6,-3,-1,2,4,5,7},
00238       {-8,-7,-4,-1,2,3,5,6},{-7,-6,-5,-1,2,3,4,8},{-8,-4,-3,-2,1,5,6,7},
00239       {-6,-5,-3,-2,1,4,7,8},{-7,-5,-4,-2,1,3,6,8},{-8,-7,-6,-2,1,3,4,5},
00240       {-7,-6,-4,-3,1,2,5,8},{-8,-7,-5,-3,1,2,4,6},{-8,-6,-5,-4,1,2,3,7},
00241       {1,2,3,4,5,6,7,8}]]),
00242   assert(f(3,2,4,ss_polynomial_2_4) =
00243     [[1,2,3,4,5,6,7,8],
00244        [{-8,-7,-6,-5,-4,-3,-2,-1},{-7,-3,-2,-1,4,5,6,8},{-6,-4,-2,-1,3,5,7,8},
00245         {-8,-5,-2,-1,3,4,6,7},{-5,-4,-3,-1,2,6,7,8},{-8,-6,-3,-1,2,4,5,7},
00246         {-8,-7,-4,-1,2,3,5,6},{-7,-6,-5,-1,2,3,4,8},{-8,-4,-3,-2,1,5,6,7},
00247         {-6,-5,-3,-2,1,4,7,8},{-7,-5,-4,-2,1,3,6,8},{-8,-7,-6,-2,1,3,4,5},
00248         {-7,-6,-4,-3,1,2,5,8},{-8,-7,-5,-3,1,2,4,6},{-8,-6,-5,-4,1,2,3,7},
00249         {1,2,3,4,5,6,7,8}]]),
00250   true)$
00251 
00252 okltest_ss_mul_w_sbox_linmap_fullcnf_fcs(f) := block(
00253   assert(f(1,2,1) = [{1,2},{{-2,1},{-1,2}}]),
00254   assert(elementp({-8,-7,-6,5,-4,-3,-2,-1}, f(1,2,4)[2])),
00255   true)$
00256 
00257 okltest_ss_mul_w_sbox_linmap_cnfp(f) := block(
00258   assert(f([{1,2},{{-2,1},{-1,2}}],1,2,1)),
00259   assert(not(f([{1,2},{{-2,1},{1,2}}],1,2,1))),
00260   true)$
00261 
00262 
00263 /* ******************************************
00264    * Representations by hitting clause-sets *
00265    ******************************************
00266 */
00267 
00268 okltest_rijnsbox2hittingcnf_fcs(f) := block(
00269  [sbox_cnf,sbox_cnf_real, sbox_cnf_max],
00270   if oklib_test_level = 0 then return(true),
00271   if oklib_test_level = 1 then return(true),
00272   sbox_cnf : f(dll_heuristics_first_formal),
00273   assert(length(sbox_cnf) > 1),
00274   assert(rijnsbox_cnfp(cs2fcs(sbox_cnf))),
00275   sbox_cnf_real : f(dll_heuristics_first_real),
00276   assert(rijnsbox_cnfp(cs2fcs(sbox_cnf_real))),
00277   sbox_cnf_max : f(dll_heuristics_max_var),
00278   assert(rijnsbox_cnfp(cs2fcs(sbox_cnf_max))),
00279   assert(hittingcsp(sbox_cnf)),
00280   assert(hittingcsp(sbox_cnf_real)),
00281   assert(hittingcsp(sbox_cnf_max)),
00282   true)$
00283 
00284