OKlibrary  0.2.1.6
ConstraintTemplateRewriteRules.mac
Go to the documentation of this file.
00001 /* Matthew Gwynne, 28.9.2010 (Swansea) */
00002 /* Copyright 2010, 2011, 2013 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/Cryptology/Lisp/CryptoSystems/Rijndael/AdvancedEncryptionStandard.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/ConstraintTemplateRewriteSystem.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/Translations.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/data/SboxCNF.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/FiniteFunctions/Permutations.mac")$
00028 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/LinearEquations.mac")$
00029 
00030 
00046 /* ***********************************************
00047    * Constraint template rewrite translation     *
00048    ***********************************************
00049 */
00050 
00051 /* The translation system given below is designed to replace the above
00052    translation system in it's entirety but must be introduced piecewise,
00053    with appropriate tests. */
00054 
00055 /* AES variables - aes_v(i,id) */
00056 /* id here is used as an identifier such as "ks" for key schedule bits, "o"
00057    for output bits etc. */
00058 /* These are used throughout for all AES constraint templates */
00059 kill(aes_v)$
00060 declare(aes_v, noun)$
00061 declare(aes_v, posfun)$
00062 aes_var(i,id) := nounify(aes_v)(i,id)$
00063 
00064 /* Given two integers n and m, a namespace, and
00065    a noun identifier, returns a list of AES variables of the form
00066    aes_v(i,id) for n <= i <= m. */
00067 generate_aes_constraint_vars(n,m,namespace, id) :=
00068   create_list(namespace(aes_var(i,id)),i,n,m)$
00069 
00070 aes_rewrite_mapping_std :
00071   [["aes_cst",aes_cstrb],["aes_key_expansion_cst",aes_key_expansion_cstrb],
00072   ["aes_round_cst",aes_round_cstrb],
00073   ["aes_final_round_cst",aes_final_round_cstrb],
00074   ["aes_subbytes_cst",aes_subbytes_cstrb],
00075   ["aes_shiftrows_cst",aes_shiftrows_cstrb],
00076   ["aes_mixcolumns_cst",aes_mixcolumns_cstrb],
00077   ["aes_mixcolumn_cst",aes_mixcolumn_cstrb]]$
00078 
00079 aes_bimc_rewrite_mapping_std :
00080   [["aes_cst",aes_cstrb],["aes_key_expansion_cst",aes_key_expansion_cstrb],
00081   ["aes_round_cst",aes_round_cstrb],
00082   ["aes_final_round_cst",aes_final_round_cstrb],
00083   ["aes_subbytes_cst",aes_subbytes_cstrb],
00084   ["aes_shiftrows_cst",aes_shiftrows_cstrb],
00085   ["aes_mixcolumns_cst",aes_mixcolumns_cstrb],
00086   ["aes_mixcolumn_cst",aes_bi_mixcolumn_cstrb]]$
00087 
00088 
00089 /* ***********************************************
00090    * Constraint template rewrite functions       *
00091    ***********************************************
00092 */
00093 
00094 /* AES constraint rewrite bundle */
00095 aes_cstrb : [aes_cstr_cstl,aes_namespace,aes_ns_var_l]$
00096 
00097 /* Namespace */
00098 kill(aes_ctr_ns)$
00099 declare(aes_ctr_ns,noun)$
00100 declare(aes_ctr_ns,posfun)$
00101 aes_namespace([args]) := apply(nounify(aes_ctr_ns),args)$
00102 
00103 
00104 /* Returns a list of the variables introduced when
00105    applying aes_ctr_ctl given the auxiliary parameter
00106    list arg_l, under the given rewrite_mapping.
00107 
00108    For example, given the constraint template instance
00109 
00110    aes_ct(1,...,384,arg_l)
00111 
00112    is rewritten using aes_ctr_ctl, under
00113    rewrite_mapping, the list of variables
00114    returned by this function are exactly those
00115    variables introduced by aes_ctr_ctl and
00116    any rewritten-subconstraints it introduces
00117    (mapped to the corresponding rewrite functions
00118    by variable mapping, that is, this function
00119    recursively generates such a variable list,
00120    based on sub-constraints it uses).
00121 */
00122 aes_ns_var_l(cst) := block(
00123   [aes_num_rounds,vars : [],namespace],
00124   namespace : cstt_namespace_new (aes_namespace,cst),
00125   aes_num_rounds : cst[3],
00126   vars : cons(
00127     generate_aes_constraint_vars(1,(aes_num_rounds+1)*128,
00128       namespace,nounify(k)),vars),
00129   vars : cons(
00130     generate_aes_constraint_vars(1,aes_num_rounds*128,
00131       namespace,nounify(o)),vars),
00132   return(lappend(vars)))$
00133 /* Rewrite function designed to rewrite the AES constraint template "aes_ct".
00134 
00135    Takes as arguments 385 variables, which are the arguments of the "aes_ct"
00136    instance being rewritten.
00137 
00138    The first 384 of these are 128 plaintext, 128 key and 128 ciphertext
00139    variables respectively. The final argument is a pair (list) of auxiliary
00140    arguments, the first being the namespace to place all variables introduced
00141    by this function within, and the second being the integer number of rounds
00142    which specifies which round-variant of AES is being rewritten.
00143 
00144    The result of this function is a list of constraint template instances
00145    representing the AES constraint template instance being rewritten.
00146 */
00147 aes_cstr_cstl(cst) := block(
00148   [bits, pBits, kBits, cBits, ekBits, ib, ob, rs : [],namespace,
00149   aes_num_rounds],
00150   aes_num_rounds : cst[3],
00151   bits : cst[2],
00152   namespace : cstt_namespace_new(aes_namespace,cst),
00153   pBits : take_elements(128,bits),
00154   kBits : take_elements(128,rest(bits,128)),
00155   cBits : rest(bits,256),
00156   ekBits :
00157     generate_aes_constraint_vars(
00158       1,(aes_num_rounds+1)*128,namespace,nounify(k)),
00159   /* Key Expansion */
00160   rs : cons(
00161     cstt_new(
00162       "aes_key_expansion_cst",append(kBits,ekBits),[aes_num_rounds],namespace),
00163     rs),
00164   ib : pBits,
00165   all_ob :
00166     generate_aes_constraint_vars(1,(aes_num_rounds)*128,namespace,nounify(o)),
00167   ob : take_elements(128,all_ob),
00168   /* Initial Round Key Addition */
00169   rs : cons(
00170     cstt_new(
00171       "aes_add_cst",append(ib,take_elements(128,ekBits),ob),[],namespace),
00172     rs),
00173   ib : ob,
00174   /* Rounds */
00175   for j : 1 thru (aes_num_rounds - 1) do block(
00176     ob : take_elements(128,rest(all_ob,j*128)),
00177     rs : cons(
00178       cstt_new("aes_round_cst",
00179         append(ib,take_elements(128,rest(ekBits,j*128)),ob),
00180         [i], namespace),
00181       rs),
00182     ib : ob
00183   ),
00184   /* Final Round */
00185   /* If we have a variant with a reduced number of rounds, truncate rather
00186      than generalise */
00187   ob : cBits,
00188   if aes_num_rounds = 10 then 
00189     rs : cons(
00190       cstt_new("aes_final_round_cst",
00191         append(ib,take_elements(128,rest(ekBits,aes_num_rounds*128)),ob),
00192         [],namespace),
00193       rs)
00194   else
00195     rs : cons(
00196       cstt_new("aes_round_cst",
00197         append(ib,take_elements(128,rest(ekBits,aes_num_rounds*128)),ob),
00198         [aes_num_rounds],namespace),
00199       rs),
00200   return(rs)
00201 )$
00202 
00203 /*
00204    AES Round
00205 
00206 */
00207 
00208 aes_round_cstrb :
00209  [aes_round_cstr_cstl, aes_round_namespace, aes_round_ns_var_l]$
00210 
00211 /* AES round namespace */
00212 kill(aes_round_ns)$
00213 declare(aes_round_ns,noun)$
00214 declare(aes_round_ns,posfun)$
00215 aes_round_namespace([args]) := apply(nounify(aes_round_ns),args)$
00216 
00217 aes_round_ns_var_l(cst) := block([vars : [],namespace],
00218   namespace : cstt_namespace_new(aes_round_namespace,cst),
00219   vars : cons(generate_aes_constraint_vars(1,128,namespace,nounify(so)),vars),
00220   vars : cons(generate_aes_constraint_vars(1,128,namespace,nounify(ro)),vars),
00221   vars : cons(generate_aes_constraint_vars(1,128,namespace,nounify(mo)),vars),
00222   return(lappend(vars)))$
00223 /* Returns a set of conditions representing AES round given
00224    128 plaintext variables, 128 key variables and 128 output
00225    variables. */
00226 aes_round_cstr_cstl(cst) := block(
00227   [namespace,bits,iBits, rkBits, oBits,tBits,rs:[]],
00228   bits : cst[2],
00229   namespace : cstt_namespace_new(aes_round_namespace,cst),
00230   iBits : take_elements(128,bits),
00231   rkBits : take_elements(128,rest(bits,128)),
00232   oBits : rest(bits,256),
00233   tBits : generate_aes_constraint_vars(1,128,namespace,nounify(so)),
00234   rs : cons(
00235     cstt_new("aes_subbytes_cst",
00236         append(iBits,tBits),
00237         [],namespace),
00238     rs),
00239   iBits : tBits,
00240   tBits : generate_aes_constraint_vars(1,128,namespace,nounify(ro)),
00241   rs : cons(
00242     cstt_new("aes_shiftrows_cst",
00243         append(iBits,tBits),
00244         [],namespace),
00245     rs),
00246   iBits : tBits,
00247   tBits : generate_aes_constraint_vars(1,128,namespace,nounify(mo)),
00248   rs : cons(
00249     cstt_new("aes_mixcolumns_cst",
00250       append(iBits, tBits),
00251       [],namespace),
00252     rs),
00253   iBits : tBits,
00254   tBits : oBits,
00255   rs : cons(
00256     cstt_new("aes_add_cst",
00257       append(iBits, rkBits, tBits),
00258       [],namespace),
00259     rs),
00260   return(rs)
00261 )$
00262 
00263 /*
00264    AES Final round
00265    
00266 */
00267 
00268 aes_final_round_cstrb :
00269  [aes_final_round_cstr_cstl, aes_final_round_namespace,aes_final_round_ns_var_l]$
00270 
00271 /* AES final round namespace */
00272 kill(aes_final_round_ns)$
00273 declare(aes_final_round_ns,noun)$
00274 declare(aes_final_round_ns,posfun)$
00275 aes_final_round_namespace([args]) := apply(nounify(aes_final_round_ns),args)$
00276 
00277 aes_final_round_ns_var_l(cst) := block(
00278   [vars : [],namespace],
00279   namespace : cstt_namespace_new(aes_final_round_namespace,cst),
00280   vars : cons(generate_aes_constraint_vars(1,128,namespace,nounify(so)),vars),
00281   vars : cons(generate_aes_constraint_vars(1,128,namespace,nounify(ro)),vars),
00282   return(lappend(vars)))$
00283 /* Returns a set of conditions representing AES round given
00284    128 plaintext variables, 128 key variables and 128 output
00285    variables. */
00286 aes_final_round_cstr_cstl(cst) := block(
00287   [namespace,bits,iBits, rkBits, oBits,tBits,rs:[]],
00288   bits : cst[2],
00289   namespace : cstt_namespace_new(aes_final_round_namespace,cst),
00290   iBits : take_elements(128,bits),
00291   rkBits : take_elements(128,rest(bits,128)),
00292   oBits : rest(bits,256),
00293   tBits : generate_aes_constraint_vars(1,128,namespace,nounify(so)),
00294   rs : cons(
00295     cstt_new("aes_subbytes_cst",
00296         append(iBits,tBits),
00297         [],namespace),
00298     rs),
00299   iBits : tBits,
00300   tBits : generate_aes_constraint_vars(1,128,namespace,nounify(ro)),
00301   rs : cons(
00302     cstt_new("aes_shiftrows_cst",
00303         append(iBits,tBits),
00304         [],namespace),
00305     rs),
00306   iBits : tBits,
00307   tBits : oBits,
00308   rs : cons(
00309     cstt_new("aes_add_cst",
00310       append(iBits, rkBits, tBits),
00311       [],namespace),
00312     rs),
00313   return(rs)
00314 )$
00315 
00316 /*
00317    Subbytes
00318    
00319 */
00320 
00321 aes_subbytes_cstrb :
00322  [aes_subbytes_cstr_cstl,aes_subbytes_namespace,aes_subbytes_ns_var_l]$
00323 
00324 
00325 /* AES subbytes namespace */
00326 kill(aes_subbytes_ns)$
00327 declare(aes_subbytes_ns,noun)$
00328 declare(aes_subbytes_ns,posfun)$
00329 aes_subbytes_namespace([args]) := apply(nounify(aes_subbytes_ns),args)$
00330 
00331 aes_subbytes_ns_var_l([a]) := []$
00332 /* Returns a set of conditions representing the AES Subbytes operation given
00333    128 plaintext variables and 128 output variables. */
00334 aes_subbytes_cstr_cstl(cst) := block(
00335   [namespace,bits,iBits, rkBits, oBits,tBits,rs:[]],
00336   bits : cst[2],
00337   namespace : cstt_namespace_new(aes_subbytes_namespace,cst),
00338   iBits : take_elements(128,bits),
00339   oBits : rest(bits,128),
00340   for i : 0 thru 15 do
00341     rs : cons(
00342       cstt_new("aes_sbox_cst",
00343         append(
00344           take_elements(8, rest(iBits,i*8)),
00345           take_elements(8, rest(oBits,i*8))),
00346         [i], namespace),
00347       rs),
00348   return(rs)
00349 )$
00350 
00351 
00352 /*
00353    Shiftrows
00354 
00355 */
00356 
00357 aes_shiftrows_cstrb :
00358  [aes_shiftrows_cstr_cstl,aes_shiftrows_namespace,aes_shiftrows_ns_var_l]$
00359 
00360 /* AES shiftrows namespace */
00361 kill(aes_shiftrows_ns)$
00362 declare(aes_shiftrows_ns,noun)$
00363 declare(aes_shiftrows_ns,posfun)$
00364 aes_shiftrows_namespace(arg_l) := apply(nounify(aes_shiftrows_ns),arg_l)$
00365 
00366 
00367 aes_shiftrows_ns_var_l([a]) := []$
00368 /* Returns a set of conditions representing the AES Shiftrows operation given
00369    128 plaintext variables and 128 output variables. */
00370 aes_shiftrows_cstr_cstl(cst) := block(
00371   [namespace,bits,iBits, oBits,count : 0],
00372   bits : cst[2],
00373   namespace : cstt_namespace_new(aes_shiftrows_namespace,cst),
00374   iBits : take_elements(128,bits),
00375   oBits : take_elements(128,rest(bits,128)),
00376   map(
00377     lambda([a,b],
00378       cstt_new("eq_cst",[a,b],
00379         [],namespace)), oBits,
00380     lappend(
00381       rijn_m2l(aes_shiftrows(rijn_l2m(partition_elements(iBits,8))))))
00382 )$
00383 
00384 
00385 /*
00386    Mixcolumns
00387 
00388 */
00389 
00390 aes_mixcolumns_cstrb :
00391  [aes_mixcolumns_cstr_cstl,aes_mixcolumns_namespace,aes_mixcolumns_ns_var_l]$
00392 
00393 /* AES mixcolumns namespace */
00394 kill(aes_mixcolumns_ns)$
00395 declare(aes_mixcolumns_ns,noun)$
00396 declare(aes_mixcolumns_ns,posfun)$
00397 aes_mixcolumns_namespace([arg_l]) := apply(nounify(aes_mixcolumns_ns),arg_l)$
00398 
00399 
00400 aes_mixcolumns_ns_var_l([a]) := []$
00401 /* Returns a set of conditions representing the AES Mixcolumns operation given
00402    128 plaintext variables and 128 output variables. */
00403 aes_mixcolumns_cstr_cstl(cst) := block(
00404   [namespace, bits,iBits, oBits, nc, mc_i : 0],
00405   bits : cst[2],
00406   namespace : cstt_namespace_new(aes_mixcolumns_namespace,cst),
00407   iBits : take_elements(128,bits),
00408   oBits : rest(bits,128),
00409   nc : length(iBits)/32,
00410   map(lambda([a,b,column], 
00411     cstt_new("aes_mixcolumn_cst",
00412       append(lappend(a),lappend(b)),
00413       [mc_i : mc_i + 1],namespace)),
00414     partition_elements(partition_elements(iBits,8),nc),
00415     partition_elements(partition_elements(oBits,8),nc),
00416     create_list(i,i,1,4))
00417 )$
00418 
00419 
00420 /*
00421    Bidirectional Mixcolumn
00422 
00423 */
00424 
00425 aes_bi_mixcolumn_cstrb :
00426  [aes_bi_mixcolumn_cstr_cstl,aes_bi_mixcolumn_namespace,aes_bi_mixcolumn_ns_var_l]$
00427 
00428 
00429 /* AES bi_mixcolumn namespace */
00430 kill(aes_bi_mixcolumn_ns)$
00431 declare(aes_bi_mixcolumn_ns,noun)$
00432 declare(aes_bi_mixcolumn_ns,posfun)$
00433 aes_bi_mixcolumn_namespace([args]) := apply(nounify(aes_bi_mixcolumn_ns),args)$
00434 
00435 aes_bi_mixcolumn_ns_var_l(cstt) := block(
00436   [cstt_new : cstt_namespace_replace(cstt,
00437     cstt_namespace_new(aes_bi_mixcolumn_namespace,cstt))],
00438   append(
00439     aes_mixcolumn_ns_var_l(cstt_new),
00440     aes_inv_mixcolumn_ns_var_l(cstt_new)))$
00441 /* Returns a set of conditions representing the AES bidirectional
00442    mixcolumn operation (the individual operation applied to a single column in
00443    AES bi_mixcolumns) given 128 plaintext variables and 128 output variables.
00444  */
00445 aes_bi_mixcolumn_cstr_cstl(cstt) := block(
00446   [cstt_new : cstt_namespace_replace(cstt,
00447     cstt_namespace_new(aes_bi_mixcolumn_namespace,cstt))],
00448   append(
00449     aes_mixcolumn_cstr_cstl(cstt_new),
00450     aes_inv_mixcolumn_cstr_cstl(cstt_new)))$
00451 
00452 
00453 /*
00454    Mixcolumn
00455 
00456 */
00457 
00458 aes_mixcolumn_cstrb :
00459  [aes_mixcolumn_cstr_cstl,aes_mixcolumn_namespace,aes_mixcolumn_ns_var_l]$
00460 
00461 
00462 /* AES mixcolumn namespace */
00463 kill(aes_mixcolumn_ns)$
00464 declare(aes_mixcolumn_ns,noun)$
00465 declare(aes_mixcolumn_ns,posfun)$
00466 aes_mixcolumn_namespace([args]) := apply(nounify(aes_mixcolumn_ns),args)$
00467 
00468 aes_mixcolumn_ns_var_l(cst) := block([vars : [],namespace],
00469   namespace :
00470     cstt_namespace_new(aes_mixcolumn_namespace,cst),
00471   vars : cons(
00472       generate_aes_constraint_vars(1,32,namespace,nounify(mc2)),vars),
00473   vars : cons(
00474       generate_aes_constraint_vars(1,32,namespace,nounify(mc3)),vars),
00475   return(lappend(vars)))$
00476 /* Returns a set of conditions representing the AES Mixcolumn operation (the 
00477    individual operation applied to a single column in AES Mixcolumns) given
00478    128 plaintext variables and 128 output variables. */
00479 aes_mixcolumn_cstr_cstl(cst) := block(
00480   [namespace,bits,iBits, oBits, nc,rs : []],
00481   bits : cst[2],
00482   namespace :
00483     cstt_namespace_new(aes_mixcolumn_namespace,cst),
00484   iBits : partition_elements(take_elements(32, bits),8),
00485   oBits : partition_elements(rest(bits, 32), 8),
00486   /* First element */
00487   for i : 0 thru 3 do block([mulAVars, mulBVars, addAVars, addBVars],
00488     mulAVars :
00489       generate_aes_constraint_vars(8*i + 1,8*i + 8,namespace,nounify(mc2)),
00490     rs : cons(
00491       cstt_new("aes_mul2_cst",
00492         append(iBits[mod(0 + i,4) + 1],mulAVars),
00493         [i],namespace),
00494       rs),
00495     mulBVars :
00496       generate_aes_constraint_vars(8*i + 1,8*i + 8,namespace,nounify(mc3)),
00497     rs : cons(
00498       cstt_new("aes_mul3_cst",
00499         append(iBits[mod(1 + i,4) + 1],mulBVars),
00500         [i],namespace),
00501       rs),
00502     rs : cons(
00503       cstt_new("aes_add_cst",
00504         append(
00505           mulAVars,mulBVars,iBits[mod(2 + i,4) + 1],
00506           iBits[mod(3 + i,4) + 1],oBits[i+1]),[4], namespace),
00507       rs)
00508   ),
00509   return(rs)
00510 )$
00511 
00512 
00513 /*
00514    Inverse Mixcolumn
00515 
00516 */
00517 
00518 aes_inv_mixcolumn_cstrb :
00519  [aes_inv_mixcolumn_cstr_cstl,aes_inv_mixcolumn_namespace,aes_inv_mixcolumn_ns_var_l]$
00520 
00521 
00522 /* AES inv_mixcolumn namespace */
00523 kill(aes_inv_mixcolumn_ns)$
00524 declare(aes_inv_mixcolumn_ns,noun)$
00525 declare(aes_inv_mixcolumn_ns,posfun)$
00526 aes_inv_mixcolumn_namespace([args]) := apply(nounify(aes_inv_mixcolumn_ns),args)$
00527 
00528 aes_inv_mixcolumn_ns_var_l(cst) := block([vars : [],namespace],
00529   namespace :
00530     cstt_namespace_new(aes_inv_mixcolumn_namespace,cst),
00531   vars : cons(
00532       generate_aes_constraint_vars(1,32,namespace,nounify(mc14)),vars),
00533   vars : cons(
00534       generate_aes_constraint_vars(1,32,namespace,nounify(mc11)),vars),
00535   vars : cons(
00536       generate_aes_constraint_vars(1,32,namespace,nounify(mc13)),vars),
00537   vars : cons(
00538       generate_aes_constraint_vars(1,32,namespace,nounify(mc9)),vars),
00539   return(lappend(vars)))$
00540 /* Returns a set of conditions representing the AES Inverse Mixcolumn operation (the 
00541    individual operation applied to a single column in AES Inverse Mixcolumns) given
00542    128 plaintext variables and 128 output variables. */
00543 aes_inv_mixcolumn_cstr_cstl(cst) := block(
00544   [namespace,bits,iBits, oBits, nc,rs : []],
00545   bits : cst[2],
00546   namespace :
00547     cstt_namespace_new(aes_inv_mixcolumn_namespace,cst),
00548   iBits : partition_elements(take_elements(32, bits),8),
00549   oBits : partition_elements(rest(bits, 32), 8),
00550   /* Perform matrix multiplication */
00551   for i : 0 thru 3 do block(
00552     [mulAVars, mulBVars, mulCVars, mulDVars, addAVars, addBVars],
00553     mulAVars :
00554       generate_aes_constraint_vars(8*i+1,8*i+8,namespace,nounify(mc14)),
00555     rs : cons(
00556       cstt_new("aes_mul14_cst",
00557         append(oBits[mod(0 + i,4) + 1],mulAVars),
00558         [i],namespace),
00559       rs),
00560     mulBVars :
00561       generate_aes_constraint_vars(8*i+1,8*i+8,namespace,nounify(mc11)),
00562     rs : cons(
00563       cstt_new("aes_mul11_cst",
00564         append(oBits[mod(1 + i,4) + 1],mulBVars),
00565         [i],namespace),
00566       rs),
00567     mulCVars :
00568       generate_aes_constraint_vars(8*i+1,8*i+8,namespace,nounify(mc13)),
00569     rs : cons(
00570       cstt_new("aes_mul13_cst",
00571         append(oBits[mod(2 + i,4) + 1],mulCVars),
00572         [i],namespace),
00573       rs),
00574     mulDVars :
00575       generate_aes_constraint_vars(8*i+1,8*i+8,namespace,nounify(mc9)),
00576     rs : cons(
00577       cstt_new("aes_mul9_cst",
00578         append(oBits[mod(3 + i,4) + 1],mulDVars),
00579         [i],namespace),
00580       rs),
00581     rs : cons(
00582       cstt_new("aes_add_cst",
00583         append(mulAVars, mulBVars, mulCVars, mulDVars, iBits[i+1]),
00584         [4],namespace),
00585       rs)
00586   ),
00587   return(rs)
00588 )$
00589 
00590 
00591 /*
00592    Key expansion
00593 
00594 */
00595 
00596 
00597 aes_key_expansion_cstrb :
00598  [aes_key_expansion_cstr_cstl,aes_key_expansion_namespace,
00599   aes_key_expansion_ns_var_l]$
00600 
00601 /* Generates a set of unit-clauses (initially simpler than simplifying constants
00602    or making partial assignments) to set the given vars (representing the bits
00603    of AES round constants) to the round constant for round n */
00604 aes_round_constant_l(n) := block([rc_el,rc_l],
00605   rc_el : xreduce(lambda([a,b],aes_field_mul_data[b,a+1]),
00606                create_list(2,i,1,(n -1)),1),
00607   rc_l : egf_coeffs(rijn_bit_field,egf_num2poly(rijn_byte_field,rc_el),7),
00608   return(rc_l)
00609 )$
00610 
00611 /* AES key expansion namespace */
00612 kill(aes_key_expansion_ns)$
00613 declare(aes_key_expansion_ns,noun)$
00614 declare(aes_key_expansion_ns,posfun)$
00615 aes_key_expansion_namespace([args]) :=
00616   apply(nounify(aes_key_expansion_ns),args)$
00617 
00618 aes_key_expansion_ns_var_l(cst) := block(
00619   [n_r : cst[3],vars : [],namespace],
00620   namespace : cstt_namespace_new(aes_key_expansion_namespace,cst),
00621   vars : cons(
00622     generate_aes_constraint_vars(1,4*8*n_r,namespace,nounify(sb)),vars),
00623   vars : cons(
00624     generate_aes_constraint_vars(1,8*n_r,namespace,nounify(ke)),vars),
00625   vars : cons(
00626     generate_aes_constraint_vars(1,8*n_r,namespace,nounify(rc)),vars),
00627   return(lappend(vars)))$
00628 /* Returns a set of conditions representing the AES keyschedule operation given
00629    128 key variables and 128 * (aes_num_rounds + 1) output variables
00630    (consecutive lots of 128 bits representing the individual round keys).
00631    
00632    The first 128 variables in the list "bits" represent the key block for the 
00633    cipher, and then the (i+1)'th consecutive 128 variables in "bits" represents
00634    the round key block for the i'th round. 
00635    
00636    */
00637 aes_key_expansion_cstr_cstl(cst) := block(
00638   [namespace,bits, n_k : 4,n_b : 4, n_r,kBits, rkBits, nc,rs : [],
00639    sboxVars, addVars,fMat, kMat, sbox_i : 0, rc_i : 0],
00640   bits : cst[2],
00641   namespace : cstt_namespace_new(aes_key_expansion_namespace,cst),
00642   n_r : cst[3],
00643   /* Primary Variables */
00644   kBits : take_elements(128,bits),
00645   rkBits : rest(bits,128),
00646   fBits : take_elements(128,rkBits),
00647   /* Split into columns */
00648   cols :  partition_elements(partition_elements(rkBits,8),4),
00649   kMat : partition_elements(partition_elements(kBits,8),4),
00650   fMat : partition_elements(partition_elements(fBits,8),4),
00651   /* Make first round key equal */
00652   for j : 1 thru n_k do
00653     for i : 1 thru n_b do
00654       rs : cons(
00655         cstt_new("eq_cst",
00656           append(kMat[j][i], fMat[j][i]),
00657           [],namespace),
00658         rs),
00659   /* Setup output bits */
00660   for j : n_k thru (n_b * (n_r +1)) - 1 do block(
00661     if mod(j, n_k) = 0 then block (
00662       sboxVars : generate_aes_constraint_vars(
00663         (j-n_k)*8*(4/n_k) +1,(j-n_k)*8*(4/n_k) +8,namespace,nounify(sb)),
00664       rs : cons(
00665         cstt_new("aes_sbox_cst",
00666           append(cols[j][2], sboxVars),
00667           [sbox_i : sbox_i + 1],namespace),
00668         rs),
00669       addVars : generate_aes_constraint_vars(
00670         (j-n_k)*(8/n_k) +1,(j-n_k)*(8/n_k) +8,namespace,nounify(ke)),
00671       rs : cons(
00672         cstt_new("aes_add_cst",
00673           append(cols[j-n_k+1][1],sboxVars,addVars),
00674           [],namespace),
00675         rs),
00676       rcVars : generate_aes_constraint_vars(
00677         (j-n_k)*(8/n_k) + 1,(j-n_k)*(8/n_k) + 8,namespace,nounify(rc)),
00678       rs : cons(
00679         cstt_new("const_cst",
00680             rcVars,
00681             cons(rc_i : rc_i + 1,aes_round_constant_l(floor(j/n_k))),
00682             namespace),
00683         rs),
00684       rs : cons(
00685         cstt_new("aes_add_cst", 
00686           append(rcVars,addVars, cols[j+1][1]),
00687           [],namespace),
00688         rs),
00689       for i : 1 thru 3 do block([offset: ((j-n_k)*(4/n_k) + i)*8],
00690         sboxVars : generate_aes_constraint_vars(
00691           offset + 1,offset + 8,namespace,nounify(sb)),
00692         rs : cons(
00693           cstt_new("aes_sbox_cst", 
00694             append(cols[j][mod(i+1,4)+1], sboxVars),
00695             [sbox_i : sbox_i + 1],namespace),
00696           rs),
00697         rs : cons(
00698           cstt_new("aes_add_cst", 
00699             append(cols[j-n_k+1][i+1],sboxVars, cols[j+1][i+1]),
00700             [],namespace),
00701           rs)
00702       )
00703     )
00704     else for i : 1 thru 4 do 
00705       rs : cons(
00706         cstt_new("aes_add_cst",
00707           append(cols[j][i], cols[j-n_k+1][i],cols[j+1][i]),
00708           [],namespace),
00709         rs)
00710   ),
00711   return(rs)
00712 )$
00713 
00714 
00715 /* ****************************************
00716    * CNF Translation functions            *
00717    ****************************************
00718 */
00719 
00720 /* Returns a list of CNF clauses representing addition within GF(2^n) given
00721    an "aes_add_cst" constraint with m * n input variables (n lots of
00722    m bits to be summed) and output variables where n is the first
00723    argument to the constraint. */
00724 aes_add_cst_cl(cst) := block(
00725  [nb, n : if cstt_args_l(cst) = [] then 2 else cstt_args_l(cst)[1]],
00726   nb : floor(length(cst[2]) / (n+1)),
00727   parity_f : lambda([[V]], even_parity_wv_cl(V)),
00728   lappend(apply(map, cons(parity_f, partition_elements(cst[2],nb)))))$
00729 
00730 /* Returns a list of CNF clauses representing equivalence between the first
00731    half of the list of variables and the second half in the constraint.
00732 
00733    Variables in the second half may also be "true", in which case, unit
00734    clauses will be introduced.
00735 */
00736 aes_eq_cst_cl(cst) := block([ nb : floor(length(cst[2]) / 2)],
00737   lappend(
00738     map(lambda([a,b], if b = true then [{a}] else [{-a,b},{a,-b}]), 
00739     take_elements(nb,cst[2]), rest(cst[2],nb))))$
00740 
00741 /* Constants */
00742 aes_const_cst_cl(cst) := block(
00743   map(lambda([a,b], if b = 1 then {a} else {-a}), cst[2],
00744     rest(cstt_args_l(cst))))$
00745 
00746 /* Returns a list of CNF clauses representing the sbox relation
00747    given the appropriate sbox constraint ("aes_sbox_cst" with 16 variables
00748    in the constraint).
00749 
00750    The clauses returned are those originally produced manually through
00751    experimentation into finding small Sbox representations (see plans
00752    and SboxMinCNF).
00753 */
00754 aes_sbox_pi_cst_cl(cst) := rename_fcl(map(listify,SboxMinCNF),cst[2])[2]$
00755 
00756 
00757 /* AES sbox namespace */
00758 kill(aes_sbox_ts_ns)$
00759 declare(aes_sbox_ts_ns,noun)$
00760 declare(aes_sbox_ts_ns,posfun)$
00761 aes_sbox_ts_namespace([args]) :=
00762   apply(nounify(aes_sbox_ts_ns),args)$
00763 
00764 /* Given an "aes_sbox_cst" constraint, returns the new variables
00765    introduced by "aes_sbox_ts_cst_cl" when given this constraint. */
00766 aes_sbox_ts_var_l(cst) := block(
00767   [bits : cst[2],namespace],
00768   namespace : cstt_namespace_new(aes_sbox_ts_namespace,cst),
00769   generate_aes_constraint_vars(1,256, namespace,nounify(sbox_ts)))$
00770 
00771 /* Given an "aes_sbox_cst" constraint, returns a clause list
00772    generated by taking the canonical translation from DNF to CNF
00773    of the AES Sbox.
00774 */
00775 aes_sbox_ts_cst_cl(cst) := block(
00776   [bits : cst[2],namespace],
00777   namespace : cstt_namespace_new(aes_sbox_ts_namespace,cst),
00778     sbox : aes_sbox_ts_gen(),
00779     vars : append(bits,
00780       generate_aes_constraint_vars(1,256, namespace,nounify(sbox_ts))),
00781     cnf : rename_fcl(sbox,vars),
00782     cnf[2])$
00783 
00784 /* Returns a list of CNF clauses representing the multiplication by 02
00785    given the appropriate constraint ("aes_mul2_cst" with 16 variables
00786    in the constraint).
00787 
00788    The clauses returned are those originally produced manually through
00789    experimentation into finding small Sbox representations (see plans
00790    and FieldMul2CNF).
00791 */
00792 aes_mul2_pi_cst_cl(cst) := rename_fcl(map(listify,FieldMul2CNF),cst[2])[2]$
00793 
00794 /* AES mul2 namespace */
00795 kill(aes_mul2_ts_ns)$
00796 declare(aes_mul2_ts_ns,noun)$
00797 declare(aes_mul2_ts_ns,posfun)$
00798 aes_mul2_ts_namespace([args]) :=
00799   apply(nounify(aes_mul2_ts_ns),args)$
00800 
00801 /* Given an "aes_mul2_cst" constraint, returns the new variables
00802    introduced by "aes_mul2_ts_cst_cl" when given this constraint. */
00803 aes_mul2_ts_var_l(cst) := block([bits : cst[2],namespace],
00804   namespace : cstt_namespace_new(aes_mul2_ts_namespace,cst),
00805   generate_aes_constraint_vars(1,256, namespace,nounify(mul2_ts)))$
00806 
00807 /* Returns a list of CNF clauses representing the multiplication by 02
00808    given the appropriate constraint ("aes_mul2_cst" with 16 variables
00809    in the constraint).
00810 
00811    The clauses returned are those given by the canonical translation
00812    using new variables. */
00813 aes_mul2_ts_cst_cl(cst) := block(
00814   [bits : cst[2],namespace],
00815   namespace : cstt_namespace_new(aes_mul2_ts_namespace,cst),
00816     rename_fcl(aes_mul_ts_gen(2),
00817       append(bits,
00818         generate_aes_constraint_vars(1,256, namespace,nounify(mul2_ts))))[2])$
00819 
00820 /* Returns a list of CNF clauses representing the multiplication by 03
00821    given the appropriate constraint ("aes_mul3_cst" with 16 variables
00822    in the constraint).
00823 
00824    The clauses returned are those originally produced manually through
00825    experimentation into finding small Sbox representations (see plans
00826    and FieldMul3CNF).
00827 */
00828 aes_mul3_pi_cst_cl(cst) := rename_fcl(map(listify,FieldMul3CNF),cst[2])[2]$
00829 
00830 /* AES mul3 namespace */
00831 kill(aes_mul3_ts_ns)$
00832 declare(aes_mul3_ts_ns,noun)$
00833 declare(aes_mul3_ts_ns,posfun)$
00834 aes_mul3_ts_namespace([args]) :=
00835   apply(nounify(aes_mul3_ts_ns),args)$
00836 
00837 /* Given an "aes_sbox_cst" constraint, returns the new variables
00838    introduced by "aes_sbox_ts_cst_cl" when given this constraint. */
00839 aes_mul3_ts_var_l(cst) := block([bits : cst[2],namespace],
00840   namespace : cstt_namespace_new(aes_mul3_ts_namespace,cst),
00841   generate_aes_constraint_vars(1,256, namespace,nounify(mul3_ts)))$
00842 
00843 /* Returns a list of CNF clauses representing the multiplication by 03
00844    given the appropriate constraint ("aes_mul3_cst" with 16 variables
00845    in the constraint).
00846 
00847    The clauses returned are those given by the canonical translation
00848    using new variables. */
00849 aes_mul3_ts_cst_cl(cst) := block(
00850   [bits : cst[2],namespace],
00851   namespace : cstt_namespace_new(aes_mul3_ts_namespace,cst),
00852     rename_fcl(aes_mul_ts_gen(3),
00853       append(bits,
00854         generate_aes_constraint_vars(1,256, namespace,nounify(mul3_ts))))[2])$
00855 
00856 
00857 /* Returns a list of CNF clauses representing the multiplication by 14
00858    given the appropriate constraint ("aes_mul14_cst" with 16 variables
00859    in the constraint).
00860 
00861    The clauses returned are those originally produced manually through
00862    experimentation into finding small Sbox representations (see plans
00863    and FieldMul14CNF).
00864 */
00865 aes_mul14_pi_cst_cl(cst) := rename_fcl(map(listify,FieldMul14CNF),cst[2])[2]$
00866 
00867 /* AES mul14 namespace */
00868 kill(aes_mul14_ts_ns)$
00869 declare(aes_mul14_ts_ns,noun)$
00870 declare(aes_mul14_ts_ns,posfun)$
00871 aes_mul14_ts_namespace([args]) :=
00872   apply(nounify(aes_mul14_ts_ns),args)$
00873 
00874 /* Given an "aes_sbox_cst" constraint, returns the new variables
00875    introduced by "aes_sbox_ts_cst_cl" when given this constraint. */
00876 aes_mul14_ts_var_l(cst) := block([bits : cst[2],namespace],
00877   namespace : cstt_namespace_new(aes_mul14_ts_namespace,cst),
00878   generate_aes_constraint_vars(1,256, namespace,nounify(mul14_ts)))$
00879 
00880 /* Returns a list of CNF clauses representing the multiplication by 14
00881    given the appropriate constraint ("aes_mul14_cst" with 16 variables
00882    in the constraint).
00883 
00884    The clauses returned are those given by the canonical translation
00885    using new variables. */
00886 aes_mul14_ts_cst_cl(cst) := block(
00887   [bits : cst[2],namespace],
00888   namespace : cstt_namespace_new(aes_mul14_ts_namespace,cst),
00889     rename_fcl(aes_mul_ts_gen(14),
00890       append(bits,
00891         generate_aes_constraint_vars(1,256, namespace,nounify(mul14_ts))))[2])$
00892 
00893 /* Returns a list of CNF clauses representing the multiplication by 11
00894    given the appropriate constraint ("aes_mul11_cst" with 16 variables
00895    in the constraint).
00896 
00897    The clauses returned are those originally produced manually through
00898    experimentation into finding small Sbox representations (see plans
00899    and FieldMul11CNF).
00900 */
00901 aes_mul11_pi_cst_cl(cst) := rename_fcl(map(listify,FieldMul11CNF),cst[2])[2]$
00902 
00903 /* AES mul11 namespace */
00904 kill(aes_mul11_ts_ns)$
00905 declare(aes_mul11_ts_ns,noun)$
00906 declare(aes_mul11_ts_ns,posfun)$
00907 aes_mul11_ts_namespace([args]) :=
00908   apply(nounify(aes_mul11_ts_ns),args)$
00909 
00910 /* Given an "aes_sbox_cst" constraint, returns the new variables
00911    introduced by "aes_sbox_ts_cst_cl" when given this constraint. */
00912 aes_mul11_ts_var_l(cst) := block([bits : cst[2],namespace],
00913   namespace : cstt_namespace_new(aes_mul11_ts_namespace,cst),
00914   generate_aes_constraint_vars(1,256, namespace,nounify(mul11_ts)))$
00915 
00916 /* Returns a list of CNF clauses representing the multiplication by 11
00917    given the appropriate constraint ("aes_mul11_cst" with 16 variables
00918    in the constraint).
00919 
00920    The clauses returned are those given by the canonical translation
00921    using new variables. */
00922 aes_mul11_ts_cst_cl(cst) := block(
00923   [bits : cst[2],namespace],
00924   namespace : cstt_namespace_new(aes_mul11_ts_namespace,cst),
00925     rename_fcl(aes_mul_ts_gen(11),
00926       append(bits,
00927         generate_aes_constraint_vars(1,256, namespace,nounify(mul11_ts))))[2])$
00928 
00929 /* Returns a list of CNF clauses representing the multiplication by 13
00930    given the appropriate constraint ("aes_mul13_cst" with 16 variables
00931    in the constraint).
00932 
00933    The clauses returned are those originally produced manually through
00934    experimentation into finding small Sbox representations (see plans
00935    and FieldMul13CNF).
00936 */
00937 aes_mul13_pi_cst_cl(cst) := rename_fcl(map(listify,FieldMul13CNF),cst[2])[2]$
00938 
00939 /* AES mul13 namespace */
00940 kill(aes_mul13_ts_ns)$
00941 declare(aes_mul13_ts_ns,noun)$
00942 declare(aes_mul13_ts_ns,posfun)$
00943 aes_mul13_ts_namespace([args]) :=
00944   apply(nounify(aes_mul13_ts_ns),args)$
00945 
00946 /* Given an "aes_sbox_cst" constraint, returns the new variables
00947    introduced by "aes_sbox_ts_cst_cl" when given this constraint. */
00948 aes_mul13_ts_var_l(cst) := block([bits : cst[2],namespace],
00949   namespace : cstt_namespace_new(aes_mul13_ts_namespace,cst),
00950   generate_aes_constraint_vars(1,256, namespace,nounify(mul13_ts)))$
00951 
00952 /* Returns a list of CNF clauses representing the multiplication by 13
00953    given the appropriate constraint ("aes_mul13_cst" with 16 variables
00954    in the constraint).
00955 
00956    The clauses returned are those given by the canonical translation
00957    using new variables. */
00958 aes_mul13_ts_cst_cl(cst) := block(
00959   [bits : cst[2],namespace],
00960   namespace : cstt_namespace_new(aes_mul13_ts_namespace,cst),
00961     rename_fcl(aes_mul_ts_gen(13),
00962       append(bits,
00963         generate_aes_constraint_vars(1,256, namespace,nounify(mul13_ts))))[2])$
00964 
00965 /* Returns a list of CNF clauses representing the multiplication by 09
00966    given the appropriate constraint ("aes_mul9_cst" with 16 variables
00967    in the constraint).
00968 
00969    The clauses returned are those originally produced manually through
00970    experimentation into finding small Sbox representations (see plans
00971    and FieldMul9CNF).
00972 */
00973 aes_mul9_pi_cst_cl(cst) := rename_fcl(map(listify,FieldMul9CNF),cst[2])[2]$
00974 
00975 /* AES mul9 namespace */
00976 kill(aes_mul9_ts_ns)$
00977 declare(aes_mul9_ts_ns,noun)$
00978 declare(aes_mul9_ts_ns,posfun)$
00979 aes_mul9_ts_namespace([args]) :=
00980   apply(nounify(aes_mul9_ts_ns),args)$
00981 
00982 /* Given an "aes_sbox_cst" constraint, returns the new variables
00983    introduced by "aes_sbox_ts_cst_cl" when given this constraint. */
00984 aes_mul9_ts_var_l(cst) := block([bits : cst[2],namespace],
00985   namespace : cstt_namespace_new(aes_mul9_ts_namespace,cst),
00986   generate_aes_constraint_vars(1,256, namespace,nounify(mul9_ts)))$
00987 
00988 /* Returns a list of CNF clauses representing the multiplication by 09
00989    given the appropriate constraint ("aes_mul9_cst" with 16 variables
00990    in the constraint).
00991 
00992    The clauses returned are those given by the canonical translation
00993    using new variables. */
00994 aes_mul9_ts_cst_cl(cst) := block(
00995   [bits : cst[2],namespace],
00996   namespace : cstt_namespace_new(aes_mul9_ts_namespace,cst),
00997     rename_fcl(aes_mul_ts_gen(9),
00998       append(bits,
00999         generate_aes_constraint_vars(1,256, namespace,nounify(mul9_ts))))[2])$
01000