Implementation of bit-vector variables in a CP solver, with an application to the generation of cryptographic S-boxes

Sammanfattning: We present a bit-vector variable implementation for the constraint programming (CP) solver Gecode and its application to the problem of finding high-quality cryptographic substitution boxes (S-boxes). S-boxes are a component in some cryptographic protocols, for example DES, which are critical to the strength of the entire system. S-boxes are arrays of bit-vectors, where each bit-vector is itself an array of bits.The desirable properties of an S-box can be described as relationships between its constituent bit-vectors. We represent substitution boxes as arrays of bit-vector variables in Gecode in order to leverage CP techniques for finding high-quality S-boxes. In a CP solver, bit-vectors can alternatively be represented as sets or as arrays of Boolean variables. Experimental evaluation indicates that modeling substitution boxes with bit-vector variables is an improvement over both set- and Boolean-based models. We additionally correct an error in previous work which invalidates the main experimental result, extend a heuristic for evaluating S-box quality, present two symmetries for substitution boxes, define several generic bit-vector propagators, and define propagators for the S-2 and S-7 DES design criteria.