OKlibrary  0.2.1.6
ConstraintTranslation.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 20.3.2011 (Swansea) */
00002 /* Copyright 2011, 2012, 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/DataEncryptionStandard/Cipher.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/CryptoSystems/DataEncryptionStandard/RoundFunction.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Cryptology/Lisp/CryptoSystems/DataEncryptionStandard/KeySchedule.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/LinearEquations.mac")$
00027 
00028 
00029 /* *************
00030    * Variables *
00031    *************
00032 */
00033 
00034 /* desr(i,r) for i in {1,...,32} and r in {-1,0,...,16} represents the 16
00035    rounds as follows:
00036 
00037     - desr(i,-1) = plaintext[des_init_permutation[i]]
00038     - desr(i,0)  = plaintext[des_init_permutation[32+i]]
00039     - desr(i,r)  = the result of round r for 1 <= r <= 16
00040 
00041    Then
00042      ciphertext[i] =
00043      append(create_list(desr(i,16),i,1,32),create_list(desr(i,15),i,1,32))[des_final_permutation[i]].
00044 
00045 */
00046 
00047 declare(desr, noun)$
00048 declare(desr, posfun)$
00049 desr_var(i,r) := nounify(desr)(i,r)$
00050 
00051 /* desk(i) for i in {1,...,64} represents the key via
00052 
00053      desk(i) = key[des_key_initial_selection[i]].
00054 
00055 */
00056 
00057 declare(desk, noun)$
00058 declare(desk, posfun)$
00059 desk_var(i) := nounify(desk)(i)$
00060 
00061 /* desi(i,r) for i in {1,...,48} and r in {1,...,16} represents the input
00062    to the S-boxes in round r.
00063 */
00064 
00065 declare(desi, noun)$
00066 declare(desi, posfun)$
00067 desi_var(i,r) := nounify(desi)(i,r)$
00068 
00069 /* deso(i,r) for i in {1,...,32} and r in {1,...,16} represents the output
00070    of the S-boxes in round r.
00071 */
00072 
00073 declare(deso, noun)$
00074 declare(deso, posfun)$
00075 deso_var(i,r) := nounify(deso)(i,r)$
00076 
00077 /* desaux(i) for i in {1,...} represents the i-th auxilliary variable
00078    introduced when translating des.
00079 */
00080 
00081 declare(desaux, noun)$
00082 declare(desaux, posfun)$
00083 desaux_var(i) := nounify(desaux)(i)$
00084 
00085 
00086 /* *******************
00087    * xor-Constraints *
00088    *******************
00089 */
00090 
00091 /* See ComputerAlgebra/Satisfiability/Lisp/LinearConditions/plans/general.hpp
00092    for xor-constraints.
00093 */
00094 
00095 /*
00096   For i in {1,...,48} and r in {1,...,16}:
00097 
00098   desi(i,r) =
00099     desr(des_expansion[i],r-1) + desk(des_round_keys_template()[r][i])
00100 
00101 */
00102 
00103 /* For r in {1,...,16}: */
00104 des_xor_desi(r) := block([key : des_round_keys_template()[r]],
00105  create_list(
00106   [[desr_var(des_expansion[i],r-1), desk_var(key[i]),
00107     desi_var(i,r)],
00108    0],
00109   i,1,48))$
00110 
00111 /*
00112   For i in {1,...,32} and r in {1,...,16}:
00113 
00114   desr(i,r) = desr(i,r-2) + deso(des_pbox[i],r).
00115 
00116 */
00117 
00118 /* For r in {1,...,16}: */
00119 des_xor_desr(r) := create_list(
00120  [[desr_var(i,r-2), deso_var(des_pbox[i],r), desr_var(i,r)], 0],
00121  i,1,32)$
00122 
00123 
00124 /* *********************
00125    * S-box constraints *
00126    *********************
00127 */
00128 
00129 /*
00130   A "DES S-box constraint for box number i" is a triple
00131 
00132   [i,[v_1,...v_6],[w_1,...,w_4]]
00133 
00134   where v_1,...,v_6 are the input variables and w_1,...,w_4 are the
00135   output variables.
00136 */
00137 
00138 /* For r in {1,...,16}: */
00139 des_sbox_deso(r) := block(
00140  [I : partition_elements(create_list(desi_var(i,r),i,1,48),6),
00141   O : partition_elements(create_list(deso_var(i,r),i,1,32),4)],
00142   create_list([i,I[i],O[i]], i,1,8))$
00143 
00144 
00145 /* ***********************
00146    * The complete system *
00147    ***********************
00148 */
00149 
00150 /* The xor-constraints in round 1 <= r <= 16: */
00151 des_round_xor(r) := append(des_xor_desi(r), des_xor_desr(r))$
00152 
00153 /* All xor-constraints: */
00154 des_xor() := lappend(create_list(des_round_xor(r),r,1,16))$
00155 
00156 /* All sbox-constraints: */
00157 des_sboxc() := lappend(create_list(des_sbox_deso(r),r,1,16))$
00158 
00159 /* All (constraint-)variables: */
00160 des_var() := append(
00161  create_list(desr_var(i,r), r,-1,16, i,1,32),
00162  create_list(desk_var(i), i,1,64),
00163  create_list(desi_var(i,r), r,1,16, i,1,48),
00164  create_list(deso_var(i,r), r,1,16, i,1,32))$
00165 
00166 /*
00167   Translating plaintext-, ciphertext- and key-assignments into formal
00168   clause-sets and partial assignments, using partial boolean vectors.
00169   A "partial boolean vector" contains besides 0,1 also possibly "und".
00170 */
00171 
00172 /* Translating the partial boolean vector, plain, of length 64, to
00173    the corresponding partial assignment on the DES plaintext variables. The
00174    partial assignment sets the i-th DES plaintext variable to plain[i],
00175    for all i where plain[i] is defined. */
00176 des_plain2pa(plain) := block(
00177   [V : create_list(desr_var(i,r), r,-1,0, i,1,32)],
00178   setify(
00179     delete(und,
00180          create_list(block([x:plain[i]],
00181              if x=und then und else (2*x-1)*V[des_final_permutation[i]]),
00182            i,1,64))))$
00183 /* Now translating plain to a formal clause-list containing exactly the
00184    unit-clauses satisfied by des_plain2pa(plain). The variable list is
00185    the list of all plaintext variables. The order of the variable-
00186    and clause-lists is the standard one on the DES plaintext variables. */
00187 des_plain2fcl(plain) := block(
00188   [V : create_list(desr_var(i,r), r,-1,0, i,1,32), L],
00189   L : sort(listify(des_plain2pa(plain)), l2order_p(interleave_l(-V,V))),
00190   [V, map(set,L)])$
00191 
00192 /* Translating the partial boolean vector, cipher, of length 64, to
00193    the partial assignment on the DES ciphertext variables. The partial
00194    assignment sets the i-th DES ciphertext variable to cipher[i],
00195    for all i where cipher[i] is defined. */
00196 des_cipher2pa(cipher) := block(
00197   [V : create_list(desr_var(i,r), r,[16,15], i,1,32)],
00198   setify(
00199     delete(und,
00200          create_list(block([x:cipher[i]],
00201              if x=und then und else (2*x-1)*V[des_final_permutation[i]]),
00202            i,1,64))))$
00203 /* Now translating cipher to a formal clause-list containing exactly the
00204    unit-clauses satisfied by des_cipher2pa(cipher). The variable list is
00205    the list of all ciphertext variables. The order of the variable-
00206    and clause-lists is the standard one on the DES ciphertext variables. */
00207 des_cipher2fcl(cipher) := block(
00208   [V : create_list(desr_var(i,r), r,[16,15], i,1,32), L],
00209   L : sort(listify(des_cipher2pa(cipher)), l2order_p(interleave_l(-V,V))),
00210   [V, map(set,L)])$
00211 
00212 /* Translating the partial boolean vector, key, of length 64, to
00213    the partial assignment on the DES key variables. The partial
00214    assignment sets the i-th DES key variable to key[i], for all i
00215    where key[i] is defined. */
00216 des_key2pa(key) := block(
00217   [V : create_list(desk_var(i), i,1,64)],
00218   setify(
00219     delete(und,
00220            create_list(
00221              block([x:key[i]],
00222                if x=und then und else (2*x-1)*V[i]),
00223              i,1,64))))$
00224 /* Now translating key to a formal clause-list containing exactly the
00225    unit-clauses satisfied by des_key2pa(key). The variable list is
00226    the list of all key variables. The order of the variable-
00227    and clause-lists is the standard one on the DES key variables. */
00228 des_key2fcl(key) := block(
00229   [V : create_list(desk_var(i), i,1,64), L],
00230   L : sort(listify(des_key2pa(key)), l2order_p(interleave_l(-V,V))),
00231   [V, map(set,L)])$
00232 
00233 
00234 
00235 /* ***********************
00236    * CNF translation     *
00237    ***********************
00238 */
00239 
00240 
00241 /* Generates a CNF formal clause-list representing the r-round DES.
00242 
00243    Sbox i is translated using the formal clause-list sbox_l[i] for i in
00244    {1,...,8}. The input and output variables of Sbox i are
00245    [sbox_l[i][1],...,sbox_l[i][10]]. All other variables in sbox_l[i] are
00246    auxilliary variables used by the representation.
00247    Xor constraints are translated using their prime implicates. */
00248 des2fcl(sbox_l) := block(
00249   [xor_cl_l, sbox_cl_l : [], num_sbox_aux_var_l,
00250    new_var_ind : 1, rename_aux_vars],
00251   xor_cl_l : create_list(even_parity_wv_cl(C[1]), C, des_xor),
00252   num_sbox_aux_var_l : create_list(length(sbox_l[i][1])-10, i, 1, 8),
00253   rename_aux_vars : lambda([sbox_cst],
00254     block([aux_vars],
00255       aux_vars :
00256         create_list(desaux_var(i),
00257           i, new_var_ind, new_var_ind + num_sbox_aux_var_l[sbox_cst[1]]-1),
00258       new_var_ind : new_var_ind + num_sbox_aux_var_l[sbox_cst[1]],
00259       rename_fcl(sbox_l[sbox_cst[1]],
00260         append(sbox_cst[2],sbox_cst[3],aux_vars))[2])),
00261   sbox_cl_l : map(rename_aux_vars, des_sboxc),
00262   return([append(des_var(),create_list(desaux_var(i),i,1,new_var_i-1)),
00263           lappend(append(xor_cl_l,reverse(sbox_cl_l)))]))$
00264