OKlibrary  0.2.1.6
Translations.mac
Go to the documentation of this file.
00001 /* Matthew Gwynne, 26.3.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 2010, 2011, 2012 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/DataStructures/Lisp/Lists.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/CryptoSystems/Rijndael/AdvancedEncryptionStandard.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/SboxAnalysis.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/FieldOperationsAnalysis.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/data/FieldMul2CNF.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/data/FieldMul3CNF.mac")$
00028 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/data/FieldMul11CNF.mac")$
00029 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/data/FieldMul13CNF.mac")$
00030 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/data/FieldMul14CNF.mac")$
00031 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/data/FieldMul9CNF.mac")$
00032 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/data/SboxCNF.mac")$
00033 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/FiniteFunctions/TseitinTranslation.mac")$
00034 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/ConstraintTemplateGlobalPropagation.mac")$
00035 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/ConstraintTemplateRewriteSystem.mac")$
00036 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/ConstraintTemplateSmallScaleRewriteRules.mac")$
00037 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/ConstraintTemplateTranslation.mac")$
00038 
00039 /* TODO: Add documentation at this level. */
00040 
00041 
00042 /* ***************************************
00043    * Sets of Conditions                  *
00044    ***************************************
00045 */
00046 
00047 
00048 /* Generates (and caches) the canonical CNF representation as a formal clause
00049    set of AES Field muliplication (within the Rijndael GF(2^8) field) by p 
00050    (given as an integer) with new variables. 
00051    
00052    New variables are introduced for each clause in the canonical DNF 
00053    representation (see dualts_fcl), where the variables are of the form dts(i)
00054    and i is the rank in the lexiographical ordering of the clauses.
00055 
00056    Caching here simply means that upon the first call to the function with
00057    argument "p", the result of the computation for that argument is stored 
00058    in a global variable "aes_mul_ts_CNF[p]" which will then be returned 
00059    immediately on subsequent calls to "aes_mul_ts_gen" with the same argument 
00060    to allow for reuse of "aes_mul_ts_gen" without the overhead of 
00061    recomputation.
00062  */
00063 aes_mul_ts_CNF : create_list(false,i,1,256)$
00064 aes_mul_ts_gen(p) := 
00065   if aes_mul_ts_CNF[p+1] = false then block([plus16 : lambda([x],x+16)],
00066       [mul_dnf : rijnmult_fulldnf_fcs(p)],
00067     aes_mul_ts_CNF[p+1] : dualts_fcl(
00068       [listify(mul_dnf[1]),
00069        sort(
00070          listify(mul_dnf[2]),
00071          lambda([a,b], is(
00072            rank_lex_ksubsets(map(plus16,a),32) < 
00073              rank_lex_ksubsets(map(plus16,b),32)))
00074         )]
00075      ),
00076      return(aes_mul_ts_CNF[p+1])
00077   ) else aes_mul_ts_CNF[p+1]$
00078 
00079 /* Generates (and caches) the canonical CNF representation as a formal clause
00080    set of AES Sbox operator with new variables. New variables are 
00081    introduced for each clause in the canonical DNF representation (see
00082    dualts_fcl), where the new variables are of the form dts(i) and i is the 
00083    rank in the lexiographical ordering of the clauses.
00084 
00085    Caching here simply means that upon the first call to the function, the
00086    result of the computation is stored in a global variable "aes_sbox_ts_CNF"
00087    which will then be returned immediately on subsequent calls to
00088    "aes_sbox_ts_gen" to allow for reuse of "aes_sbox_ts_gen" without the
00089    overhead of recomputation.
00090  */
00091 aes_sbox_ts_CNF : false;
00092 aes_sbox_ts_gen() :=
00093   if aes_sbox_ts_CNF = false then block([plus16 : lambda([x],x+16)],
00094       [sbox_dnf : rijnsbox_fulldnf_fcs()],
00095     aes_sbox_ts_CNF : dualts_fcl(
00096       [listify(sbox_dnf[1]),
00097        sort(
00098          listify(sbox_dnf[2]),
00099          lambda([a,b], is(
00100            rank_lex_ksubsets(map(plus16,a),32) <
00101              rank_lex_ksubsets(map(plus16,b),32)))
00102         )]
00103      ),
00104      return(aes_sbox_ts_CNF)
00105   ) else aes_sbox_ts_CNF$
00106 
00107 
00108 /*************************************************************
00109  * Constraint template rewrite-based translations            *
00110  *************************************************************
00111 */
00112 
00113 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/ConstraintTemplateRewriteRules.mac");
00114 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/ConstraintTemplateRewriteSystem.mac");
00115 
00116 
00117 /* AES */
00118 
00119 /* AES Translations
00120 
00121          Boxes -
00122              For each box we have the following translation
00123 
00124              aes_small_box - Each box is represented by the smallest known cnf
00125              aes_ts_box    - Each box is represented by the canonical
00126                              translation using new variables.
00127              aes_rbase_box - Each box is represented by a CNF which is
00128                              an r_1 base.
00129 
00130          MixColumns -
00131              For the translation of the MixColumns component, we may either
00132              add additional constraints translating the inversion as well
00133              or simply translate the component in the forward direction.
00134 
00135              aes_mc_forward
00136              aes_mc_bidirectional
00137 
00138 */
00139 
00140 declare(aes_small_box, noun)$
00141 declare(aes_full_box, noun)$
00142 declare(aes_ts_box, noun)$
00143 declare(aes_rbase_box, noun)$
00144 declare(aes_mc_forward, noun)$
00145 declare(aes_mc_bidirectional, noun)$
00146 declare(aes_combined_box, noun)$
00147 declare(aes_core_round_box, noun)$
00148 declare(aes_mc_boolm, noun)$
00149 declare(aes_mc_box, noun)$
00150 
00151 
00152 /* Constraint rewrite translations */
00153 
00154 /* Given the number of rounds, produces a list of constraint templates
00155    which model AES using standard parameters. */
00156 /* TODO: Add the full version that allows all parameters */
00157 aes_csttl(r, mc_tran) :=
00158   rewrite_all_csttl(
00159     [cstt_new("aes_cst",
00160               generate_aes_constraint_vars(1,3*128,cstt_id_ns,"aes_cst"),
00161               [r],cstt_id_ns)],
00162     if mc_tran = aes_mc_bidirectional then aes_bimc_rewrite_mapping_std
00163     else aes_rewrite_mapping_std)$
00164 aes_cstt_std_l(r) := aes_csttl(r, aes_mc_forward)$
00165 
00166 
00167 aes_cstt_vars_l(r, mc_tran) :=
00168   append(
00169     generate_aes_constraint_vars(1,3*128,cstt_id_ns,"aes_cst"),
00170     rewrite_all_cstt_vars_l(
00171       [cstt_new("aes_cst",
00172         generate_aes_constraint_vars(1,3*128,cstt_id_ns,"aes_cst"),
00173         [r],cstt_id_ns)],
00174       if mc_tran = aes_mc_bidirectional then aes_bimc_rewrite_mapping_std
00175       else aes_rewrite_mapping_std))$
00176 aes_cstt_vars_std_l(r) := aes_cstt_vars_l(r,aes_mc_forward)$
00177 
00178 
00179 aes_fcl(r, box_tran, mc_tran) := block(
00180   [aes_csttl : aes_csttl(r,mc_tran),aes_vars_l, prop_csttl],
00181   aes_vars_l : aes_cstt_vars_l(r,mc_tran),
00182   prop_csttl : prop_all_csttl(aes_csttl, aes_vars_l, aes_propagations),
00183   csttl2fcl(prop_csttl[1],prop_csttl[2],
00184     if box_tran = aes_small_box then
00185       aes_pi_translation_mapping
00186     else
00187       aes_ts_translation_mapping))$
00188 
00189 aes_std_fcl(r) := aes_fcl(r, aes_small_box, aes_ts_box)$
00190 
00191 /* Small Scale AES */
00192 
00193 ss_csttl(r,ss_num_columns, ss_num_rows, ss_exp, final_round_b, mc_tran) :=
00194   block([num_block_bits : ss_num_columns * ss_num_rows * ss_exp],
00195     rewrite_all_csttl(
00196       [cstt_new("ss_cst",
00197         generate_aes_constraint_vars(1,3*num_block_bits,
00198           cstt_id_ns,"ss_cst"),
00199           [r,ss_num_columns, ss_num_rows,2, ss_exp,
00200            ss_polynomial(2,ss_exp),ss_sbox_matrix(2,ss_exp),
00201            ss_affine_constant(2,ss_exp),
00202            ss_mixcolumns_matrix(2,ss_exp,ss_num_rows),final_round_b],
00203            cstt_id_ns)],
00204     if mc_tran = aes_mc_bidirectional then ss_bimc_rewrite_mapping_std
00205     else if mc_tran = aes_mc_boolm then ss_boolm_rewrite_mapping_std
00206     else if mc_tran = aes_mc_box then ss_boxmc_rewrite_mapping_std
00207     else if mc_tran = aes_combined_box then ss_boxcombined_rewrite_mapping_std
00208     else if mc_tran = aes_core_round_box then ss_round_column_rewrite_mapping_std
00209     else ss_rewrite_mapping_std))$
00210 /*aes_cstt_std_l(r) := aes_csttl(r, aes_mc_forward)$*/
00211 
00212 ss_cstt_vars_l(r, ss_num_columns, ss_num_rows, ss_exp, final_round_b, mc_tran) :=
00213   append(
00214     generate_aes_constraint_vars(1,3*(ss_num_columns*ss_num_rows*ss_exp),
00215         cstt_id_ns,"ss_cst"),
00216     rewrite_all_cstt_vars_l(
00217       [cstt_new("ss_cst",
00218         generate_aes_constraint_vars(1,3*(ss_num_columns*ss_num_rows*ss_exp),
00219           cstt_id_ns,"ss_cst"),
00220         [r,ss_num_columns, ss_num_rows,2, ss_exp,
00221            ss_polynomial(2,ss_exp),ss_sbox_matrix(2,ss_exp),
00222            ss_affine_constant(2,ss_exp),
00223            ss_mixcolumns_matrix(2,ss_exp,ss_num_rows),final_round_b],
00224            cstt_id_ns)],
00225       if mc_tran = aes_mc_bidirectional then ss_bimc_rewrite_mapping_std
00226       else if mc_tran = aes_mc_boolm then ss_boolm_rewrite_mapping_std
00227       else if mc_tran = aes_mc_box then ss_boxmc_rewrite_mapping_std
00228       else if mc_tran = aes_combined_box then ss_boxcombined_rewrite_mapping_std
00229       else if mc_tran = aes_core_round_box then ss_round_column_rewrite_mapping_std
00230       else ss_rewrite_mapping_std))$
00231 
00232 ss_fcl(r, ss_num_columns, ss_num_rows, ss_exp, final_round_b, box_tran, mc_tran) := block(
00233   [ss_csttl : ss_csttl(r,ss_num_columns, ss_num_rows, ss_exp, final_round_b,mc_tran),
00234   ss_vars_l, prop_csttl],
00235   ss_vars_l : ss_cstt_vars_l(r,ss_num_columns,
00236       ss_num_rows, ss_exp, final_round_b,mc_tran),
00237   prop_csttl : prop_all_csttl(ss_csttl, ss_vars_l, ss_propagations),
00238   csttl2fcl(prop_csttl[1],prop_csttl[2],
00239     if box_tran = aes_small_box then
00240       ss_pi_translation_mapping
00241     else if box_tran = aes_rbase_box then
00242       ss_rbase_translation_mapping
00243     else if box_tran = aes_full_box then
00244       ss_full_translation_mapping
00245     else
00246       ss_ts_translation_mapping))$
00247 
00248 output_ss_fcl(name,r, ss_num_columns, ss_num_rows, ss_exp, final_round_b, box_tran, mc_tran) :=
00249   block([FF, FF_std],
00250     if oklib_monitor then print("Starting translation..."),
00251     FF : ss_fcl(r, ss_num_columns, ss_num_rows, ss_exp, final_round_b, box_tran, mc_tran),
00252     if oklib_monitor then print("Starting standardisation..."),
00253     FF_std : standardise_fcl(FF),
00254     if oklib_monitor then print("Starting output..."),
00255     output_fcl_v(sconcat("Small Scale AES with ",
00256                    "r=",r,",c=",ss_num_columns,",rw=",ss_num_rows,
00257                    ",e=",ss_exp,",final=",final_round_b,
00258                    ",box_tran=",box_tran,",mc_tran=",mc_tran),
00259                  FF_std[1],name,
00260       FF_std[2]))$
00261   
00262 output_ss_fcl_std(r, ss_num_columns, ss_num_rows, ss_exp, final_round_b, box_tran, mc_tran) :=
00263   output_ss_fcl(
00264     sconcat("ssaes_r", r, "_c",ss_num_columns, "_rw",ss_num_rows,"_e",ss_exp,
00265       "_f",if final_round_b then 1 else 0, ".cnf"),
00266     r, ss_num_columns, ss_num_rows, ss_exp, final_round_b, box_tran, mc_tran)$
00267     
00268 
00269 ss_trans_fcl(cst, box_tran, mc_tran) := block(
00270   [ss_csttl,ss_vars_l, prop_csttl,rm],
00271   rm :
00272     if mc_tran = aes_mc_bidirectional then ss_bimc_rewrite_mapping_std
00273     else if mc_tran = aes_mc_boolm then ss_boolm_rewrite_mapping_std
00274     else if mc_tran = aes_mc_box then ss_boxmc_rewrite_mapping_std
00275     else if mc_tran = aes_combined_box then ss_boxcombined_rewrite_mapping_std
00276     else if mc_tran = aes_core_round_box then ss_round_column_rewrite_mapping_std
00277     else ss_rewrite_mapping_std,
00278   ss_csttl : rewrite_all_csttl([cst],ss_rewrite_mapping_std),
00279   ss_vars_l : append(cstt_vars_l(cst),rewrite_all_cstt_vars_l([cst], rm)),
00280   prop_csttl : prop_all_csttl(ss_csttl, ss_vars_l, ss_propagations),
00281   csttl2fcl(prop_csttl[1],prop_csttl[2],
00282     if box_tran = aes_small_box then
00283       ss_pi_translation_mapping
00284     else
00285       ss_ts_translation_mapping))$
00286 
00287 
00288 /**************************************************************
00289  * Special output formats                                     *
00290  **************************************************************
00291 */
00292 
00293 /* Generates a Dimacs CNF file and a file containing XOR clauses
00294    where together the files are a translation of the verification
00295    of the AES cipher specified by the given parameters.
00296 
00297    Inputs:
00298      n (string)
00299        The file to output the Dimacs CNF to.
00300      r (positive integer)
00301        The number of rounds in the AES variant to translate.
00302      ss_num_columns (positive integer)
00303        The number of columns in the AES variant block.
00304      ss_num_rows ({1,2,4})
00305        The number of rows in the AES variant block.
00306      ss_exp (positive integer)
00307        The exponent of the GF(2^ss_exp) finite field the AES variant
00308        is defined over.
00309      final_round_b (boolean)
00310        Whether or not the AES variant has a special final round consisting
00311        of only key addition, SubBytes and ShiftRows.
00312      box_tran ({aes_small_box, aes_ts_box, aes_rbase_box})
00313        How to translate the "small components" of the AES cipher to CNF:
00314        using the smallest known representation (aes_small_box), the canonical
00315        translation using new variables (aes_ts_box) or the smallest known
00316        r_1-base (aes_rbase_box).
00317      mc_tran
00318        How to translate the MixColumn operation of the AES cipher:
00319        translating the MixColumn in the encryption direction
00320        (aes_mc_forward), translating the MixColumn in the encryption and
00321        decryption direction (aes_mc_bidirectional), translating the
00322        MixColumn directly as a series of addition constraints at the
00323        bit-level (aes_mc_boolm), or translating the MixColumn operation
00324        as one box (aes_mc_box).
00325 
00326   Outputs:
00327     Two files are output:
00328       name
00329         A Dimacs CNF file containing the CNF translation of the AES cipher
00330         specified by the parameters, excluding any addition constraints
00331         generated by the translation.
00332       n_xor
00333         All addition constraints generated by the translation of the
00334         AES cipher specified by the parameters, given in the form
00335 
00336         x1 2 ... -n 0
00337 
00338         representing v_1 + ... + v_(n-1) = v_n (i.e., v_1, ..., -v_n as a
00339         whole have odd parity). This input format is supported by
00340         the cryptominisat solver, which has the additional command line
00341         option "--alsoread", allowing one to pass these XOR clauses to
00342         the solver from a separate file.
00343 */
00344 output_ss_fcl_wxor(name,r, ss_num_columns, ss_num_rows, ss_exp, final_round_b, box_tran, mc_tran) :=
00345 block(
00346   [ss_csttl : ss_csttl(r,ss_num_columns, ss_num_rows, ss_exp, final_round_b,mc_tran),
00347   ss_vars_l, prop_csttl, xor_csttl, FF],
00348   ss_vars_l : ss_cstt_vars_l(r,ss_num_columns,
00349       ss_num_rows, ss_exp, final_round_b,mc_tran),
00350   prop_csttl : prop_all_csttl(ss_csttl, ss_vars_l, ss_propagations),
00351   [xor_csttl,prop_csttl[1]] :
00352     partition_list(prop_csttl[1],lambda([a],is(cstt_name(a) = "ss_add_cst"))),
00353   FF : csttl2fcl(prop_csttl[1],prop_csttl[2],
00354     if box_tran = aes_small_box then
00355       ss_pi_translation_mapping
00356     else if box_tran = aes_rbase_box then
00357       ss_rbase_translation_mapping
00358     else
00359       ss_ts_translation_mapping),
00360   if oklib_monitor then print("Starting standardisation..."),
00361   FF_std : standardise_fcl(FF),
00362   xor_csttl : csttl_rename_vars(xor_csttl,FF_std[2],FF_std[1][1]),
00363   if oklib_monitor then print("Starting output of clauses..."),
00364   output_fcl_v(sconcat("Small Scale AES with ",
00365                  "r=",r,",c=",ss_num_columns,",rw=",ss_num_rows,
00366                  ",e=",ss_exp,",final=",final_round_b,
00367                  ",box_tran=",box_tran,",mc_tran=",mc_tran),
00368                FF_std[1],name,
00369     FF_std[2]),
00370   if oklib_monitor then print("Starting output of xor clauses..."),
00371   /* Each ss_add_cst constraint stands for nb additions of m variables
00372      where the (j+1)-th variable in the i-th addition is the (j*nb+i)-th
00373      variable in the ss_add_cst variable list. */
00374   with_stdout(sconcat(name,"_xor"),
00375     for cst in xor_csttl do block(
00376       [nb, m : if cstt_args_l(cst) = [] then 2 else cstt_args_l(cst)[1]],
00377       nb : floor(length(cst[2]) / (m+1)),
00378       for i : 1 thru nb do (
00379         print_nlb(
00380           sconcat("x ",
00381             lreduce(lambda([S,v],sconcat(S,v," ")),
00382               endcons(-cst[2][m*nb+i],
00383                 create_list(cst[2][j*nb + i],j,0,m-1)),"")," 0")))))
00384 )$
00385 
00386 
00387 /* Takes a partial assignment, along with small scale parameters
00388    and returns true if the partial assignment represents a valid
00389    small scale encryption using those parameters. */
00390 ss_validate(pa, r, ss_num_columns, ss_num_rows, ss_exp, final_round_b) :=
00391 block([block_size],
00392   block_size : ss_num_columns * ss_num_rows * ss_exp,
00393   P : ss_pa2matrix(pa, create_list(i,i,1,block_size),
00394     2, ss_exp, ss_polynomial(2,ss_exp), ss_num_rows),
00395   K : ss_pa2matrix(pa, create_list(i,i,block_size+1,2*block_size),
00396     2, ss_exp, ss_polynomial(2,ss_exp), ss_num_rows),
00397   C : ss_pa2matrix(pa, create_list(i,i,2*block_size+1,3*block_size),
00398     2, ss_exp, ss_polynomial(2,ss_exp), ss_num_rows),
00399   return(
00400     is(ss_encrypt(P,K,r,2,ss_exp) = C))
00401 )$
00402 
00403 
00404 /******************************************************************
00405  * Testing cryptographic properties                               *
00406  ******************************************************************
00407 */
00408 
00409 /* Outputs to file "name" a CNF which is satisfiable iff the AES cipher
00410    specified by input parameters has at least one key K and at least one
00411    plaintext P, such that the plaintext encrypted with K yields P. */
00412 output_ss_fcl_id_p(name,r, ss_num_columns, ss_num_rows, ss_exp, final_round_b, box_tran, mc_tran) :=
00413   block([FF, FF_std,block_size : ss_num_columns * ss_num_rows * ss_exp],
00414     if oklib_monitor then print("Starting translation..."),
00415     FF : ss_fcl(r, ss_num_columns, ss_num_rows, ss_exp, final_round_b, box_tran, mc_tran),
00416     FF : [append(
00417             take_elements(2*block_size,FF[1]), /* Plaintext + Key */
00418             rest(FF[1], 3*block_size)), /* The rest of the variables */
00419           substitute_cl(FF[2],
00420             osm2hm(map("[",
00421                 rest(take_elements(3*block_size,FF[1]),2*block_size),
00422                 take_elements(block_size,FF[1]))))],
00423     if oklib_monitor then print("Starting standardisation..."),
00424     FF_std : standardise_fcl(FF),
00425     if oklib_monitor then print("Starting output..."),
00426     output_fcl_v(sconcat("Checking for key identical on single plaintext",
00427                    "for Small Scale AES with ",
00428                    "r=",r,",c=",ss_num_columns,",rw=",ss_num_rows,
00429                    ",e=",ss_exp,",final=",final_round_b,
00430                    ",box_tran=",box_tran,",mc_tran=",mc_tran),
00431                  FF_std[1],name,
00432       FF_std[2]))$  
00433 output_ss_fcl_id_p_std(r, ss_num_columns, ss_num_rows, ss_exp, final_round_b, box_tran, mc_tran) :=
00434   output_ss_fcl_id_p(
00435     sconcat("ssaes_id_p_r", r, "_c",ss_num_columns, "_rw",ss_num_rows,"_e",
00436       ss_exp,"_f",if final_round_b then 1 else 0, ".cnf"),
00437     r, ss_num_columns, ss_num_rows, ss_exp, final_round_b, box_tran, mc_tran)$
00438 
00439 
00440 /******************************************************************
00441  * Statistics                                                     *
00442  ******************************************************************
00443 */
00444 
00445 /* Given the appropriate parameters, computes the number of sboxes
00446    in the associated small scale AES. The parameters are the number
00447    of rounds, and the number of columns and rows in the block. */
00448 nsbox_ss(r,num_columns,num_rows) :=
00449   (r*num_columns*num_rows) + (r * num_rows)$
00450 
00451 /* Given the appropriate parameters, computes the number of multiplications
00452    by the finite field element e (given as a polynomial) in the associated
00453    small scale AES. The parameters are the field element, given as a
00454    polynomial, number of rounds, and the number of columns, the small scale
00455    exponent, the mixcolumns matrix, whether or not to use a special final
00456    round (true/false) and the MixColumns translation to use (aes_mc_forward or
00457    aes_mc_bidirectional). */
00458 nmul_ss_gen(e,r,num_cols,ss_exp,mixcolumns_matrix, final_round_b, mc_trans) :=
00459 block([inv_mixcolumns_matrix, nmul, nmul_inv],
00460   inv_mixcolumns_matrix :
00461     ss_mixcolumns_matrix2inv_mixcolumns_matrix(2,ss_exp,mixcolumns_matrix),
00462   nmul : length(sublist(m2l_r(mixcolumns_matrix), lambda([a],is(a=e)))),
00463   if mc_trans = aes_mc_bidirectional then
00464     nmul_inv :
00465       length(sublist(m2l_r(inv_mixcolumns_matrix), lambda([a],is(a=e))))
00466   else nmul_inv : 0,
00467   if final_round_b then r : r -1,
00468   return(r * (nmul + nmul_inv) * num_cols))$
00469 nmul_ss(e,r,num_cols, num_rows,ss_exp, final_round_b, mc_trans) :=
00470   nmul_ss_gen(e,r,num_cols,ss_exp,
00471     ss_mixcolumns_matrix(2,ss_exp,num_rows), final_round_b, mc_trans)$
00472 /* Returns a set-map mapping field elements to the number of multiplications
00473    by those field elements in the AES translation specified by the arguments.
00474 */
00475 nmul_ss_gen_sm(r,num_cols,ss_exp,mixcolumns_matrix, final_round_b, mc_trans) :=
00476 block([inv_mixcolumns_matrix],
00477   inv_mixcolumns_matrix :
00478     ss_mixcolumns_matrix2inv_mixcolumns_matrix(2,ss_exp,mixcolumns_matrix),
00479   if final_round_b and r = 1 then []
00480   else setify(
00481     map(lambda([e],[e,
00482         nmul_ss_gen(e,r,num_cols,ss_exp,mixcolumns_matrix,
00483           final_round_b, mc_trans)]),
00484       append(m2l_r(mixcolumns_matrix),
00485         if mc_trans = aes_mc_bidirectional then m2l_r(inv_mixcolumns_matrix)
00486         else []))))$
00487 nmul_ss_sm(r,num_cols,ss_exp, final_round_b, mc_trans) :=
00488   nmul_ss_gen_sm(r,num_cols,ss_exp,
00489     ss_mixcolumns_matrix(2, ss_exp, num_cols),final_round_b, mc_trans)$
00490 
00491 
00492 /* Takes the number of rounds, number of columns, exponent of the field,
00493    the mixcolumns matrix, whether or not there is a special final round and
00494    which MixColumns translation to use and returns a set-map with elements
00495    of the form [n,m] where m is the number of boolean additions of arity n
00496    in the AES translation generated by ss_cstl with the provided input
00497    parameters.
00498 
00499    For example, a + b + c + d = e where a,b,c,d and e are boolean variables
00500    would be a boolean addition of arity four.
00501 
00502    Note that this function currently assumes that the MixColumns matrix,
00503    in the AES cipher specified by the parameters, doesn't contain a 0.
00504    This is the case for all currently used MixColumns matrices. */
00505 nadd_ss_sm(r,num_cols, num_rows, ss_exp, final_round_b, mc_trans) :=
00506   block([m: if mc_trans = aes_mc_bidirectional then 2 else 1,
00507     r_w_mc : if final_round_b then r-1 else r,
00508     block_size : num_cols * num_rows * ss_exp],
00509   if num_rows = 2 and num_cols = 1 then
00510     {[2, block_size * (r+1) + ss_exp*r + (num_cols-1) * num_rows*ss_exp*r +
00511     num_rows*num_cols*r_w_mc*m*ss_exp]}
00512   else if num_rows = 3 and num_cols = 1 and final_round_b and r = 1 then
00513     {[2, block_size * (r+1) + ss_exp*r]}
00514   else if num_rows = 3 and num_cols = 1 then
00515     {[2, block_size * (r+1) + ss_exp*r], /* Round keys and key schedule */
00516      [3,num_rows*num_cols*r_w_mc*m*ss_exp]} /* MixColumns */
00517   else if num_rows = 2 then
00518     {[2, block_size * (r+1) + num_rows*num_cols*r_w_mc*m*ss_exp +
00519       ((num_cols-1) * num_rows + (num_rows-1))*ss_exp*r],
00520       /* Round keys, MixColumns and some of the key schedule */
00521     [3,ss_exp*r]} /* Key Schedule */
00522   else if num_rows = 3 then
00523       {[2, block_size * (r+1) +
00524        ((num_cols-1) * num_rows + (num_rows-1))*ss_exp*r],
00525        /* Round keys, and some of the key schedule */
00526       [3,r*ss_exp+num_rows*num_cols*r_w_mc*m*ss_exp]}
00527       /* Key Schedule and MixColumns */
00528   else if num_cols = 1 and final_round_b and r = 1 then
00529     {[2, block_size * (r+1) + ss_exp*r]}
00530   else if num_cols = 1 then
00531     {[2, block_size * (r+1) + ss_exp*r],
00532     [num_rows,num_rows*num_cols*r_w_mc*m*ss_exp]} /* MixColumns */
00533   else if final_round_b and r = 1 then
00534     {[2, (block_size) * (r+1) +
00535      ((num_cols-1) * num_rows + (num_rows-1))*ss_exp*r],
00536      /* Round Keys, and some of key schedule */
00537     [3,r*ss_exp]} /* Key Schedule*/
00538   else
00539     {[2, (block_size) * (r+1) +
00540      ((num_cols-1) * num_rows + (num_rows-1))*ss_exp*r],
00541     [3,r*ss_exp],
00542     [num_rows,num_rows*num_cols*r_w_mc*m*ss_exp]})$
00543 nadd_ss(r,num_cols,num_rows,ss_exp, final_round_b, mc_trans) :=
00544   sum_l(listify(map(second,
00545       nadd_ss_sm(r,num_cols,num_rows,ss_exp, final_round_b, mc_trans))))$
00546 
00547 /* Takes the number of rounds and returns the number of constants which appear
00548    as "ss_const" constraints in the AES translation. */
00549 nconstants_ss(r) := r$
00550 
00551 
00552 /* Given the appropriate parameters, computes the number of variables
00553    in the small scale AES clause-list translation.
00554 
00555    The parameters are the number of rounds, the number of columns, the small
00556    scale exponent, the mixcolumns matrix to use, the number of variables
00557    introduced by the sbox CNF translation, a list-map from the field elements
00558    in the mixcolumns to the number of variables introduced in the CNF
00559    translation of each multiplication, whether or not to use a special
00560    final round, and whether to include the MixColumns inversion or not
00561    (aes_mc_forward vs aes_mc_bidirectional). */
00562 nvar_ss_gen(r,num_cols,num_rows,ss_exp,mixcolumns_matrix,
00563             num_sbox_vars,num_mul_vars_map,final_round_b,mc_trans) :=
00564 block([mul_h : osm2hm(num_mul_vars_map), block_size],
00565   block_size : num_cols * num_rows * ss_exp,
00566   if final_round_b then
00567     return(
00568       (block_size * 3) + /* Input */
00569       (2 * r * block_size) + /* AES constraint (round keys + output) */
00570       ((r-1) * 2 * block_size) + /* Normal rounds */
00571       block_size + /* Normal rounds */
00572       (r * num_cols * num_rows * num_sbox_vars) + /* Subbytes - sboxes */
00573       sum_l(map(lambda([e],ev_hm_d(mul_h,e,0) +
00574             if e # 0 and e # 1 then ss_exp else 0),
00575           m2l_r(mixcolumns_matrix))) * num_cols * (r-1) +
00576       /* MixColumns - forward */
00577       (if mc_trans = aes_mc_bidirectional then
00578         sum_l(map(lambda([e],ev_hm_d(mul_h,e,0) +
00579               if e # 0 and e # 1 then ss_exp else 0),
00580             m2l_r(ss_mixcolumns_matrix2inv_mixcolumns_matrix(
00581                 2,ss_exp,mixcolumns_matrix)))) else 0) * num_cols * (r-1) +
00582       /* MixColumns - inv */
00583       ((ss_exp * r) + (num_rows * r * (ss_exp + num_sbox_vars)))
00584       /* Key Schedule */)
00585   else
00586     return(
00587       (block_size * 3) + /* Input */
00588       (2 * r * block_size) + /* AES constraint (round keys + output) */
00589       (2 * r * block_size) + /* Normal rounds */
00590       (r * num_cols * num_rows * num_sbox_vars) + /* Subbytes - sboxes */
00591       sum_l(map(lambda([e],ev_hm_d(mul_h,e,0) +
00592             if e # 0 and e # 1 then ss_exp else 0),
00593           m2l_r(mixcolumns_matrix))) * num_cols * r +
00594       /* MixColumns - forward */
00595       (if mc_trans = aes_mc_bidirectional then
00596         sum_l(map(lambda([e],ev_hm_d(mul_h,e,0) +
00597               if e # 0 and e # 1 then ss_exp else 0),
00598             m2l_r(ss_mixcolumns_matrix2inv_mixcolumns_matrix(
00599                 2,ss_exp,mixcolumns_matrix)))) else 0) * num_cols * r +
00600       /* MixColumns - inv */
00601       ((ss_exp * r) + (num_rows * r * (ss_exp + num_sbox_vars)))
00602       /* Key Schedule */))$
00603 nvar_ss(r,num_cols,num_rows,ss_exp,final_round_b,box_tran,mc_trans) :=
00604   if box_tran = aes_small_box then
00605     nvar_ss_gen(r,num_cols,num_rows,ss_exp,
00606         ss_mixcolumns_matrix(2,ss_exp,num_rows),
00607         nvar_fcs(ev_hm(ss_sbox_cnfs,ss_exp))-(2*ss_exp),
00608         create_list(
00609           [nat2poly(e,2),
00610           nvar_fcs(ev_hm_d(ss_field_cnfs,[ss_exp,e],[{},{}]))-2*ss_exp],
00611           e,2,2^ss_exp-1),
00612         final_round_b, mc_trans)
00613   else if box_tran = aes_rbase_box then
00614     nvar_ss_gen(r,num_cols,num_rows,ss_exp,
00615         ss_mixcolumns_matrix(2,ss_exp,num_rows),
00616         nvar_list_fcs(ev_hm(ss_sbox_rbase_cnfs,ss_exp))-(2*ss_exp),
00617         create_list(
00618           [nat2poly(e,2),
00619            nvar_fcs(ev_hm_d(ss_field_rbase_cnfs,[ss_exp,e],[{},{}]))
00620              -(2*ss_exp)],
00621           e,2,2^ss_exp-1),
00622         final_round_b, mc_trans)
00623   else
00624     nvar_ss_gen(r,num_cols,num_rows,ss_exp,
00625         ss_mixcolumns_matrix(2,ss_exp,num_rows),
00626         nvar_full_dualts(2*ss_exp,2^ss_exp)-(2*ss_exp),
00627         create_list(
00628           [nat2poly(e,2), nvar_full_dualts(2*ss_exp,2^ss_exp)-(2*ss_exp)],
00629           e,2,2^ss_exp-1),
00630         final_round_b, mc_trans)$
00631 
00632 /* Given the appropriate parameters, computes the number of clauses
00633    in the small scale AES clause-list translation.
00634 
00635    The parameters are the number of rounds, the number of columns, the small
00636    scale exponent, the mixcolumns matrix to use, the number of variables
00637    introduced by the sbox CNF translation, a list-map from the field elements
00638    in the mixcolumns to the number of variables introduced in the CNF
00639    translation of each multiplication, whether or not to use a special
00640    final round, and whether to include the MixColumns inversion or not
00641    (aes_mc_forward vs aes_mc_bidirectional). */
00642 ncl_ss_gen(r,num_cols,num_rows,ss_exp,mixcolumns_matrix,
00643             num_sbox_cl,num_mul_cl_map,final_round_b,mc_trans) :=
00644 block([mul_h : osm2hm(num_mul_cl_map), block_size],
00645   block_size : num_cols * num_rows * ss_exp,
00646   if final_round_b then
00647     return(
00648       4 * block_size * (r+1) + /* Addition constraints (binary) */
00649       (r * num_cols * num_rows * num_sbox_cl) + /* Subbytes - sboxes */
00650       sum_l(map(lambda([e],ev_hm_d(mul_h,e,0)),
00651           m2l_r(mixcolumns_matrix))) * num_cols * (r-1) +
00652       sum_l(map(lambda([R], 2^length(sublist(R,lambda([e],is(e#0))))),
00653         args(mixcolumns_matrix))) * ss_exp * num_cols * (r-1) +
00654       /* MixColumns - forward */
00655       (if mc_trans = aes_mc_bidirectional then
00656         sum_l(map(lambda([e],ev_hm_d(mul_h,e,0)),
00657             m2l_r(ss_mixcolumns_matrix2inv_mixcolumns_matrix(
00658                 2,ss_exp,mixcolumns_matrix)))) else 0) * num_cols * (r-1) +
00659       (if mc_trans = aes_mc_bidirectional then
00660         sum_l(map(lambda([R], 2^length(sublist(R,lambda([e],is(e#0))))),
00661           args(ss_mixcolumns_matrix2inv_mixcolumns_matrix(
00662                 2,ss_exp,mixcolumns_matrix)))) else 0) * ss_exp * num_cols * (r-1) +
00663       /* MixColumns - inv */
00664       ((ss_exp * r) + (num_rows * r * num_sbox_cl)) +
00665       if num_cols > 1 then
00666         ((num_rows * (num_cols-1) * 4) + ((num_rows-1) * 4) + 8) * ss_exp * r
00667       else
00668         ((num_cols-1) * num_rows + 1) * 4 * ss_exp * r
00669       /* Key Schedule */)
00670   else
00671     return(
00672       4 * block_size * (r+1) + /* Addition constraints (binary) */
00673       (r * num_cols * num_rows * num_sbox_cl) + /* Subbytes - sboxes */
00674       sum_l(map(lambda([e],ev_hm_d(mul_h,e,0)),
00675           m2l_r(mixcolumns_matrix))) * num_cols * r +
00676       sum_l(map(lambda([R], 2^length(sublist(R,lambda([e],is(e#0))))),
00677         args(mixcolumns_matrix))) * ss_exp * num_cols * r +
00678       /* MixColumns - forward */
00679       (if mc_trans = aes_mc_bidirectional then
00680         sum_l(map(lambda([e],ev_hm_d(mul_h,e,0)),
00681             m2l_r(ss_mixcolumns_matrix2inv_mixcolumns_matrix(
00682                 2,ss_exp,mixcolumns_matrix)))) else 0) * num_cols * r +
00683       (if mc_trans = aes_mc_bidirectional then
00684         sum_l(map(lambda([R], 2^length(sublist(R,lambda([e],is(e#0))))),
00685           args(ss_mixcolumns_matrix2inv_mixcolumns_matrix(
00686                 2,ss_exp,mixcolumns_matrix)))) else 0) * ss_exp * num_cols * r +
00687       /* MixColumns - inv */
00688       ((ss_exp * r) + (num_rows * r * num_sbox_cl)) +
00689       if num_cols > 1 then
00690         ((num_rows * (num_cols-1) * 4) + ((num_rows-1) * 4) + 8) * ss_exp * r
00691       else
00692         ((num_cols-1) * num_rows + 1) * 4 * ss_exp * r
00693       /* Key Schedule */))$
00694 ncl_ss(r,num_cols,num_rows,ss_exp,final_round_b,box_tran,mc_trans) :=
00695   if box_tran = aes_small_box then
00696     ncl_ss_gen(r,num_cols,num_rows,ss_exp,
00697         ss_mixcolumns_matrix(2,ss_exp,num_rows),
00698         ncl_fcs(ev_hm(ss_sbox_cnfs,ss_exp)),
00699         create_list(
00700           [nat2poly(e,2), ncl_fcs(ev_hm_d(ss_field_cnfs,[ss_exp,e],[{},{}]))],
00701           e,2,2^ss_exp-1),
00702         final_round_b, mc_trans)
00703   else if box_tran = aes_rbase_box then
00704     ncl_ss_gen(r,num_cols,num_rows,ss_exp,
00705         ss_mixcolumns_matrix(2,ss_exp,num_rows),
00706         ncl_list_fcs(ev_hm(ss_sbox_rbase_cnfs,ss_exp)),
00707         create_list(
00708           [nat2poly(e,2),
00709           ncl_fcs(ev_hm_d(ss_field_rbase_cnfs,[ss_exp,e],[{},{}]))],
00710           e,2,2^ss_exp-1),
00711         final_round_b, mc_trans)
00712   else
00713     ncl_ss_gen(r,num_cols,num_rows,ss_exp,
00714         ss_mixcolumns_matrix(2,ss_exp,num_rows),
00715         ncl_full_dualts(2*ss_exp,2^ss_exp),
00716         create_list(
00717           [nat2poly(e,2), ncl_full_dualts(2*ss_exp,2^ss_exp)],
00718           e,2,2^ss_exp-1),
00719         final_round_b, mc_trans)$
00720 
00721 /* Given the appropriate parameters, computes the number of clauses
00722    of each length in the small scale AES clause-list translation, returning
00723    the result as a list of pairs with the first element of each pair
00724    being the size of the clause, and the second being the number of clauses
00725    of that size in the translation.
00726 
00727    The parameters are the number of rounds, the number of columns, the number
00728    of rows, the small scale exponent, the mixcolumns matrix to use, the number
00729    of variables introduced by the sbox CNF translation, a list-map from the
00730    field elements in the MixColumns to the number of variables introduced in
00731    the CNF translation of each multiplication, whether or not to use a special
00732    final round, and whether to include the MixColumns inversion or not
00733    (aes_mc_forward vs aes_mc_bidirectional). */
00734 ncl_list_ss_gen(r,num_cols,num_rows,ss_exp,mixcolumns_matrix,
00735             ncl_list_sbox,ncl_list_mul_map,final_round_b,mc_trans) :=
00736 block([ncl_list_mul_h : sm2hm(ncl_list_mul_map)],
00737 multi_list_distribution2list_distribution(
00738   append(
00739     map(lambda([a],[a[1],nsbox_ss(r,num_cols,num_rows) * a[2]]),
00740         ncl_list_sbox),
00741     lappend(map(lambda([e],
00742           map(lambda([a], [a[1],a[2]*e[2]]),
00743             ev_hm_d(ncl_list_mul_h,e[1],[]))),
00744         listify(nmul_ss_gen_sm(r,num_cols,ss_exp,mixcolumns_matrix,
00745             final_round_b,mc_trans)))),
00746     [[1, nconstants_ss(r)*ss_exp]],
00747     map(lambda([P], [P[1]+1,2^(P[1]) * P[2]]),
00748       listify(nadd_ss_sm(r,num_cols,num_rows,ss_exp,final_round_b,mc_trans)))
00749     )))$
00750 ncl_list_ss(r,num_cols,num_rows,ss_exp,final_round_b,box_tran,mc_trans) :=
00751 block([mixcolumns_matrix : ss_mixcolumns_matrix(2,ss_exp,num_rows),
00752        inv_mixcolumns_matrix, mixcolumns_mult_l],
00753   inv_mixcolumns_matrix :
00754     ss_mixcolumns_matrix2inv_mixcolumns_matrix(2,ss_exp,mixcolumns_matrix),
00755   mixcolumns_mult_l :
00756     unique(append(m2l_r(mixcolumns_matrix),m2l_r(inv_mixcolumns_matrix))),
00757   mixcolumns_mult_l :
00758     sublist(mixcolumns_mult_l, lambda([a], is(a # 1) and is(a # 0))),
00759   if box_tran = aes_small_box then
00760     ncl_list_ss_gen(r,num_cols,num_rows,ss_exp,
00761         ss_mixcolumns_matrix(2,ss_exp,num_rows),
00762         ncl_list_fcs(ev_hm(ss_sbox_cnfs,ss_exp)),
00763         create_list(
00764           [e, ncl_list_fcs(
00765             ev_hm(ss_field_cnfs,[ss_exp,poly2nat(e,2)]))],
00766           e, mixcolumns_mult_l),
00767         final_round_b, mc_trans)
00768   else if box_tran = aes_rbase_box then
00769       ncl_list_ss_gen(r,num_cols,num_rows,ss_exp,
00770         ss_mixcolumns_matrix(2,ss_exp,num_rows),
00771         ncl_list_fcs(ev_hm(ss_sbox_rbase_cnfs,ss_exp)),
00772         create_list(
00773           [e, ncl_list_fcs(
00774             ev_hm(ss_field_rbase_cnfs,[ss_exp,poly2nat(e,2)]))],
00775           e, mixcolumns_mult_l),
00776         final_round_b, mc_trans)
00777   else
00778       ncl_list_ss_gen(r,num_cols,num_rows,ss_exp,
00779         ss_mixcolumns_matrix(2,ss_exp,num_rows),
00780         ncl_list_full_dualts(2*ss_exp,2^ss_exp),
00781         create_list(
00782           [e, ncl_list_full_dualts(2*ss_exp,2^ss_exp)],
00783           e, mixcolumns_mult_l),
00784         final_round_b, mc_trans))$
00785 
00786 
00787 /* Given the appropriate parameters returns basic statistics on
00788    the number of each component in the AES translation specified
00789    by the parameters.
00790 
00791    The result is of the form:
00792 
00793    [full_r,special_r,#round_sbox,#round_add,#mc_l,#ks_sbox,#ks_add,#ks_const]
00794 
00795    where:
00796       full_r       is the number of full rounds including MixColumns
00797       special_r    is the number of final rounds excluding MixColumns (0/1)
00798       #round_sbox  is the number of Sboxes occurring in the round components
00799       #round_add   is the number of round additions
00800       #mc_l        is a list of pairs mapping field elements to the number
00801                    of multiplications by those field elements that occur
00802                    in the translation (in the MixColumns operation)
00803       #ks_sbox     is the number of Sboxes occurring in the AES key expansion
00804       #ks_add      is the number of additions occurring in the AES key
00805                    expansion
00806       #ks_const    is the number of constant additions in the AES key
00807                    expansion
00808 
00809    The parameters are the number of rounds, the number of columns, the number
00810    of rows, the small scale exponent, the mixcolumns matrix to use, whether or
00811    not to use a special final round, and whether to include the MixColumns
00812    inversion or not (aes_mc_forward vs aes_mc_bidirectional). */
00813 component_statistics_ss_gen(r,num_cols,num_rows,ss_exp,mixcolumns_matrix,
00814   final_round_b,mc_trans) :=
00815 block([mc_r : if final_round_b then r-1 else r,
00816        mc_c : if mc_trans = aes_mc_bidirectional then 2 else 1],
00817   [
00818     mc_r,
00819     if final_round_b then 1 else 0,
00820     r * num_cols * num_rows,
00821     ss_exp*num_cols*num_rows*(r+1) + num_rows*num_cols*ss_exp*mc_r*mc_c,
00822     listify(nmul_ss_gen_sm(r,num_cols,ss_exp,mixcolumns_matrix,
00823       final_round_b, mc_trans)),
00824     num_rows * r,
00825     (if num_cols = 1 then 1 else num_rows) * ss_exp * r +
00826       (num_cols-1) * num_rows*ss_exp*r,
00827     ss_exp * r])$
00828 component_statistics_ss(r,num_cols,num_rows,ss_exp,final_round_b,mc_trans) :=
00829   component_statistics_ss_gen(r,num_cols,num_rows,ss_exp,
00830     ss_mixcolumns_matrix(2,ss_exp,num_rows),final_round_b,mc_trans)$
00831 
00832 
00833 /******************************************************************
00834  * Data translation                                               *
00835  ******************************************************************
00836 */
00837 
00838 /* AES data translation */
00839 
00840 /* TODO: Move such constants to constants (i.e. AES row size, column size etc). */
00841 
00842 output_aes_random_pc_pair(seed, num_rounds) :=
00843  /* Constants: AES uses the GF(2^8) field and has 4 columns and 4 rows.  */
00844  output_ss_random_pc_pair(seed, 2,8, ss_polynomial_2_8, 4, 4, num_rounds)$
00845 
00846 
00847 /* Takes a hexidecimal string in the notation typically used for Rijndael
00848    blocks (discussed in [Design of Rijndael] and in CryptoSystems plans), and,
00849    given the variable list (assumed to be in the correct left to right bit
00850    ordering), generates a PA to the given variables to the given constant: */
00851 aes_hex2pa(hex_s, var_l) :=
00852   setify(map(
00853            lambda([a,b], if b = 0 then -a else a),
00854            var_l,
00855            lappend(map(
00856                     lambda([a], egf_coeffs(rijn_bit_field,a,7)),
00857                     hex2gf2t8l(hex_s)))
00858   ))$
00859 
00860 /* Small scale data translation */
00861 
00862 ss_random_matrix(b,e,mod_poly, num_rows, num_cols) :=
00863     genmatrix(lambda([x,y], ss_stand(nat2poly(random(b^e),b),b,mod_poly)),
00864       num_rows, num_cols)$
00865 
00866 ss_matrix2pa(m,var_list,b,e,mod_poly) := block([nl, bits],
00867   nl : ss_m2natl(m,b),
00868   bits : lappend(map(lambda([a],int2polyadic_padd(a,b,e)), nl)),
00869   return(
00870     map(lambda([bit_,var_], if bit_ > 0 then var_ else -var_), bits,var_list))
00871   )$
00872 
00873 /* Assumes all of var_list occur as vars in lit_set in some form */
00874 ss_pa2matrix(lit_set, var_list,b,e,mod_poly, num_rows) := block([nl, bits],
00875   bits : map(lambda([a], if member(a,lit_set) then 1 else 0), var_list),
00876   nl : map(lambda([a], polyadic2int(a,b)),partition_elements(bits,e)),
00877   return(ss_natl2m(nl,b,num_rows)))$
00878 
00879 ss_pa2matrix_std(lit_set, e,num_rows, num_cols) :=
00880   ss_pa2matrix(lit_set,
00881     create_list(i,i,e*num_rows*num_cols+1,2*e*num_rows*num_cols),
00882     2,e,ss_polynomial(2,e),num_rows)$
00883 
00884 /* Outputs random plaintext, ciphertext pair as a clause-set with
00885    the associated unit-clauses, given the small scale parameters. */
00886 output_ss_random_pc_pair(seed, num_rounds, num_cols, num_rows,ss_exp, final_round_b) :=
00887   block(
00888     [s, plaintext, key, ciphertext, comment, filename, plaintext_vars,
00889      ciphertext_vars, pc_phi, pc_unit_fcs, b : 2,
00890      mod_poly : ss_polynomial(2,ss_exp)],
00891     s : make_random_state(seed),
00892     set_random_state(s),
00893     plaintext : ss_random_matrix(b,ss_exp,mod_poly,num_rows,num_cols),
00894     key : ss_random_matrix(b,ss_exp,mod_poly,num_rows, num_cols),
00895     if final_round_b then
00896       ciphertext : ss_encrypt_wf(plaintext, key, num_rounds, b,ss_exp)
00897     else
00898       ciphertext : ss_encrypt(plaintext, key, num_rounds, b,ss_exp),
00899     comment : sconcat(
00900       "S : ", seed, " ",
00901       "P : ", ss_matrix2hex(plaintext, b,ss_exp,mod_poly), " ",
00902       "K : ", ss_matrix2hex(key, b,ss_exp,mod_poly)," ",
00903       "C : ", ss_matrix2hex(ciphertext, b,ss_exp,mod_poly), " ",
00904       "A : ", [b,ss_exp,mod_poly,num_rows,num_cols, num_rounds]),
00905     filename : sconcat(
00906       "ssaes_pcpair_r", num_rounds , "_c", num_cols, "_rw", num_rows, "_e",
00907       ss_exp,"_f", if final_round_b then 1 else 0,"_s", seed, ".cnf"),
00908     plaintext_vars : create_list(i,i,1, ss_exp * num_rows * num_cols),
00909     ciphertext_vars : create_list(i,i,
00910       2*ss_exp * num_rows * num_cols+1, 3*ss_exp * num_rows * num_cols),
00911     pc_phi : append(
00912       ss_matrix2pa(plaintext, plaintext_vars, b, ss_exp, mod_poly),
00913       ss_matrix2pa(ciphertext, ciphertext_vars, b, ss_exp, mod_poly)),
00914     pc_unit_fcs : [setify(create_list(i,i,1, 3*ss_exp * num_rows * num_cols)),
00915                    setify(map(set, pc_phi))],
00916     output_fcs(comment, pc_unit_fcs, filename))$
00917 output_ss_random_pk_pair(seed, num_rounds, num_cols, num_rows,ss_exp, final_round_b) :=
00918   block(
00919     [s, plaintext, key, ciphertext, comment, filename, plaintext_vars,
00920      ciphertext_vars, pc_phi, pc_unit_fcs, b : 2,
00921      mod_poly : ss_polynomial(2,ss_exp)],
00922     s : make_random_state(seed),
00923     set_random_state(s),
00924     plaintext : ss_random_matrix(b,ss_exp,mod_poly,num_rows,num_cols),
00925     key : ss_random_matrix(b,ss_exp,mod_poly,num_rows, num_cols),
00926     if final_round_b then
00927       ciphertext : ss_encrypt_wf(plaintext, key, num_rounds, b,ss_exp)
00928     else
00929       ciphertext : ss_encrypt(plaintext, key, num_rounds, b,ss_exp),
00930     comment : sconcat(
00931       "S : ", seed, " ",
00932       "P : ", ss_matrix2hex(plaintext, b,ss_exp,mod_poly), " ",
00933       "K : ", ss_matrix2hex(key, b,ss_exp,mod_poly)," ",
00934       "C : ", ss_matrix2hex(ciphertext, b,ss_exp,mod_poly), " ",
00935       "A : ", [b,ss_exp,mod_poly,num_rows,num_cols, num_rounds]),
00936     filename : sconcat(
00937       "ssaes_pkpair_r", num_rounds , "_c", num_cols, "_rw", num_rows, "_e",
00938       ss_exp,"_f", if final_round_b then 1 else 0,"_s", seed, ".cnf"),
00939     plaintext_vars : create_list(i,i,1, ss_exp * num_rows * num_cols),
00940     key_vars : create_list(i,i,
00941       ss_exp * num_rows * num_cols+1, 2*ss_exp * num_rows * num_cols),
00942     pc_phi : append(
00943       ss_matrix2pa(plaintext, plaintext_vars, b, ss_exp, mod_poly),
00944       ss_matrix2pa(key, key_vars, b, ss_exp, mod_poly)),
00945     pc_unit_fcs : [setify(create_list(i,i,1, 3*ss_exp * num_rows * num_cols)),
00946                    setify(map(set, pc_phi))],
00947     output_fcs(comment, pc_unit_fcs, filename))$
00948 output_ss_random_kc_pair(seed, num_rounds, num_cols, num_rows,ss_exp, final_round_b) :=
00949   block(
00950     [s, plaintext, key, ciphertext, comment, filename, plaintext_vars,
00951      ciphertext_vars, pc_phi, pc_unit_fcs, b : 2,
00952      mod_poly : ss_polynomial(2,ss_exp)],
00953     s : make_random_state(seed),
00954     set_random_state(s),
00955     plaintext : ss_random_matrix(b,ss_exp,mod_poly,num_rows,num_cols),
00956     key : ss_random_matrix(b,ss_exp,mod_poly,num_rows, num_cols),
00957     if final_round_b then
00958       ciphertext : ss_encrypt_wf(plaintext, key, num_rounds, b,ss_exp)
00959     else
00960       ciphertext : ss_encrypt(plaintext, key, num_rounds, b,ss_exp),
00961     comment : sconcat(
00962       "S : ", seed, " ",
00963       "P : ", ss_matrix2hex(plaintext, b,ss_exp,mod_poly), " ",
00964       "K : ", ss_matrix2hex(key, b,ss_exp,mod_poly)," ",
00965       "C : ", ss_matrix2hex(ciphertext, b,ss_exp,mod_poly), " ",
00966       "A : ", [b,ss_exp,mod_poly,num_rows,num_cols, num_rounds]),
00967     filename : sconcat(
00968       "ssaes_kcpair_r", num_rounds , "_c", num_cols, "_rw", num_rows, "_e",
00969       ss_exp,"_f", if final_round_b then 1 else 0,"_s", seed, ".cnf"),
00970     ciphertext_vars : create_list(i,i,
00971       2*ss_exp * num_rows * num_cols+1, 3*ss_exp * num_rows * num_cols),
00972     key_vars : create_list(i,i,
00973       ss_exp * num_rows * num_cols+1, 2*ss_exp * num_rows * num_cols),
00974     pc_phi : append(
00975       ss_matrix2pa(plaintext, key_vars, b, ss_exp, mod_poly),
00976       ss_matrix2pa(key, ciphertext_vars, b, ss_exp, mod_poly)),
00977     pc_unit_fcs : [setify(create_list(i,i,1, 3*ss_exp * num_rows * num_cols)),
00978                    setify(map(set, pc_phi))],
00979     output_fcs(comment, pc_unit_fcs, filename))$
00980 
00981 
00982 /******************************************************************************
00983  * Global propagation                                                         *
00984  ******************************************************************************
00985 */
00986 
00987 aes_propagations : [prop_eq_csttl]$
00988 ss_propagations : [prop_eq_csttl]$
00989 
00990 
00991 /******************************************************************************
00992  * CNF translations                                                           *
00993  ******************************************************************************
00994 */
00995 
00996 /* AES */
00997 
00998 /* Translation mapping, mapping constraint templates to the corresponding
00999    translation functions where constraints are translated to CNF clause-set
01000    representations using subsets of the prime implicates: */
01001 aes_pi_translation_mapping : [
01002   ["aes_add_cst", [aes_add_cst_cl, lambda([[a]],[])]],
01003   ["const_cst", [aes_const_cst_cl, lambda([[a]],[])]],
01004   ["aes_mul2_cst", [aes_mul2_pi_cst_cl, lambda([[a]],[])]],
01005   ["aes_mul3_cst", [aes_mul3_pi_cst_cl, lambda([[a]],[])]],
01006   ["aes_mul14_cst", [aes_mul14_pi_cst_cl, lambda([[a]],[])]],
01007   ["aes_mul13_cst", [aes_mul13_pi_cst_cl, lambda([[a]],[])]],
01008   ["aes_mul11_cst", [aes_mul11_pi_cst_cl, lambda([[a]],[])]],
01009   ["aes_mul9_cst", [aes_mul9_pi_cst_cl, lambda([[a]],[])]],
01010   ["aes_sbox_cst", [aes_sbox_pi_cst_cl, lambda([[a]],[])]]]$
01011 
01012 /* Translation mapping, mapping constraint templates to the corresponding
01013    translation functions where constraints are translated to representations
01014    using subsets of the prime implicates: */
01015 aes_ts_translation_mapping : [
01016   ["aes_add_cst", [aes_add_cst_cl, lambda([[a]],[])]],
01017   ["const_cst", [aes_const_cst_cl, lambda([[a]],[])]],
01018   ["aes_mul2_cst", [aes_mul2_ts_cst_cl, aes_mul2_ts_var_l]],
01019   ["aes_mul3_cst", [aes_mul3_ts_cst_cl, aes_mul3_ts_var_l]],
01020   ["aes_mul14_cst", [aes_mul14_ts_cst_cl, aes_mul14_ts_var_l]],
01021   ["aes_mul13_cst", [aes_mul13_ts_cst_cl, aes_mul13_ts_var_l]],
01022   ["aes_mul11_cst", [aes_mul11_ts_cst_cl, aes_mul11_ts_var_l]],
01023   ["aes_mul9_cst", [aes_mul9_ts_cst_cl, aes_mul9_ts_var_l]],
01024   ["aes_sbox_cst", [aes_sbox_ts_cst_cl, aes_sbox_ts_var_l]]]$
01025 
01026 /* Small Scale */
01027 
01028 /* Translation mapping, mapping constraint templates to the corresponding
01029    translation functions where constraints are translated to CNF clause-set
01030    representations using subsets of the prime implicates: */
01031 ss_pi_translation_mapping : [
01032   ["ss_add_cst", [aes_add_cst_cl, lambda([[a]],[])]],
01033   ["const_cst", [aes_const_cst_cl, lambda([[a]],[])]],
01034   ["ss_mul_cst", [ss_mul_pi_cst_cl, lambda([[a]],[])]],
01035   ["ss_sbox_w_mul_cst", [ss_sbox_w_mul_pi_cst_cl, lambda([[a]],[])]],
01036   ["ss_sbox_cst", [ss_sbox_pi_cst_cl, lambda([[a]],[])]],
01037   ["ss_round_column_cst",
01038     [ss_round_column_pi_cst_cl, lambda([a],[])]]]$
01039 
01040 /* Translation mapping, mapping constraint templates to the corresponding
01041    translation functions where constraints are translated to CNF clause-set
01042    representations using r_1 bases: */
01043 ss_rbase_translation_mapping : [
01044   ["ss_add_cst", [aes_add_cst_cl, lambda([[a]],[])]],
01045   ["const_cst", [aes_const_cst_cl, lambda([[a]],[])]],
01046   ["ss_mul_cst", [ss_mul_rbase_cst_cl, lambda([[a]],[])]],
01047   ["ss_sbox_w_mul_cst", [ss_sbox_w_mul_rbase_cst_cl, lambda([[a]],[])]],
01048   ["ss_sbox_cst", [ss_sbox_rbase_cst_cl, lambda([[a]],[])]],
01049   ["ss_round_column_cst",
01050     [ss_round_column_rbase_cst_cl, lambda([a],[])]]]$
01051 
01052 /* Translation mapping, mapping constraint templates to the corresponding
01053    translation functions where constraints are translated to representations
01054    using the canonical translation: */
01055 ss_ts_translation_mapping : [
01056   ["ss_add_cst", [aes_add_cst_cl, lambda([[a]],[])]],
01057   ["const_cst", [aes_const_cst_cl, lambda([[a]],[])]],
01058   ["ss_mul_cst", [ss_mul_ts_cst_cl, ss_mul_ts_var_l]],
01059   ["ss_sbox_cst", [ss_sbox_ts_cst_cl, ss_sbox_ts_var_l]],
01060   ["ss_sbox_w_mul_cst", [ss_sbox_w_mul_ts_cst_cl, ss_sbox_w_mul_ts_var_l]],
01061   ["ss_round_column_cst",
01062     [ss_round_column_ts_cst_cl, ss_round_column_ts_var_l]],
01063   ["ss_mixcolumn_cst", [ss_mixcolumn_ts_cst_cl, ss_mixcolumn_ts_var_l]]]$
01064 
01065 /* Translation mapping, mapping constraint templates to the corresponding
01066    translation functions where constraints are translated to representations
01067    using the canonical CNF: */
01068 ss_full_translation_mapping : [
01069   ["ss_add_cst", [aes_add_cst_cl, lambda([[a]],[])]],
01070   ["const_cst", [aes_const_cst_cl, lambda([[a]],[])]],
01071   ["ss_mul_cst", [ss_mul_full_cst_cl, lambda([[a]],[])]],
01072   ["ss_sbox_cst", [ss_sbox_full_cst_cl, lambda([[a]],[])]],
01073   ["ss_sbox_w_mul_cst", [ss_sbox_w_mul_full_cst_cl, lambda([[a]],[])]],
01074   ["ss_round_column_cst",
01075     [ss_round_column_full_cst_cl, lambda([[a]],[])]],
01076   ["ss_mixcolumn_cst", [ss_mixcolumn_full_cst_cl, lambda([[a]],[])]]]$
01077