OKlibrary  0.2.1.6
Sboxes.mac
Go to the documentation of this file.
00001 /* Matthew Gwynne, 26.3.2011 (Swansea) */
00002 /* Copyright 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/TestSystem/Lisp/Asserts.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/CryptoSystems/DataEncryptionStandard/Sboxes.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/FiniteFunctions/Basics.mac")$
00025 
00026 kill(f)$
00027 
00028 okltest_desmatrix2bf(f) := block(
00029   assert(
00030     okltest_des_sbox_bf(
00031       buildq([f],
00032         lambda([i], f(des_sbox_matrices[i]))))),      
00033   true)$
00034 
00035 okltest_des_sbox_bf(f) := block(
00036   assert(create_list(f(1)(I),I,lex_bv_l(6)) =
00037     [[1,1,1,0],[0,0,0,0],[0,1,0,0],[1,1,1,1],[1,1,0,1],[0,1,1,1],[0,0,0,1],
00038      [0,1,0,0],[0,0,1,0],[1,1,1,0],[1,1,1,1],[0,0,1,0],[1,0,1,1],[1,1,0,1],
00039      [1,0,0,0],[0,0,0,1],[0,0,1,1],[1,0,1,0],[1,0,1,0],[0,1,1,0],[0,1,1,0],
00040      [1,1,0,0],[1,1,0,0],[1,0,1,1],[0,1,0,1],[1,0,0,1],[1,0,0,1],[0,1,0,1],
00041      [0,0,0,0],[0,0,1,1],[0,1,1,1],[1,0,0,0],[0,1,0,0],[1,1,1,1],[0,0,0,1],
00042      [1,1,0,0],[1,1,1,0],[1,0,0,0],[1,0,0,0],[0,0,1,0],[1,1,0,1],[0,1,0,0],
00043      [0,1,1,0],[1,0,0,1],[0,0,1,0],[0,0,0,1],[1,0,1,1],[0,1,1,1],[1,1,1,1],
00044      [0,1,0,1],[1,1,0,0],[1,0,1,1],[1,0,0,1],[0,0,1,1],[0,1,1,1],[1,1,1,0],
00045      [0,0,1,1],[1,0,1,0],[1,0,1,0],[0,0,0,0],[0,1,0,1],[0,1,1,0],[0,0,0,0],
00046      [1,1,0,1]]),
00047   assert(create_list(f(2)(I),I,lex_bv_l(6)) =
00048     [[1,1,1,1],[0,0,1,1],[0,0,0,1],[1,1,0,1],[1,0,0,0],[0,1,0,0],[1,1,1,0],
00049      [0,1,1,1],[0,1,1,0],[1,1,1,1],[1,0,1,1],[0,0,1,0],[0,0,1,1],[1,0,0,0],
00050      [0,1,0,0],[1,1,1,0],[1,0,0,1],[1,1,0,0],[0,1,1,1],[0,0,0,0],[0,0,1,0],
00051      [0,0,0,1],[1,1,0,1],[1,0,1,0],[1,1,0,0],[0,1,1,0],[0,0,0,0],[1,0,0,1],
00052      [0,1,0,1],[1,0,1,1],[1,0,1,0],[0,1,0,1],[0,0,0,0],[1,1,0,1],[1,1,1,0],
00053      [1,0,0,0],[0,1,1,1],[1,0,1,0],[1,0,1,1],[0,0,0,1],[1,0,1,0],[0,0,1,1],
00054      [0,1,0,0],[1,1,1,1],[1,1,0,1],[0,1,0,0],[0,0,0,1],[0,0,1,0],[0,1,0,1],
00055      [1,0,1,1],[1,0,0,0],[0,1,1,0],[1,1,0,0],[0,1,1,1],[0,1,1,0],[1,1,0,0],
00056      [1,0,0,1],[0,0,0,0],[0,0,1,1],[0,1,0,1],[0,0,1,0],[1,1,1,0],[1,1,1,1],
00057      [1,0,0,1]]),
00058   assert(create_list(f(3)(I),I,lex_bv_l(6)) =
00059     [[1,0,1,0],[1,1,0,1],[0,0,0,0],[0,1,1,1],[1,0,0,1],[0,0,0,0],[1,1,1,0],
00060      [1,0,0,1],[0,1,1,0],[0,0,1,1],[0,0,1,1],[0,1,0,0],[1,1,1,1],[0,1,1,0],
00061      [0,1,0,1],[1,0,1,0],[0,0,0,1],[0,0,1,0],[1,1,0,1],[1,0,0,0],[1,1,0,0],
00062      [0,1,0,1],[0,1,1,1],[1,1,1,0],[1,0,1,1],[1,1,0,0],[0,1,0,0],[1,0,1,1],
00063      [0,0,1,0],[1,1,1,1],[1,0,0,0],[0,0,0,1],[1,1,0,1],[0,0,0,1],[0,1,1,0],
00064      [1,0,1,0],[0,1,0,0],[1,1,0,1],[1,0,0,1],[0,0,0,0],[1,0,0,0],[0,1,1,0],
00065      [1,1,1,1],[1,0,0,1],[0,0,1,1],[1,0,0,0],[0,0,0,0],[0,1,1,1],[1,0,1,1],
00066      [0,1,0,0],[0,0,0,1],[1,1,1,1],[0,0,1,0],[1,1,1,0],[1,1,0,0],[0,0,1,1],
00067      [0,1,0,1],[1,0,1,1],[1,0,1,0],[0,1,0,1],[1,1,1,0],[0,0,1,0],[0,1,1,1],
00068      [1,1,0,0]]),
00069   assert(create_list(f(4)(I),I,lex_bv_l(6)) =
00070     [[0,1,1,1],[1,1,0,1],[1,1,0,1],[1,0,0,0],[1,1,1,0],[1,0,1,1],[0,0,1,1],
00071      [0,1,0,1],[0,0,0,0],[0,1,1,0],[0,1,1,0],[1,1,1,1],[1,0,0,1],[0,0,0,0],
00072      [1,0,1,0],[0,0,1,1],[0,0,0,1],[0,1,0,0],[0,0,1,0],[0,1,1,1],[1,0,0,0],
00073      [0,0,1,0],[0,1,0,1],[1,1,0,0],[1,0,1,1],[0,0,0,1],[1,1,0,0],[1,0,1,0],
00074      [0,1,0,0],[1,1,1,0],[1,1,1,1],[1,0,0,1],[1,0,1,0],[0,0,1,1],[0,1,1,0],
00075      [1,1,1,1],[1,0,0,1],[0,0,0,0],[0,0,0,0],[0,1,1,0],[1,1,0,0],[1,0,1,0],
00076      [1,0,1,1],[0,0,0,1],[0,1,1,1],[1,1,0,1],[1,1,0,1],[1,0,0,0],[1,1,1,1],
00077      [1,0,0,1],[0,0,0,1],[0,1,0,0],[0,0,1,1],[0,1,0,1],[1,1,1,0],[1,0,1,1],
00078      [0,1,0,1],[1,1,0,0],[0,0,1,0],[0,1,1,1],[1,0,0,0],[0,0,1,0],[0,1,0,0],
00079      [1,1,1,0]]),
00080   assert(create_list(f(5)(I),I,lex_bv_l(6)) =
00081     [[0,0,1,0],[1,1,1,0],[1,1,0,0],[1,0,1,1],[0,1,0,0],[0,0,1,0],[0,0,0,1],
00082      [1,1,0,0],[0,1,1,1],[0,1,0,0],[1,0,1,0],[0,1,1,1],[1,0,1,1],[1,1,0,1],
00083      [0,1,1,0],[0,0,0,1],[1,0,0,0],[0,1,0,1],[0,1,0,1],[0,0,0,0],[0,0,1,1],
00084      [1,1,1,1],[1,1,1,1],[1,0,1,0],[1,1,0,1],[0,0,1,1],[0,0,0,0],[1,0,0,1],
00085      [1,1,1,0],[1,0,0,0],[1,0,0,1],[0,1,1,0],[0,1,0,0],[1,0,1,1],[0,0,1,0],
00086      [1,0,0,0],[0,0,0,1],[1,1,0,0],[1,0,1,1],[0,1,1,1],[1,0,1,0],[0,0,0,1],
00087      [1,1,0,1],[1,1,1,0],[0,1,1,1],[0,0,1,0],[1,0,0,0],[1,1,0,1],[1,1,1,1],
00088      [0,1,1,0],[1,0,0,1],[1,1,1,1],[1,1,0,0],[0,0,0,0],[0,1,0,1],[1,0,0,1],
00089      [0,1,1,0],[1,0,1,0],[0,0,1,1],[0,1,0,0],[0,0,0,0],[0,1,0,1],[1,1,1,0],
00090      [0,0,1,1]]),
00091   assert(create_list(f(6)(I),I,lex_bv_l(6)) =
00092     [[1,1,0,0],[1,0,1,0],[0,0,0,1],[1,1,1,1],[1,0,1,0],[0,1,0,0],[1,1,1,1],
00093      [0,0,1,0],[1,0,0,1],[0,1,1,1],[0,0,1,0],[1,1,0,0],[0,1,1,0],[1,0,0,1],
00094      [1,0,0,0],[0,1,0,1],[0,0,0,0],[0,1,1,0],[1,1,0,1],[0,0,0,1],[0,0,1,1],
00095      [1,1,0,1],[0,1,0,0],[1,1,1,0],[1,1,1,0],[0,0,0,0],[0,1,1,1],[1,0,1,1],
00096      [0,1,0,1],[0,0,1,1],[1,0,1,1],[1,0,0,0],[1,0,0,1],[0,1,0,0],[1,1,1,0],
00097      [0,0,1,1],[1,1,1,1],[0,0,1,0],[0,1,0,1],[1,1,0,0],[0,0,1,0],[1,0,0,1],
00098      [1,0,0,0],[0,1,0,1],[1,1,0,0],[1,1,1,1],[0,0,1,1],[1,0,1,0],[0,1,1,1],
00099      [1,0,1,1],[0,0,0,0],[1,1,1,0],[0,1,0,0],[0,0,0,1],[1,0,1,0],[0,1,1,1],
00100      [0,0,0,1],[0,1,1,0],[1,1,0,1],[0,0,0,0],[1,0,1,1],[1,0,0,0],[0,1,1,0],
00101      [1,1,0,1]]),
00102   assert(create_list(f(7)(I),I,lex_bv_l(6)) =
00103     [[0,1,0,0],[1,1,0,1],[1,0,1,1],[0,0,0,0],[0,0,1,0],[1,0,1,1],[1,1,1,0],
00104      [0,1,1,1],[1,1,1,1],[0,1,0,0],[0,0,0,0],[1,0,0,1],[1,0,0,0],[0,0,0,1],
00105      [1,1,0,1],[1,0,1,0],[0,0,1,1],[1,1,1,0],[1,1,0,0],[0,0,1,1],[1,0,0,1],
00106      [0,1,0,1],[0,1,1,1],[1,1,0,0],[0,1,0,1],[0,0,1,0],[1,0,1,0],[1,1,1,1],
00107      [0,1,1,0],[1,0,0,0],[0,0,0,1],[0,1,1,0],[0,0,0,1],[0,1,1,0],[0,1,0,0],
00108      [1,0,1,1],[1,0,1,1],[1,1,0,1],[1,1,0,1],[1,0,0,0],[1,1,0,0],[0,0,0,1],
00109      [0,0,1,1],[0,1,0,0],[0,1,1,1],[1,0,1,0],[1,1,1,0],[0,1,1,1],[1,0,1,0],
00110      [1,0,0,1],[1,1,1,1],[0,1,0,1],[0,1,1,0],[0,0,0,0],[1,0,0,0],[1,1,1,1],
00111      [0,0,0,0],[1,1,1,0],[0,1,0,1],[0,0,1,0],[1,0,0,1],[0,0,1,1],[0,0,1,0],
00112      [1,1,0,0]]),
00113   assert(create_list(f(8)(I),I,lex_bv_l(6)) =
00114     [[1,1,0,1],[0,0,0,1],[0,0,1,0],[1,1,1,1],[1,0,0,0],[1,1,0,1],[0,1,0,0],
00115      [1,0,0,0],[0,1,1,0],[1,0,1,0],[1,1,1,1],[0,0,1,1],[1,0,1,1],[0,1,1,1],
00116      [0,0,0,1],[0,1,0,0],[1,0,1,0],[1,1,0,0],[1,0,0,1],[0,1,0,1],[0,0,1,1],
00117      [0,1,1,0],[1,1,1,0],[1,0,1,1],[0,1,0,1],[0,0,0,0],[0,0,0,0],[1,1,1,0],
00118      [1,1,0,0],[1,0,0,1],[0,1,1,1],[0,0,1,0],[0,1,1,1],[0,0,1,0],[1,0,1,1],
00119      [0,0,0,1],[0,1,0,0],[1,1,1,0],[0,0,0,1],[0,1,1,1],[1,0,0,1],[0,1,0,0],
00120      [1,1,0,0],[1,0,1,0],[1,1,1,0],[1,0,0,0],[0,0,1,0],[1,1,0,1],[0,0,0,0],
00121      [1,1,1,1],[0,1,1,0],[1,1,0,0],[1,0,1,0],[1,0,0,1],[1,1,0,1],[0,0,0,0],
00122      [1,1,1,1],[0,0,1,1],[0,0,1,1],[0,1,0,1],[0,1,0,1],[0,1,1,0],[1,0,0,0],
00123      [1,0,1,1]]),
00124   true)$
00125 
00126 okltest_des_6t1_sbox_bf(f) := block(
00127   assert(
00128     okltest_des_sbox_bf(
00129       buildq([f], lambda([i],
00130           buildq([i], lambda([x],
00131               append(f(i,1)(x), f(i,2)(x), f(i,3)(x), f(i,4)(x)))))))),
00132   true)$
00133 
00134 okltest_des_comb_sbox_bf(f) := block(
00135   assert(f([])([]) = []),
00136   assert(
00137     okltest_des_sbox_bf(
00138       buildq([f], lambda([i], f(create_list((i-1)*4+j, j, 1,4)))))),
00139   assert(
00140     f([1,2])([0,0,0,0,0,0]) = [1,1]),
00141   assert(
00142     f([1,2])([0,1,0,0,1,0,0]) = [1,0]),
00143   if oklib_test_level = 0 then return(true),
00144   assert(block([lex_bv_l_12 : lex_bv_l(12)],
00145     create_list(f([1,2,3,4,9,10,11,12])(I),I,lex_bv_l_12) =
00146     create_list(append(des_sbox_bf(1)(I),des_sbox_bf(3)(I)),I,lex_bv_l_12))),
00147   true)$
00148