Feature/quasidifferential implementation

claasp/components/and_component.py

@@ -128,6 +128,7 @@ class And(MultiInputNonlinearLogicalOperator):
         sage: print(component3.description)  # 6 total bits / output_bit_size 2 = 3 operands
         ['AND', 3]
     """
+
     def __init__(
         self,
         current_round_number,
@@ -396,7 +397,7 @@ def sat_constraints(self):
         output_bit_ids = self._generate_output_ids()
         constraints = []
         for i, output_bit_id in enumerate(output_bit_ids):
-            constraints.extend(sat_utils.cnf_and(output_bit_id, input_bit_ids[i::self.output_bit_size]))
+            constraints.extend(sat_utils.cnf_and(output_bit_id, input_bit_ids[i :: self.output_bit_size]))
 
         return output_bit_ids, constraints
 
@@ -425,8 +426,10 @@ def smt_constraints(self):
         output_bit_ids = self._generate_output_ids()
         constraints = []
         for i, output_bit_id in enumerate(output_bit_ids):
-            operation = smt_utils.smt_and(input_bit_ids[i::self.output_bit_size])
+            operation = smt_utils.smt_and(input_bit_ids[i :: self.output_bit_size])
             equation = smt_utils.smt_equivalent((output_bit_id, operation))
             constraints.append(smt_utils.smt_assert(equation))
 
         return output_bit_ids, constraints
+
+

claasp/components/cipher_output_component.py

@@ -50,6 +50,7 @@ class CipherOutput(Component):
         sage: print(component.description)
         ['cipher_output']
     """
