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