OKlibrary  0.2.1.6
SmallScaleAdvancedEncryptionStandard.mac
Go to the documentation of this file.
00001 /* Matthew Gwynne, 28.1.2010 (Swansea) */
00002 /* Copyright 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/Cryptology/Lisp/CryptoSystems/Rijndael/ByteField.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/CryptoSystems/Rijndael/Block.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/CryptoSystems/Rijndael/SmallScaleAdvancedEncryptionStandard.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/CryptoSystems/Rijndael/AdvancedEncryptionStandard.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/CryptoSystems/Rijndael/tests/AdvancedEncryptionStandard.mac")$
00028 oklib_plain_include(eigen)$ /* (for function columnvector) */
00029 
00030 
00031 kill(f)$
00032 
00033 /* **************************************
00034    * Special bit-linear byte operations *
00035    **************************************
00036 */
00037 
00038 okltest_ss_sbox_linmap_gen(f) := block(
00039   assert(f(0,2,4,ss_polynomial_2_4,ss_sbox_matrix(2,4)) = 0),
00040   assert(f(1,2,4,ss_polynomial_2_4,ss_sbox_matrix(2,4)) = x^3+x^2+1),
00041   assert(f(x,2,4,ss_polynomial_2_4,ss_sbox_matrix(2,4)) = x^3+x+1),
00042   true)$
00043 
00044 okltest_ss_mul_w_sbox_linmap_gen(f) := block(
00045   assert(okltest_ss_sbox_linmap_gen(
00046       buildq([f], lambda([field_element,b,e,mod_poly, sbox_matrix],
00047           f(field_element,1,b,e,mod_poly, sbox_matrix))))),
00048   assert(f(x,x,2,4,ss_polynomial_2_4,ss_sbox_matrix(2,4)) = x^2+1),
00049   true)$
00050 
00051 
00052 /* *********
00053    * S box *
00054    *********
00055 */
00056 
00057 okltest_ss_sbox_linmap_gen(f) := block(
00058   assert(f(0,2,4,ss_polynomial_2_4,ss_sbox_matrix(2,4)) = 0),
00059   assert(f(1,2,4,ss_polynomial_2_4,ss_sbox_matrix(2,4)) = x^3+x^2+1),
00060   assert(f(x,2,4,ss_polynomial_2_4,ss_sbox_matrix(2,4)) = x^3+x+1),
00061   true)$
00062 
00063 okltest_ss_sbox_gen(f) := block(
00064   /* Test vector for b=2 e=4 generated using "Small Scale Variants of the AES
00065   (SR) Polynomial System Generator" in Sage */
00066   assert(create_list(poly2nat(
00067         f(nat2poly(i,2),2,4,ss_polynomial_2_4,
00068           ss_sbox_matrix_2_4,ss_affine_constant_2_4),2),i,0,15) =
00069     [6,11,5,4,2,14,7,10,9,13,15,12,3,1,0,8]),
00070   assert(f(0,2,8,ss_polynomial_2_8,
00071       ss_sbox_matrix_2_8,ss_affine_constant_2_8) = x^6+x^5+x+1),
00072   assert(f(x^6+x^4+x,2,8,ss_polynomial_2_8,
00073       ss_sbox_matrix_2_8,ss_affine_constant_2_8) = 0),
00074   assert(f(x^7+x^6+x^5+x^4+x^3+x^2+x+1,2,8,ss_polynomial_2_8,
00075       ss_sbox_matrix_2_8,ss_affine_constant_2_8) = x^4+x^2+x),
00076   if oklib_test_level=0 then return(true),
00077   for b : 0 thru 255 do
00078     assert(f(b,2,8,ss_polynomial_2_8,
00079       ss_sbox_matrix_2_8,ss_affine_constant_2_8) = rijn_lookup_sbox(b)),
00080   true)$
00081 
00082 okltest_ss_inv_sbox_gen(f) := block(
00083   assert(create_list(poly2nat(
00084         f(nat2poly(i,2),2,4,ss_polynomial_2_4,
00085           ss_inv_sbox_matrix_2_4,ss_inv_affine_constant_2_4),2),i,
00086       [6,11,5,4,2,14,7,10,9,13,15,12,3,1,0,8]) =
00087     [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15]),
00088   assert(f(0,2,8,ss_polynomial_2_8,
00089       ss_inv_sbox_matrix_2_8,ss_inv_affine_constant_2_8) = x^6+x^4+x),
00090   assert(f(x^6+x^5+x+1,2,8,ss_polynomial_2_8,
00091       ss_inv_sbox_matrix_2_8,ss_inv_affine_constant_2_8) = 0),
00092   assert(f(x^4+x^2+x,2,8,ss_polynomial_2_8,
00093       ss_inv_sbox_matrix_2_8,ss_inv_affine_constant_2_8) =
00094     x^7+x^6+x^5+x^4+x^3+x^2+x+1),
00095   if oklib_test_level=0 then return(true),
00096   for b : 0 thru 255 do
00097     assert(f(b,2,8,ss_polynomial_2_8,
00098       ss_inv_sbox_matrix_2_8,ss_inv_affine_constant_2_8) =
00099     rijn_lookup_inv_sbox(b)),
00100   true)$
00101 
00102 
00103 okltest_ss_sbox_bf(f) := (
00104   assert(okltest_rijn_sbox_vec(buildq([f], lambda([V],f(V,2,8))))),
00105   true)$
00106 
00107 okltest_ss_sbox_w_add_bf(f) := (
00108   assert(f([0,0,0,0,0,0,0,0],2,4) = [0,1,1,0]),
00109   assert(f([0,0,0,0,0,0,0,1],2,4) = [0,1,1,1]),
00110   assert(f([0,0,0,0,1,0,0,1],2,4) = [1,1,1,1]),
00111   assert(f([0,0,0,0,1,1,0,1],2,4) = [1,0,1,1]),
00112   assert(f([1,1,1,1,0,0,0,0],2,4) = [1,0,0,0]),
00113   assert(f([1,1,1,1,1,1,1,1],2,4) = [0,1,1,1]),
00114   assert(f([1,0,1,1,1,0,1,0],2,4) = [0,1,1,0]),
00115   true)$
00116 
00117 okltest_ss_sbox_w_mul_bf(f) := (
00118   assert(f([0,0,0,0],1,2,4) = [0,1,1,0]),
00119   assert(f([0,0,0,1],1,2,4) = [1,0,1,1]),
00120   assert(f([1,0,0,1],1,2,4) = [1,1,0,1]),
00121   assert(f([0,0,0,0],x,2,4) = [1,1,0,0]),
00122   assert(f([0,0,0,1],x,2,4) = [0,1,0,1]),
00123   assert(f([1,0,0,1],x,2,4) = [1,0,0,1]),
00124   true)$
00125 
00126 
00127 /* *************
00128    * Sub-bytes *
00129    *************
00130 */
00131 
00132 
00133 okltest_ss_subbytes(f) := block([sbox_f],
00134   sbox_f : lambda([p],ss_sbox(p,2,8)),
00135   assert(f(diagmatrix(4,0),sbox_f) =
00136     genmatrix(lambda([a,b],x^6+x^5+x+1),4,4)),
00137   assert(f(diagmatrix(4,1),sbox_f) =
00138     genmatrix(lambda([a,b],
00139       if a = b then x^6+x^5+x^4+x^3+x^2 else x^6+x^5+x+1),4,4)),
00140   assert(f(rijn_l2m(
00141         map(nat2polybin,[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16])),sbox_f) =
00142     rijn_l2m(map(nat2polybin,
00143         [124,119,123,242,107,111,197,48,1,103,43,254,215,171,118,202]))),
00144   true)$
00145 
00146 okltest_ss_inv_subbytes(f) := block([inv_sbox_f],
00147   inv_sbox_f : lambda([p], ss_inv_sbox(p,2,8)),
00148   assert(f(genmatrix(lambda([a,b],x^6+x^5+x+1),4,4),inv_sbox_f) =
00149     diagmatrix(4,0)),
00150   assert(f(
00151       genmatrix(lambda([a,b],
00152           if a = b then x^6+x^5+x^4+x^3+x^2
00153           else x^6+x^5+x+1),4,4),inv_sbox_f) = diagmatrix(4,1)),
00154   assert(totaldisrep(f(rijn_l2m(map(nat2polybin,[124,119,123,242,107,111,197,
00155             48,1,103,43,254,215,171,118,202])),inv_sbox_f)) =
00156     rijn_l2m(map(nat2polybin, [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16]))),
00157   true)$
00158 
00159 /* **************
00160    * Shift rows *
00161    **************
00162 */
00163 
00164 okltest_ss_shiftrows(f) := block(
00165   assert(f(diagmatrix(4,0))=diagmatrix(4,0)),
00166   assert(f(apply(matrix,create_list([0,1,x,x+1],i,0,3))) =
00167       apply(matrix,create_list(rotate([0,1,x,x+1],-i),i,0,3))),
00168   true)$
00169 
00170 okltest_ss_inv_shiftrows(f) := block(
00171   assert(f(diagmatrix(4,0))=diagmatrix(4,0)),
00172   assert(f(apply(matrix,create_list(rotate([0,1,x,x+1],-i),i,0,3))) =
00173       apply(matrix,create_list([0,1,x,x+1],i,0,3))),
00174   true)$
00175 
00176 /* ***************
00177    * Mix columns *
00178    ***************
00179 */
00180 
00181 okltest_ss_mixcolumn_gen(f) := block(
00182   assert(f(ss_natl2m([0,0,0,0],2,4),2,8,
00183       ss_polynomial_2_8,ss_mixcolumns_matrix_2_8_4) =
00184     ss_natl2m([0,0,0,0],2,4)),
00185   assert(f(ss_natl2m([50,67,7,52],2,4),2,8,
00186       ss_polynomial_2_8,ss_mixcolumns_matrix_2_8_4) =
00187     ss_natl2m([146, 137, 35, 122],2,4)),
00188   true)$
00189 
00190 okltest_ss_mixcolumn_gen_bf(f) := block(
00191   assert(f(create_list(0,i,1,32),2,8,
00192       ss_polynomial_2_8,ss_mixcolumns_matrix_2_8_4) =
00193     create_list(0,i,1,32)),
00194   assert(f(
00195       [0,0,1,1,0,0,1,0,0,1,0,0,0,0,1,1,0,0,0,0,0,1,1,1,0,0,1,1,0,1,0,0],2,8,
00196       ss_polynomial_2_8,ss_mixcolumns_matrix_2_8_4) =
00197     [1,0,0,1,0,0,1,0,1,0,0,0,1,0,0,1,0,0,1,0,0,0,1,1,0,1,1,1,1,0,1,0]),
00198   true)$
00199 
00200 okltest_ss_mixcolumn_gen_boolm(f) := block(
00201   assert(f(2,4,ss_polynomial(2,4),ss_mixcolumns_matrix(2,4,4)) =
00202     matrix(
00203       [0,1,0,0,1,1,0,0,1,0,0,0,1,0,0,0],
00204       [0,0,1,0,0,1,1,0,0,1,0,0,0,1,0,0],
00205       [1,0,0,1,1,0,1,1,0,0,1,0,0,0,1,0],
00206       [1,0,0,0,1,0,0,1,0,0,0,1,0,0,0,1],
00207       [1,0,0,0,0,1,0,0,1,1,0,0,1,0,0,0],
00208       [0,1,0,0,0,0,1,0,0,1,1,0,0,1,0,0],
00209       [0,0,1,0,1,0,0,1,1,0,1,1,0,0,1,0],
00210       [0,0,0,1,1,0,0,0,1,0,0,1,0,0,0,1],
00211       [1,0,0,0,1,0,0,0,0,1,0,0,1,1,0,0],
00212       [0,1,0,0,0,1,0,0,0,0,1,0,0,1,1,0],
00213       [0,0,1,0,0,0,1,0,1,0,0,1,1,0,1,1],
00214       [0,0,0,1,0,0,0,1,1,0,0,0,1,0,0,1],
00215       [1,1,0,0,1,0,0,0,1,0,0,0,0,1,0,0],
00216       [0,1,1,0,0,1,0,0,0,1,0,0,0,0,1,0],
00217       [1,0,1,1,0,0,1,0,0,0,1,0,1,0,0,1],
00218       [1,0,0,1,0,0,0,1,0,0,0,1,1,0,0,0])),
00219   assert(
00220     okltest_ss_mixcolumn_gen_bf(
00221       buildq([f],
00222         lambda([V,b,e,mod_poly,mixcolumns_matrix],
00223           ss_stand_vec(
00224             m2l_r(f(b,e,mod_poly,mixcolumns_matrix) . columnvector(V)),2))))),
00225   true)$
00226 
00227 okltest_ss_round_column_gen_bf(f) := block(
00228     assert(f(create_list(0,i,1,32),2,8,
00229       ss_polynomial_2_8,ss_mixcolumns_matrix_2_8_4,
00230       lambda([p],ss_sbox(p,2,8))) =
00231     [0,1,1,0,0,0,1,1,0,1,1,0,0,0,1,1,0,1,1,0,0,0,1,1,0,1,1,0,0,0,1,1]),
00232   assert(f(
00233       [0,0,1,1,0,0,1,0,0,1,0,0,0,0,1,1,0,0,0,0,0,1,1,1,0,0,1,1,0,1,0,0],2,8,
00234       ss_polynomial_2_8,ss_mixcolumns_matrix_2_8_4,
00235       lambda([p],ss_sbox(p,2,8))) =
00236     [1,0,1,1,0,1,0,1,0,1,0,1,1,0,1,1,1,0,0,0,0,0,0,0,1,0,0,0,1,0,1,0]),
00237   if oklib_test_level = 0 then return(true),
00238   okltest_ss_mixcolumn_gen_bf(
00239     buildq([f],lambda([V,b,e,poly,mc],f(V,b,e,poly,mc,lambda([p],p))))),
00240   true)$
00241 
00242 okltest_ss_inv_mixcolumn_gen(f) := block(
00243   assert(f(ss_natl2m([0,0,0,0],2,4),2,8,
00244       ss_polynomial_2_8,ss_inv_mixcolumns_matrix_2_8_4) =
00245     ss_natl2m([0,0,0,0],2,4)),
00246   assert(f(ss_natl2m([146, 137, 35, 122],2,4),2,8,
00247       ss_polynomial_2_8,ss_inv_mixcolumns_matrix_2_8_4)=
00248     ss_natl2m([50,67,7,52],2,4)),
00249   true)$
00250 
00251 okltest_ss_mixcolumns_gen(f) := block([mixcolumn_f],
00252   assert(f(matrix([0]), 2,4,ss_polynomial(2,4),
00253       ss_mixcolumns_matrix(2,4,1)) = matrix([0])),
00254   assert(f(ss_natl2m([0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],2,4),
00255         2,8,ss_polynomial(2,8),ss_mixcolumns_matrix(2,8,4)) =
00256       ss_natl2m([0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],2,4)),
00257   assert(f(ss_natl2m(
00258           [50,136,49,224,67,90,49,55,246,48,152,7,168,141,162,52],2,4),
00259         2,8,ss_polynomial(2,8), ss_mixcolumns_matrix(2,8,4))= ss_natl2m(
00260       [54,138,227,52,110,147,34,192,56,34,228,167,81,96,38,164],2,4)),
00261   true)$
00262 
00263 okltest_ss_inv_mixcolumns_gen(f) := block([inv_mixcolumn_f],
00264   assert(f(ss_natl2m([0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],2,4),
00265         2,8,ss_polynomial(2,8),ss_inv_mixcolumns_matrix(2,8,4)) =
00266       ss_natl2m([0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],2,4)),
00267   assert(f(ss_natl2m(
00268           [54,138,227,52,110,147,34,192,56,34,228,167,81,96,38,164],2,4),
00269         2,8,ss_polynomial(2,8),ss_inv_mixcolumns_matrix(2,8,4))= ss_natl2m(
00270     [50,136,49,224,67,90,49,55,246,48,152,7,168,141,162,52],2,4)),
00271   true)$
00272 
00273 /* *****************
00274    * Key expansion *
00275    *****************
00276 */
00277 
00278 okltest_ss_key_expansion_gen(f) := block(
00279   assert(f(ss_natl2m([0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],2,4),10,2,
00280       ss_polynomial_2_4,lambda([p],ss_sbox(p,2,4))) =
00281     map(lambda([p], ss_natl2m(p,2,4)),
00282       partition_elements(map(hex2int,charlist(
00283         sconcat("00000000000000007666766676667666211C577A211C577ACBE",
00284           "29C98BD84EAFEB3E22F7A92FE780015883AF2A80CD00C13B9294B81475",
00285           "14B6177483CC97B9830451A0D26C45D5C6D22042F22EB7FB7122958067",
00286           "AED055A17"))),16))),
00287   assert(f(ss_natl2m([0,0,0,0],2,2),10,2,
00288       ss_polynomial_2_4,lambda([p],ss_sbox(p,2,4))) =
00289     map(lambda([p], ss_natl2m(p,2,2)),
00290       partition_elements(map(hex2int,charlist(
00291         sconcat("000076762C5A92C88149632AF6DC07DB76AD3994B420"))),4))),
00292   assert(f(ss_natl2m([0],2,1),10,2,
00293       ss_polynomial_2_4,lambda([p],ss_sbox(p,2,4))) =
00294     map(lambda([p],ss_natl2m(p,2,2)),
00295       map("[",map(hex2int,charlist(sconcat("078D9E6B7F2")))))),
00296   /* Extreme Cases for sbox */
00297   assert(f(ss_natl2m([0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],2,4),10,2,
00298       ss_polynomial_2_8,rijn_sbox) =
00299     map(lambda([p],ss_natl2m(p,2,4)),
00300       [[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],
00301        [98,99,99,99,98,99,99,99,98,99,99,99,98,99,99,99],
00302        [155,152,152,201,249,251,251,170,155,152,152,201,249,251,251,170],
00303        [144,151,52,80,105,108,207,250,242,244,87,51,11,15,172,153],
00304        [238,6,218,123,135,106,21,129,117,158,66,178,126,145,238,43],
00305        [127,46,43,136,248,68,62,9,141,218,124,187,243,75,146,144],
00306        [236,97,75,133,20,37,117,140,153,255,9,55,106,180,155,167],
00307        [33,117,23,135,53,80,98,11,172,175,107,60,198,27,240,155],
00308        [14,249,3,51,59,169,97,56,151,6,10,4,81,29,250,159],
00309        [177,212,216,226,138,125,185,218,29,123,179,222,76,102,73,65],
00310        [180,239,91,203,62,146,226,17,35,233,81,207,111,143,24,142]])),
00311   true)$
00312 
00313 /* *********************************
00314    * AES encryption and decryption *
00315    *********************************
00316 */
00317 
00318 okltest_ss_round_gen(f) := block(
00319   assert(f(matrix([0]),matrix([0]),2,4,ss_polynomial_2_4,
00320       lambda([a],ss_sbox(a,2,4)),ss_mixcolumns_matrix(2,4,1)) =
00321     matrix([x^2+x])),
00322   assert(f(ss_natl2m([25,160,154,233,61,244,198,248,227,226,141,72,190,43,
00323     42,8],2,4),ss_natl2m([160,136,35,42,250,84,163,108,254,44,57,118,23,177,57,5],2,4),2,8,ss_polynomial_2_8,
00324     rijn_lookup_sbox,ss_mixcolumns_matrix(2,8,4))=
00325     ss_natl2m([164,238,162,207,252,114,239,68,45,86,113,142,141,81,242,28],2,4)),
00326   assert(f(ss_natl2m([72,103,77,214,108,29,227,95,78,157,177,88,238,13,56,
00327     231],2,4),ss_natl2m([239,168,182,219,68,82,113,11,165,91,37,173,65,127,59,0],2,4),2,8,ss_polynomial_2_8,
00328     rijn_lookup_sbox,ss_mixcolumns_matrix(2,8,4)) =
00329     ss_natl2m([224,126,108,114,247,65,112,85,181,48,74,109,254,31,10,56],2,4)),
00330   true)$
00331 
00332 okltest_ss_inv_round_gen(f) := block(
00333   assert(f(ss_natl2m([164,238,162,207,252,114,239,68,45,86,113,142,141,81,
00334     242,28],2,4),ss_natl2m([160,136,35,42,250,84,163,108,254,44,57,118,23,177,57,5],2,4),2,8,ss_polynomial(2,8),
00335     rijn_lookup_inv_sbox,ss_inv_mixcolumns_matrix(2,8,4))=
00336     ss_natl2m([25,160,154,233,61,244,198,248,227,226,141,72,190,43,42,8],2,4)),
00337   assert(f(ss_natl2m([224,126,108,114,247,65,112,85,181,48,74,109,254,31,10,
00338     56],2,4),ss_natl2m([239,168,182,219,68,82,113,11,165,91,37,173,65,127,59,0],2,4),2,8,ss_polynomial(2,8),
00339     rijn_lookup_inv_sbox,ss_inv_mixcolumns_matrix(2,8,4)) =
00340     ss_natl2m([72,103,77,214,108,29,227,95,78,157,177,88,238,13,56,231],2,4)),
00341   true)$
00342 
00343 
00344 okltest_ss_encrypt_wf_gen(f) := block(
00345     assert(f(ss_natl2m([0],2,1),ss_natl2m([0],2,1),10,2,4,ss_polynomial_2_4,
00346         lambda([p],ss_sbox(p,2,4)),ss_mixcolumns_matrix(2,4,1)) =
00347       ss_natl2m([7],2,1)),
00348   assert(f(ss_natl2m([0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],2,4),ss_natl2m([0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],2,4),10,2,8,ss_polynomial_2_8,
00349     rijn_lookup_sbox,ss_mixcolumns_matrix(2,8,4)) = 
00350     ss_natl2m([102,233,75,212,239,138,44,59,136,76,250,89,202,52,43,46],2,4)),
00351   assert(f(ss_natl2m(
00352         [50,136,49,224,67,90,49,55,246,48,152,7,168,141,162,52],2,4),
00353       ss_natl2m([43,40,171,9,126,174,247,207,21,210,21,79,22,166,136,60],2,4),10,2,8,ss_polynomial_2_8,
00354       rijn_lookup_sbox,ss_mixcolumns_matrix(2,8,4)) = 
00355     ss_natl2m([87,22,170,250,44,198,139,155,139,155,229,13,48,227,242,6],2,4)),
00356   true)$
00357 
00358 okltest_ss_encrypt_gen(f) := block(
00359     assert(f(ss_natl2m([0],2,1),ss_natl2m([0],2,1),10,2,4,ss_polynomial_2_4,
00360         lambda([p],ss_sbox(p,2,4)),ss_mixcolumns_matrix(2,4,1)) =
00361       ss_natl2m([7],2,1)),
00362     assert(f(diagmatrix(4,0),diagmatrix(4,0),10,2,8,ss_polynomial_2_8,
00363         lambda([p],ss_sbox(p,2,8)),
00364         ss_mixcolumns_matrix(2,8,4)) =
00365       ss_natl2m([14,30,142,142,75,16,210,251,167,99,179,16,123,178,155,169],
00366         2,4)),    
00367     true)$
00368 
00369 okltest_ss_decrypt_wf_gen(f) := block(
00370     assert(f(ss_natl2m([7],2,1),ss_natl2m([0],2,1),10,2,4,ss_polynomial_2_4,
00371         lambda([p],ss_sbox(p,2,4)),lambda([p],ss_inv_sbox(p,2,4)),
00372         ss_inv_mixcolumns_matrix(2,4,1)) = ss_natl2m([0],2,1)),
00373   assert(f(
00374       ss_natl2m([102,233,75,212,239,138,44,59,136,76,250,89,202,52,43,46],2,4),
00375       ss_natl2m([0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],2,4),10,2,8,
00376       ss_polynomial_2_8,rijn_lookup_sbox,rijn_lookup_inv_sbox,
00377       ss_inv_mixcolumns_matrix(2,8,4)) = 
00378     ss_natl2m([0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],2,4)),
00379   assert(f(ss_natl2m(
00380         [87,22,170,250,44,198,139,155,139,155,229,13,48,227,242,6],2,4),
00381       ss_natl2m([43,40,171,9,126,174,247,207,21,210,21,79,22,166,136,60],2,4),
00382       10,2,8,ss_polynomial_2_8,rijn_lookup_sbox,rijn_inv_sbox,
00383       ss_inv_mixcolumns_matrix(2,8,4)) =
00384     ss_natl2m([50,136,49,224,67,90,49,55,246,48,152,7,168,141,162,52],2,4)
00385     ),
00386   true)$
00387 
00388 okltest_ss_decrypt_gen(f) := block(
00389     assert(f(ss_natl2m([7],2,1),ss_natl2m([0],2,1),10,2,4,ss_polynomial_2_4,
00390         lambda([p],ss_sbox(p,2,4)),lambda([p],ss_inv_sbox(p,2,4)),
00391         ss_inv_mixcolumns_matrix(2,4,1)) = ss_natl2m([0],2,1)),
00392     assert(f(
00393         ss_natl2m([14,30,142,142,75,16,210,251,167,99,179,16,123,178,155,169],
00394         2,4),diagmatrix(4,0),10,2,8,ss_polynomial_2_8,
00395         lambda([p],ss_sbox(p,2,8)),lambda([p],ss_inv_sbox(p,2,8)),
00396         ss_inv_mixcolumns_matrix(2,8,4)) = diagmatrix(4,0)),
00397     true)$
00398 
00399 /* **********************************************************
00400    * Small scale AES instantiations                         *
00401    **********************************************************
00402 */
00403 
00404 okltest_ss_encrypt(f) := block(
00405     assert(f(ss_natl2m([0],2,1),ss_natl2m([0],2,1),10,2,4) =
00406       ss_natl2m([7],2,1)),
00407     assert(f(diagmatrix(4,0),diagmatrix(4,0),10,2,8) =
00408       ss_natl2m([14,30,142,142,75,16,210,251,167,99,179,16,123,178,155,169],
00409         2,4)),    
00410     true)$
00411 
00412 okltest_ss_encrypt_wf(f) := block(
00413     assert(f(ss_natl2m([0],2,1),ss_natl2m([0],2,1),10,2,4) =
00414       ss_natl2m([7],2,1)),
00415   assert(f(ss_natl2m([0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],2,4),ss_natl2m([0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],2,4),10,2,8) = 
00416     ss_natl2m([102,233,75,212,239,138,44,59,136,76,250,89,202,52,43,46],2,4)),
00417   assert(f(ss_natl2m(
00418         [50,136,49,224,67,90,49,55,246,48,152,7,168,141,162,52],2,4),
00419       ss_natl2m([43,40,171,9,126,174,247,207,21,210,21,79,22,166,136,60],2,4),10,2,8) = 
00420     ss_natl2m([87,22,170,250,44,198,139,155,139,155,229,13,48,227,242,6],2,4)),
00421   true)$
00422 
00423 okltest_ss_decrypt_wf(f) := block(
00424     assert(f(ss_natl2m([7],2,1),ss_natl2m([0],2,1),10,2,4) =
00425       ss_natl2m([0],2,1)),
00426   assert(f(
00427       ss_natl2m([102,233,75,212,239,138,44,59,136,76,250,89,202,52,43,46],2,4),
00428       ss_natl2m([0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],2,4),10,2,8) = 
00429     ss_natl2m([0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0],2,4)),
00430   assert(f(ss_natl2m(
00431         [87,22,170,250,44,198,139,155,139,155,229,13,48,227,242,6],2,4),
00432       ss_natl2m([43,40,171,9,126,174,247,207,21,210,21,79,22,166,136,60],2,4),
00433       10,2,8) =
00434     ss_natl2m([50,136,49,224,67,90,49,55,246,48,152,7,168,141,162,52],2,4)
00435     ),
00436   true)$
00437 
00438 okltest_ss_decrypt(f) := block(
00439     assert(f(ss_natl2m([7],2,1),ss_natl2m([0],2,1),10,2,4) =
00440       ss_natl2m([0],2,1)),
00441     assert(f(
00442         ss_natl2m([14,30,142,142,75,16,210,251,167,99,179,16,123,178,155,169],
00443         2,4),diagmatrix(4,0),10,2,8) = diagmatrix(4,0)),
00444     true)$
00445 
00446 okltest_ss_encrypt_natl(f) := block(
00447     assert(f([0],[0],10,2,4,1) = [7]),
00448     assert(f(create_list(0,i,1,16),create_list(0,i,1,16),10,2,8,4) =
00449       [14,30,142,142,75,16,210,251,167,99,179,16,123,178,155,169]),
00450     true)$
00451 
00452 okltest_ss_decrypt_natl(f) := block(
00453     assert(f([7],[0],10,2,4,1) = [0]),
00454     assert(
00455       f(
00456         [14,30,142,142,75,16,210,251,167,99,179,16,123,178,155,169],
00457         create_list(0,i,1,16),10,2,8,4) = create_list(0,i,1,16)),
00458     true)$
00459 
00460 okltest_ss_encrypt_bin(f) := block(
00461     assert(f([0,0,0,0],[0,0,0,0],10,2,4,1) = [0,1,1,1]),
00462     assert(f(create_list(0,i,1,128),create_list(0,i,1,128),10,2,8,4) =
00463       hexstr2binv("0E1E8E8E4B10D2FBA763B3107BB29BA9")),
00464     true)$
00465 
00466 okltest_ss_decrypt_bin(f) := block(
00467     assert(f([0,1,1,1],[0,0,0,0],10,2,4,1) = [0,0,0,0]),
00468     assert(
00469       f(hexstr2binv("0E1E8E8E4B10D2FBA763B3107BB29BA9"),
00470         create_list(0,i,1,128),10,2,8,4) = create_list(0,i,1,128)),
00471     true)$
00472 
00473 okltest_ss_encrypt_hex(f) := block(
00474     assert(f("0","0",10,2,4,1,1) = "7"),
00475     assert(f("0","0",10,2,8,4,4) =
00476       "0E1E8E8E4B10D2FBA763B3107BB29BA9"),
00477     true)$
00478 
00479 okltest_ss_decrypt_hex(f) := block(
00480     assert(f("7","0",10,2,4,1,1) = "0"),
00481     assert(
00482       f("0E1E8E8E4B10D2FBA763B3107BB29BA9",
00483         "0",10,2,8,4,4) = "00000000000000000000000000000000"),
00484     true)$
00485