# HG changeset patch # User Martin Albrecht # Date 1243939880 -3600 # Node ID 9a36f457fb4b2eaa66e92aa48d72285a6e5a1da4 # Parent 39cd4790b09a26f825e8d65e33f7ded9d566edf4 added support for constructing CNF for mq.SBox diff -r 39cd4790b09a -r 9a36f457fb4b sage/crypto/mq/sbox.py --- a/sage/crypto/mq/sbox.py Fri Dec 12 18:06:27 2008 +0000 +++ b/sage/crypto/mq/sbox.py Tue Jun 02 11:51:20 2009 +0100 @@ -334,7 +334,7 @@ The rows of $A$ encode the differences $\Delta I$ of the input and the columns encode the difference $\Delta O$ for the - output. The bits are ordered according to the endianess of + output. The bits are ordered according to the endianness of this S-box. The value at $A[\Delta I,\Delta O]$ encoded how often $\Delta O$ is the actual output difference given $\Delta I$ as input difference. @@ -724,3 +724,180 @@ P = PolynomialRing(k,'x') return P.lagrange_polynomial(l) + def cnf(self, xi=None, yi=None, format=None): + """ + Return a representation of this S-Box in conjuctive normal + form. + + This function examines the truth tables for each output bit of + the S-Box and thus has complexity `n * 2^m` for an ``m x n`` + S-Box. + + INPUT: + + - ``xi`` - indices for the input variables (default: ``1...m``) + + - ``yi`` - indices for the output variables (default: ``m+1 ... m+n``) + + - ``format`` - output format, see below (default: ``None``) + + FORMATS: + + - ``None`` - return a list of tuples of integers where each + tuple represents a clause, the absolute value of an integer + represents a variable and the sign of an integer indicates + inversion. + + - ``symbolic`` - a string that can be parsed by the + ``SymbolicLogic`` package. + + - ``dimacs`` - a string in DIMACS format which is the gold + standard for SAT-solver input (cf. http://www.satlib.org/). + + - ``dimacs_headless`` - a string in DIMACS format, but without + the header. This is useful for concatenation of outputs. + + EXAMPLE: + + We give a very small example to explain the output format:: + + sage: S = mq.SBox(1,2,0,3); S + (1, 2, 0, 3) + sage: cnf = S.cnf(); cnf + [(1, 2, -3), (1, 2, 4), + (1, -2, 3), (1, -2, -4), + (-1, 2, -3), (-1, 2, -4), + (-1, -2, 3), (-1, -2, 4)] + + This output completely describes the S-Box. For instance, we + can check that ``S([0,1]) -> [1,0]`` satisfies every clause if + the first input bit corresponds to the index ``1`` and the + last output bit corresponds to the index ``3`` in the + output. + + We can convert this representation to the DIMACS format:: + + sage: print S.cnf(format='dimacs') + p cnf 4 8 + 1 2 -3 0 + 1 2 4 0 + 1 -2 3 0 + 1 -2 -4 0 + -1 2 -3 0 + -1 2 -4 0 + -1 -2 3 0 + -1 -2 4 0 + + For concatenation we can strip the header:: + + sage: print S.cnf(format='dimacs_headless') + 1 2 -3 0 + 1 2 4 0 + 1 -2 3 0 + 1 -2 -4 0 + -1 2 -3 0 + -1 2 -4 0 + -1 -2 3 0 + -1 -2 4 0 + + This might be helpful in combination with the ``xi`` and + ``yi`` parameter to assign indices manually:: + + sage: print S.cnf(xi=[10,20],yi=[30,40], format='dimacs_headless') + 10 20 -30 0 + 10 20 40 0 + 10 -20 30 0 + 10 -20 -40 0 + -10 20 -30 0 + -10 20 -40 0 + -10 -20 30 0 + -10 -20 40 0 + + We can also return a string which is parse-able by the + ``SymbolicLogic`` package:: + + sage: log = SymbolicLogic() + sage: s = log.statement(S.cnf(format='symbolic')) + sage: log.truthtable(s)[1:] + [['False', 'False', 'False', 'False', 'False'], + ['False', 'False', 'False', 'True', 'False'], + ['False', 'False', 'True', 'False', 'False'], + ['False', 'False', 'True', 'True', 'True'], + ['False', 'True', 'False', 'False', 'True'], + ['False', 'True', 'False', 'True', 'True'], + ['False', 'True', 'True', 'False', 'True'], + ['False', 'True', 'True', 'True', 'True'], + ['True', 'False', 'False', 'False', 'True'], + ['True', 'False', 'False', 'True', 'True'], + ['True', 'False', 'True', 'False', 'True'], + ['True', 'False', 'True', 'True', 'True'], + ['True', 'True', 'False', 'False', 'True'], + ['True', 'True', 'False', 'True', 'True'], + ['True', 'True', 'True', 'False', 'True'], + ['True', 'True', 'True', 'True', 'True']] + + + This function respects endianness of the S-Box:: + + sage: S = mq.SBox(1,2,0,3, big_endian=False); S + (1, 2, 0, 3) + sage: cnf = S.cnf(); cnf + [(1, 2, -4), (1, 2, 3), + (-1, 2, 4), (-1, 2, -3), + (1, -2, -4), (1, -2, -3), + (-1, -2, 4), (-1, -2, 3)] + + TESTS: + + sage: S = mq.SBox(1,2,0,3, big_endian=False) + sage: S.cnf([1000,1001,1002], [2000,2001,2002]) + Traceback (most recent call last): + ... + TypeError: first arg required to have length 2, got 3 instead. + """ + m, n = self.m, self.n + + if xi is None: + xi = [i+1 for i in range(m)] + + if yi is None: + yi = [m+i+1 for i in range(n)] + + if len(xi) != m: + raise TypeError("first arg required to have length %d, got %d instead."%(m,len(xi))) + + if len(xi) != n: + raise TypeError("second arg required to have length %d, got %d instead."%(n,len(yi))) + + output_bits = range(n) + if not self._big_endian: + output_bits = list(reversed(output_bits)) + + C = [] # the set of clauses + for e in xrange(2**m): + x = self.to_bits(e) + y = self(x) # evaluate at x + for output_bit in output_bits: # consider each bit + clause = [(-1)**(int(v)) * i for v,i in zip(x, xi)] + clause.append( (-1)**(1-int(y[output_bit])) * yi[output_bit] ) + C.append(tuple(clause)) + + if format is None: + return C + elif format == 'symbolic': + gd = self.ring().gens() + formula = [] + for clause in C: + clause = "|".join([str(gd[abs(v)-1]).replace("-","~") for v in clause]) + formula.append("("+clause+")") + return " & ".join(formula) + + elif format.startswith('dimacs'): + if format == "dimacs_headless": + header = "" + else: + header = "p cnf %d %d\n"%(m+n,len(C)) + values = " 0\n".join([" ".join(map(str,line)) for line in C]) + return header + values + " 0\n" + else: + raise ValueError("Format '%s' not supported."%(format,))