Ticket #6185: sbox_cnf.patch

File sbox_cnf.patch, 7.3 KB (added by malb, 12 years ago)
  • sage/crypto/mq/sbox.py

    # HG changeset patch
    # User Martin Albrecht <malb@informatik.uni-bremen.de>
    # 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 b  
    334334
    335335        The rows of $A$ encode the differences $\Delta I$ of the input
    336336        and the columns encode the difference $\Delta O$ for the
    337         output. The bits are ordered according to the endianess of
     337        output. The bits are ordered according to the endianness of
    338338        this S-box. The value at $A[\Delta I,\Delta O]$ encoded how
    339339        often $\Delta O$ is the actual output difference given $\Delta
    340340        I$ as input difference.
     
    724724        P = PolynomialRing(k,'x')
    725725        return P.lagrange_polynomial(l)
    726726           
     727    def cnf(self, xi=None, yi=None, format=None):
     728        """
     729        Return a representation of this S-Box in conjuctive normal
     730        form.
     731
     732        This function examines the truth tables for each output bit of
     733        the S-Box and thus has complexity `n * 2^m` for an ``m x n``
     734        S-Box.
     735
     736        INPUT:
     737       
     738        - ``xi`` - indices for the input variables (default: ``1...m``)
     739
     740        - ``yi`` - indices for the output variables (default: ``m+1 ... m+n``)
     741
     742        - ``format`` - output format, see below (default: ``None``)
     743
     744        FORMATS:
     745
     746        - ``None`` - return a list of tuples of integers where each
     747          tuple represents a clause, the absolute value of an integer
     748          represents a variable and the sign of an integer indicates
     749          inversion.
     750
     751        - ``symbolic`` - a string that can be parsed by the
     752          ``SymbolicLogic`` package.
     753
     754        - ``dimacs`` - a string in DIMACS format which is the gold
     755          standard for SAT-solver input (cf. http://www.satlib.org/).
     756
     757        - ``dimacs_headless`` - a string in DIMACS format, but without
     758          the header. This is useful for concatenation of outputs.
     759
     760        EXAMPLE:
     761
     762        We give a very small example to explain the output format::
     763
     764            sage: S = mq.SBox(1,2,0,3); S
     765            (1, 2, 0, 3)
     766            sage: cnf = S.cnf(); cnf
     767            [(1, 2, -3),  (1, 2, 4),
     768             (1, -2, 3),  (1, -2, -4),
     769             (-1, 2, -3), (-1, 2, -4),
     770             (-1, -2, 3), (-1, -2, 4)]
     771 
     772        This output completely describes the S-Box. For instance, we
     773        can check that ``S([0,1]) -> [1,0]`` satisfies every clause if
     774        the first input bit corresponds to the index ``1`` and the
     775        last output bit corresponds to the index ``3`` in the
     776        output.
     777
     778        We can convert this representation to the DIMACS format::
     779
     780            sage: print S.cnf(format='dimacs')
     781            p cnf 4 8
     782            1 2 -3 0
     783            1 2 4 0
     784            1 -2 3 0
     785            1 -2 -4 0
     786            -1 2 -3 0
     787            -1 2 -4 0
     788            -1 -2 3 0
     789            -1 -2 4 0
     790       
     791        For concatenation we can strip the header::
     792
     793            sage: print S.cnf(format='dimacs_headless')
     794            1 2 -3 0
     795            1 2 4 0
     796            1 -2 3 0
     797            1 -2 -4 0
     798            -1 2 -3 0
     799            -1 2 -4 0
     800            -1 -2 3 0
     801            -1 -2 4 0
     802       
     803        This might be helpful in combination with the ``xi`` and
     804        ``yi`` parameter to assign indices manually::
     805
     806            sage: print S.cnf(xi=[10,20],yi=[30,40], format='dimacs_headless')
     807            10 20 -30 0
     808            10 20 40 0
     809            10 -20 30 0
     810            10 -20 -40 0
     811            -10 20 -30 0
     812            -10 20 -40 0
     813            -10 -20 30 0
     814            -10 -20 40 0
     815
     816        We can also return a string which is parse-able by the
     817        ``SymbolicLogic`` package::
     818
     819            sage: log = SymbolicLogic()
     820            sage: s = log.statement(S.cnf(format='symbolic'))
     821            sage: log.truthtable(s)[1:]
     822            [['False', 'False', 'False', 'False', 'False'],
     823             ['False', 'False', 'False', 'True', 'False'],
     824             ['False', 'False', 'True', 'False', 'False'],
     825             ['False', 'False', 'True', 'True', 'True'],
     826             ['False', 'True', 'False', 'False', 'True'],
     827             ['False', 'True', 'False', 'True', 'True'],
     828             ['False', 'True', 'True', 'False', 'True'],
     829             ['False', 'True', 'True', 'True', 'True'],
     830             ['True', 'False', 'False', 'False', 'True'],
     831             ['True', 'False', 'False', 'True', 'True'],
     832             ['True', 'False', 'True', 'False', 'True'],
     833             ['True', 'False', 'True', 'True', 'True'],
     834             ['True', 'True', 'False', 'False', 'True'],
     835             ['True', 'True', 'False', 'True', 'True'],
     836             ['True', 'True', 'True', 'False', 'True'],
     837             ['True', 'True', 'True', 'True', 'True']]
     838
     839
     840        This function respects endianness of the S-Box::
     841
     842            sage: S = mq.SBox(1,2,0,3, big_endian=False); S
     843            (1, 2, 0, 3)
     844            sage: cnf = S.cnf(); cnf
     845            [(1, 2, -4), (1, 2, 3),
     846             (-1, 2, 4), (-1, 2, -3),
     847             (1, -2, -4), (1, -2, -3),
     848             (-1, -2, 4), (-1, -2, 3)]
     849
     850        TESTS:
     851
     852            sage: S = mq.SBox(1,2,0,3, big_endian=False)
     853            sage: S.cnf([1000,1001,1002], [2000,2001,2002])
     854            Traceback (most recent call last):
     855            ...
     856            TypeError: first arg required to have length 2, got 3 instead.
     857        """
     858        m, n = self.m, self.n
     859
     860        if xi is None:
     861            xi = [i+1 for i in range(m)]
     862
     863        if yi is None:
     864            yi = [m+i+1 for i in range(n)]
     865
     866        if len(xi) != m:
     867            raise TypeError("first arg required to have length %d, got %d instead."%(m,len(xi)))
     868
     869        if len(xi) != n:
     870            raise TypeError("second arg required to have length %d, got %d instead."%(n,len(yi)))
     871
     872        output_bits = range(n)
     873        if not self._big_endian:
     874            output_bits = list(reversed(output_bits))
     875
     876        C = [] # the set of clauses
     877        for e in xrange(2**m):
     878            x = self.to_bits(e)
     879            y = self(x) # evaluate at x
     880            for output_bit in output_bits: # consider each bit
     881                clause = [(-1)**(int(v)) * i for v,i in zip(x, xi)]
     882                clause.append( (-1)**(1-int(y[output_bit])) *  yi[output_bit] )
     883                C.append(tuple(clause))
     884
     885        if format is None:
     886            return C
     887        elif format == 'symbolic':
     888            gd = self.ring().gens()
     889            formula = []
     890            for clause in C:
     891                clause = "|".join([str(gd[abs(v)-1]).replace("-","~") for v in clause])
     892                formula.append("("+clause+")")
     893            return " & ".join(formula)
     894
     895        elif format.startswith('dimacs'):
     896            if format == "dimacs_headless":
     897                header = ""
     898            else:
     899                header = "p cnf %d %d\n"%(m+n,len(C))
     900            values = " 0\n".join([" ".join(map(str,line)) for line in C])
     901            return header + values + " 0\n"
     902        else:
     903            raise ValueError("Format '%s' not supported."%(format,))