+
     def __init__(
         self,
         current_round_number,
@@ -290,29 +291,23 @@ def cp_continuous_differential_propagation_constraints(self, model):
         component_id = self.id
         ninputs = self.input_bit_size
         num_links = len(self.input_id_links)
-        
+
         cp_declarations = []
         cp_constraints = []
-        
+
         for i in range(num_links):
             link_size = len(self.input_bit_positions[i])
-            cp_declarations.append(
-                f"array[0..{link_size - 1}] of var -1.0..1.0: x{i+1}_{component_id};"
-            )
-
-        cp_declarations.append(
-            f"array[0..{ninputs - 1}] of var -1.0..1.0: {component_id};"
-        )
-
+            cp_declarations.append(f"array[0..{link_size - 1}] of var -1.0..1.0: x{i + 1}_{component_id};")
+
+        cp_declarations.append(f"array[0..{ninputs - 1}] of var -1.0..1.0: {component_id};")
+
         output_idx = 0
         for i in range(num_links):
             link_size = len(self.input_bit_positions[i])
             for j in range(link_size):
-                cp_constraints.append(
-                    f"constraint {component_id}[{output_idx}] = x{i+1}_{component_id}[{j}];"
-                )
+                cp_constraints.append(f"constraint {component_id}[{output_idx}] = x{i + 1}_{component_id}[{j}];")
                 output_idx += 1
-        
+
         return cp_declarations, cp_constraints
 
     def get_byte_based_vectorized_python_code(self, params):
@@ -743,3 +738,68 @@ def smt_xor_linear_mask_propagation_constraints(self, model=None):
             constraints.append(smt_utils.smt_assert(equation))
 
         return output_bit_ids + input_bit_ids, constraints
+
+    def smt_xor_quasidifferential_propagation_constraints(
+        self,
+        model,
+    ):
+        """
+        Return SMT constraints for CIPHER OUTPUT quasidifferential propagation.
+
+        A cipher output (and, unless overridden for fork-handling,
+        an intermediate output -- see IntermediateOutput) is a pure
+        copy of its input. For an identity map, Theorem 3.2 (5) gives
+        trivial propagation for BOTH the difference and the mask:
+        b = a and u = v, with weight 0.
+
+        NOTE: if this component's input wire is also consumed
+        elsewhere (a "fork" in the cipher's data-flow graph), the
+        mask-propagation rule is NOT plain equality but an
+        XOR-combination of all the branches' masks (the dual of the
+        XOR-of-differences rule at a join point). The input mask read
+        here is then this component's own branch mask, given by
+        ``model._qdt_input_bit_ids``, and the model ties the branches to
+        the source in ``SmtXorQuasidifferentialModel._fork_constraints``.
+
+        INPUT:
+
+        - ``model`` -- **model object**; a ``SmtXorQuasidifferentialModel`` instance
+
+        EXAMPLES::
+
+            sage: from claasp.ciphers.single_component_ciphers.constant_cipher import ConstantCipher
+            sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel
+            sage: cipher = ConstantCipher(output_bit_size=3, value=2)
+            sage: output = cipher.component_from_id('cipher_output_0_1')
+            sage: variables, constraints = output.smt_xor_quasidifferential_propagation_constraints(SmtXorQuasidifferentialModel(cipher))
+            sage: constraints
+            ['(assert (= cipher_output_0_1_0 constant_0_0_0))',
+             '(assert (= cipher_output_0_1_1 constant_0_0_1))',
+             '(assert (= cipher_output_0_1_2 constant_0_0_2))',
+             '(assert (= qdt_cipher_output_0_1_0 qdt_constant_0_0_0))',
+             '(assert (= qdt_cipher_output_0_1_1 qdt_constant_0_0_1))',
+             '(assert (= qdt_cipher_output_0_1_2 qdt_constant_0_0_2))']
+        """
+
+        input_bit_ids = self._generate_input_ids()
+        output_bit_ids = self._generate_output_ids()
+
+        qdt_input_bit_ids = model._qdt_input_bit_ids(self)
+        qdt_output_bit_ids = [f"qdt_{bit_id}" for bit_id in output_bit_ids]
+
+        constraints = []
+
+        for output_bit_id, input_bit_id in zip(output_bit_ids, input_bit_ids):
+            equation = smt_utils.smt_equivalent([output_bit_id, input_bit_id])
+            constraints.append(smt_utils.smt_assert(equation))
+
+        for output_bit_id, input_bit_id in zip(qdt_output_bit_ids, qdt_input_bit_ids):
+            equation = smt_utils.smt_equivalent([output_bit_id, input_bit_id])
+            constraints.append(smt_utils.smt_assert(equation))
+
+        variables = output_bit_ids + qdt_output_bit_ids
+
+        return (
+            variables,
+            constraints,
+        )

claasp/components/constant_component.py

@@ -97,6 +97,7 @@ class Constant(Component):
         sage: print(component.description)
         ['0b0001000']
     """
+
     def __init__(self, current_round_number, current_round_number_of_components, output_bit_size, value):
         component_id = f"{CONSTANT}_{current_round_number}_{current_round_number_of_components}"
         component_type = CONSTANT
@@ -208,17 +209,12 @@ def cp_continuous_differential_propagation_constraints(self, model):
         """
         size = self.output_bit_size
 
-        cp_declarations = [
-            f"array[0..{size - 1}] of var -1.0..1.0: {self.id};"
-        ]
+        cp_declarations = [f"array[0..{size - 1}] of var -1.0..1.0: {self.id};"]
 
-        cp_constraints = [
-            f"constraint {self.id}[{i}] = -1.0;"
-            for i in range(size)
-        ]
+        cp_constraints = [f"constraint {self.id}[{i}] = -1.0;" for i in range(size)]
 
         return cp_declarations, cp_constraints
-    
+
     def cp_deterministic_truncated_xor_differential_trail_constraints(self):
         return self.cp_xor_differential_propagation_constraints()
 
@@ -769,3 +765,58 @@ def smt_xor_linear_mask_propagation_constraints(self, model=None):
         output_bit_ids = self._generate_output_ids(suffix=constants.OUTPUT_BIT_ID_SUFFIX)
 
         return output_bit_ids, []
+
+    def smt_xor_quasidifferential_propagation_constraints(
+        self,
+        model,
+    ):
+        """
+        Return SMT constraints for CONSTANT quasidifferential propagation.
+
+        Per Beyne & Rijmen, Theorem 3.2 (4): for a translation
+        F(x) = x + t (a constant is exactly such a translation),
+
+            D^F_(v,b),(u,a) = chi_v(t) * delta_v(u) * delta_b(a)
+
+        This factors into:
+
+        - the difference contributed by a constant is always 0
+          (identical to smt_xor_differential_propagation_constraints);
+        - the mask v is a FREE parameter: it never affects the local
+          weight (which is always 0 regardless of v), only the sign
+          chi_v(t) of the correlation. This weight-based search does
+          not track signs, so v is simply left unconstrained here --
+          exactly as smt_xor_linear_mask_propagation_constraints
+          already does for the ordinary linear model. Leaving it free
+          (rather than e.g. fixing it to 0) keeps it available for
+          any later sign/key-dependence analysis (cf.
+          generic_with_constant_sign_linear_constraints in
+          xor_component.py, and Section 4.4 of the paper).
+
+        INPUT:
+
+        - ``model`` -- **model object**; a ``SmtXorQuasidifferentialModel`` instance
+
+        EXAMPLES::
+
+            sage: from claasp.ciphers.single_component_ciphers.constant_cipher import ConstantCipher
+            sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel
+            sage: cipher = ConstantCipher(output_bit_size=3, value=2)
+            sage: constant = cipher.component_from_id('constant_0_0')
+            sage: variables, constraints = constant.smt_xor_quasidifferential_propagation_constraints(SmtXorQuasidifferentialModel(cipher))
+            sage: variables
+            ['constant_0_0_0', 'constant_0_0_1', 'constant_0_0_2', 'qdt_constant_0_0_0', 'qdt_constant_0_0_1', 'qdt_constant_0_0_2']
+            sage: constraints
+            ['(assert (not constant_0_0_0))', '(assert (not constant_0_0_1))', '(assert (not constant_0_0_2))']
+        """
+
+        output_bit_ids, diff_constraints = self.smt_xor_differential_propagation_constraints(model)
+
+        qdt_output_bit_ids = [f"qdt_{bit_id}" for bit_id in output_bit_ids]
+
+        variables = output_bit_ids + qdt_output_bit_ids
+
+        return (
+            variables,
+            diff_constraints,
+        )

claasp/components/fsr_component.py

@@ -94,6 +94,7 @@ class Fsr(Component):
         sage: print(component.output_bit_size)
         0
     """
+
     def __init__(
         self,
         current_round_number,

claasp/components/idea_modmul_component.py

@@ -50,7 +50,7 @@ class IdeaModmul(Modular):
         sage: print(component.description)
         ['IDEA_MODMUL', 2, 5]
     """
-    
+
     def __init__(
         self,
         current_round_number,
@@ -78,9 +78,7 @@ def algebraic_polynomials(self, model):
 
             Not implemented.
         """
-        raise NotImplementedError(
-            "Algebraic polynomials for idea_modmul are not yet implemented."
-        )
+        raise NotImplementedError("Algebraic polynomials for idea_modmul are not yet implemented.")
 
     def cms_constraints(self):
         """
@@ -90,9 +88,7 @@ def cms_constraints(self):
 
             Not implemented.
         """
-        raise NotImplementedError(
-            "CMS constraints for idea_modmul are not yet implemented."
-        )
+        raise NotImplementedError("CMS constraints for idea_modmul are not yet implemented.")
 
     def cp_constraints(self):
         """
@@ -102,14 +98,12 @@ def cp_constraints(self):
 
             Not implemented.
         """
-        raise NotImplementedError(
-            "CP constraints for idea_modmul are not yet implemented."
-        )
+        raise NotImplementedError("CP constraints for idea_modmul are not yet implemented.")
 
     def get_bit_based_vectorized_python_code(self, params):
         """
         Generate Python code for bit-based vectorized modular multiplication.
-        
+
         INPUT:
 
         - ``params`` -- **list**; the parameters for the function
@@ -124,7 +118,7 @@ def get_bit_based_vectorized_python_code(self, params):
         # Retrieve stored parameters
         num_inputs = self.description[1]
         modulus = self.description[2]
-        
+
         return [
             f"  {self.id} = bit_vector_idea_modmul([{','.join(params)}], "
             f"{num_inputs}, {self.output_bit_size}, {modulus})"
@@ -133,15 +127,15 @@ def get_bit_based_vectorized_python_code(self, params):
     def get_byte_based_vectorized_python_code(self, params):
         """
         Generate byte-based vectorized Python code for MODMUL evaluation.
-        
+
         INPUT:
 
         - ``params`` -- **string**; the parameters for the function
         """
         # Retrieve stored modulus and word_size
         modulus = self.description[2]
         word_size = self.output_bit_size
-        
+
         return [f"  {self.id} = byte_vector_idea_modmul({params}, {modulus}, {word_size})"]
 
     def sat_constraints(self):
@@ -152,9 +146,7 @@ def sat_constraints(self):
 
             Not implemented.
         """
-        raise NotImplementedError(
-            "SAT constraints for idea_modmul are not yet implemented."
-        )
+        raise NotImplementedError("SAT constraints for idea_modmul are not yet implemented.")
 
     def smt_constraints(self):
         """
@@ -164,6 +156,4 @@ def smt_constraints(self):
 
             Not implemented.
         """
-        raise NotImplementedError(
-            "SMT constraints for idea_modmul are not yet implemented."
-        )
+        raise NotImplementedError("SMT constraints for idea_modmul are not yet implemented.")

claasp/components/intermediate_output_component.py

@@ -74,6 +74,7 @@ class IntermediateOutput(CipherOutput):
         sage: print(component.description)
         ['round_output']
     """
+
     def __init__(
         self,
         current_round_number,