OKlibrary  0.2.1.6
Translations.mac
Go to the documentation of this file.
00001 /* Matthew Gwynne, 19.8.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 2010, 2011 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library; either version 3 of the
00006 License, or any later version. */
00007 
00022 oklib_include("OKlib/ComputerAlgebra/TestSystem/Lisp/Asserts.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/FiniteFunctions/TseitinTranslation.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/Cryptanalysis/Rijndael/Translations.mac")$
00025 
00026 kill(f)$
00027 
00028 okltest_aes_mul_ts_gen(f) := block([FF],
00029   if oklib_test_level = 0 then return(true),
00030   FF : f(2),
00031   assert(length(FF[1]) = 16+256),
00032   assert(elementp(setify(create_list(dts_var(i),i,1,256)),setify(FF[2]))),
00033   assert(elementp({11,-dts_var(256)}, setify(FF[2]))),
00034   assert(elementp({-12,-9,-5,-2,1,3,4,6,7,8,10,11,13,14,15,16,dts_var(10)},
00035     setify(FF[2]))),
00036   FF : f(3),
00037   assert(length(FF[1]) = 16+256),
00038   assert(elementp(setify(create_list(dts_var(i),i,1,256)),setify(FF[2]))),
00039   assert(elementp({11,-dts_var(256)}, setify(FF[2]))),
00040   assert(elementp({-12,-9,-4,-3,-2,1,5,6,7,8,10,11,13,14,15,16,dts_var(10)},
00041     setify(FF[2]))),
00042   if oklib_test_level = 1 then return(true),
00043   for e in [9,11,13,14] do (
00044     FF : f(e),
00045     assert(length(FF[1]) = 16+256),
00046     assert(elementp(setify(create_list(dts_var(i),i,1,256)),setify(FF[2])))),
00047   true)$
00048 
00049 
00050 okltest_aes_sbox_ts_gen(f) := block([FF],
00051   if oklib_test_level = 0 then return(true),
00052   FF : f(),
00053   assert(length(FF[1]) = 16+256),
00054   assert(elementp(setify(create_list(dts_var(i),i,1,256)),setify(FF[2]))),
00055   assert(elementp({-11,-dts_var(90)}, setify(FF[2]))),
00056   assert(elementp({-12,-9,-7,-6,-4,-1,2,3,5,8,10,11,13,14,15,16,dts_var(10)},
00057     setify(FF[2]))),
00058   true)$
00059 
00060 /******************************************************************
00061  * Statistics                                                     *
00062  ******************************************************************
00063 */
00064 
00065 okltest_nsbox_ss(f) := block([n : 4],
00066   if oklib_test_level = 0 then n : 2,
00067   for r : 1 thru n do block([csttl],
00068     for c : 1 thru n do (
00069       for rw : 1 thru n do (
00070         csttl : ss_csttl(r,c, rw, 4, false, aes_mc_forward),
00071         assert(
00072           length(sublist(csttl,
00073               lambda([C], is(cstt_name(C) = "ss_sbox_cst")))) =
00074           f(r,c,rw))))),
00075   true)$
00076 
00077 okltest_nmul_ss_gen(f) := block(
00078   [n : 4, rowcols : [1,2,4],mc_trans : [aes_mc_forward,aes_mc_bidirectional],
00079    f_b_l : [true,false]],
00080   if oklib_test_level = 0 or oklib_test_level = 1 then (
00081     n : 1,rowcols : [1,2],f_b_l : [false], mc_trans : [aes_mc_forward]),
00082   for e in ['x,'x+1] do
00083     for r : 1 thru n do block([csttl],
00084       for c in rowcols do (
00085         for rw in rowcols do 
00086           for f_b in f_b_l do
00087             for mc_tran in mc_trans do (
00088                csttl : ss_csttl(r,c, rw, 4, f_b, mc_tran),
00089                assert(
00090                  length(sublist(csttl,
00091                      lambda([C],is(cstt_name(C) = "ss_mul_cst") and
00092                        is(C[3] = e)))) =
00093                  f(e,r,c,4,ss_mixcolumns_matrix(2,4,rw),f_b,mc_tran))))),
00094   true)$
00095 
00096 okltest_nmul_ss(f) := block(
00097   [n : 4, rowcols : [1,2,4],mc_trans : [aes_mc_forward,aes_mc_bidirectional],
00098    f_b_l : [true,false]],
00099   if oklib_test_level = 0 or oklib_test_level = 1 then (
00100     n : 1,rowcols : [1,2],f_b_l : [false], mc_trans : [aes_mc_forward]),
00101   for e in ['x,'x+1] do
00102     for r : 1 thru n do block([csttl],
00103       for c in rowcols do (
00104         for rw in rowcols do 
00105           for f_b in f_b_l do
00106             for mc_tran in mc_trans do (
00107                csttl : ss_csttl(r,c, rw, 4, f_b, mc_tran),
00108                assert(
00109                  length(sublist(csttl,
00110                      lambda([C],is(cstt_name(C) = "ss_mul_cst") and
00111                        is(C[3] = e)))) =
00112                  f(e,r,c,rw,4,f_b,mc_tran))))),
00113   true)$
00114 
00115 okltest_nadd_ss_sm(f) := block(
00116   [measure_num_add_f : lambda([cstl],
00117      multi_list_distribution2list_distribution(
00118        map(lambda([a],
00119            if length(a) = 3 then [2,length(a[2])/3]
00120            else [third(a),length(a[2])/(third(a)+1)]),
00121          sublist(cstl,lambda([a], is(first(a) = "ss_add_cst"))))))],
00122   assert(f(1,1,1,4,false,aes_mc_bidirectional) = {[1,8],[2,12]}),
00123   assert(f(1,1,2,8,false,aes_mc_bidirectional) = {[2,72]}),
00124   assert(f(1,2,2,8,false,aes_mc_bidirectional) = {[2,152],[3,8]}),
00125   assert(f(1,2,3,8,false,aes_mc_bidirectional) = {[2,136],[3,104]}),
00126   assert(f(1,1,3,4,false,aes_mc_forward) = {[2,28],[3,12]}),
00127   assert(f(1,4,4,8,false,aes_mc_bidirectional) = {[2,376],[3,8],[4,256]}),
00128   if oklib_test_level = 0 then return(true),
00129   if oklib_test_level = 1 then return(true),
00130   for r : 1 thru 4 do
00131     for c : 1 thru 4 do
00132       for rw : 1 thru 4 do
00133         for e in [4,8] do
00134         for f_b in [true,false] do
00135             for mc_tran in [aes_mc_forward,aes_mc_bidirectional] do (
00136               assert(
00137                 f(r,c,rw,e,f_b,mc_tran) =
00138                 setify(measure_num_add_f(ss_csttl(r,c,rw,e,f_b,mc_tran))))),  
00139   true)$
00140 
00141 okltest_nadd_ss(f) := (
00142   assert(f(1,1,1,4,false,aes_mc_bidirectional) = 20),
00143   assert(f(1,1,2,8,false,aes_mc_bidirectional) = 72),
00144   assert(f(1,2,2,8,false,aes_mc_bidirectional) = 160),
00145   assert(f(1,2,3,8,false,aes_mc_bidirectional) = 240),
00146   assert(f(1,1,3,4,false,aes_mc_forward) = 40),
00147   assert(f(1,4,4,8,false,aes_mc_bidirectional) = 640),
00148   true)$
00149 
00150 okltest_nconstants_ss(f) := (
00151   for r : 1 thru 20 do assert(f(r) = r),
00152   true)$
00153 
00154 okltest_nvar_ss_gen(f) := (
00155   assert(f(1,1,1,4,ss_mixcolumns_matrix(2,4,1),16,
00156       [['x,16],['x+1,16]],false,aes_mc_forward) = 68),
00157   assert(f(1,4,4,8,ss_mixcolumns_matrix(2,8,4),256,
00158       [['x,256],['x+1,256], [x^3+1,256],[x^3+x+1,256],[x^3+x^2+1,256],
00159       [x^3+x^2+x,256]],false,aes_mc_bidirectional) = 31400),
00160   assert(f(1,4,4,8,ss_mixcolumns_matrix(2,8,4),256,
00161       [], true,aes_mc_bidirectional) = 5928),
00162   assert(f(1,4,4,8,ss_mixcolumns_matrix(2,8,4),256,
00163       [], true,aes_mc_forward) = 5928),
00164   assert(f(1,4,4,8,ss_mixcolumns_matrix(2,8,4),256,
00165       [[x,256],[x+1,256],[x^3+1,256],[x^3+x+1,256],
00166       [x^3+x^2+1,256],[x^3+x^2+x,256]], false,aes_mc_forward) = 14504),
00167   true)$
00168 
00169 okltest_nvar_ss(f) := (
00170   assert(f(1,1,1,4,false,aes_ts_box,aes_mc_forward) = 68),
00171   assert(f(1,4,4,8,false,aes_ts_box,aes_mc_bidirectional) = 31400),
00172   assert(f(1,4,4,8,true,aes_ts_box,aes_mc_bidirectional) = 5928),
00173   assert(f(1,4,4,8,true,aes_ts_box,aes_mc_forward) = 5928),
00174   assert(f(1,4,4,8,false,aes_ts_box,aes_mc_forward) = 14504),
00175   assert(f(1,4,4,4,false,aes_small_box,aes_mc_forward) = 596),
00176   true)$
00177 
00178 okltest_ncl_ss_gen(f) := (
00179     assert(f(1,1,1,4,ss_mixcolumns_matrix(2,4,1),145,
00180       [['x,145],['x+1,145]],false,aes_mc_forward) = 350),
00181   assert(f(1,4,4,8,ss_mixcolumns_matrix(2,8,4),4353,
00182       [['x,4353],['x+1,4353], [x^3+1,4353],[x^3+x+1,4353],[x^3+x^2+1,4353],
00183       [x^3+x^2+x,4353]],false,aes_mc_bidirectional) = 510620),
00184   assert(f(1,4,4,8,ss_mixcolumns_matrix(2,8,4),4353,
00185       [], true,aes_mc_bidirectional) = 88636),
00186   assert(f(1,4,4,8,ss_mixcolumns_matrix(2,8,4),4353,
00187       [], true,aes_mc_forward) = 88636),
00188   assert(f(1,4,4,8,ss_mixcolumns_matrix(2,8,4),4353,
00189       [[x,4353],[x+1,4353],[x^3+1,4353],[x^3+x+1,4353],
00190       [x^3+x^2+1,4353],[x^3+x^2+x,4353]], false,aes_mc_forward) = 229980),
00191   true)$
00192 
00193 okltest_ncl_ss(f) := (
00194   assert(f(1,1,1,4,false,aes_ts_box,aes_mc_forward) = 350),
00195   assert(f(1,4,4,8,false,aes_ts_box,aes_mc_bidirectional) = 510620),
00196   assert(f(1,4,4,8,true,aes_ts_box,aes_mc_bidirectional) = 88636),
00197   assert(f(1,4,4,8,true,aes_ts_box,aes_mc_forward) = 88636),
00198   assert(f(1,4,4,8,false,aes_ts_box,aes_mc_forward) = 229980),
00199   assert(f(1,4,4,4,false,aes_small_box,aes_mc_forward) = 2652),
00200   assert(f(10,4,4,8,true,aes_small_box,aes_mc_forward) = 153048),
00201   true)$
00202 
00203 okltest_ncl_list_ss_gen(f) := (
00204   assert(f(1,1,1,4,ss_mixcolumns_matrix(2,4,1),
00205       ncl_list_full_dualts(8,16), [], false, aes_mc_bidirectional) =
00206     [[1,4],[2,272],[3,48],[9,32],[16,2]]),
00207   assert(f(1,4,4,8,ss_mixcolumns_matrix(2,8,4),
00208       ncl_list_full_dualts(16,256), [], true, aes_mc_bidirectional)
00209     = [[1,8],[2,81920],[3,1504],[4,64],[17,5120],[256,20]]),
00210   assert(f(1,2,2,4, ss_mixcolumns_matrix(2,4,2),ncl_list_full_dualts(8,16),
00211       [[x,ncl_list_full_dualts(8,16)],[x+1,ncl_list_full_dualts(8,16)]],
00212       false, aes_mc_bidirectional) =
00213     [[1,4],[2,2816],[3,304],[4,32],[9,352],[16,22]]),
00214   assert(f(1,2,2,4, ss_mixcolumns_matrix(2,4,2),ncl_list_full_dualts(8,16),
00215       [[x,ncl_list_full_dualts(8,16)],[x+1,ncl_list_full_dualts(8,16)]],
00216       false, aes_mc_forward) =
00217     [[1,4],[2,1792],[3,240],[4,32],[9,224],[16,14]]),
00218   true)$
00219 
00220 okltest_ncl_list_ss(f) := (
00221   assert(f(1,1,1,4,false, aes_ts_box, aes_mc_bidirectional) =
00222     [[1,4],[2,272],[3,48],[9,32],[16,2]]),
00223   assert(f(1,4,4,8,true,aes_ts_box, aes_mc_bidirectional)
00224     = [[1,8],[2,81920],[3,1504],[4,64],[17,5120],[256,20]]),
00225   assert(f(1,2,2,4,false,aes_ts_box, aes_mc_bidirectional) =
00226     [[1,4],[2,2816],[3,304],[4,32],[9,352],[16,22]]),
00227   assert(f(1,2,2,4, false, aes_ts_box, aes_mc_forward) =
00228     [[1,4],[2,1792],[3,240],[4,32],[9,224],[16,14]]),
00229   assert(f(1,2,2,4, false, aes_small_box, aes_mc_forward) =
00230     [[1,4],[2,20],[3,352],[4,120],[5,12]]),
00231   true)$
00232 
00233 okltest_component_statistics_ss_gen(f) := block(
00234   assert(f(1,4,4,8,ss_mixcolumns_matrix(2,8,4),true, aes_mc_forward) =
00235     [0,1,16,256,[],4,128,8]),
00236   assert(f(1,4,4,8,ss_mixcolumns_matrix(2,8,4),false, aes_mc_forward) =
00237     [1,0,16,384,[[1,32],[x,16],[x+1,16]],4,128,8]),
00238   if oklib_test_level = 0 then return(true),
00239   if oklib_test_level = 1 then return(true),
00240   for r : 1 thru 4 do
00241     for c in [1,2,4] do
00242       for rw in [1,2,4] do
00243         for e in [4,8] do
00244         for f_b in [true,false] do
00245             for mc_tran in [aes_mc_forward,aes_mc_bidirectional] do (
00246               assert(
00247                 f(r,c,rw,e,ss_mixcolumns_matrix(2,e,rw),f_b,mc_tran)[4] +
00248                 f(r,c,rw,e,ss_mixcolumns_matrix(2,e,rw),f_b,mc_tran)[7] =
00249                 sum_l(map(second,listify(nadd_ss_sm(r,c,rw,e,f_b,mc_tran)))))),
00250   true)$
00251 
00252 /******************************************************************
00253  * Data translation                                               *
00254  ******************************************************************
00255 */
00256 
00257 okltest_aes_hex2pa(f) := block(
00258   assert(f("",[]) = {}),
00259   assert(f("0",[1,2,3,4,5,6,7,8]) = {-8,-7,-6,-5,-4,-3,-2,-1}),
00260   assert(f("00",[1,2,3,4,5,6,7,8]) = {-8,-7,-6,-5,-4,-3,-2,-1}),
00261   assert(f("01",[1,2,3,4,5,6,7,8]) = {8,-7,-6,-5,-4,-3,-2,-1}),
00262   assert(f("A5",[1,2,3,4,5,6,7,8]) =  {-7,-5,-4,-2,1,3,6,8}),
00263   assert(f("54A5",[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16]) = 
00264     {-15,-13,-12,-10,-8,-7,-5,-3,-1,2,4,6,9,11,14,16}),
00265   true)$
00266 
00267 okltest_ss_random_matrix(f) := block(
00268   set_random_state(make_random_state(0)),
00269   assert(f(2,4,ss_polynomial_2_4,1,1) = matrix([x^3+x^2])),
00270   set_random_state(make_random_state(0)),
00271   assert(f(2,8,ss_polynomial_2_8,4,4) =
00272     matrix([x^7+x^5+x^3+x^2,x^5+x^3+x^2+x+1,x^6+x^5+x^4+x^2+1,x^7+x^6],
00273       [x^6+x+1,x^7+x^6+x^5+x^4+x^3+x+1,x^7+x^6+x+1,x^6+x^5+x^2+x+1],
00274       [x^3+1,x^7+x^6+x^4+x+1,x^4+x^2+1,x^7+x^6+x^5+x^4+x],
00275       [x^5+x^2,x^6+x^4+x^2+x+1,x^6+x^2+x,x^7+x^6+x^4+x^3])),
00276   true)$
00277 
00278 okltest_ss_matrix2pa(f) := block(
00279   assert(f(matrix(),[],2,1,1) = []),
00280   assert(f(matrix([1]),[1],2,1,1) = [1]),
00281   assert(f(matrix([1],[0]),[1,2],2,1,1) = [1,-2]),
00282   assert(f(matrix([x^6+x^4+x^3,x^7+x^3+x^2,x^5+x^4+x^3+x,x^7+x^6+1],
00283         [x^7+x^6+x^5+x^2+x,x^5+x^2+x+1,x^6+x^4+x^2+x+1,x^7+x^5+x^3+x^2+x],
00284         [x^6+x^4+x^3,x^6+x^4+1,x^7+x^5+x^2+1,x^4+x^3+1],
00285         [x^6+x^3+x^2+1,x^6+x^3,x^3+1,x^7+x^4+x^2]),create_list(i,i,1,128),
00286       2,8,ss_polynomial_2_8) =
00287       [-1,2,-3,4,5,-6,-7,-8,9,10,11,-12,-13,14,15,-16,-17,18,-19,20,21,
00288       -22,-23,-24,-25,26,-27,-28,29,30,-31,32,33,-34,-35,-36,37,38,-39,
00289       -40,-41,-42,43,-44,-45,46,47,48,-49,50,-51,52,-53,-54,-55,56,-57,
00290       58,-59,-60,61,-62,-63,-64,-65,-66,67,68,69,-70,71,-72,-73,74,-75,76,
00291       -77,78,79,80,81,-82,83,-84,-85,86,-87,88,-89,-90,-91,-92,93,-94,-95,
00292       96,97,98,-99,-100,-101,-102,-103,104,105,-106,107,-108,109,110,111,
00293       -112,-113,-114,-115,116,117,-118,-119,120,121,-122,-123,124,-125,126,
00294       -127,-128]),
00295   true)$
00296 
00297 okltest_ss_pa2matrix(f) := block(
00298   assert(f([],[],2,1,1,1) = matrix()),
00299   assert(f([1],[1],2,1,1,1) = matrix([1])),
00300   assert(f([1,-2],[1,2],2,1,1,2) = matrix([1],[0])),
00301   assert(f([-1,2,-3,4,5,-6,-7,-8,9,10,11,-12,-13,14,15,-16,-17,18,-19,20,21,
00302       -22,-23,-24,-25,26,-27,-28,29,30,-31,32,33,-34,-35,-36,37,38,-39,
00303       -40,-41,-42,43,-44,-45,46,47,48,-49,50,-51,52,-53,-54,-55,56,-57,
00304       58,-59,-60,61,-62,-63,-64,-65,-66,67,68,69,-70,71,-72,-73,74,-75,76,
00305       -77,78,79,80,81,-82,83,-84,-85,86,-87,88,-89,-90,-91,-92,93,-94,-95,
00306       96,97,98,-99,-100,-101,-102,-103,104,105,-106,107,-108,109,110,111,
00307       -112,-113,-114,-115,116,117,-118,-119,120,121,-122,-123,124,-125,126,
00308       -127,-128],create_list(i,i,1,128),2,8,ss_polynomial_2_8,4) =
00309     matrix([x^6+x^4+x^3,x^7+x^3+x^2,x^5+x^4+x^3+x,x^7+x^6+1],
00310         [x^7+x^6+x^5+x^2+x,x^5+x^2+x+1,x^6+x^4+x^2+x+1,x^7+x^5+x^3+x^2+x],
00311         [x^6+x^4+x^3,x^6+x^4+1,x^7+x^5+x^2+1,x^4+x^3+1],
00312         [x^6+x^3+x^2+1,x^6+x^3,x^3+1,x^7+x^4+x^2])),
00313   true)$
00314