diff --git a/claasp/cipher_modules/models/cp/mzn_model.py b/claasp/cipher_modules/models/cp/mzn_model.py index b2a4c76c..dd330dbb 100644 --- a/claasp/cipher_modules/models/cp/mzn_model.py +++ b/claasp/cipher_modules/models/cp/mzn_model.py @@ -15,34 +15,31 @@ # along with this program. If not, see . # **************************************************************************** -import math import itertools +import math +import os import subprocess import time - from copy import deepcopy from datetime import timedelta -from sage.crypto.sbox import SBox - from minizinc import Instance, Model, Solver, Status +from sage.crypto.sbox import SBox from claasp.cipher_modules.component_analysis_tests import branch_number from claasp.cipher_modules.models.cp.minizinc_utils import usefulfunctions -from claasp.cipher_modules.models.utils import convert_solver_solution_to_dictionary -from claasp.name_mappings import CIPHER, CIPHER_OUTPUT, INTERMEDIATE_OUTPUT, SATISFIABLE, SBOX, UNSATISFIABLE -from claasp.cipher_modules.models.cp.solvers import ( - CP_SOLVERS_INTERNAL, - CP_SOLVERS_EXTERNAL, - SOLVER_DEFAULT, -) +from claasp.cipher_modules.models.cp.solvers import CP_SOLVERS_INTERNAL, CP_SOLVERS_EXTERNAL, SOLVER_DEFAULT +from claasp.name_mappings import SBOX, CIPHER, CIPHER_OUTPUT, CONSTANT, INTERMEDIATE_OUTPUT, LINEAR_LAYER, MIX_COLUMN, WORD_OPERATION, SATISFIABLE, UNSATISFIABLE + +from claasp.cipher_modules.models.utils import write_model_to_file, convert_solver_solution_to_dictionary SOLVE_SATISFY = "solve satisfy;" CONSTRAINT_TYPE_ERROR = "Constraint type not defined" class MznModel: - def __init__(self, cipher, window_size_list=None, probability_weight_per_round=None, sat_or_milp="sat"): + + def __init__(self, cipher, sat_or_milp='sat'): self._cipher = cipher self.initialise_model() if sat_or_milp not in ("sat", "milp"): @@ -66,17 +63,9 @@ def __init__(self, cipher, window_size_list=None, probability_weight_per_round=N self.mzn_carries_output_directives = [] self.input_postfix = "x" self.output_postfix = "y" - self.window_size_list = window_size_list - self.probability_weight_per_round = probability_weight_per_round self.carries_vars = [] - if probability_weight_per_round and len(probability_weight_per_round) != self._cipher.number_of_rounds: - raise ValueError("probability_weight_per_round size must be equal to cipher_number_of_rounds") - self.probability_modadd_vars_per_round = [[] for _ in range(self._cipher.number_of_rounds)] - - if window_size_list and len(window_size_list) != self._cipher.number_of_rounds: - raise ValueError("window_size_list size must be equal to cipher_number_of_rounds") - + def initialise_model(self): self._variables_list = [] self._model_constraints = [] @@ -172,6 +161,37 @@ def add_solution_to_components_values_internal( component_solution["weight"] = component_weight components_values[f"solution{solution_number}"][f"{component}"] = component_solution + def build_generic_cp_model_from_dictionary(self, component_and_model_types, fixed_variables=None): + variables = [] + self._variables_list = [] + + fixed_constraints = [] + if fixed_variables: + if hasattr(self, "fix_variables_value_constraints_for_ARX"): + fixed_constraints = self.fix_variables_value_constraints_for_ARX( + fixed_variables + ) + else: + fixed_constraints = self.fix_variables_value_constraints( + fixed_variables + ) + component_types = [CIPHER_OUTPUT, CONSTANT, INTERMEDIATE_OUTPUT, LINEAR_LAYER, MIX_COLUMN, SBOX, WORD_OPERATION] + operation_types = ['AND', 'MODADD', 'MODSUB', 'NOT', 'OR', 'ROTATE', 'SHIFT', 'SHIFT_BY_VARIABLE_AMOUNT', 'XOR'] + self._model_constraints = fixed_constraints + + for component_and_model_type in component_and_model_types: + component = component_and_model_type["component_object"] + model_type = component_and_model_type["model_type"] + operation = component.description[0] + if component.type not in component_types or ( + WORD_OPERATION == component.type and operation not in operation_types): + print(f'{component.id} not yet implemented') + else: + cp_generic_propagation_constraints = getattr(component, model_type) + variables, constraints = cp_generic_propagation_constraints(self) + self._model_constraints.extend(constraints) + self._variables_list.extend(variables) + def build_mix_column_truncated_table(self, component): """ Return a model that generates the list of possible input/output couples for the given mix column. diff --git a/claasp/cipher_modules/models/cp/mzn_models/mzn_cipher_model_arx_optimized.py b/claasp/cipher_modules/models/cp/mzn_models/mzn_cipher_model_arx_optimized.py index c37e0bb1..dd03e61e 100644 --- a/claasp/cipher_modules/models/cp/mzn_models/mzn_cipher_model_arx_optimized.py +++ b/claasp/cipher_modules/models/cp/mzn_models/mzn_cipher_model_arx_optimized.py @@ -21,8 +21,9 @@ class MznCipherModelARXOptimized(MznModel): - def __init__(self, cipher, window_size_list=None, probability_weight_per_round=None, sat_or_milp="sat"): - super().__init__(cipher, window_size_list, probability_weight_per_round, sat_or_milp) + + def __init__(self, cipher, sat_or_milp='sat'): + super().__init__(cipher, sat_or_milp) def build_cipher_model(self, fixed_variables=[]): """ diff --git a/claasp/cipher_modules/models/cp/mzn_models/mzn_deterministic_truncated_xor_differential_model_arx_optimized.py b/claasp/cipher_modules/models/cp/mzn_models/mzn_deterministic_truncated_xor_differential_model_arx_optimized.py index 66f93361..0b02bfa4 100644 --- a/claasp/cipher_modules/models/cp/mzn_models/mzn_deterministic_truncated_xor_differential_model_arx_optimized.py +++ b/claasp/cipher_modules/models/cp/mzn_models/mzn_deterministic_truncated_xor_differential_model_arx_optimized.py @@ -21,8 +21,9 @@ class MznDeterministicTruncatedXorDifferentialModelARXOptimized(MznModel): - def __init__(self, cipher, window_size_list=None, probability_weight_per_round=None, sat_or_milp="sat"): - super().__init__(cipher, window_size_list, probability_weight_per_round, sat_or_milp) + + def __init__(self, cipher, sat_or_milp='sat'): + super().__init__(cipher, sat_or_milp) def build_deterministic_truncated_xor_differential_trail_model(self, fixed_variables=[]): """ diff --git a/claasp/cipher_modules/models/cp/mzn_models/mzn_xor_differential_model_arx_optimized.py b/claasp/cipher_modules/models/cp/mzn_models/mzn_xor_differential_model_arx_optimized.py index 419cf517..1dbd73d7 100644 --- a/claasp/cipher_modules/models/cp/mzn_models/mzn_xor_differential_model_arx_optimized.py +++ b/claasp/cipher_modules/models/cp/mzn_models/mzn_xor_differential_model_arx_optimized.py @@ -31,8 +31,15 @@ def __init__( sat_or_milp="sat", include_word_operations_mzn_file=True, ): + self.window_size_list = window_size_list + self.probability_weight_per_round = probability_weight_per_round self.include_word_operations_mzn_file = include_word_operations_mzn_file - super().__init__(cipher, window_size_list, probability_weight_per_round, sat_or_milp) + super().__init__(cipher, sat_or_milp) + if probability_weight_per_round and len(probability_weight_per_round) != self._cipher.number_of_rounds: + raise ValueError("probability_weight_per_round size must be equal to cipher_number_of_rounds") + + if window_size_list and len(window_size_list) != self._cipher.number_of_rounds: + raise ValueError("window_size_list size must be equal to cipher_number_of_rounds") @staticmethod def _create_minizinc_1d_array_from_list(mzn_list): diff --git a/tests/unit/cipher_modules/models/cp/mzn_model_test.py b/tests/unit/cipher_modules/models/cp/mzn_model_test.py index a8fc7add..88f0ed6e 100644 --- a/tests/unit/cipher_modules/models/cp/mzn_model_test.py +++ b/tests/unit/cipher_modules/models/cp/mzn_model_test.py @@ -13,7 +13,9 @@ from claasp.cipher_modules.models.cp.mzn_models.mzn_deterministic_truncated_xor_differential_model_arx_optimized import ( MznDeterministicTruncatedXorDifferentialModelARXOptimized, ) -from claasp.cipher_modules.models.utils import set_fixed_variables +from claasp.cipher_modules.models.cp.mzn_models.mzn_xor_linear_model import MznXorLinearModel +from claasp.cipher_modules.models.utils import set_fixed_variables, integer_to_bit_list +from minizinc import Model, Solver, Instance, Status @pytest.mark.filterwarnings("ignore::DeprecationWarning:") @@ -120,3 +122,127 @@ def test_model_constraints(): speck = SpeckBlockCipher(number_of_rounds=4) mzn = MznModel(speck) mzn.model_constraints() + +def test_build_generic_cp_model_from_dictionary(): + + """ + Differential ARX validation for Speck. + + The input and output differences used in the tests are taken from + Table 4 (Differential Characteristics for Speck32/48/64) of: + + Kai Fu et al., "MILP-Based Automatic Search Algorithms for + Differential and Linear Trails for Speck", https://eprint.iacr.org/2016/407.pdf + """ + speck = SpeckBlockCipher(number_of_rounds=3) + model = MznXorDifferentialModelARXOptimized(speck) + component_and_model_types = [] + + for component in speck.get_all_components(): + component_and_model_types.append({ + "component_object": component, + "model_type": "minizinc_xor_differential_propagation_constraints" + }) + + fixed_variables = [] + + fixed_variables.append( + set_fixed_variables( + component_id="plaintext", + constraint_type="equal", + bit_positions=list(range(32)), + bit_values=integer_to_bit_list(0x02110A04, 32, 'big') + ) + ) + + fixed_variables.append( + set_fixed_variables( + component_id="key", + constraint_type="equal", + bit_positions=list(range(64)), + bit_values=[0] * 64 + ) + ) + + fixed_variables.append( + set_fixed_variables( + component_id="cipher_output_2_12", + constraint_type="equal", + bit_positions=list(range(32)), + bit_values=integer_to_bit_list(0x80008000, 32, 'big') + ) + ) + + model.build_generic_cp_model_from_dictionary(component_and_model_types, fixed_variables) + + #Caso especial para ARX + model.init_constraints() + + result = model.solve_for_ARX(solver_name="cp-sat") + + assert result.status in { + Status.SATISFIED, + Status.OPTIMAL_SOLUTION, + Status.ALL_SOLUTIONS, + } + +def test_build_generic_cp_model_from_dictionary_xor_linear(): + """ + Linear validation for Speck. + + The linear input/output masks used in the tests are taken from + Table 6 of: + + Kai Fu et al., "MILP-Based Automatic Search Algorithms for + Differential and Linear Trails for Speck", https://eprint.iacr.org/2016/407.pdf + """ + speck = SpeckBlockCipher(number_of_rounds=3) + model = MznXorLinearModel(speck) + component_and_model_types = [] + + for component in speck.get_all_components(): + component_and_model_types.append({ + "component_object": component, + "model_type": "cp_xor_linear_mask_propagation_constraints" + }) + + fixed_variables = [] + + fixed_variables.append( + set_fixed_variables( + component_id="plaintext", + constraint_type="equal", + bit_positions=list(range(32)), + bit_values=integer_to_bit_list(0x03805224, 32, 'big') + ) + ) + + fixed_variables.append( + set_fixed_variables( + component_id="key", + constraint_type="equal", + bit_positions=list(range(64)), + bit_values=[0] * 64 + ) + ) + + fixed_variables.append( + set_fixed_variables( + component_id="cipher_output_2_12", + constraint_type="equal", + bit_positions=list(range(32)), + bit_values=integer_to_bit_list(0x40A000C1, 32, 'big') + ) + ) + + model.build_generic_cp_model_from_dictionary(component_and_model_types, fixed_variables) + + model.initialise_model() + + result = model.solve_for_ARX(solver_name="cp-sat") + + assert result.status in { + Status.SATISFIED, + Status.OPTIMAL_SOLUTION, + Status.ALL_SOLUTIONS, + } \ No newline at end of file