OKlibrary  0.2.1.6
SboxAnalysis.mac
Go to the documentation of this file.
00001 /* Matthew Gwynne, 26.3.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/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Conversions.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/CryptoSystems/Rijndael/AdvancedEncryptionStandard.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/CryptoSystems/Rijndael/SmallScaleAdvancedEncryptionStandard.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/HittingClauseSets.mac")$
00028 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/FiniteFunctions/Permutations.mac")$
00029 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/CryptoSystems/Rijndael/data/Sbox.mac")$
00030 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Generators.mac")$
00031 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/FieldOperationsAnalysis.mac")$
00032 
00033 
00034 /* ******************************************
00035    * Sbox Analysis                          *
00036    ******************************************
00037 */
00038 
00039 
00040 /* Generation of the full DNF clause-set representing the AES sbox: */
00041 rijnsbox_fulldnf_fcl() := perm2dnffcl(1+aes_sbox_l)$
00042 rijnsbox_fulldnf_fcs() := fcl2fcs(rijnsbox_fulldnf_fcl())$
00043 
00044 /* Generation of the full CNF clause-set representing the AES sbox: */
00045 rijnsbox_fullcnf_fcs() :=
00046  cs2fcs(setdifference(full_cs(16), 
00047              map(comp_sl,fcs2cs(rijnsbox_fulldnf_fcs()))))$
00048 
00049 /* Output the full CNF clause-set of the permutation given by the AES
00050    S-box to the file "AES_Sbox_full.cnf":
00051 */
00052 output_rijnsbox_fullcnf_stdname() :=
00053   output_fcs(
00054     sconcat("The AES Sbox in full CNF representation."),
00055     rijnsbox_fullcnf_fcs(),
00056     "AES_Sbox_full.cnf")$
00057 
00058 /* Tests whether a formal CNF clause-set represents the AES sbox:
00059 
00060    This function is useful when generating Sbox representations as
00061    one can then test whether such representations are equivalent
00062    to the Sbox. See plans/SboxAnalysis.hpp .
00063 */
00064 rijnsbox_cnfp(FF) := 
00065  is(cs2fcs(dualtreehittingcls_fcs(FF,dll_heuristics_first_real)) = rijnsbox_fulldnf_fcs())$
00066 
00067 
00068 /* ******************************************************
00069    * Small Scale Sbox Analysis                          *
00070    ******************************************************
00071 */
00072 
00073 
00074 /* Generation of the full DNF clause-set representing the small scale AES Sbox
00075    given the base of the small scale byte field, the exponent of the field,
00076    the modulo polynomial defining the field, as well as the sbox matrix and
00077    affine constant required for the sbox definition: */
00078 ss_sbox_fulldnf_gen_fcl(b,e,mod_poly, sbox_matrix,affine_constant) :=
00079   perm2dnffcl(1+map(lambda([ap],
00080         poly2nat(ss_sbox_gen(nat2poly(ap,b),
00081             b,e,mod_poly, sbox_matrix,affine_constant),b)),
00082       create_list(i,i,0,b^e-1)))$
00083 ss_sbox_fulldnf_fcl(b,e,mod_poly) :=
00084   ss_sbox_fulldnf_gen_fcl(b,e,mod_poly,
00085                           ss_sbox_matrix(b,e),ss_affine_constant(b,e))$
00086 ss_sbox_fulldnf_gen_fcs(b,e,mod_poly, sbox_matrix,affine_constant) :=
00087   fcl2fcs(ss_sbox_fulldnf_gen_fcl(b,e,mod_poly, sbox_matrix,affine_constant))$
00088 ss_sbox_fulldnf_fcs(b,e,mod_poly) := fcl2fcs(ss_sbox_fulldnf_fcl(b,e,mod_poly))$
00089 
00090 /* Generation of the full CNF clause-set representing the small scale AES
00091    sbox: */
00092 ss_sbox_fullcnf_gen_fcs(b,e,mod_poly,sbox_matrix,sbox_affine_constant) :=
00093  cs2fcs(setdifference(full_cs(2*e), 
00094              map(comp_sl,fcs2cs(ss_sbox_fulldnf_fcs(b,e,mod_poly)))))$
00095 ss_sbox_fullcnf_fcs(b,e,mod_poly) :=
00096   ss_sbox_fullcnf_gen_fcs(b,e,mod_poly,
00097     ss_sbox_matrix(b,e), ss_affine_constant(b,e))$
00098 
00099 /* Output the full CNF clause-set of the permutation given by the small scale
00100    AES Sbox:
00101 */
00102 output_ss_sbox_fullcnf_gen_stdname(b,e,mod_poly,sbox_matrix,sbox_affine_constant) :=
00103   output_fcs(
00104     sconcat("AES Sbox function given the full CNF representation."),
00105     ss_sbox_fullcnf_fcs(b,e,mod_poly, sbox_matrix, sbox_affine_constant),
00106     sconcat("AES_sbox_",b,"_",e,"_full.cnf"))$
00107 output_ss_sbox_fullcnf_stdname(b,e,mod_poly) :=
00108   output_fcs(
00109     sconcat("AES Sbox function given the full CNF representation."),
00110     ss_sbox_fullcnf_fcs(b,e,mod_poly),
00111     sconcat("AES_sbox_",b,"_",e,"_full.cnf"))$
00112 
00113 /* Tests whether a formal CNF clause-set represents the small scale AES sbox
00114    given the appropriate parameters:
00115 
00116    This function is useful when generating Sbox representations as
00117    one can then test whether such representations are equivalent
00118    to the Sbox. See plans/SboxAnalysis.hpp .
00119 */
00120 ss_sbox_gen_cnfp(FF,b,e,mod_poly,sbox_matrix,sbox_affine_constant) := 
00121   is(cs2fcs(dualtreehittingcls_fcs(FF,dll_heuristics_first_real)) =
00122     ss_sbox_fulldnf_gen_fcs(b,e,mod_poly,sbox_matrix,sbox_affine_constant))$
00123 ss_sbox_cnfp(FF,b,e,mod_poly) := 
00124   ss_sbox_gen_cnfp(FF,b,e,mod_poly, ss_sbox_matrix(b,e),
00125     ss_affine_constant(b,e))$
00126 
00127 
00128 /* *****************************************************************
00129    * Small Scale Sbox linear map Analysis                          *
00130    *****************************************************************
00131 */
00132 
00133 
00134 /* Generation of the full DNF clause-set representing the small scale AES Sbox
00135    linear map the base of the small scale byte field, the exponent of the
00136    field, the modulo polynomial defining the field, as well as the sbox
00137    matrix: */
00138 ss_sbox_linmap_fulldnf_gen_fcl(b,e,mod_poly, sbox_matrix) :=
00139   ss_field_op_fulldnf_gen_fcl(
00140     lambda([a], ss_sbox_linmap_gen(a,b,e,mod_poly,sbox_matrix)),b,e)$
00141 ss_sbox_linmap_fulldnf_fcl(b,e,mod_poly) :=
00142   ss_sbox_linmap_fulldnf_gen_fcl(b,e,mod_poly,
00143                           ss_sbox_matrix(b,e))$
00144 ss_sbox_linmap_fulldnf_gen_fcs(b,e,mod_poly, sbox_matrix) :=
00145   fcl2fcs(ss_sbox_linmap_fulldnf_gen_fcl(b,e,mod_poly, sbox_matrix))$
00146 ss_sbox_linmap_fulldnf_fcs(b,e,mod_poly) :=
00147   fcl2fcs(ss_sbox_linmap_fulldnf_fcl(b,e,mod_poly))$
00148 
00149 /* Generation of the full CNF clause-set representing the small scale AES
00150    sbox linear map: */
00151 ss_sbox_linmap_fullcnf_gen_fcs(b,e,mod_poly,sbox_matrix) :=
00152   ss_field_op_fullcnf_gen_fcs(
00153     lambda([a], ss_sbox_linmap_gen(a,b,e,mod_poly,sbox_matrix)),b,e)$
00154 ss_sbox_linmap_fullcnf_fcs(b,e) :=
00155   ss_sbox_linmap_fullcnf_gen_fcs(b,e,ss_polynomial(b,e),ss_sbox_matrix(b,e))$
00156 
00157 /* Converts a matrix to a "_" separated string, row by row: */
00158 ss_matrix2str(m) :=
00159   if length(m) > 0 then block([l : m2l_r(m)],
00160     lreduce(lambda([a,b], sconcat(a,"_",b)), rest(l), sconcat(first(l))))$
00161 
00162 /* Output the full CNF clause-set of the permutation given by the small scale
00163    AES Sbox linear map:
00164 */
00165 output_ss_sbox_linmap_fullcnf_gen_stdname(b,e,mod_poly,sbox_matrix) :=
00166   output_fcs(
00167     sconcat("AES Sbox linear (", sbox_matrix ,") map given the full",
00168       "CNF representation."),
00169     ss_sbox_linmap_fullcnf_gen_fcs(b,e,mod_poly, sbox_matrix),
00170     sconcat("AES_sbox_lin_",b,"_",e,"_",ss_matrix2str(sbox_matrix),
00171       "_full.cnf"))$
00172 output_ss_sbox_linmap_fullcnf_stdname(b,e) := block(
00173   [sbox_matrix : ss_sbox_matrix(b,e)],
00174   output_fcs(
00175     sconcat("AES Sbox linear (", sbox_matrix ,") map given the full",
00176       "CNF representation."),
00177     ss_sbox_linmap_fullcnf_fcs(b,e),
00178     sconcat("AES_sbox_lin_",b,"_",e,"_",ss_matrix2str(sbox_matrix),
00179       "_full.cnf")))$
00180 
00181 /* Tests whether a formal CNF clause-set represents the small scale AES sbox
00182    linear map given the appropriate parameters.
00183 
00184    This function is useful when generating Sbox representations as
00185    one can then test whether such representations are equivalent
00186    to the Sbox. See plans/SboxAnalysis.hpp .
00187 */
00188 ss_sbox_linmap_gen_cnfp(FF,b,e,mod_poly,sbox_matrix) :=
00189   ss_field_op_gen_cnfp(FF,
00190     lambda([a], ss_sbox_linmap_gen(a,b,e,mod_poly,sbox_matrix)),b,e)$
00191 ss_sbox_linmap_cnfp(FF,b,e) := 
00192   ss_sbox_linmap_gen_cnfp(FF,b,e,ss_polynomial(b,e), ss_sbox_matrix(b,e))$
00193 
00194 
00195 /* ******************************************************************
00196    * Small scale multiplication then Sbox linear map analysis       *
00197    ******************************************************************
00198 */
00199 
00200 
00201 /* Generation of the full DNF clause-set representing the small scale AES Sbox
00202    linear map the base of the small scale byte field, the exponent of the
00203    field, the modulo polynomial defining the field, as well as the sbox
00204    matrix: */
00205 ss_mul_w_sbox_linmap_fulldnf_gen_fcl(a,b,e,mod_poly, sbox_matrix) :=
00206   ss_field_op_fulldnf_gen_fcl(
00207     lambda([fe], ss_mul_w_sbox_linmap_gen(fe,a,b,e,mod_poly,sbox_matrix)),b,e)$
00208 ss_mul_w_sbox_linmap_fulldnf_fcl(a,b,e,mod_poly) :=
00209   ss_mul_w_sbox_linmap_fulldnf_gen_fcl(a,b,e,mod_poly,ss_sbox_matrix(b,e))$
00210 ss_mul_w_sbox_linmap_fulldnf_gen_fcs(a,b,e,mod_poly, sbox_matrix) :=
00211   fcl2fcs(ss_mul_w_sbox_linmap_fulldnf_gen_fcl(a,b,e,mod_poly, sbox_matrix))$
00212 ss_mul_w_sbox_linmap_fulldnf_fcs(a,b,e,mod_poly) :=
00213   fcl2fcs(ss_mul_w_sbox_linmap_fulldnf_fcl(a,b,e,mod_poly))$
00214 
00215 /* Generation of the full CNF clause-set representing the small scale AES
00216    sbox linear map: */
00217 ss_mul_w_sbox_linmap_fullcnf_gen_fcs(a,b,e,mod_poly,sbox_matrix) :=
00218   ss_field_op_fullcnf_gen_fcs(
00219     lambda([fe], ss_mul_w_sbox_linmap_gen(fe,a,b,e,mod_poly,sbox_matrix)),b,e)$
00220 ss_mul_w_sbox_linmap_fullcnf_fcs(a,b,e) :=
00221   ss_mul_w_sbox_linmap_fullcnf_gen_fcs(a,b,e,ss_polynomial(b,e),
00222     ss_sbox_matrix(b,e))$
00223 
00224 /* Output the full CNF clause-set of the permutation given by the small scale
00225    AES Sbox linear map:
00226 */
00227 output_ss_mul_w_sbox_linmap_fullcnf_gen_stdname(a,b,e,mod_poly,sbox_matrix) :=
00228   output_fcs(
00229     sconcat("AES Sbox linear (", sbox_matrix ,") map given the full",
00230       "CNF representation."),
00231     ss_sbox_fullcnf_fcs(a,b,e,mod_poly, sbox_matrix),
00232     sconcat("AES_sbox_mul_w_lin_",a,"_",b,"_",e,"_",
00233       ss_matrix2str(sbox_matrix),"_full.cnf"))$
00234 output_ss_mul_w_sbox_linmap_fullcnf_stdname(a,b,e) := block(
00235   [sbox_matrix : ss_sbox_matrix(b,e)],
00236   output_fcs(
00237     sconcat("AES Sbox linear (", sbox_matrix ,") map given the full",
00238       "CNF representation."),
00239     ss_mul_w_sbox_linmap_fullcnf_fcs(a,b,e),
00240     sconcat("AES_sbox_mul_w_lin_",a,"_",b,"_",e,"_",
00241       ss_matrix2str(sbox_matrix),"_full.cnf")))$
00242 
00243 /* Tests whether a formal CNF clause-set represents the small scale AES sbox
00244    linear map given the appropriate parameters.
00245 
00246    This function is useful when generating Sbox representations as
00247    one can then test whether such representations are equivalent
00248    to the Sbox. See plans/SboxAnalysis.hpp .
00249 */
00250 ss_mul_w_sbox_linmap_gen_cnfp(FF,a,b,e,mod_poly,sbox_matrix) :=
00251   ss_field_op_gen_cnfp(FF,
00252     lambda([fe], ss_mul_w_sbox_linmap_gen(fe,a,b,e,mod_poly,sbox_matrix)),b,e)$
00253 ss_mul_w_sbox_linmap_cnfp(FF,a,b,e) := 
00254   ss_mul_w_sbox_linmap_gen_cnfp(FF,a,b,e,ss_polynomial(b,e),
00255     ss_sbox_matrix(b,e))$
00256 
00257 
00258 /* ******************************************
00259    * Representations by hitting clause-sets *
00260    ******************************************
00261 */
00262 
00263 /* Generation of a CNF hitting clause-set, given a heuristics h for
00264    a backtracking solver (without reduction): */
00265 rijnsbox2hittingcnf_fcs(h) := dualtreehittingcls_condensed_fcs(rijnsbox_fulldnf_fcs(),h)$
00266 
00267