| 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,)) |