OKlibrary  0.2.1.6
Sboxes.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 19.3.2011 (Swansea) */
00002 /* Copyright 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/Cryptology/Lisp/CryptoSystems/DataEncryptionStandard/Sboxes.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/FiniteFunctions/Basics.mac")$
00025 
00026 
00027 /* The DES S-boxes as full DNF/CNF: */
00028 des_sbox_fulldnf_cl(i) := bf2relation_fulldnf_cl(des_sbox_bf(i),6)$
00029 des_sbox_fullcnf_fcs(i) := bf2relation_fullcnf_fcs(des_sbox_bf(i),6)$
00030 
00031 /* The boolean function for the j-th bit of the i-th DES S-box as
00032    full DNF/CNF: */
00033 des_sbox_bit_fulldnf_cl(i,j) :=
00034   bf2relation_fulldnf_cl(bfnm2n1(des_sbox_bf(i),j),6)$
00035 des_sbox_bit_fullcnf_fcs(i,j) :=
00036   bf2relation_fullcnf_fcs(bfnm2n1(des_sbox_bf(i),j),6)$
00037 
00038 /* Output the full DNF/CNF clause-set representing the i-th DES S-box to the
00039    file "AES_Sbox_full.cnf":
00040 */
00041 output_dessbox_fulldnf_stdname(i) :=
00042   outputext_fcl(
00043     sconcat("The DES Sbox ",i," in full DNF representation."),
00044     cl2fcl(des_sbox_fulldnf_cl(i)),
00045     sconcat("DES_Sbox_",i,"_fullDNF.cnf"))$
00046 output_dessbox_fullcnf_stdname(i) :=
00047   outputext_fcs(
00048     sconcat("The DES Sbox ",i," in full CNF representation."),
00049     des_sbox_fullcnf_fcs(i),
00050     sconcat("DES_Sbox_",i,"_fullCNF.cnf"))$
00051 
00052 /* Output the full DNF/CNF clause-set representing boolean function for the
00053    j-th bit of the i-th DES S-box as full DNF/CNF:
00054 */
00055 output_dessbox_bit_fulldnf_stdname(i,j) :=
00056   outputext_fcl(
00057     sconcat("The boolean function for the ",j,"-th bit DES Sbox ",i,
00058             " in full DNF representation."),
00059     cl2fcl(des_sbox_bit_fulldnf_cl(i,j)),
00060     sconcat("DES_Sbox_",i,"_",j,"_fullDNF.cnf"))$
00061 output_dessbox_bit_fullcnf_stdname(i,j) :=
00062   outputext_fcs(
00063     sconcat("The boolean function for the ",j,"-th bit DES Sbox ",i,
00064             " in full CNF representation."),
00065     des_sbox_bit_fullcnf_fcs(i,j),
00066     sconcat("DES_Sbox_",i,"_",j,"_fullCNF.cnf"))$
00067 
00068 
00069