Since the seminal papers [1] and [2] by Bard, Courtois and Jefferson it seems accepted wisdom that the right thing to do for constructing a CNF representation of a block cipher is to construct an algebraic system of equations first (cf. [3]). This system of equations is then converted to CNF using some ANF to CNF converted (e.g. [4]) which deals with the negative impact of the XORs just introduced via the ANF. On the other hand, it is straight forward to compute some CNF for a given S-Box directly by considering its truth table. Sage now contains code which does this for you:
sage: sr = mq.SR(1,1,1,4,gf2=True,polybori=True) sage: S = sr.sbox() sage: print S.cnf()
[(1, 2, 3, 4, –5), (1, 2, 3, 4, 6), (1, 2, 3, 4, 7), (1, 2, 3, 4, –8), (1, 2, 3, –4, 5), (1, 2, 3, –4, –6), (1, 2, 3, –4, 7), (1, 2, 3, –4, 8), (1, 2, –3, 4, –5), (1, 2, –3, 4, 6), (1, 2, –3, 4, –7),(1, 2, –3, 4, 8), (1, 2, –3, –4, –5), (1, 2, –3, –4, 6), (1, 2, –3, –4, –7), (1, 2, –3, –4, –8), (1, –2, 3, 4, –5), (1, –2, 3, 4, –6), (1, –2, 3, 4, 7), (1, –2, 3, 4, –8), (1, –2, 3, –4, 5), (1, –2, 3, –4, 6), (1, –2, 3, –4, 7), (1, –2, 3, –4, –8), (1, –2, –3, 4, –5), (1, –2, –3, 4, 6), (1, –2, –3,4, 7), (1, –2, –3, 4, 8), (1, –2, –3, –4, 5), (1, –2, –3, –4, –6), (1, –2, –3, –4, 7), (1, –2, –3, –4, –8), (–1, 2, 3, 4, 5), (–1, 2, 3, 4, –6), (–1, 2, 3, 4, –7), (–1, 2, 3, 4, 8), (–1, 2, 3, –4, 5), (–1, 2, 3, –4, 6), (–1, 2, 3, –4, –7), (–1, 2, 3, –4, 8), (–1, 2, –3, 4, 5), (–1, 2, –3, 4, 6), (–1, 2, –3, 4, 7), (–1, 2, –3, 4, 8), (–1, 2, –3, –4, 5), (–1, 2, –3, –4, 6), (–1, 2, –3, –4, –7), (–1, 2, –3, –4, –8), (–1, –2, 3, 4, –5), (–1, –2, 3, 4, –6), (–1, –2, 3, 4, 7), (–1, –2, 3, 4, 8), (–1,–2, 3, –4, –5), (–1, –2, 3, –4, –6), (–1, –2, 3, –4, –7), (–1, –2, 3, –4, 8), (–1, –2, –3, 4, –5), (–1, –2, –3, 4, –6), (–1, –2, –3, 4, –7), (–1, –2, –3, 4, –8), (–1, –2, –3, –4, 5), (–1, –2, –3, –4,–6), (–1, –2, –3, –4, –7), (–1, –2, –3, –4, –8)]
I am not claiming that this naive approach produces an optimal representation, it seems more compact than what ANF to CNF converters produce, though.
