OKlibrary  0.2.1.6
FieldOperationsAnalysis.mac
Go to the documentation of this file.
00001 /* Matthew Gwynne, 9.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/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")\$
00023 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")\$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/HittingClauseSets.mac")\$
00025 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/CryptoSystems/Rijndael/ByteField.mac")\$
00026 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/CryptoSystems/Rijndael/SmallScaleWordFields.mac")\$
00027 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/FiniteFunctions/Permutations.mac")\$
00028 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Generators.mac")\$
00029
00030
00031 /* ************************************************************
00032    * General small scale field analysis                       *
00033    ************************************************************
00034 */
00035
00036
00037 /* Generation of the full DNF clause-set representing the small scale AES
00038    field operation given by f over some small scale field with
00039    base b and exponent e: */
00040 ss_field_op_fulldnf_gen_fcl(f,b,e) :=
00041   perm2dnffcl(1+map(lambda([ap], poly2nat(f(nat2poly(ap,b)),b)),
00042       create_list(i,i,0,b^e-1)))\$
00043
00044 /* Generation of the full CNF clause-set representing the small scale AES
00045    field operation f: */
00046 ss_field_op_fullcnf_gen_fcs(f,b,e) :=
00047  cs2fcs(setdifference(full_cs(2*e),
00048              map(comp_sl,fcs2cs(fcl2fcs(
00049                    ss_field_op_fulldnf_gen_fcl(f,b,e))))))\$
00050
00051 /* Tests whether a formal CNF clause-set represents the small scale AES sbox
00052    field operation f given the appropriate parameters.
00053
00054    This function is useful when generating Sbox representations as
00055    one can then test whether such representations are equivalent
00056    to the Sbox. See plans/SboxAnalysis.hpp .
00057 */
00058 ss_field_op_gen_cnfp(FF,f,b,e) :=
00059   is(cs2fcs(dualtreehittingcls_fcs(FF,dll_heuristics_first_real)) =
00060     fcl2fcs(ss_field_op_fulldnf_gen_fcl(f,b,e)))\$
00061
00062
00063 /* ******************************************
00064    * Rijndael field multiplication analysis *
00065    ******************************************
00066 */
00067
00068 /* Generation of the (unique, full) DNF clause-set representing the
00069    multiplication with the field element a (as an integer) in the
00070    Rijndael GF(2^8) field.
00071    Prerequisite: 1 <= a <= 255.
00072 */
00073 rijnmult_fulldnf_fcl(a) :=
00074   perm2dnffcl(1+map(lambda([b], rijn_natmul(a,b)), create_list(i,i,0,255)))\$
00075 rijnmult_fulldnf_fcs(a) := fcl2fcs(rijnmult_fulldnf_fcl(a))\$
00076
00077 /* Generation of the full CNF clause-set representing the
00078    multiplication with the given field element (as an integer) in the
00079    Rijndael GF(2^8) field.
00080    Prerequisite: 1 <= field_element <= 255.
00081 */
00082 rijnmult_fullcnf_fcs(field_element) := block(
00083   [full16cs : fcs2cs(full_fcs(16)),
00084    aes_fieldmul_cs : fcs2cs(rijnmult_fulldnf_fcs(field_element))],
00085   cs2fcs(setdifference(full16cs, map(comp_sl,aes_fieldmul_cs))))\$
00086
00087
00088 /* Output the full CNF clause-set of the permutation given by multiplication
00089    with a field-element different from zero:
00090 */
00091 output_rijnmult_fullcnf_stdname(field_element) :=
00092   output_fcs(
00093     sconcat("Full CNF representation of the AES byte-field multiplication by ",field_element, "."),
00094     rijnmult_fullcnf_fcs(field_element),
00095     sconcat("AES_byte_field_mul_full_",field_element,".cnf"))\$
00096
00097
00098 /* Tests whether a formal CNF clause-set FF represents an AES field
00099    multiplication: */
00100 rijnmult_cnfp(field_element,FF) :=
00101  is(cs2fcs(dualtreehittingcls_fcs(FF,dll_heuristics_first_real)) =
00102    rijnmult_fulldnf_fcs(field_element))\$
00103
00104
00105 /* *********************************************
00106    * Small scale field multiplication analysis *
00107    *********************************************
00108 */
00109
00110 /* Generation of the (unique, full) DNF clause-set representing the
00111    multiplication with the field element a (as an integer) in the
00112    small scale GF(b^e) field with the given parameters.
00113    Prerequisite: 0 <= a <= b^e-1 (integer).
00114 */
00115 ssmult_fulldnf_fcl(a,b,e,mod_poly) :=
00116   perm2dnffcl(1+map(lambda([ap], ss_natmul(a,ap,b,mod_poly)),
00117     create_list(i,i,0,b^e-1)))\$
00118 ssmult_fulldnf_fcs(a,b,e,mod_poly) := fcl2fcs(ssmult_fulldnf_fcl(a,b,e,mod_poly))\$
00119
00120 /* Generation of the full CNF clause-set representing the
00121    multiplication with the given field element (as an integer) in the
00122    small scale GF(b^e) field.
00123    Prerequisite: 1 <= field_element <= b^e-1.
00124 */
00125 ssmult_fullcnf_fcs(field_element, b,e, mod_poly) := block(
00126   [fullcs : fcs2cs(full_fcs(2*e)),
00127    aes_fieldmul_cs : fcs2cs(ssmult_fulldnf_fcs(field_element,b,e,mod_poly))],
00128   cs2fcs(setdifference(fullcs, map(comp_sl,aes_fieldmul_cs))))\$
00129 ssmult_fullcnf_fcs(field_element, b,e, mod_poly) := block(
00130   [fullcs : fcs2cs(full_fcs(2*e)),
00131    aes_fieldmul_cs : fcs2cs(ssmult_fulldnf_fcs(field_element,b,e,mod_poly))],
00132   cs2fcs(setdifference(fullcs, map(comp_sl,aes_fieldmul_cs))))\$
00133
00134
00135 /* Output the full CNF clause-set of the permutation given by multiplication
00136    with a field-element different from zero:
00137 */
00138 output_ssmult_fullcnf_stdname(field_element, b,e, mod_poly) :=
00139   output_fcs(
00140     sconcat("Full CNF representation of the Small scale AES byte-field multiplication by ",field_element, "."),
00141     ssmult_fullcnf_fcs(field_element, b,e, mod_poly),
00142     sconcat("ss_byte",b,"_",e,"_field_mul_full_",field_element,".cnf"))\$
00143
00144
00145 /* Tests whether a formal CNF clause-set FF represents an small scale AES
00146    field multiplication: */
00147 ssmult_gen_cnfp(field_element, FF, b, e, mod_poly) :=
00148  is(cs2fcs(dualtreehittingcls_fcs(FF,dll_heuristics_first_real)) =
00149    ssmult_fulldnf_fcs(field_element, b, e, mod_poly))\$
00150 ssmult_cnfp(field_element, FF, b, e) :=
00151   ssmult_gen_cnfp(field_element, FF, b, e, ss_polynomial(b,e))\$
00152
00153
00154 /* *********************************************
00155    * Small scale field inversion analysis *
00156    *********************************************
00157 */
00158
00159 /* Generation of the (unique, full) DNF clause-set representing the
00160    inversion in the small scale GF(b^e) field with the given parameters.
00161 */
00162 ssinv_fulldnf_fcl(b,e,mod_poly) :=
00163 perm2dnffcl(1+map(lambda([ap], ss_natinv(ap,b,mod_poly)),
00164     create_list(i,i,0,b^e-1)))\$
00165 ssinv_fulldnf_fcs(a,e,mod_poly) := fcl2fcs(ssinv_fulldnf_fcl(a,e,mod_poly))\$
00166
00167 /* Generation of the full CNF clause-set representing the
00168    inversion in the small scale field.
00169 */
00170 ssinv_fullcnf_fcs(b,e, mod_poly) := block(
00171   [fullcs : fcs2cs(full_fcs(2*e)),
00172    aes_fieldmul_cs : fcs2cs(ssinv_fulldnf_fcs(b,e,mod_poly))],
00173   cs2fcs(setdifference(fullcs, map(comp_sl,aes_fieldmul_cs))))\$
00174 ssinv_fullcnf_fcs(b,e, mod_poly) := block(
00175   [fullcs : fcs2cs(full_fcs(2*e)),
00176    aes_fieldmul_cs : fcs2cs(ssinv_fulldnf_fcs(b,e,mod_poly))],
00177   cs2fcs(setdifference(fullcs, map(comp_sl,aes_fieldmul_cs))))\$
00178
00179
00180 /* Output the full CNF clause-set of the permutation given by inversion:
00181 */
00182 output_ssinv_fullcnf_stdname(b,e, mod_poly) :=
00183   output_fcs(
00184     sconcat("Full CNF representation of the Small scale AES byte-field inversion."),
00185     ssinv_fullcnf_fcs(b,e, mod_poly),
00186     sconcat("ss_byte",b,"_",e,"_field_inv_full.cnf"))\$
00187
00188
00189 /* Tests whether a formal CNF clause-set FF represents an AES field
00190    inversion: */
00191 ssinv_cnfp(FF, b, e, mod_poly) :=
00192  is(cs2fcs(dualtreehittingcls_fcs(FF,dll_heuristics_first_real)) =
00193    ssinv_fulldnf_fcs(b, e, mod_poly))\$
00194
00195
00196 /* ******************************************
00197    * Representations by hitting clause-sets *
00198    ******************************************
00199 */
00200
00201 /* Generation of a CNF hitting clause-set, given a heuristics h for
00202    a backtracking solver (without reduction): */
00203 rijnmult2hittingcnf_fcs(field_element,h) :=
00204   dualtreehittingcls_condensed_fcs(rijnmult_fulldnf_fcs(field_element),h)\$
00205