diff --git a/claasp/cipher.py b/claasp/cipher.py
index 0b481fa0..4e3b22c9 100644
--- a/claasp/cipher.py
+++ b/claasp/cipher.py
@@ -1381,6 +1381,8 @@ def polynomial_system_at_round(self, r):
algebraic_model = AlgebraicModel(self)
return algebraic_model.polynomial_system_at_round(r)
+ def get_key_schedule(self):
+ return editor.get_key_schedule(self)
def remove_key_schedule(self):
return editor.remove_key_schedule(self)
diff --git a/claasp/cipher_modules/models/cp/mzn_models/mzn_deterministic_truncated_xor_differential_model.py b/claasp/cipher_modules/models/cp/mzn_models/mzn_bitwise_deterministic_truncated_xor_differential_model.py
similarity index 93%
rename from claasp/cipher_modules/models/cp/mzn_models/mzn_deterministic_truncated_xor_differential_model.py
rename to claasp/cipher_modules/models/cp/mzn_models/mzn_bitwise_deterministic_truncated_xor_differential_model.py
index 9ced27d3..cf0f13a5 100644
--- a/claasp/cipher_modules/models/cp/mzn_models/mzn_deterministic_truncated_xor_differential_model.py
+++ b/claasp/cipher_modules/models/cp/mzn_models/mzn_bitwise_deterministic_truncated_xor_differential_model.py
@@ -31,7 +31,7 @@
from claasp.cipher_modules.models.cp.solvers import MODEL_DEFAULT_PATH, SOLVER_DEFAULT
-class MznDeterministicTruncatedXorDifferentialModel(MznModel):
+class MznBitwiseDeterministicTruncatedXorDifferentialModel(MznModel):
def __init__(self, cipher):
super().__init__(cipher)
@@ -86,11 +86,11 @@ def build_deterministic_truncated_xor_differential_trail_model(self, fixed_varia
EXAMPLES::
- sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_deterministic_truncated_xor_differential_model import MznDeterministicTruncatedXorDifferentialModel
+ sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_bitwise_deterministic_truncated_xor_differential_model import MznBitwiseDeterministicTruncatedXorDifferentialModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: from claasp.cipher_modules.models.utils import set_fixed_variables, integer_to_bit_list
sage: speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=2)
- sage: cp = MznDeterministicTruncatedXorDifferentialModel(speck)
+ sage: cp = MznBitwiseDeterministicTruncatedXorDifferentialModel(speck)
sage: fixed_variables = [set_fixed_variables('key', 'equal', range(64), integer_to_bit_list(0, 64, 'little'))]
sage: cp.build_deterministic_truncated_xor_differential_trail_model(fixed_variables)
"""
@@ -132,9 +132,9 @@ def final_deterministic_truncated_xor_differential_constraints(self, minimize=Fa
EXAMPLES::
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
- sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_deterministic_truncated_xor_differential_model import MznDeterministicTruncatedXorDifferentialModel
+ sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_bitwise_deterministic_truncated_xor_differential_model import MznBitwiseDeterministicTruncatedXorDifferentialModel
sage: speck = SpeckBlockCipher(number_of_rounds=2)
- sage: cp = MznDeterministicTruncatedXorDifferentialModel(speck)
+ sage: cp = MznBitwiseDeterministicTruncatedXorDifferentialModel(speck)
sage: cp.final_deterministic_truncated_xor_differential_constraints()[:-1]
['solve satisfy;']
"""
@@ -173,11 +173,11 @@ def find_lowest_varied_patterns_bitwise_deterministic_truncated_xor_differential
EXAMPLES::
- sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_deterministic_truncated_xor_differential_model import MznDeterministicTruncatedXorDifferentialModel
+ sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_bitwise_deterministic_truncated_xor_differential_model import MznBitwiseDeterministicTruncatedXorDifferentialModel
sage: from claasp.cipher_modules.models.utils import set_fixed_variables
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=1)
- sage: cp = MznDeterministicTruncatedXorDifferentialModel(speck)
+ sage: cp = MznBitwiseDeterministicTruncatedXorDifferentialModel(speck)
sage: plaintext = set_fixed_variables(
....: component_id='plaintext',
....: constraint_type='not_equal',
@@ -233,11 +233,11 @@ def find_all_deterministic_truncated_xor_differential_trails(self, number_of_rou
EXAMPLES::
- sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_deterministic_truncated_xor_differential_model import MznDeterministicTruncatedXorDifferentialModel
+ sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_bitwise_deterministic_truncated_xor_differential_model import MznBitwiseDeterministicTruncatedXorDifferentialModel
sage: from claasp.cipher_modules.models.utils import set_fixed_variables
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=3)
- sage: cp = MznDeterministicTruncatedXorDifferentialModel(speck)
+ sage: cp = MznBitwiseDeterministicTruncatedXorDifferentialModel(speck)
sage: plaintext = set_fixed_variables(
....: component_id='plaintext',
....: constraint_type='not_equal',
@@ -285,11 +285,11 @@ def find_one_deterministic_truncated_xor_differential_trail(self, number_of_roun
EXAMPLES::
- sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_deterministic_truncated_xor_differential_model import MznDeterministicTruncatedXorDifferentialModel
+ sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_bitwise_deterministic_truncated_xor_differential_model import MznBitwiseDeterministicTruncatedXorDifferentialModel
sage: from claasp.cipher_modules.models.utils import set_fixed_variables
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=1)
- sage: cp = MznDeterministicTruncatedXorDifferentialModel(speck)
+ sage: cp = MznBitwiseDeterministicTruncatedXorDifferentialModel(speck)
sage: plaintext = set_fixed_variables(
....: component_id='plaintext',
....: constraint_type='not_equal',
@@ -340,9 +340,9 @@ def input_deterministic_truncated_xor_differential_constraints(self):
EXAMPLES::
sage: from claasp.ciphers.block_ciphers.aes_block_cipher import AESBlockCipher
- sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_deterministic_truncated_xor_differential_model import MznDeterministicTruncatedXorDifferentialModel
+ sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_bitwise_deterministic_truncated_xor_differential_model import MznBitwiseDeterministicTruncatedXorDifferentialModel
sage: aes = AESBlockCipher()
- sage: cp = MznDeterministicTruncatedXorDifferentialModel(aes)
+ sage: cp = MznBitwiseDeterministicTruncatedXorDifferentialModel(aes)
sage: cp.input_deterministic_truncated_xor_differential_constraints()
(['array[0..127] of var 0..2: key;',
'array[0..127] of var 0..2: plaintext;',
@@ -379,9 +379,9 @@ def output_constraints(self, component):
EXAMPLES::
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
- sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_deterministic_truncated_xor_differential_model import MznDeterministicTruncatedXorDifferentialModel
+ sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_bitwise_deterministic_truncated_xor_differential_model import MznBitwiseDeterministicTruncatedXorDifferentialModel
sage: speck = SpeckBlockCipher(number_of_rounds=3)
- sage: cp = MznDeterministicTruncatedXorDifferentialModel(speck)
+ sage: cp = MznBitwiseDeterministicTruncatedXorDifferentialModel(speck)
sage: output_component = speck.component_from(0, 5)
sage: cp.output_constraints(output_component)
([],
@@ -412,9 +412,9 @@ def output_inverse_constraints(self, component):
EXAMPLES::
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
- sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_deterministic_truncated_xor_differential_model import MznDeterministicTruncatedXorDifferentialModel
+ sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_bitwise_deterministic_truncated_xor_differential_model import MznBitwiseDeterministicTruncatedXorDifferentialModel
sage: speck = SpeckBlockCipher(number_of_rounds=3)
- sage: cp = MznDeterministicTruncatedXorDifferentialModel(speck)
+ sage: cp = MznBitwiseDeterministicTruncatedXorDifferentialModel(speck)
sage: output_component = speck.component_from(0, 5)
sage: cp.output_inverse_constraints(output_component)
([],
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_bitwise_deterministic_truncated_xor_differential_model_arx_optimized.py
similarity index 89%
rename from claasp/cipher_modules/models/cp/mzn_models/mzn_deterministic_truncated_xor_differential_model_arx_optimized.py
rename to claasp/cipher_modules/models/cp/mzn_models/mzn_bitwise_deterministic_truncated_xor_differential_model_arx_optimized.py
index 35ea098f..8b0017b8 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_bitwise_deterministic_truncated_xor_differential_model_arx_optimized.py
@@ -22,7 +22,7 @@
CIPHER_OUTPUT, WORD_OPERATION)
-class MznDeterministicTruncatedXorDifferentialModelARXOptimized(MznModel):
+class MznBitwiseDeterministicTruncatedXorDifferentialModelARXOptimized(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)
@@ -42,9 +42,9 @@ def build_deterministic_truncated_xor_differential_trail_model(self, fixed_varia
EXAMPLES::
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
- sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_deterministic_truncated_xor_differential_model_arx_optimized import MznDeterministicTruncatedXorDifferentialModelARXOptimized
+ sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_bitwise_deterministic_truncated_xor_differential_model_arx_optimized import MznBitwiseDeterministicTruncatedXorDifferentialModelARXOptimized
sage: speck = SpeckBlockCipher(number_of_rounds=22)
- sage: minizinc = MznDeterministicTruncatedXorDifferentialModelARXOptimized(speck)
+ sage: minizinc = MznBitwiseDeterministicTruncatedXorDifferentialModelARXOptimized(speck)
sage: minizinc.build_deterministic_truncated_xor_differential_trail_model()
...
"""
diff --git a/claasp/cipher_modules/models/cp/mzn_models/mzn_bitwise_impossible_xor_differential_model.py b/claasp/cipher_modules/models/cp/mzn_models/mzn_bitwise_impossible_xor_differential_model.py
new file mode 100644
index 00000000..a2da1bd6
--- /dev/null
+++ b/claasp/cipher_modules/models/cp/mzn_models/mzn_bitwise_impossible_xor_differential_model.py
@@ -0,0 +1,927 @@
+
+# ****************************************************************************
+# Copyright 2023 Technology Innovation Institute
+#
+# This program is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# This program is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program. If not, see .
+# ****************************************************************************
+
+
+import os
+import math
+import itertools
+import subprocess
+from copy import deepcopy
+
+from claasp.cipher_modules.models.cp.mzn_model import solve_satisfy
+from claasp.cipher_modules.models.utils import write_model_to_file, convert_solver_solution_to_dictionary, check_if_implemented_component
+from claasp.cipher_modules.models.cp.mzn_models.mzn_bitwise_deterministic_truncated_xor_differential_model import MznBitwiseDeterministicTruncatedXorDifferentialModel
+
+from claasp.name_mappings import (CONSTANT, INTERMEDIATE_OUTPUT, CIPHER_OUTPUT, LINEAR_LAYER, SBOX, MIX_COLUMN,
+ WORD_OPERATION, DETERMINISTIC_TRUNCATED_XOR_DIFFERENTIAL, IMPOSSIBLE_XOR_DIFFERENTIAL)
+from claasp.cipher_modules.models.cp.solvers import CP_SOLVERS_EXTERNAL, SOLVER_DEFAULT
+
+
+class MznBitwiseImpossibleXorDifferentialModel(MznBitwiseDeterministicTruncatedXorDifferentialModel):
+
+ def __init__(self, cipher):
+ super().__init__(cipher)
+ self.inverse_cipher = cipher.cipher_inverse()
+ self.middle_round = 1
+ self.key_schedule_bits_distribution = {}
+ self.key_involvements = self.get_state_key_bits_positions()
+ self.inverse_key_involvements = self.get_inverse_state_key_bits_positions()
+
+ def add_solution_to_components_values(self, component_id, component_solution, components_values, j, output_to_parse,
+ solution_number, string):
+ inverse_cipher = self.inverse_cipher
+ if component_id in self._cipher.inputs:
+ components_values[f'solution{solution_number}'][f'{component_id}'] = component_solution
+ elif component_id in self.inverse_cipher.inputs:
+ components_values[f'solution{solution_number}'][f'inverse_{component_id}'] = component_solution
+ elif f'{component_id}_i' in string:
+ components_values[f'solution{solution_number}'][f'{component_id}_i'] = component_solution
+ elif f'{component_id}_o' in string:
+ components_values[f'solution{solution_number}'][f'{component_id}_o'] = component_solution
+ elif f'inverse_{component_id} ' in string:
+ components_values[f'solution{solution_number}'][f'inverse_{component_id}'] = component_solution
+ elif f'{component_id} ' in string:
+ components_values[f'solution{solution_number}'][f'{component_id}'] = component_solution
+
+ def build_impossible_backward_model(self, backward_components, clean = True):
+ inverse_variables = []
+ inverse_constraints = []
+ key_components, key_ids = self.extract_key_schedule()
+ constant_components, constant_ids = self.extract_constants()
+ for component in backward_components:
+ if check_if_implemented_component(component):
+ variables, constraints = self.propagate_deterministically(component)
+ inverse_variables.extend(variables)
+ inverse_constraints.extend(constraints)
+
+ if clean:
+ components_to_invert = [backward_components[i] for i in range(len(backward_components))]
+ for component in backward_components:
+ for id_link in component.input_id_links:
+ input_component = self.get_component_from_id(id_link, self.inverse_cipher)
+ if input_component not in backward_components and id_link not in key_ids + constant_ids:
+ components_to_invert.append(input_component)
+ inverse_variables, inverse_constraints = self.clean_inverse_impossible_variables_constraints_with_extensions(components_to_invert, inverse_variables, inverse_constraints)
+
+ return inverse_variables, inverse_constraints
+
+ def build_impossible_forward_model(self, forward_components, clean = False):
+ direct_variables = []
+ direct_constraints = []
+ for component in forward_components:
+ if check_if_implemented_component(component):
+ variables, constraints = self.propagate_deterministically(component)
+ direct_variables.extend(variables)
+ direct_constraints.extend(constraints)
+
+ if clean:
+ direct_variables, direct_constraints = self.clean_inverse_impossible_variables_constraints(forward_components, direct_variables, direct_constraints)
+
+ return direct_variables, direct_constraints
+
+ def build_impossible_xor_differential_trail_with_extensions_model(self, fixed_variables, number_of_rounds, initial_round, middle_round, final_round, intermediate_components):
+ """
+ Build the CP model for the search of deterministic truncated XOR differential trails with extensions for key recovery.
+
+ INPUT:
+
+ - ``fixed_variables`` -- **list** (default: `[]`); dictionaries containing the variables to be fixed in standard
+ format
+ - ``number_of_rounds`` -- **integer** ; number of rounds
+ - ``initial_round`` -- **integer** ; initial round of the impossible differential trail
+ - ``middle_round`` -- **integer** ; incosistency round of the impossible differential trail
+ - ``final_round`` -- **integer** ; final round of the impossible differential trail
+ - ``intermediate_components`` -- **Boolean** ; check inconsistency on intermediate components of the inconsistency round or only on outputs
+
+ EXAMPLES::
+
+ sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_bitwise_impossible_xor_differential_model import MznBitwiseImpossibleXorDifferentialModel
+ sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
+ sage: from claasp.cipher_modules.models.utils import set_fixed_variables, integer_to_bit_list
+ sage: speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=5)
+ sage: cp = MznBitwiseImpossibleXorDifferentialModel(speck)
+ sage: fixed_variables = [set_fixed_variables('key', 'equal', range(64), integer_to_bit_list(0, 64, 'little'))]
+ sage: cp.build_impossible_xor_differential_trail_with_extensions_model(fixed_variables, 5, 2, 3, 4, False)
+ """
+ self.initialise_model()
+ if number_of_rounds is None:
+ number_of_rounds = self._cipher.number_of_rounds
+ inverse_cipher = self.inverse_cipher
+ if final_round is None:
+ final_round = self._cipher.number_of_rounds - 1
+ key_components, key_ids = self.extract_key_schedule()
+ constant_components, constant_ids = self.extract_constants()
+ self._variables_list = []
+ constraints = self.fix_variables_value_constraints(fixed_variables)
+ deterministic_truncated_xor_differential = constraints
+ self.middle_round = middle_round
+
+ forward_components = []
+ for n_r in list(range(initial_round - 1, middle_round)) + list(range(final_round, number_of_rounds)):
+ forward_components.extend(self._cipher.get_components_in_round(n_r))
+
+ backward_components = []
+ for n_r in list(range(initial_round - 1)) + list(range(middle_round - 1, final_round)):
+ backward_components.extend(inverse_cipher.get_components_in_round(number_of_rounds - 1 - n_r))
+
+ components_to_link = []
+ for component in self.inverse_cipher.get_all_components():
+ comp_r = self.get_component_round(component.id)
+ if comp_r == initial_round - 2 or comp_r == final_round - 1:
+ for id_link in component.input_id_links:
+ if self.get_component_round(id_link) > comp_r:
+ for input_component in self.inverse_cipher.get_all_components():
+ if input_component.id == id_link:
+ components_to_link.append([self.get_inverse_component_correspondance(input_component), id_link])
+
+ link_constraints = self.link_constraints_for_trail_with_extensions(components_to_link)
+ key_schedule_variables, key_schedule_constraints = self.constraints_for_key_schedule()
+ constants_variables, constants_constraints = self.constraints_for_constants()
+
+ direct_variables, direct_constraints = self.build_impossible_forward_model(forward_components)
+ inverse_variables, inverse_constraints = self.build_impossible_backward_model(backward_components)
+
+ variables = direct_variables + inverse_variables
+ constraints = direct_constraints + inverse_constraints
+
+ self._variables_list.extend(variables)
+ self._variables_list.extend(key_schedule_variables)
+ self._variables_list.extend(constants_variables)
+ deterministic_truncated_xor_differential.extend(constraints)
+ variables, constraints = self.input_impossible_constraints_with_extensions(number_of_rounds, initial_round, middle_round, final_round)
+ self._model_prefix.extend(variables)
+ self._variables_list.extend(constraints)
+ deterministic_truncated_xor_differential.extend(link_constraints)
+ deterministic_truncated_xor_differential.extend(key_schedule_constraints)
+ deterministic_truncated_xor_differential.extend(constants_constraints)
+ deterministic_truncated_xor_differential.extend(self.final_impossible_constraints_with_extensions(number_of_rounds, initial_round, middle_round, final_round, intermediate_components))
+ set_of_constraints = self._variables_list + deterministic_truncated_xor_differential
+
+ cleaned_constraints = []
+ for constraint in self._model_prefix + set_of_constraints:
+ if constraint not in cleaned_constraints:
+ cleaned_constraints.append(constraint)
+
+ self._model_constraints = cleaned_constraints
+
+ def build_impossible_xor_differential_trail_model(self, fixed_variables=[], number_of_rounds=None, initial_round = 1, middle_round=1, final_round = None, intermediate_components = True):
+ """
+ Build the CP model for the search of deterministic truncated XOR differential trails.
+
+ INPUT:
+
+ - ``fixed_variables`` -- **list** (default: `[]`); dictionaries containing the variables to be fixed in standard
+ format
+ - ``number_of_rounds`` -- **integer** (default: `None`); number of rounds
+ - ``initial_round`` -- **integer** (default: `1`); initial round of the impossible differential
+ - ``middle_round`` -- **integer** (default: `1`); incosistency round of the impossible differential
+ - ``final_round`` -- **integer** (default: `None`); final round of the impossible differential
+ - ``intermediate_components`` -- **Boolean** (default: `True`); check inconsistency on intermediate components of the inconsistency round or only on outputs
+
+ EXAMPLES::
+
+ sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_bitwise_impossible_xor_differential_model import MznBitwiseImpossibleXorDifferentialModel
+ sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
+ sage: from claasp.cipher_modules.models.utils import set_fixed_variables, integer_to_bit_list
+ sage: speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=4)
+ sage: cp = MznBitwiseImpossibleXorDifferentialModel(speck)
+ sage: fixed_variables = [set_fixed_variables('key', 'equal', range(64), integer_to_bit_list(0, 64, 'little'))]
+ sage: cp.build_impossible_xor_differential_trail_model(fixed_variables, 4, 1, 3, 4, False)
+ """
+ self.initialise_model()
+ if number_of_rounds is None:
+ number_of_rounds = self._cipher.number_of_rounds
+ if final_round is None:
+ final_round = self._cipher.number_of_rounds
+ inverse_cipher = self.inverse_cipher
+
+ self._variables_list = []
+ constraints = self.fix_variables_value_constraints(fixed_variables)
+ deterministic_truncated_xor_differential = constraints
+ self.middle_round = middle_round
+
+ forward_components = []
+ for r in range(middle_round):
+ forward_components.extend(self._cipher.get_components_in_round(r))
+ backward_components = []
+ for r in range(number_of_rounds - middle_round + 1):
+ backward_components.extend(inverse_cipher.get_components_in_round(r))
+
+ direct_variables, direct_constraints = self.build_impossible_forward_model(forward_components)
+ self._variables_list.extend(direct_variables)
+ deterministic_truncated_xor_differential.extend(direct_constraints)
+
+ inverse_variables, inverse_constraints = self.build_impossible_backward_model(backward_components, clean = False)
+ inverse_variables, inverse_constraints = self.clean_inverse_impossible_variables_constraints(backward_components, inverse_variables, inverse_constraints)
+ self._variables_list.extend(inverse_variables)
+ deterministic_truncated_xor_differential.extend(inverse_constraints)
+
+ variables, constraints = self.input_impossible_constraints(number_of_rounds = number_of_rounds, middle_round = middle_round)
+ self._model_prefix.extend(variables)
+ self._variables_list.extend(constraints)
+ deterministic_truncated_xor_differential.extend(self.final_impossible_constraints(number_of_rounds, initial_round, middle_round, final_round, intermediate_components))
+ set_of_constraints = self._variables_list + deterministic_truncated_xor_differential
+
+ self._model_constraints = self._model_prefix + self.clean_constraints(set_of_constraints, initial_round, middle_round, final_round)
+
+ def clean_constraints(self, set_of_constraints, initial_round, middle_round, final_round):
+ number_of_rounds = self._cipher.number_of_rounds
+ input_component = 'plaintext'
+ model_constraints = []
+ forward_components = []
+ for r in range(initial_round - 1, middle_round):
+ forward_components.extend([component.id for component in self._cipher.get_components_in_round(r)])
+ backward_components = []
+ for r in range(number_of_rounds - final_round, number_of_rounds - middle_round + 1):
+ backward_components.extend(['inverse_' + component.id for component in self.inverse_cipher.get_components_in_round(r)])
+ key_components, key_ids = self.extract_key_schedule()
+ components_to_keep = forward_components + backward_components + key_ids + ['inverse_' + id_link for id_link in key_ids] + ['array['] + [solve_satisfy]
+ if initial_round == 1 and final_round == self._cipher.number_of_rounds:
+ for i in range(len(set_of_constraints) - 1):
+ if set_of_constraints[i] not in set_of_constraints[i+1:]:
+ model_constraints.append(set_of_constraints[i])
+ model_constraints.append(set_of_constraints[-1])
+ return model_constraints
+ if initial_round == 1:
+ components_to_keep.extend(self._cipher.inputs)
+ if final_round == number_of_rounds:
+ components_to_keep.extend(['inverse_' + id_link for id_link in self.inverse_cipher.inputs])
+ if initial_round > 1:
+ for component in self._cipher.get_components_in_round(initial_round - 2):
+ if 'output' in component.id:
+ components_to_keep.append(component.id)
+ input_component = component
+ for constraint in set_of_constraints:
+ for id_link in components_to_keep:
+ if id_link in constraint and constraint not in model_constraints:
+ model_constraints.append(constraint)
+
+ return model_constraints
+
+ def clean_inverse_impossible_variables_constraints(self, backward_components, inverse_variables, inverse_constraints):
+ for component in backward_components:
+ inverse_variables, inverse_constraints = self.set_inverse_component_id_in_constraints(component, inverse_variables, inverse_constraints)
+ inverse_variables, inverse_constraints = self.clean_repetitions_in_constraints(inverse_variables, inverse_constraints)
+ return inverse_variables, inverse_constraints
+
+ def clean_inverse_impossible_variables_constraints_with_extensions(self, backward_components, inverse_variables, inverse_constraints):
+ key_components, key_ids = self.extract_key_schedule()
+ constant_components, constant_ids = self.extract_constants()
+ for component in backward_components:
+ if component.id not in key_ids + constant_ids:
+ inverse_variables, inverse_constraints = self.set_inverse_component_id_in_constraints(component, inverse_variables, inverse_constraints)
+ inverse_variables, inverse_constraints = self.clean_repetitions_in_constraints(inverse_variables, inverse_constraints)
+ return inverse_variables, inverse_constraints
+
+ def clean_repetitions_in_constraints(self, inverse_variables, inverse_constraints):
+ for c in range(len(inverse_constraints)):
+ start = 0
+ while 'cipher_output' in inverse_constraints[c][start:]:
+ new_start = inverse_constraints[c].index('cipher_output', start)
+ inverse_constraints[c] = inverse_constraints[c][:new_start] + 'inverse_' + inverse_constraints[c][new_start:]
+ start = new_start + 9
+ start = 0
+ while 'inverse_inverse_' in inverse_constraints[c][start:]:
+ new_start = inverse_constraints[c].index('inverse_inverse_', start)
+ inverse_constraints[c] = inverse_constraints[c][:new_start] + inverse_constraints[c][new_start + 8:]
+ start = new_start
+ for v in range(len(inverse_variables)):
+ start = 0
+ while 'inverse_inverse_' in inverse_variables[v][start:]:
+ new_start = inverse_variables[v].index('inverse_inverse_', start)
+ inverse_variables[v] = inverse_variables[v][:new_start] + inverse_variables[v][new_start + 8:]
+ start = new_start
+
+ return inverse_variables, inverse_constraints
+
+ def constraints_for_key_schedule(self):
+ key_components, key_ids = self.extract_key_schedule()
+ return self.build_impossible_forward_model(key_components)
+
+ def constraints_for_constants(self):
+ constant_components, constant_ids = self.extract_constants()
+ return self.build_impossible_forward_model(constant_components)
+
+ def extract_constants(self):
+ cipher = self._cipher
+ constant_components_ids = []
+ constant_components = []
+ for component in cipher.get_all_components():
+ if 'constant' in component.id:
+ constant_components_ids.append(component.id)
+ constant_components.append(component)
+ elif '_' in component.id:
+ component_inputs = component.input_id_links
+ ks = True
+ for comp_input in component_inputs:
+ if 'constant' not in comp_input:
+ ks = False
+ if ks:
+ constant_components_ids.append(component.id)
+ constant_components.append(component)
+
+ return constant_components, constant_components_ids
+
+ def extract_key_schedule(self):
+ cipher = self._cipher
+ key_schedule_components_ids = ['key']
+ key_schedule_components = []
+ for component in cipher.get_all_components():
+ component_inputs = component.input_id_links
+ ks = True
+ for comp_input in component_inputs:
+ if 'constant' not in comp_input and comp_input not in key_schedule_components_ids:
+ ks = False
+ if ks:
+ key_schedule_components_ids.append(component.id)
+ key_schedule_components.append(component)
+ master_key_bits = []
+ for id_link, bit_positions in zip(component_inputs, component.input_bit_positions):
+ if id_link == 'key':
+ master_key_bits.extend(bit_positions)
+ else:
+ if id_link in self.key_schedule_bits_distribution:
+ master_key_bits.extend(self.key_schedule_bits_distribution[id_link])
+ self.key_schedule_bits_distribution[component.id] = list(set(master_key_bits))
+
+ return key_schedule_components, key_schedule_components_ids
+
+ def final_impossible_constraints_with_extensions(self, number_of_rounds, initial_round, middle_round, final_round, intermediate_components):
+ """
+ Constraints for output and incompatibility.
+
+ INPUT:
+
+ - ``number_of_rounds`` -- **integer** ; number of rounds
+ - ``initial_round`` -- **integer** ; initial round of the impossible differential trail
+ - ``middle_round`` -- **integer** ; incosistency round of the impossible differential trail
+ - ``final_round`` -- **integer** ; final round of the impossible differential trail
+ - ``intermediate_components`` -- **Boolean** ; check inconsistency on intermediate components of the inconsistency round or only on outputs
+
+ EXAMPLES::
+
+ sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_bitwise_impossible_xor_differential_model import MznBitwiseImpossibleXorDifferentialModel
+ sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
+ sage: from claasp.cipher_modules.models.utils import set_fixed_variables, integer_to_bit_list
+ sage: speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=5)
+ sage: cp = MznBitwiseImpossibleXorDifferentialModel(speck)
+ sage: cp.final_impossible_constraints_with_extensions(5, 2, 3, 4, False)
+ ['solve satisfy;',
+ ...
+ 'output["plaintext = "++ show(plaintext) ++ "\\n" ++"key = "++ show(key) ++ "\\n" ++"inverse_plaintext = "++ show(inverse_plaintext) ++ "\\n" ++"inverse_intermediate_output_0_6 = "++ show(inverse_intermediate_output_0_6)++ "\\n" ++ "0" ++ "\\n" ++"intermediate_output_1_12 = "++ show(intermediate_output_1_12)++ "\\n" ++ "0" ++ "\\n" ++"intermediate_output_2_12 = "++ show(intermediate_output_2_12)++ "\\n" ++ "0" ++ "\\n" ++"inverse_intermediate_output_2_12 = "++ show(inverse_intermediate_output_2_12)++ "\\n" ++ "0" ++ "\\n" ++"inverse_intermediate_output_3_12 = "++ show(inverse_intermediate_output_3_12)++ "\\n" ++ "0" ++ "\\n" ++"cipher_output_4_12 = "++ show(cipher_output_4_12)++ "\\n" ++ "0" ++ "\\n" ++"intermediate_output_2_12 = "++ show(intermediate_output_2_12)++ "\\n" ++ "0" ++ "\\n" ++"inverse_intermediate_output_2_12 = "++ show(inverse_intermediate_output_2_12)++ "\\n" ++ "0" ++ "\\n" ];']
+ """
+ key_schedule_components, key_schedule_components_ids = self.extract_key_schedule()
+ cipher_inputs = self._cipher.inputs
+ cipher = self._cipher
+ inverse_cipher = self.inverse_cipher
+ cp_constraints = [solve_satisfy]
+ new_constraint = 'output['
+ incompatibility_constraint = 'constraint '
+ for element in cipher_inputs:
+ new_constraint = f'{new_constraint}\"{element} = \"++ show({element}) ++ \"\\n\" ++'
+ for element in cipher_inputs:
+ if element not in key_schedule_components_ids:
+ new_constraint = f'{new_constraint}\"inverse_{element} = \"++ show(inverse_{element}) ++ \"\\n\" ++'
+ for id_link in self._cipher.get_all_components_ids():
+ if id_link not in key_schedule_components_ids and self.get_component_round(id_link) in list(range(initial_round - 1, middle_round)) + list(range(final_round, number_of_rounds)) and 'constant' not in id_link and 'output' in id_link:
+ new_constraint = new_constraint + f'\"{id_link} = \"++ show({id_link})++ \"\\n\" ++ \"0\" ++ \"\\n\" ++'
+ if id_link not in key_schedule_components_ids and self.get_component_round(id_link) in list(range(initial_round - 1)) + list(range(middle_round - 1, final_round)) and 'constant' not in id_link and 'output' in id_link:
+ new_constraint = new_constraint + f'\"inverse_{id_link} = \"++ show(inverse_{id_link})++ \"\\n\" ++ \"0\" ++ \"\\n\" ++'
+ if intermediate_components:
+ for component in cipher.get_components_in_round(middle_round-1):
+ if component.type != CONSTANT and component.id not in key_schedule_components_ids:
+ component_id = component.id
+ input_id_links = component.input_id_links
+ input_bit_positions = component.input_bit_positions
+ component_inputs = []
+ input_bit_size = 0
+ for id_link, bit_positions in zip(input_id_links, input_bit_positions):
+ component_inputs.extend([f'{id_link}[{position}]' for position in bit_positions])
+ input_bit_size += len(bit_positions)
+ #new_constraint = new_constraint + \
+ # f'\"{id_link} = \"++ show({id_link})++ \"\\n\" ++ \"0\" ++ \"\\n\" ++'
+ #new_constraint = new_constraint + \
+ # f'\"inverse_{component_id} = \"++ show(inverse_{component_id})++ \"\\n\" ++ \"0\" ++ \"\\n\" ++'
+ for i in range(input_bit_size):
+ incompatibility_constraint += f'({component_inputs[i]}+inverse_{component_id}[{i}]=1) \\/ '
+ else:
+ for component in cipher.get_components_in_round(middle_round-1):
+ if 'output' in component.id and component.id not in key_schedule_components_ids:
+ new_constraint = new_constraint + \
+ f'\"{component.id} = \"++ show({component.id})++ \"\\n\" ++ \"0\" ++ \"\\n\" ++'
+ new_constraint = new_constraint + \
+ f'\"inverse_{component.id} = \"++ show(inverse_{component.id})++ \"\\n\" ++ \"0\" ++ \"\\n\" ++'
+ for i in range(component.output_bit_size):
+ incompatibility_constraint += f'({component.id}[{i}]+inverse_{component.id}[{i}]=1) \\/ '
+ incompatibility_constraint = incompatibility_constraint[:-4] + ';'
+ new_constraint = new_constraint[:-2] + '];'
+ cp_constraints.append(incompatibility_constraint)
+ cp_constraints.append(new_constraint)
+
+ return cp_constraints
+
+ def final_impossible_constraints(self, number_of_rounds, initial_round, middle_round, final_round, intermediate_components):
+ """
+ Constraints for output and incompatibility.
+
+ INPUT:
+
+ - ``number_of_rounds`` -- **integer** ; number of rounds
+ - ``initial_round`` -- **integer** ; initial round of the impossible differential trail
+ - ``middle_round`` -- **integer** ; incosistency round of the impossible differential trail
+ - ``final_round`` -- **integer** ; final round of the impossible differential trail
+ - ``intermediate_components`` -- **Boolean** ; check inconsistency on intermediate components of the inconsistency round or only on outputs
+
+ EXAMPLES::
+
+ sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_bitwise_impossible_xor_differential_model import MznBitwiseImpossibleXorDifferentialModel
+ sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
+ sage: from claasp.cipher_modules.models.utils import set_fixed_variables, integer_to_bit_list
+ sage: speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=5)
+ sage: cp = MznBitwiseImpossibleXorDifferentialModel(speck)
+ sage: cp.final_impossible_constraints(3, 2, 3, 4, False)
+ ['solve satisfy;',
+ ...
+ 'output["key = "++ show(key) ++ "\\n" ++"intermediate_output_0_5 = "++ show(intermediate_output_0_5) ++ "\\n" ++"intermediate_output_0_6 = "++ show(intermediate_output_0_6) ++ "\\n" ++"inverse_key = "++ show(inverse_key) ++ "\\n" ++ "0" ++ "\\n" ++"inverse_intermediate_output_3_12 = "++ show(inverse_intermediate_output_3_12) ++ "\\n" ++ "0" ++ "\\n" ++"intermediate_output_0_6 = "++ show(intermediate_output_0_6)++ "\\n" ++ "0" ++ "\\n" ++"intermediate_output_1_12 = "++ show(intermediate_output_1_12)++ "\\n" ++ "0" ++ "\\n" ++"intermediate_output_2_12 = "++ show(intermediate_output_2_12)++ "\\n" ++ "0" ++ "\\n" ++"inverse_intermediate_output_2_12 = "++ show(inverse_intermediate_output_2_12)++ "\\n" ++ "0" ++ "\\n" ++"inverse_intermediate_output_3_12 = "++ show(inverse_intermediate_output_3_12)++ "\\n" ++ "0" ++ "\\n" ++"inverse_cipher_output_4_12 = "++ show(inverse_cipher_output_4_12)++ "\\n" ++ "0" ++ "\\n" ];']
+ """
+ if initial_round == 1:
+ cipher_inputs = self._cipher.inputs
+ else:
+ cipher_inputs = ['key']
+ for component in self._cipher.get_components_in_round(initial_round - 2):
+ if 'output' in component.id:
+ cipher_inputs.append(component.id)
+ cipher = self._cipher
+ inverse_cipher = self.inverse_cipher
+ if final_round == self._cipher.number_of_rounds:
+ cipher_outputs = inverse_cipher.inputs
+ else:
+ cipher_outputs = ['key']
+ for component in self.inverse_cipher.get_components_in_round(self._cipher.number_of_rounds - final_round):
+ if 'output' in component.id:
+ cipher_outputs.append(component.id)
+ cp_constraints = [solve_satisfy]
+ new_constraint = 'output['
+ incompatibility_constraint = 'constraint'
+ key_schedule_components, key_schedule_components_ids = self.extract_key_schedule()
+ for element in cipher_inputs:
+ new_constraint = f'{new_constraint}\"{element} = \"++ show({element}) ++ \"\\n\" ++'
+ for element in cipher_outputs:
+ new_constraint = f'{new_constraint}\"inverse_{element} = \"++ show(inverse_{element}) ++ \"\\n\" ++ \"0\" ++ \"\\n\" ++'
+ if intermediate_components:
+ for component in cipher.get_components_in_round(middle_round-1):
+ if component.type != CONSTANT and component.id not in key_schedule_components_ids:
+ component_id = component.id
+ input_id_links = component.input_id_links
+ input_bit_positions = component.input_bit_positions
+ component_inputs = []
+ input_bit_size = 0
+ for id_link, bit_positions in zip(input_id_links, input_bit_positions):
+ component_inputs.extend([f'{id_link}[{position}]' for position in bit_positions])
+ input_bit_size += len(bit_positions)
+ new_constraint = new_constraint + \
+ f'\"{id_link} = \"++ show({id_link})++ \"\\n\" ++ \"0\" ++ \"\\n\" ++'
+ new_constraint = new_constraint + \
+ f'\"inverse_{component_id} = \"++ show(inverse_{component_id})++ \"\\n\" ++ \"0\" ++ \"\\n\" ++'
+ for i in range(input_bit_size):
+ incompatibility_constraint += f'({component_inputs[i]}+inverse_{component_id}[{i}]=1) \\/ '
+ else:
+ for component in cipher.get_all_components():
+ if 'output' in component.id and component.id not in key_schedule_components_ids:
+ if self.get_component_round(component.id) <= middle_round - 1:
+ new_constraint = new_constraint + \
+ f'\"{component.id} = \"++ show({component.id})++ \"\\n\" ++ \"0\" ++ \"\\n\" ++'
+ if self.get_component_round(component.id) >= middle_round - 1:
+ new_constraint = new_constraint + \
+ f'\"inverse_{component.id} = \"++ show(inverse_{component.id})++ \"\\n\" ++ \"0\" ++ \"\\n\" ++'
+ if self.get_component_round(component.id) == middle_round - 1:
+ for i in range(component.output_bit_size):
+ incompatibility_constraint += f'({component.id}[{i}]+inverse_{component.id}[{i}]=1) \\/ '
+ incompatibility_constraint = incompatibility_constraint[:-4] + ';'
+ new_constraint = new_constraint[:-2] + '];'
+ cp_constraints.append(incompatibility_constraint)
+ cp_constraints.append(new_constraint)
+
+ return cp_constraints
+
+ def find_all_impossible_xor_differential_trails(self, number_of_rounds, fixed_values=[], solver_name=None, initial_round = 1, middle_round=2, final_round = None, intermediate_components = True, num_of_processors=None, timelimit=None, solve_with_API=False, solve_external = True):
+ """
+ Search for all impossible XOR differential trails of a cipher.
+
+ INPUT:
+
+ - ``number_of_rounds`` -- **integer** (default: `None`); number of rounds
+ - ``fixed_values`` -- **list** (default: `[]`); dictionaries containing the variables to be fixed in standard
+ format
+ - ``initial_round`` -- **integer** (default: `1`); initial round of the impossible differential
+ - ``middle_round`` -- **integer** (default: `1`); incosistency round of the impossible differential
+ - ``final_round`` -- **integer** (default: `None`); final round of the impossible differential
+ - ``intermediate_components`` -- **Boolean** (default: `True`); check inconsistency on intermediate components of the inconsistency round or only on outputs
+ - ``num_of_processors`` -- **Integer** (default: `None`); number of processors used for MiniZinc search
+ - ``timelimit`` -- **Integer** (default: `None`); time limit of MiniZinc search
+
+ EXAMPLES::
+
+ sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_bitwise_impossible_xor_differential_model import MznBitwiseImpossibleXorDifferentialModel
+ sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
+ sage: from claasp.cipher_modules.models.utils import set_fixed_variables, integer_to_bit_list
+ sage: speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=4)
+ sage: cp = MznBitwiseImpossibleXorDifferentialModel(speck)
+ sage: fixed_variables = [set_fixed_variables('key', 'equal', range(64), integer_to_bit_list(0, 64, 'little'))]
+ sage: fixed_variables.append(set_fixed_variables('plaintext', 'not_equal', range(32), integer_to_bit_list(0, 32, 'little')))
+ sage: fixed_variables.append(set_fixed_variables('inverse_cipher_output_3_12', 'not_equal', range(32), integer_to_bit_list(0, 32, 'little')))
+ sage: trail = cp.find_all_impossible_xor_differential_trails(4, fixed_variables, 'Chuffed', 1, 3, 4, False) #doctest: +SKIP
+
+ """
+ self.build_impossible_xor_differential_trail_model(fixed_values, number_of_rounds, initial_round, middle_round, final_round, intermediate_components)
+
+ if solve_with_API:
+ return self.solve_for_ARX(solver_name = solver_name, timeout_in_seconds_ = timelimit, processes_ = num_of_processors, all_solutions_ = True)
+ return self.solve(IMPOSSIBLE_XOR_DIFFERENTIAL, solver_name = solver_name, number_of_rounds = number_of_rounds, initial_round = initial_round, middle_round = middle_round, final_round = final_round, timeout_in_seconds_ = timelimit, processes_ = num_of_processors, all_solutions_ = True, solve_external = solve_external)
+
+ def find_lowest_complexity_impossible_xor_differential_trail(self, number_of_rounds=None, fixed_values=[], solver_name=None, initial_round = 1, middle_round=2, final_round = None, intermediate_components = True, num_of_processors=None, timelimit=None, solve_with_API=False, solve_external = True):
+ """
+ Search for the impossible XOR differential trail of a cipher with the highest number of known bits in plaintext and ciphertext difference.
+
+ INPUT:
+
+ - ``number_of_rounds`` -- **integer** (default: `None`); number of rounds
+ - ``fixed_values`` -- **list** (default: `[]`); dictionaries containing the variables to be fixed in standard
+ format
+ - ``initial_round`` -- **integer** (default: `1`); initial round of the impossible differential
+ - ``middle_round`` -- **integer** (default: `1`); incosistency round of the impossible differential
+ - ``final_round`` -- **integer** (default: `None`); final round of the impossible differential
+ - ``intermediate_components`` -- **Boolean** (default: `True`); check inconsistency on intermediate components of the inconsistency round or only on outputs
+ - ``num_of_processors`` -- **Integer** (default: `None`); number of processors used for MiniZinc search
+ - ``timelimit`` -- **Integer** (default: `None`); time limit of MiniZinc search
+
+ EXAMPLES::
+
+ sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_bitwise_impossible_xor_differential_model import MznBitwiseImpossibleXorDifferentialModel
+ sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
+ sage: from claasp.cipher_modules.models.utils import set_fixed_variables, integer_to_bit_list
+ sage: speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=4)
+ sage: cp = MznBitwiseImpossibleXorDifferentialModel(speck)
+ sage: fixed_variables = [set_fixed_variables('key', 'equal', range(64), integer_to_bit_list(0, 64, 'little'))]
+ sage: fixed_variables.append(set_fixed_variables('plaintext', 'not_equal', range(32), integer_to_bit_list(0, 32, 'little')))
+ sage: fixed_variables.append(set_fixed_variables('inverse_cipher_output_3_12', 'not_equal', range(32), integer_to_bit_list(0, 32, 'little')))
+ sage: trail = cp.find_lowest_complexity_impossible_xor_differential_trail(4, fixed_variables, 'Chuffed', 1, 3, 4, intermediate_components = False)
+ """
+ self.build_impossible_xor_differential_trail_model(fixed_values, number_of_rounds, initial_round, middle_round, final_round, intermediate_components)
+ self._model_constraints.remove(f'solve satisfy;')
+ self._model_constraints.append(f'solve minimize count(plaintext, 2) + count(inverse_{self._cipher.get_all_components_ids()[-1]}, 2);')
+
+ if solve_with_API:
+ return self.solve_for_ARX(solver_name = solver_name, timeout_in_seconds_ = timelimit, processes_ = num_of_processors)
+ return self.solve('impossible_xor_differential_one_solution', solver_name = solver_name, number_of_rounds = number_of_rounds, initial_round = initial_round, middle_round = middle_round, final_round = final_round, timeout_in_seconds_ = timelimit, processes_ = num_of_processors, solve_external = solve_external)
+
+ def find_one_impossible_xor_differential_trail_with_extensions(self, number_of_rounds=None, fixed_values=[], solver_name=None, initial_round = 1, middle_round=2, final_round = None, intermediate_components = True, num_of_processors=None, timelimit=None, solve_with_API=False, solve_external = True):
+ """
+ Search for one impossible XOR differential trail of a cipher with forward and backward deterministic extensions for key recovery.
+
+ INPUT:
+
+ - ``number_of_rounds`` -- **integer** (default: `None`); number of rounds
+ - ``fixed_values`` -- **list** (default: `[]`); dictionaries containing the variables to be fixed in standard
+ format
+ - ``initial_round`` -- **integer** (default: `1`); initial round of the impossible differential
+ - ``middle_round`` -- **integer** (default: `1`); incosistency round of the impossible differential
+ - ``final_round`` -- **integer** (default: `None`); final round of the impossible differential
+ - ``intermediate_components`` -- **Boolean** (default: `True`); check inconsistency on intermediate components of the inconsistency round or only on outputs
+ - ``num_of_processors`` -- **Integer** (default: `None`); number of processors used for MiniZinc search
+ - ``timelimit`` -- **Integer** (default: `None`); time limit of MiniZinc search
+
+ EXAMPLES::
+
+ sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_bitwise_impossible_xor_differential_model import MznBitwiseImpossibleXorDifferentialModel
+ sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
+ sage: from claasp.cipher_modules.models.utils import set_fixed_variables, integer_to_bit_list
+ sage: speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=7)
+ sage: cp = MznBitwiseImpossibleXorDifferentialModel(speck)
+ sage: fixed_variables = [set_fixed_variables('key', 'equal', range(64), integer_to_bit_list(0, 64, 'little'))]
+ sage: fixed_variables.append(set_fixed_variables('plaintext', 'not_equal', range(32), integer_to_bit_list(0, 32, 'little')))
+ sage: fixed_variables.append(set_fixed_variables('cipher_output_6_12', 'not_equal', range(32), integer_to_bit_list(0, 32, 'little')))
+ sage: trail = cp.find_one_impossible_xor_differential_trail_with_extensions(7, fixed_variables, 'Chuffed', 2, 4, 6, intermediate_components = False)
+ """
+ self.build_impossible_xor_differential_trail_with_extensions_model(fixed_values, number_of_rounds, initial_round, middle_round, final_round, intermediate_components)
+
+ if solve_with_API:
+ return self.solve_for_ARX(solver_name = solver_name, timeout_in_seconds_ = timelimit, processes_ = num_of_processors)
+ return self.solve('impossible_xor_differential_one_solution', solver_name = solver_name, number_of_rounds = number_of_rounds, initial_round = initial_round, middle_round = middle_round, final_round = final_round, timeout_in_seconds_ = timelimit, processes_ = num_of_processors, solve_external = solve_external)
+
+ def find_one_impossible_xor_differential_trail(self, number_of_rounds=None, fixed_values=[], solver_name=None, initial_round = 1, middle_round=2, final_round = None, intermediate_components = True, num_of_processors=None, timelimit=None, solve_with_API=False, solve_external = True):
+ """
+ Search for one impossible XOR differential trail of a cipher.
+
+ INPUT:
+
+ - ``number_of_rounds`` -- **integer** (default: `None`); number of rounds
+ - ``fixed_values`` -- **list** (default: `[]`); dictionaries containing the variables to be fixed in standard
+ format
+ - ``initial_round`` -- **integer** (default: `1`); initial round of the impossible differential
+ - ``middle_round`` -- **integer** (default: `1`); incosistency round of the impossible differential
+ - ``final_round`` -- **integer** (default: `None`); final round of the impossible differential
+ - ``intermediate_components`` -- **Boolean** (default: `True`); check inconsistency on intermediate components of the inconsistency round or only on outputs
+ - ``num_of_processors`` -- **Integer** (default: `None`); number of processors used for MiniZinc search
+ - ``timelimit`` -- **Integer** (default: `None`); time limit of MiniZinc search
+
+ EXAMPLES::
+
+ sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_bitwise_impossible_xor_differential_model import MznBitwiseImpossibleXorDifferentialModel
+ sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
+ sage: from claasp.cipher_modules.models.utils import set_fixed_variables, integer_to_bit_list
+ sage: speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=4)
+ sage: cp = MznBitwiseImpossibleXorDifferentialModel(speck)
+ sage: fixed_variables = [set_fixed_variables('key', 'equal', range(64), integer_to_bit_list(0, 64, 'little'))]
+ sage: fixed_variables.append(set_fixed_variables('plaintext', 'not_equal', range(32), integer_to_bit_list(0, 32, 'little')))
+ sage: fixed_variables.append(set_fixed_variables('inverse_cipher_output_3_12', 'not_equal', range(32), integer_to_bit_list(0, 32, 'little')))
+ sage: trail = cp.find_one_impossible_xor_differential_trail(4, fixed_variables, 'Chuffed', 1, 3, 4, intermediate_components = False)
+ """
+ self.build_impossible_xor_differential_trail_model(fixed_values, number_of_rounds, initial_round, middle_round, final_round, intermediate_components)
+
+ if solve_with_API:
+ return self.solve_for_ARX(solver_name = solver_name, timeout_in_seconds_ = timelimit, processes_ = num_of_processors)
+ return self.solve('impossible_xor_differential_one_solution', solver_name = solver_name, number_of_rounds = number_of_rounds, initial_round = initial_round, middle_round = middle_round, final_round = final_round, timeout_in_seconds_ = timelimit, processes_ = num_of_processors, solve_external = solve_external)
+
+ def get_component_from_id(self, id_link, curr_cipher):
+ for component in curr_cipher.get_all_components():
+ if component.id == id_link:
+ return component
+ return None
+
+ def get_component_round(self, id_link):
+ if '_' in id_link:
+ last_us = - id_link[::-1].index('_') - 1
+ start = - id_link[last_us - 1::-1].index('_') + last_us
+
+ return int(id_link[start:len(id_link) + last_us])
+ else:
+ return 0
+
+ def get_direct_component_correspondance(self, forward_component):
+ for inverse_component in self.inverse_cipher.get_all_components():
+ if inverse_component.get_inverse_component_correspondance(inverse_component) == forward_component:
+ return inverse_component
+
+ def get_inverse_component_correspondance(self, backward_component):
+
+ for component in self._cipher.get_all_components():
+ if backward_component.id == component.id:
+ direct_inputs = component.input_id_links
+ inverse_outputs = []
+ for component in self.inverse_cipher.get_all_components():
+ if backward_component.id in component.input_id_links:
+ inverse_outputs.append(component.id)
+ correspondance = [dir_i for dir_i in direct_inputs if dir_i in inverse_outputs]
+ if len(correspondance) > 1:
+ return 'Not invertible'
+ else:
+ return correspondance[0]
+
+ def get_inverse_state_key_bits_positions(self):
+ key_bits = self.key_schedule_bits_distribution
+ for component in self.inverse_cipher.get_all_components():
+ if component.id not in key_bits:
+ component_key_bits = []
+ for id_link in component.input_id_links:
+ if id_link in key_bits:
+ component_key_bits.extend(key_bits[id_link])
+ key_bits[component.id] = list(set(component_key_bits))
+
+ return key_bits
+
+ def get_state_key_bits_positions(self):
+ key_bits = self.key_schedule_bits_distribution
+ for component in self._cipher.get_all_components():
+ if component.id not in key_bits:
+ component_key_bits = []
+ for id_link in component.input_id_links:
+ if id_link in key_bits:
+ component_key_bits.extend(key_bits[id_link])
+ key_bits[component.id] = list(set(component_key_bits))
+
+ return key_bits
+
+ def input_impossible_constraints_with_extensions(self, number_of_rounds=None, initial_round=None, middle_round=None, final_round=None):
+
+ if number_of_rounds is None:
+ number_of_rounds = self._cipher.number_of_rounds
+
+ cp_constraints = []
+ cp_declarations = [f'array[0..{bit_size - 1}] of var 0..2: {input_};'
+ for input_, bit_size in zip(self._cipher.inputs, self._cipher.inputs_bit_size)]
+ cipher = self._cipher
+ inverse_cipher = self.inverse_cipher
+
+ key_components, key_ids = self.extract_key_schedule()
+ constant_components, constant_ids = self.extract_constants()
+
+ forward_components = []
+ for component in self._cipher.get_all_components():
+ comp_r = self.get_component_round(component.id)
+ if comp_r >= initial_round - 1 and comp_r <= middle_round - 1 or comp_r > final_round - 1:
+ forward_components.append(component)
+ components_to_direct = []
+ for component in forward_components:
+ for id_link in component.input_id_links:
+ input_component = self.get_component_from_id(id_link, cipher)
+ if input_component not in key_ids + constant_ids + forward_components + components_to_direct and input_component != None:
+ components_to_direct.append(input_component)
+ forward_components.extend(components_to_direct)
+ forward_components.extend(key_components)
+ forward_components.extend(constant_components)
+
+ backward_components = []
+ for component in inverse_cipher.get_all_components():
+ comp_r = self.get_component_round(component.id)
+ if comp_r < initial_round - 1 or comp_r >= middle_round - 1 and comp_r <= final_round - 1:
+ backward_components.append(component)
+ components_to_invert = []
+ for component in backward_components:
+ for id_link in component.input_id_links:
+ input_component = self.get_component_from_id(id_link, inverse_cipher)
+ if input_component not in key_ids + constant_ids + backward_components + components_to_invert and input_component != None:
+ components_to_invert.append(input_component)
+ backward_components.extend(components_to_invert)
+
+ for component in forward_components:
+ output_id_link = component.id
+ output_size = int(component.output_bit_size)
+ if 'output' in component.type:
+ cp_declarations.append(f'array[0..{output_size - 1}] of var 0..2: {output_id_link};')
+ cp_constraints.append(f'constraint count({output_id_link},2) < {output_size};')
+ elif CONSTANT not in component.type:
+ cp_declarations.append(f'array[0..{output_size - 1}] of var 0..2: {output_id_link};')
+
+ for component in backward_components:
+ output_id_link = component.id
+ output_size = int(component.output_bit_size)
+ if 'output' in component.type:
+ cp_declarations.append(f'array[0..{output_size - 1}] of var 0..2: inverse_{output_id_link};')
+ cp_constraints.append(f'constraint count(inverse_{output_id_link},2) < {output_size};')
+ if self.get_component_round(component.id) == final_round - 1 or self.get_component_round(component.id) == initial_round - 2:
+ cp_constraints.append(f'constraint count(inverse_{output_id_link},1) > 0;')
+ elif CONSTANT not in component.type:
+ cp_declarations.append(f'array[0..{output_size - 1}] of var 0..2: inverse_{output_id_link};')
+
+ cp_constraints.append(f'constraint count(plaintext,2) < {self._cipher.output_bit_size};')
+
+ for component in self._cipher.get_all_components():
+ if CIPHER_OUTPUT in component.type:
+ cp_constraints.append(f'constraint count({component.id},2) < {self._cipher.output_bit_size};')
+
+ return cp_declarations, cp_constraints
+
+ def input_impossible_constraints(self, number_of_rounds=None, middle_round=None):
+
+ if number_of_rounds is None:
+ number_of_rounds = self._cipher.number_of_rounds
+
+ cp_constraints = []
+ cp_declarations = [f'array[0..{bit_size - 1}] of var 0..2: {input_};'
+ for input_, bit_size in zip(self._cipher.inputs, self._cipher.inputs_bit_size)]
+ cipher = self._cipher
+ inverse_cipher = self.inverse_cipher
+ forward_components = []
+ for r in range(middle_round):
+ forward_components.extend(self._cipher.get_components_in_round(r))
+ backward_components = []
+ for r in range(number_of_rounds - middle_round + 1):
+ backward_components.extend(inverse_cipher.get_components_in_round(r))
+ cp_declarations.extend([f'array[0..{bit_size - 1}] of var 0..2: inverse_{input_};' for input_, bit_size in zip(inverse_cipher.inputs, inverse_cipher.inputs_bit_size)])
+ for component in forward_components:
+ output_id_link = component.id
+ output_size = int(component.output_bit_size)
+ if 'output' in component.type:
+ cp_declarations.append(f'array[0..{output_size - 1}] of var 0..2: {output_id_link};')
+ elif CIPHER_OUTPUT in component.type:
+ cp_declarations.append(f'array[0..{output_size - 1}] of var 0..2: {output_id_link};')
+ cp_constraints.append(f'constraint count({output_id_link},2) < {output_size};')
+ elif CONSTANT not in component.type:
+ cp_declarations.append(f'array[0..{output_size - 1}] of var 0..2: {output_id_link};')
+ for component in backward_components:
+ output_id_link = component.id
+ output_size = int(component.output_bit_size)
+ if 'output' in component.type:
+ cp_declarations.append(f'array[0..{output_size - 1}] of var 0..2: inverse_{output_id_link};')
+ elif CIPHER_OUTPUT in component.type:
+ cp_declarations.append(f'array[0..{output_size - 1}] of var 0..2: inverse_{output_id_link};')
+ cp_constraints.append(f'constraint count(inverse_{output_id_link},2) < {output_size};')
+ cp_constraints.append(f'constraint count(inverse_{output_id_link},1) > 0;')
+ elif CONSTANT not in component.type:
+ cp_declarations.append(f'array[0..{output_size - 1}] of var 0..2: inverse_{output_id_link};')
+ cp_constraints.append('constraint count(plaintext,1) > 0;')
+
+ return cp_declarations, cp_constraints
+
+ def is_cross_round_component(self, component, discarded_ids):
+ component_round = self.get_component_round(component.id)
+ for input_id in component.input_id_links:
+ if input_id not in discarded_ids and self.get_component_round(input_id) != component_round:
+ return True
+ return False
+
+ def link_constraints_for_trail_with_extensions(self, components_to_link):
+ linking_constraints = []
+ for pairs in components_to_link:
+ linking_constraints.append(f'constraint {pairs[0]} = inverse_{pairs[1]};')
+
+ return linking_constraints
+
+ def _parse_solver_output(self, output_to_parse, number_of_rounds, initial_round, middle_round, final_round):
+ components_values, memory, time = self.parse_solver_information(output_to_parse, True, True)
+ all_components = [*self._cipher.inputs]
+ for r in list(range(initial_round - 1, middle_round)) + list(range(final_round, number_of_rounds)):
+ all_components.extend([component.id for component in [*self._cipher.get_components_in_round(r)]])
+ for r in list(range(initial_round - 1)) + list(range(middle_round - 1, final_round)):
+ all_components.extend(['inverse_' + component.id for component in [*self.inverse_cipher.get_components_in_round(number_of_rounds - r - 1)]])
+ all_components.extend(['inverse_' + id_link for id_link in [*self.inverse_cipher.inputs]])
+ all_components.extend(['inverse_' + id_link for id_link in [*self._cipher.inputs]])
+ for component_id in all_components:
+ solution_number = 1
+ for j, string in enumerate(output_to_parse):
+ if f'{component_id}' in string and 'inverse_' not in component_id + string:
+ value = self.format_component_value(component_id, string)
+ component_solution = {}
+ component_solution['value'] = value
+ self.add_solution_to_components_values(component_id, component_solution, components_values, j,
+ output_to_parse, solution_number, string)
+ elif f'{component_id}' in string and 'inverse_' in component_id:
+ value = self.format_component_value(component_id, string)
+ component_solution = {}
+ component_solution['value'] = value
+ self.add_solution_to_components_values(component_id, component_solution, components_values, j,
+ output_to_parse, solution_number, string)
+ elif '----------' in string:
+ solution_number += 1
+
+ return time, memory, components_values
+
+ def set_inverse_component_id_in_constraints(self, component, inverse_variables, inverse_constraints):
+ for v in range(len(inverse_variables)):
+ start = 0
+ while component.id in inverse_variables[v][start:]:
+ new_start = inverse_variables[v].index(component.id, start)
+ inverse_variables[v] = inverse_variables[v][:new_start] + 'inverse_' + inverse_variables[v][new_start:]
+ start = new_start + 9
+ for c in range(len(inverse_constraints)):
+ start = 0
+ while component.id in inverse_constraints[c][start:]:
+ new_start = inverse_constraints[c].index(component.id, start)
+ inverse_constraints[c] = inverse_constraints[c][:new_start] + 'inverse_' + inverse_constraints[c][new_start:]
+ start = new_start + 9
+
+ return inverse_variables, inverse_constraints
+
+ def solve(self, model_type, solver_name=None, number_of_rounds=None, initial_round=None, middle_round=None, final_round=None, processes_=None, timeout_in_seconds_=None, all_solutions_=False, solve_external = False):
+ cipher_name = self.cipher_id
+ input_file_path = f'{cipher_name}_Mzn_{model_type}_{solver_name}.mzn'
+ command = self.get_command_for_solver_process(input_file_path, model_type, solver_name, processes_, timeout_in_seconds_)
+ solver_process = subprocess.run(command, stdout=subprocess.PIPE, stderr=subprocess.PIPE, encoding="utf-8")
+ os.remove(input_file_path)
+ if solver_process.returncode >= 0:
+ solutions = []
+ solver_output = solver_process.stdout.splitlines()
+ if model_type in ['deterministic_truncated_xor_differential',
+ 'deterministic_truncated_xor_differential_one_solution',
+ 'impossible_xor_differential',
+ 'impossible_xor_differential_one_solution',
+ 'impossible_xor_differential_attack']:
+ solve_time, memory, components_values = self._parse_solver_output(solver_output, number_of_rounds, initial_round, middle_round, final_round)
+ total_weight = 0
+ else:
+ solve_time, memory, components_values, total_weight = self._parse_solver_output(solver_output, number_of_rounds, initial_round, middle_round, final_round)
+ if components_values == {}:
+ solution = convert_solver_solution_to_dictionary(self.cipher_id, model_type, solver_name,
+ solve_time, memory,
+ components_values, total_weight)
+ if 'UNSATISFIABLE' in solver_output[0]:
+ solution['status'] = 'UNSATISFIABLE'
+ else:
+ solution['status'] = 'SATISFIABLE'
+ solutions.append(solution)
+ else:
+ self.add_solutions_from_components_values(components_values, memory, model_type, solutions, solve_time,
+ solver_name, solver_output, 0, solve_external)
+ if model_type in ['xor_differential_one_solution',
+ 'xor_linear_one_solution',
+ 'deterministic_truncated_one_solution',
+ 'impossible_xor_differential_one_solution']:
+ return solutions[0]
+ else:
+ return solutions
\ No newline at end of file
diff --git a/claasp/cipher_modules/models/cp/mzn_models/mzn_impossible_xor_differential_model.py b/claasp/cipher_modules/models/cp/mzn_models/mzn_impossible_xor_differential_model.py
index 72b76ce5..a2b306ec 100644
--- a/claasp/cipher_modules/models/cp/mzn_models/mzn_impossible_xor_differential_model.py
+++ b/claasp/cipher_modules/models/cp/mzn_models/mzn_impossible_xor_differential_model.py
@@ -1,927 +1,90 @@
# ****************************************************************************
# Copyright 2023 Technology Innovation Institute
-#
+#
# This program is free software: you can redistribute it and/or modify
# it under the terms of the GNU General Public License as published by
# the Free Software Foundation, either version 3 of the License, or
# (at your option) any later version.
-#
+#
# This program is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
# GNU General Public License for more details.
-#
+#
# You should have received a copy of the GNU General Public License
# along with this program. If not, see .
# ****************************************************************************
+"""
+The search methods presented in this class differ from those of the classes
+:py:class:`Mzn Bitwise Impossible Xor Differential Model
+`
-import os
-import math
-import itertools
-import subprocess
-from copy import deepcopy
+and :py:class:`Mzn Wordwise Impossible Xor Differential Model
+`.
-from claasp.cipher_modules.models.cp.mzn_model import solve_satisfy
-from claasp.cipher_modules.models.utils import write_model_to_file, convert_solver_solution_to_dictionary, check_if_implemented_component
-from claasp.cipher_modules.models.cp.mzn_models.mzn_deterministic_truncated_xor_differential_model import MznDeterministicTruncatedXorDifferentialModel
+Indeed, this class implements the framework proposed by `Cui et al.` which uses
+infeasibility of a XOR DIFFERENTIAL model to detect an impossible differential trail.
+"""
-from claasp.name_mappings import (CONSTANT, INTERMEDIATE_OUTPUT, CIPHER_OUTPUT, LINEAR_LAYER, SBOX, MIX_COLUMN,
- WORD_OPERATION, DETERMINISTIC_TRUNCATED_XOR_DIFFERENTIAL, IMPOSSIBLE_XOR_DIFFERENTIAL)
-from claasp.cipher_modules.models.cp.solvers import CP_SOLVERS_EXTERNAL, SOLVER_DEFAULT
+from claasp.cipher_modules.models.cp import solvers
+from claasp.cipher_modules.models.cp.mzn_models.mzn_xor_differential_model import MznXorDifferentialModel
+from claasp.cipher_modules.models.utils import enumerate_impossible_xor_differential_trails
-class MznImpossibleXorDifferentialModel(MznDeterministicTruncatedXorDifferentialModel):
-
+class MznImpossibleXorDifferentialModel(MznXorDifferentialModel):
def __init__(self, cipher):
super().__init__(cipher)
- self.inverse_cipher = cipher.cipher_inverse()
- self.middle_round = 1
- self.key_schedule_bits_distribution = {}
- self.key_involvements = self.get_state_key_bits_positions()
- self.inverse_key_involvements = self.get_inverse_state_key_bits_positions()
-
- def add_solution_to_components_values(self, component_id, component_solution, components_values, j, output_to_parse,
- solution_number, string):
- inverse_cipher = self.inverse_cipher
- if component_id in self._cipher.inputs:
- components_values[f'solution{solution_number}'][f'{component_id}'] = component_solution
- elif component_id in self.inverse_cipher.inputs:
- components_values[f'solution{solution_number}'][f'inverse_{component_id}'] = component_solution
- elif f'{component_id}_i' in string:
- components_values[f'solution{solution_number}'][f'{component_id}_i'] = component_solution
- elif f'{component_id}_o' in string:
- components_values[f'solution{solution_number}'][f'{component_id}_o'] = component_solution
- elif f'inverse_{component_id} ' in string:
- components_values[f'solution{solution_number}'][f'inverse_{component_id}'] = component_solution
- elif f'{component_id} ' in string:
- components_values[f'solution{solution_number}'][f'{component_id}'] = component_solution
-
- def build_impossible_backward_model(self, backward_components, clean = True):
- inverse_variables = []
- inverse_constraints = []
- key_components, key_ids = self.extract_key_schedule()
- constant_components, constant_ids = self.extract_constants()
- for component in backward_components:
- if check_if_implemented_component(component):
- variables, constraints = self.propagate_deterministically(component)
- inverse_variables.extend(variables)
- inverse_constraints.extend(constraints)
-
- if clean:
- components_to_invert = [backward_components[i] for i in range(len(backward_components))]
- for component in backward_components:
- for id_link in component.input_id_links:
- input_component = self.get_component_from_id(id_link, self.inverse_cipher)
- if input_component not in backward_components and id_link not in key_ids + constant_ids:
- components_to_invert.append(input_component)
- inverse_variables, inverse_constraints = self.clean_inverse_impossible_variables_constraints_with_extensions(components_to_invert, inverse_variables, inverse_constraints)
-
- return inverse_variables, inverse_constraints
-
- def build_impossible_forward_model(self, forward_components, clean = False):
- direct_variables = []
- direct_constraints = []
- for component in forward_components:
- if check_if_implemented_component(component):
- variables, constraints = self.propagate_deterministically(component)
- direct_variables.extend(variables)
- direct_constraints.extend(constraints)
-
- if clean:
- direct_variables, direct_constraints = self.clean_inverse_impossible_variables_constraints(forward_components, direct_variables, direct_constraints)
-
- return direct_variables, direct_constraints
-
- def build_impossible_xor_differential_trail_with_extensions_model(self, fixed_variables, number_of_rounds, initial_round, middle_round, final_round, intermediate_components):
- """
- Build the CP model for the search of deterministic truncated XOR differential trails with extensions for key recovery.
-
- INPUT:
-
- - ``fixed_variables`` -- **list** (default: `[]`); dictionaries containing the variables to be fixed in standard
- format
- - ``number_of_rounds`` -- **integer** ; number of rounds
- - ``initial_round`` -- **integer** ; initial round of the impossible differential trail
- - ``middle_round`` -- **integer** ; incosistency round of the impossible differential trail
- - ``final_round`` -- **integer** ; final round of the impossible differential trail
- - ``intermediate_components`` -- **Boolean** ; check inconsistency on intermediate components of the inconsistency round or only on outputs
-
- EXAMPLES::
-
- sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_impossible_xor_differential_model import MznImpossibleXorDifferentialModel
- sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
- sage: from claasp.cipher_modules.models.utils import set_fixed_variables, integer_to_bit_list
- sage: speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=5)
- sage: cp = MznImpossibleXorDifferentialModel(speck)
- sage: fixed_variables = [set_fixed_variables('key', 'equal', range(64), integer_to_bit_list(0, 64, 'little'))]
- sage: cp.build_impossible_xor_differential_trail_with_extensions_model(fixed_variables, 5, 2, 3, 4, False)
- """
- self.initialise_model()
- if number_of_rounds is None:
- number_of_rounds = self._cipher.number_of_rounds
- inverse_cipher = self.inverse_cipher
- if final_round is None:
- final_round = self._cipher.number_of_rounds - 1
- key_components, key_ids = self.extract_key_schedule()
- constant_components, constant_ids = self.extract_constants()
- self._variables_list = []
- constraints = self.fix_variables_value_constraints(fixed_variables)
- deterministic_truncated_xor_differential = constraints
- self.middle_round = middle_round
-
- forward_components = []
- for n_r in list(range(initial_round - 1, middle_round)) + list(range(final_round, number_of_rounds)):
- forward_components.extend(self._cipher.get_components_in_round(n_r))
-
- backward_components = []
- for n_r in list(range(initial_round - 1)) + list(range(middle_round - 1, final_round)):
- backward_components.extend(inverse_cipher.get_components_in_round(number_of_rounds - 1 - n_r))
-
- components_to_link = []
- for component in self.inverse_cipher.get_all_components():
- comp_r = self.get_component_round(component.id)
- if comp_r == initial_round - 2 or comp_r == final_round - 1:
- for id_link in component.input_id_links:
- if self.get_component_round(id_link) > comp_r:
- for input_component in self.inverse_cipher.get_all_components():
- if input_component.id == id_link:
- components_to_link.append([self.get_inverse_component_correspondance(input_component), id_link])
-
- link_constraints = self.link_constraints_for_trail_with_extensions(components_to_link)
- key_schedule_variables, key_schedule_constraints = self.constraints_for_key_schedule()
- constants_variables, constants_constraints = self.constraints_for_constants()
-
- direct_variables, direct_constraints = self.build_impossible_forward_model(forward_components)
- inverse_variables, inverse_constraints = self.build_impossible_backward_model(backward_components)
-
- variables = direct_variables + inverse_variables
- constraints = direct_constraints + inverse_constraints
-
- self._variables_list.extend(variables)
- self._variables_list.extend(key_schedule_variables)
- self._variables_list.extend(constants_variables)
- deterministic_truncated_xor_differential.extend(constraints)
- variables, constraints = self.input_impossible_constraints_with_extensions(number_of_rounds, initial_round, middle_round, final_round)
- self._model_prefix.extend(variables)
- self._variables_list.extend(constraints)
- deterministic_truncated_xor_differential.extend(link_constraints)
- deterministic_truncated_xor_differential.extend(key_schedule_constraints)
- deterministic_truncated_xor_differential.extend(constants_constraints)
- deterministic_truncated_xor_differential.extend(self.final_impossible_constraints_with_extensions(number_of_rounds, initial_round, middle_round, final_round, intermediate_components))
- set_of_constraints = self._variables_list + deterministic_truncated_xor_differential
-
- cleaned_constraints = []
- for constraint in self._model_prefix + set_of_constraints:
- if constraint not in cleaned_constraints:
- cleaned_constraints.append(constraint)
-
- self._model_constraints = cleaned_constraints
-
- def build_impossible_xor_differential_trail_model(self, fixed_variables=[], number_of_rounds=None, initial_round = 1, middle_round=1, final_round = None, intermediate_components = True):
- """
- Build the CP model for the search of deterministic truncated XOR differential trails.
-
- INPUT:
-
- - ``fixed_variables`` -- **list** (default: `[]`); dictionaries containing the variables to be fixed in standard
- format
- - ``number_of_rounds`` -- **integer** (default: `None`); number of rounds
- - ``initial_round`` -- **integer** (default: `1`); initial round of the impossible differential
- - ``middle_round`` -- **integer** (default: `1`); incosistency round of the impossible differential
- - ``final_round`` -- **integer** (default: `None`); final round of the impossible differential
- - ``intermediate_components`` -- **Boolean** (default: `True`); check inconsistency on intermediate components of the inconsistency round or only on outputs
-
- EXAMPLES::
-
- sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_impossible_xor_differential_model import MznImpossibleXorDifferentialModel
- sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
- sage: from claasp.cipher_modules.models.utils import set_fixed_variables, integer_to_bit_list
- sage: speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=4)
- sage: cp = MznImpossibleXorDifferentialModel(speck)
- sage: fixed_variables = [set_fixed_variables('key', 'equal', range(64), integer_to_bit_list(0, 64, 'little'))]
- sage: cp.build_impossible_xor_differential_trail_model(fixed_variables, 4, 1, 3, 4, False)
- """
- self.initialise_model()
- if number_of_rounds is None:
- number_of_rounds = self._cipher.number_of_rounds
- if final_round is None:
- final_round = self._cipher.number_of_rounds
- inverse_cipher = self.inverse_cipher
-
- self._variables_list = []
- constraints = self.fix_variables_value_constraints(fixed_variables)
- deterministic_truncated_xor_differential = constraints
- self.middle_round = middle_round
-
- forward_components = []
- for r in range(middle_round):
- forward_components.extend(self._cipher.get_components_in_round(r))
- backward_components = []
- for r in range(number_of_rounds - middle_round + 1):
- backward_components.extend(inverse_cipher.get_components_in_round(r))
-
- direct_variables, direct_constraints = self.build_impossible_forward_model(forward_components)
- self._variables_list.extend(direct_variables)
- deterministic_truncated_xor_differential.extend(direct_constraints)
-
- inverse_variables, inverse_constraints = self.build_impossible_backward_model(backward_components, clean = False)
- inverse_variables, inverse_constraints = self.clean_inverse_impossible_variables_constraints(backward_components, inverse_variables, inverse_constraints)
- self._variables_list.extend(inverse_variables)
- deterministic_truncated_xor_differential.extend(inverse_constraints)
-
- variables, constraints = self.input_impossible_constraints(number_of_rounds = number_of_rounds, middle_round = middle_round)
- self._model_prefix.extend(variables)
- self._variables_list.extend(constraints)
- deterministic_truncated_xor_differential.extend(self.final_impossible_constraints(number_of_rounds, initial_round, middle_round, final_round, intermediate_components))
- set_of_constraints = self._variables_list + deterministic_truncated_xor_differential
-
- self._model_constraints = self._model_prefix + self.clean_constraints(set_of_constraints, initial_round, middle_round, final_round)
-
- def clean_constraints(self, set_of_constraints, initial_round, middle_round, final_round):
- number_of_rounds = self._cipher.number_of_rounds
- input_component = 'plaintext'
- model_constraints = []
- forward_components = []
- for r in range(initial_round - 1, middle_round):
- forward_components.extend([component.id for component in self._cipher.get_components_in_round(r)])
- backward_components = []
- for r in range(number_of_rounds - final_round, number_of_rounds - middle_round + 1):
- backward_components.extend(['inverse_' + component.id for component in self.inverse_cipher.get_components_in_round(r)])
- key_components, key_ids = self.extract_key_schedule()
- components_to_keep = forward_components + backward_components + key_ids + ['inverse_' + id_link for id_link in key_ids] + ['array['] + [solve_satisfy]
- if initial_round == 1 and final_round == self._cipher.number_of_rounds:
- for i in range(len(set_of_constraints) - 1):
- if set_of_constraints[i] not in set_of_constraints[i+1:]:
- model_constraints.append(set_of_constraints[i])
- model_constraints.append(set_of_constraints[-1])
- return model_constraints
- if initial_round == 1:
- components_to_keep.extend(self._cipher.inputs)
- if final_round == number_of_rounds:
- components_to_keep.extend(['inverse_' + id_link for id_link in self.inverse_cipher.inputs])
- if initial_round > 1:
- for component in self._cipher.get_components_in_round(initial_round - 2):
- if 'output' in component.id:
- components_to_keep.append(component.id)
- input_component = component
- for constraint in set_of_constraints:
- for id_link in components_to_keep:
- if id_link in constraint and constraint not in model_constraints:
- model_constraints.append(constraint)
-
- return model_constraints
-
- def clean_inverse_impossible_variables_constraints(self, backward_components, inverse_variables, inverse_constraints):
- for component in backward_components:
- inverse_variables, inverse_constraints = self.set_inverse_component_id_in_constraints(component, inverse_variables, inverse_constraints)
- inverse_variables, inverse_constraints = self.clean_repetitions_in_constraints(inverse_variables, inverse_constraints)
- return inverse_variables, inverse_constraints
-
- def clean_inverse_impossible_variables_constraints_with_extensions(self, backward_components, inverse_variables, inverse_constraints):
- key_components, key_ids = self.extract_key_schedule()
- constant_components, constant_ids = self.extract_constants()
- for component in backward_components:
- if component.id not in key_ids + constant_ids:
- inverse_variables, inverse_constraints = self.set_inverse_component_id_in_constraints(component, inverse_variables, inverse_constraints)
- inverse_variables, inverse_constraints = self.clean_repetitions_in_constraints(inverse_variables, inverse_constraints)
- return inverse_variables, inverse_constraints
-
- def clean_repetitions_in_constraints(self, inverse_variables, inverse_constraints):
- for c in range(len(inverse_constraints)):
- start = 0
- while 'cipher_output' in inverse_constraints[c][start:]:
- new_start = inverse_constraints[c].index('cipher_output', start)
- inverse_constraints[c] = inverse_constraints[c][:new_start] + 'inverse_' + inverse_constraints[c][new_start:]
- start = new_start + 9
- start = 0
- while 'inverse_inverse_' in inverse_constraints[c][start:]:
- new_start = inverse_constraints[c].index('inverse_inverse_', start)
- inverse_constraints[c] = inverse_constraints[c][:new_start] + inverse_constraints[c][new_start + 8:]
- start = new_start
- for v in range(len(inverse_variables)):
- start = 0
- while 'inverse_inverse_' in inverse_variables[v][start:]:
- new_start = inverse_variables[v].index('inverse_inverse_', start)
- inverse_variables[v] = inverse_variables[v][:new_start] + inverse_variables[v][new_start + 8:]
- start = new_start
-
- return inverse_variables, inverse_constraints
-
- def constraints_for_key_schedule(self):
- key_components, key_ids = self.extract_key_schedule()
- return self.build_impossible_forward_model(key_components)
-
- def constraints_for_constants(self):
- constant_components, constant_ids = self.extract_constants()
- return self.build_impossible_forward_model(constant_components)
-
- def extract_constants(self):
- cipher = self._cipher
- constant_components_ids = []
- constant_components = []
- for component in cipher.get_all_components():
- if 'constant' in component.id:
- constant_components_ids.append(component.id)
- constant_components.append(component)
- elif '_' in component.id:
- component_inputs = component.input_id_links
- ks = True
- for comp_input in component_inputs:
- if 'constant' not in comp_input:
- ks = False
- if ks:
- constant_components_ids.append(component.id)
- constant_components.append(component)
-
- return constant_components, constant_components_ids
-
- def extract_key_schedule(self):
- cipher = self._cipher
- key_schedule_components_ids = ['key']
- key_schedule_components = []
- for component in cipher.get_all_components():
- component_inputs = component.input_id_links
- ks = True
- for comp_input in component_inputs:
- if 'constant' not in comp_input and comp_input not in key_schedule_components_ids:
- ks = False
- if ks:
- key_schedule_components_ids.append(component.id)
- key_schedule_components.append(component)
- master_key_bits = []
- for id_link, bit_positions in zip(component_inputs, component.input_bit_positions):
- if id_link == 'key':
- master_key_bits.extend(bit_positions)
- else:
- if id_link in self.key_schedule_bits_distribution:
- master_key_bits.extend(self.key_schedule_bits_distribution[id_link])
- self.key_schedule_bits_distribution[component.id] = list(set(master_key_bits))
-
- return key_schedule_components, key_schedule_components_ids
-
- def final_impossible_constraints_with_extensions(self, number_of_rounds, initial_round, middle_round, final_round, intermediate_components):
- """
- Constraints for output and incompatibility.
-
- INPUT:
-
- - ``number_of_rounds`` -- **integer** ; number of rounds
- - ``initial_round`` -- **integer** ; initial round of the impossible differential trail
- - ``middle_round`` -- **integer** ; incosistency round of the impossible differential trail
- - ``final_round`` -- **integer** ; final round of the impossible differential trail
- - ``intermediate_components`` -- **Boolean** ; check inconsistency on intermediate components of the inconsistency round or only on outputs
-
- EXAMPLES::
-
- sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_impossible_xor_differential_model import MznImpossibleXorDifferentialModel
- sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
- sage: from claasp.cipher_modules.models.utils import set_fixed_variables, integer_to_bit_list
- sage: speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=5)
- sage: cp = MznImpossibleXorDifferentialModel(speck)
- sage: cp.final_impossible_constraints_with_extensions(5, 2, 3, 4, False)
- ['solve satisfy;',
- ...
- 'output["plaintext = "++ show(plaintext) ++ "\\n" ++"key = "++ show(key) ++ "\\n" ++"inverse_plaintext = "++ show(inverse_plaintext) ++ "\\n" ++"inverse_intermediate_output_0_6 = "++ show(inverse_intermediate_output_0_6)++ "\\n" ++ "0" ++ "\\n" ++"intermediate_output_1_12 = "++ show(intermediate_output_1_12)++ "\\n" ++ "0" ++ "\\n" ++"intermediate_output_2_12 = "++ show(intermediate_output_2_12)++ "\\n" ++ "0" ++ "\\n" ++"inverse_intermediate_output_2_12 = "++ show(inverse_intermediate_output_2_12)++ "\\n" ++ "0" ++ "\\n" ++"inverse_intermediate_output_3_12 = "++ show(inverse_intermediate_output_3_12)++ "\\n" ++ "0" ++ "\\n" ++"cipher_output_4_12 = "++ show(cipher_output_4_12)++ "\\n" ++ "0" ++ "\\n" ++"intermediate_output_2_12 = "++ show(intermediate_output_2_12)++ "\\n" ++ "0" ++ "\\n" ++"inverse_intermediate_output_2_12 = "++ show(inverse_intermediate_output_2_12)++ "\\n" ++ "0" ++ "\\n" ];']
- """
- key_schedule_components, key_schedule_components_ids = self.extract_key_schedule()
- cipher_inputs = self._cipher.inputs
- cipher = self._cipher
- inverse_cipher = self.inverse_cipher
- cp_constraints = [solve_satisfy]
- new_constraint = 'output['
- incompatibility_constraint = 'constraint '
- for element in cipher_inputs:
- new_constraint = f'{new_constraint}\"{element} = \"++ show({element}) ++ \"\\n\" ++'
- for element in cipher_inputs:
- if element not in key_schedule_components_ids:
- new_constraint = f'{new_constraint}\"inverse_{element} = \"++ show(inverse_{element}) ++ \"\\n\" ++'
- for id_link in self._cipher.get_all_components_ids():
- if id_link not in key_schedule_components_ids and self.get_component_round(id_link) in list(range(initial_round - 1, middle_round)) + list(range(final_round, number_of_rounds)) and 'constant' not in id_link and 'output' in id_link:
- new_constraint = new_constraint + f'\"{id_link} = \"++ show({id_link})++ \"\\n\" ++ \"0\" ++ \"\\n\" ++'
- if id_link not in key_schedule_components_ids and self.get_component_round(id_link) in list(range(initial_round - 1)) + list(range(middle_round - 1, final_round)) and 'constant' not in id_link and 'output' in id_link:
- new_constraint = new_constraint + f'\"inverse_{id_link} = \"++ show(inverse_{id_link})++ \"\\n\" ++ \"0\" ++ \"\\n\" ++'
- if intermediate_components:
- for component in cipher.get_components_in_round(middle_round-1):
- if component.type != CONSTANT and component.id not in key_schedule_components_ids:
- component_id = component.id
- input_id_links = component.input_id_links
- input_bit_positions = component.input_bit_positions
- component_inputs = []
- input_bit_size = 0
- for id_link, bit_positions in zip(input_id_links, input_bit_positions):
- component_inputs.extend([f'{id_link}[{position}]' for position in bit_positions])
- input_bit_size += len(bit_positions)
- #new_constraint = new_constraint + \
- # f'\"{id_link} = \"++ show({id_link})++ \"\\n\" ++ \"0\" ++ \"\\n\" ++'
- #new_constraint = new_constraint + \
- # f'\"inverse_{component_id} = \"++ show(inverse_{component_id})++ \"\\n\" ++ \"0\" ++ \"\\n\" ++'
- for i in range(input_bit_size):
- incompatibility_constraint += f'({component_inputs[i]}+inverse_{component_id}[{i}]=1) \\/ '
- else:
- for component in cipher.get_components_in_round(middle_round-1):
- if 'output' in component.id and component.id not in key_schedule_components_ids:
- new_constraint = new_constraint + \
- f'\"{component.id} = \"++ show({component.id})++ \"\\n\" ++ \"0\" ++ \"\\n\" ++'
- new_constraint = new_constraint + \
- f'\"inverse_{component.id} = \"++ show(inverse_{component.id})++ \"\\n\" ++ \"0\" ++ \"\\n\" ++'
- for i in range(component.output_bit_size):
- incompatibility_constraint += f'({component.id}[{i}]+inverse_{component.id}[{i}]=1) \\/ '
- incompatibility_constraint = incompatibility_constraint[:-4] + ';'
- new_constraint = new_constraint[:-2] + '];'
- cp_constraints.append(incompatibility_constraint)
- cp_constraints.append(new_constraint)
- return cp_constraints
-
- def final_impossible_constraints(self, number_of_rounds, initial_round, middle_round, final_round, intermediate_components):
+ def find_one_impossible_xor_differential_trail(self, number_of_active_key_bits=1, number_of_active_pt_bits=1, number_of_active_ct_bits=1, solver_name=solvers.SOLVER_DEFAULT):
"""
- Constraints for output and incompatibility.
+ Returns one impossible XOR differential trail.
- INPUT:
+ INPUTS:
- - ``number_of_rounds`` -- **integer** ; number of rounds
- - ``initial_round`` -- **integer** ; initial round of the impossible differential trail
- - ``middle_round`` -- **integer** ; incosistency round of the impossible differential trail
- - ``final_round`` -- **integer** ; final round of the impossible differential trail
- - ``intermediate_components`` -- **Boolean** ; check inconsistency on intermediate components of the inconsistency round or only on outputs
+ - ``fixed_values`` -- *list of dict*, the variables to be fixed in
+ standard format (see :py:meth:`~GenericModel.set_fixed_variables`)
+ - ``solver_name`` -- *str*, the solver to call
- EXAMPLES::
+ EXAMPLE::
+ # to retrieve one of the trails of Table 2 from https://eprint.iacr.org/2016/689
+ sage: from claasp.ciphers.block_ciphers.lblock_block_cipher import LBlockBlockCipher
+ sage: lblock = LBlockBlockCipher(number_of_rounds=16)
sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_impossible_xor_differential_model import MznImpossibleXorDifferentialModel
- sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
- sage: from claasp.cipher_modules.models.utils import set_fixed_variables, integer_to_bit_list
- sage: speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=5)
- sage: cp = MznImpossibleXorDifferentialModel(speck)
- sage: cp.final_impossible_constraints(3, 2, 3, 4, False)
- ['solve satisfy;',
- ...
- 'output["key = "++ show(key) ++ "\\n" ++"intermediate_output_0_5 = "++ show(intermediate_output_0_5) ++ "\\n" ++"intermediate_output_0_6 = "++ show(intermediate_output_0_6) ++ "\\n" ++"inverse_key = "++ show(inverse_key) ++ "\\n" ++ "0" ++ "\\n" ++"inverse_intermediate_output_3_12 = "++ show(inverse_intermediate_output_3_12) ++ "\\n" ++ "0" ++ "\\n" ++"intermediate_output_0_6 = "++ show(intermediate_output_0_6)++ "\\n" ++ "0" ++ "\\n" ++"intermediate_output_1_12 = "++ show(intermediate_output_1_12)++ "\\n" ++ "0" ++ "\\n" ++"intermediate_output_2_12 = "++ show(intermediate_output_2_12)++ "\\n" ++ "0" ++ "\\n" ++"inverse_intermediate_output_2_12 = "++ show(inverse_intermediate_output_2_12)++ "\\n" ++ "0" ++ "\\n" ++"inverse_intermediate_output_3_12 = "++ show(inverse_intermediate_output_3_12)++ "\\n" ++ "0" ++ "\\n" ++"inverse_cipher_output_4_12 = "++ show(inverse_cipher_output_4_12)++ "\\n" ++ "0" ++ "\\n" ];']
- """
- if initial_round == 1:
- cipher_inputs = self._cipher.inputs
- else:
- cipher_inputs = ['key']
- for component in self._cipher.get_components_in_round(initial_round - 2):
- if 'output' in component.id:
- cipher_inputs.append(component.id)
- cipher = self._cipher
- inverse_cipher = self.inverse_cipher
- if final_round == self._cipher.number_of_rounds:
- cipher_outputs = inverse_cipher.inputs
- else:
- cipher_outputs = ['key']
- for component in self.inverse_cipher.get_components_in_round(self._cipher.number_of_rounds - final_round):
- if 'output' in component.id:
- cipher_outputs.append(component.id)
- cp_constraints = [solve_satisfy]
- new_constraint = 'output['
- incompatibility_constraint = 'constraint'
- key_schedule_components, key_schedule_components_ids = self.extract_key_schedule()
- for element in cipher_inputs:
- new_constraint = f'{new_constraint}\"{element} = \"++ show({element}) ++ \"\\n\" ++'
- for element in cipher_outputs:
- new_constraint = f'{new_constraint}\"inverse_{element} = \"++ show(inverse_{element}) ++ \"\\n\" ++ \"0\" ++ \"\\n\" ++'
- if intermediate_components:
- for component in cipher.get_components_in_round(middle_round-1):
- if component.type != CONSTANT and component.id not in key_schedule_components_ids:
- component_id = component.id
- input_id_links = component.input_id_links
- input_bit_positions = component.input_bit_positions
- component_inputs = []
- input_bit_size = 0
- for id_link, bit_positions in zip(input_id_links, input_bit_positions):
- component_inputs.extend([f'{id_link}[{position}]' for position in bit_positions])
- input_bit_size += len(bit_positions)
- new_constraint = new_constraint + \
- f'\"{id_link} = \"++ show({id_link})++ \"\\n\" ++ \"0\" ++ \"\\n\" ++'
- new_constraint = new_constraint + \
- f'\"inverse_{component_id} = \"++ show(inverse_{component_id})++ \"\\n\" ++ \"0\" ++ \"\\n\" ++'
- for i in range(input_bit_size):
- incompatibility_constraint += f'({component_inputs[i]}+inverse_{component_id}[{i}]=1) \\/ '
- else:
- for component in cipher.get_all_components():
- if 'output' in component.id and component.id not in key_schedule_components_ids:
- if self.get_component_round(component.id) <= middle_round - 1:
- new_constraint = new_constraint + \
- f'\"{component.id} = \"++ show({component.id})++ \"\\n\" ++ \"0\" ++ \"\\n\" ++'
- if self.get_component_round(component.id) >= middle_round - 1:
- new_constraint = new_constraint + \
- f'\"inverse_{component.id} = \"++ show(inverse_{component.id})++ \"\\n\" ++ \"0\" ++ \"\\n\" ++'
- if self.get_component_round(component.id) == middle_round - 1:
- for i in range(component.output_bit_size):
- incompatibility_constraint += f'({component.id}[{i}]+inverse_{component.id}[{i}]=1) \\/ '
- incompatibility_constraint = incompatibility_constraint[:-4] + ';'
- new_constraint = new_constraint[:-2] + '];'
- cp_constraints.append(incompatibility_constraint)
- cp_constraints.append(new_constraint)
-
- return cp_constraints
-
- def find_all_impossible_xor_differential_trails(self, number_of_rounds, fixed_values=[], solver_name=None, initial_round = 1, middle_round=2, final_round = None, intermediate_components = True, num_of_processors=None, timelimit=None, solve_with_API=False, solve_external = True):
- """
- Search for all impossible XOR differential trails of a cipher.
-
- INPUT:
-
- - ``number_of_rounds`` -- **integer** (default: `None`); number of rounds
- - ``fixed_values`` -- **list** (default: `[]`); dictionaries containing the variables to be fixed in standard
- format
- - ``initial_round`` -- **integer** (default: `1`); initial round of the impossible differential
- - ``middle_round`` -- **integer** (default: `1`); incosistency round of the impossible differential
- - ``final_round`` -- **integer** (default: `None`); final round of the impossible differential
- - ``intermediate_components`` -- **Boolean** (default: `True`); check inconsistency on intermediate components of the inconsistency round or only on outputs
- - ``num_of_processors`` -- **Integer** (default: `None`); number of processors used for MiniZinc search
- - ``timelimit`` -- **Integer** (default: `None`); time limit of MiniZinc search
-
- EXAMPLES::
-
- sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_impossible_xor_differential_model import MznImpossibleXorDifferentialModel
- sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
- sage: from claasp.cipher_modules.models.utils import set_fixed_variables, integer_to_bit_list
- sage: speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=4)
- sage: cp = MznImpossibleXorDifferentialModel(speck)
- sage: fixed_variables = [set_fixed_variables('key', 'equal', range(64), integer_to_bit_list(0, 64, 'little'))]
- sage: fixed_variables.append(set_fixed_variables('plaintext', 'not_equal', range(32), integer_to_bit_list(0, 32, 'little')))
- sage: fixed_variables.append(set_fixed_variables('inverse_cipher_output_3_12', 'not_equal', range(32), integer_to_bit_list(0, 32, 'little')))
- sage: trail = cp.find_all_impossible_xor_differential_trails(4, fixed_variables, 'Chuffed', 1, 3, 4, False) #doctest: +SKIP
-
- """
- self.build_impossible_xor_differential_trail_model(fixed_values, number_of_rounds, initial_round, middle_round, final_round, intermediate_components)
+ sage: mzn = MznImpossibleXorDifferentialModel(lblock)
+ sage: trail = mzn.find_one_impossible_xor_differential_trail(1,0,0) # doctest: +SKIP
+ ...
- if solve_with_API:
- return self.solve_for_ARX(solver_name = solver_name, timeout_in_seconds_ = timelimit, processes_ = num_of_processors, all_solutions_ = True)
- return self.solve(IMPOSSIBLE_XOR_DIFFERENTIAL, solver_name = solver_name, number_of_rounds = number_of_rounds, initial_round = initial_round, middle_round = middle_round, final_round = final_round, timeout_in_seconds_ = timelimit, processes_ = num_of_processors, all_solutions_ = True, solve_external = solve_external)
-
- def find_lowest_complexity_impossible_xor_differential_trail(self, number_of_rounds=None, fixed_values=[], solver_name=None, initial_round = 1, middle_round=2, final_round = None, intermediate_components = True, num_of_processors=None, timelimit=None, solve_with_API=False, solve_external = True):
"""
- Search for the impossible XOR differential trail of a cipher with the highest number of known bits in plaintext and ciphertext difference.
-
- INPUT:
- - ``number_of_rounds`` -- **integer** (default: `None`); number of rounds
- - ``fixed_values`` -- **list** (default: `[]`); dictionaries containing the variables to be fixed in standard
- format
- - ``initial_round`` -- **integer** (default: `1`); initial round of the impossible differential
- - ``middle_round`` -- **integer** (default: `1`); incosistency round of the impossible differential
- - ``final_round`` -- **integer** (default: `None`); final round of the impossible differential
- - ``intermediate_components`` -- **Boolean** (default: `True`); check inconsistency on intermediate components of the inconsistency round or only on outputs
- - ``num_of_processors`` -- **Integer** (default: `None`); number of processors used for MiniZinc search
- - ``timelimit`` -- **Integer** (default: `None`); time limit of MiniZinc search
-
- EXAMPLES::
-
- sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_impossible_xor_differential_model import MznImpossibleXorDifferentialModel
- sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
- sage: from claasp.cipher_modules.models.utils import set_fixed_variables, integer_to_bit_list
- sage: speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=4)
- sage: cp = MznImpossibleXorDifferentialModel(speck)
- sage: fixed_variables = [set_fixed_variables('key', 'equal', range(64), integer_to_bit_list(0, 64, 'little'))]
- sage: fixed_variables.append(set_fixed_variables('plaintext', 'not_equal', range(32), integer_to_bit_list(0, 32, 'little')))
- sage: fixed_variables.append(set_fixed_variables('inverse_cipher_output_3_12', 'not_equal', range(32), integer_to_bit_list(0, 32, 'little')))
- sage: trail = cp.find_lowest_complexity_impossible_xor_differential_trail(4, fixed_variables, 'Chuffed', 1, 3, 4, intermediate_components = False)
- """
- self.build_impossible_xor_differential_trail_model(fixed_values, number_of_rounds, initial_round, middle_round, final_round, intermediate_components)
- self._model_constraints.remove(f'solve satisfy;')
- self._model_constraints.append(f'solve minimize count(plaintext, 2) + count(inverse_{self._cipher.get_all_components_ids()[-1]}, 2);')
+ return enumerate_impossible_xor_differential_trails(self, number_of_active_key_bits, number_of_active_pt_bits,
+ number_of_active_ct_bits, solver_name,
+ output_only_one_solution=True)
- if solve_with_API:
- return self.solve_for_ARX(solver_name = solver_name, timeout_in_seconds_ = timelimit, processes_ = num_of_processors)
- return self.solve('impossible_xor_differential_one_solution', solver_name = solver_name, number_of_rounds = number_of_rounds, initial_round = initial_round, middle_round = middle_round, final_round = final_round, timeout_in_seconds_ = timelimit, processes_ = num_of_processors, solve_external = solve_external)
-
- def find_one_impossible_xor_differential_trail_with_extensions(self, number_of_rounds=None, fixed_values=[], solver_name=None, initial_round = 1, middle_round=2, final_round = None, intermediate_components = True, num_of_processors=None, timelimit=None, solve_with_API=False, solve_external = True):
+ def find_all_impossible_xor_differential_trails(self, number_of_active_key_bits=1, number_of_active_pt_bits=1, number_of_active_ct_bits=1, solver_name=solvers.SOLVER_DEFAULT):
"""
- Search for one impossible XOR differential trail of a cipher with forward and backward deterministic extensions for key recovery.
+ Returns all impossible XOR differential trails.
- INPUT:
+ INPUTS:
- - ``number_of_rounds`` -- **integer** (default: `None`); number of rounds
- - ``fixed_values`` -- **list** (default: `[]`); dictionaries containing the variables to be fixed in standard
- format
- - ``initial_round`` -- **integer** (default: `1`); initial round of the impossible differential
- - ``middle_round`` -- **integer** (default: `1`); incosistency round of the impossible differential
- - ``final_round`` -- **integer** (default: `None`); final round of the impossible differential
- - ``intermediate_components`` -- **Boolean** (default: `True`); check inconsistency on intermediate components of the inconsistency round or only on outputs
- - ``num_of_processors`` -- **Integer** (default: `None`); number of processors used for MiniZinc search
- - ``timelimit`` -- **Integer** (default: `None`); time limit of MiniZinc search
+ - ``fixed_values`` -- *list of dict*, the variables to be fixed in
+ standard format (see :py:meth:`~GenericModel.set_fixed_variables`)
+ - ``solver_name`` -- *str*, the solver to call
- EXAMPLES::
+ EXAMPLE::
+ # to retrieve the trails of Table 2 from https://eprint.iacr.org/2016/689
+ sage: from claasp.ciphers.block_ciphers.lblock_block_cipher import LBlockBlockCipher
+ sage: lblock = LBlockBlockCipher(number_of_rounds=16)
sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_impossible_xor_differential_model import MznImpossibleXorDifferentialModel
- sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
- sage: from claasp.cipher_modules.models.utils import set_fixed_variables, integer_to_bit_list
- sage: speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=7)
- sage: cp = MznImpossibleXorDifferentialModel(speck)
- sage: fixed_variables = [set_fixed_variables('key', 'equal', range(64), integer_to_bit_list(0, 64, 'little'))]
- sage: fixed_variables.append(set_fixed_variables('plaintext', 'not_equal', range(32), integer_to_bit_list(0, 32, 'little')))
- sage: fixed_variables.append(set_fixed_variables('cipher_output_6_12', 'not_equal', range(32), integer_to_bit_list(0, 32, 'little')))
- sage: trail = cp.find_one_impossible_xor_differential_trail_with_extensions(7, fixed_variables, 'Chuffed', 2, 4, 6, intermediate_components = False)
- """
- self.build_impossible_xor_differential_trail_with_extensions_model(fixed_values, number_of_rounds, initial_round, middle_round, final_round, intermediate_components)
-
- if solve_with_API:
- return self.solve_for_ARX(solver_name = solver_name, timeout_in_seconds_ = timelimit, processes_ = num_of_processors)
- return self.solve('impossible_xor_differential_one_solution', solver_name = solver_name, number_of_rounds = number_of_rounds, initial_round = initial_round, middle_round = middle_round, final_round = final_round, timeout_in_seconds_ = timelimit, processes_ = num_of_processors, solve_external = solve_external)
-
- def find_one_impossible_xor_differential_trail(self, number_of_rounds=None, fixed_values=[], solver_name=None, initial_round = 1, middle_round=2, final_round = None, intermediate_components = True, num_of_processors=None, timelimit=None, solve_with_API=False, solve_external = True):
- """
- Search for one impossible XOR differential trail of a cipher.
+ sage: mzn = MznImpossibleXorDifferentialModel(lblock)
+ sage: trails = mzn.find_all_impossible_xor_differential_trails(1,0,0) # doctest: +SKIP
+ ...
- INPUT:
- - ``number_of_rounds`` -- **integer** (default: `None`); number of rounds
- - ``fixed_values`` -- **list** (default: `[]`); dictionaries containing the variables to be fixed in standard
- format
- - ``initial_round`` -- **integer** (default: `1`); initial round of the impossible differential
- - ``middle_round`` -- **integer** (default: `1`); incosistency round of the impossible differential
- - ``final_round`` -- **integer** (default: `None`); final round of the impossible differential
- - ``intermediate_components`` -- **Boolean** (default: `True`); check inconsistency on intermediate components of the inconsistency round or only on outputs
- - ``num_of_processors`` -- **Integer** (default: `None`); number of processors used for MiniZinc search
- - ``timelimit`` -- **Integer** (default: `None`); time limit of MiniZinc search
-
- EXAMPLES::
-
- sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_impossible_xor_differential_model import MznImpossibleXorDifferentialModel
- sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
- sage: from claasp.cipher_modules.models.utils import set_fixed_variables, integer_to_bit_list
- sage: speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=4)
- sage: cp = MznImpossibleXorDifferentialModel(speck)
- sage: fixed_variables = [set_fixed_variables('key', 'equal', range(64), integer_to_bit_list(0, 64, 'little'))]
- sage: fixed_variables.append(set_fixed_variables('plaintext', 'not_equal', range(32), integer_to_bit_list(0, 32, 'little')))
- sage: fixed_variables.append(set_fixed_variables('inverse_cipher_output_3_12', 'not_equal', range(32), integer_to_bit_list(0, 32, 'little')))
- sage: trail = cp.find_one_impossible_xor_differential_trail(4, fixed_variables, 'Chuffed', 1, 3, 4, intermediate_components = False)
"""
- self.build_impossible_xor_differential_trail_model(fixed_values, number_of_rounds, initial_round, middle_round, final_round, intermediate_components)
-
- if solve_with_API:
- return self.solve_for_ARX(solver_name = solver_name, timeout_in_seconds_ = timelimit, processes_ = num_of_processors)
- return self.solve('impossible_xor_differential_one_solution', solver_name = solver_name, number_of_rounds = number_of_rounds, initial_round = initial_round, middle_round = middle_round, final_round = final_round, timeout_in_seconds_ = timelimit, processes_ = num_of_processors, solve_external = solve_external)
-
- def get_component_from_id(self, id_link, curr_cipher):
- for component in curr_cipher.get_all_components():
- if component.id == id_link:
- return component
- return None
-
- def get_component_round(self, id_link):
- if '_' in id_link:
- last_us = - id_link[::-1].index('_') - 1
- start = - id_link[last_us - 1::-1].index('_') + last_us
-
- return int(id_link[start:len(id_link) + last_us])
- else:
- return 0
-
- def get_direct_component_correspondance(self, forward_component):
- for inverse_component in self.inverse_cipher.get_all_components():
- if inverse_component.get_inverse_component_correspondance(inverse_component) == forward_component:
- return inverse_component
-
- def get_inverse_component_correspondance(self, backward_component):
-
- for component in self._cipher.get_all_components():
- if backward_component.id == component.id:
- direct_inputs = component.input_id_links
- inverse_outputs = []
- for component in self.inverse_cipher.get_all_components():
- if backward_component.id in component.input_id_links:
- inverse_outputs.append(component.id)
- correspondance = [dir_i for dir_i in direct_inputs if dir_i in inverse_outputs]
- if len(correspondance) > 1:
- return 'Not invertible'
- else:
- return correspondance[0]
-
- def get_inverse_state_key_bits_positions(self):
- key_bits = self.key_schedule_bits_distribution
- for component in self.inverse_cipher.get_all_components():
- if component.id not in key_bits:
- component_key_bits = []
- for id_link in component.input_id_links:
- if id_link in key_bits:
- component_key_bits.extend(key_bits[id_link])
- key_bits[component.id] = list(set(component_key_bits))
-
- return key_bits
-
- def get_state_key_bits_positions(self):
- key_bits = self.key_schedule_bits_distribution
- for component in self._cipher.get_all_components():
- if component.id not in key_bits:
- component_key_bits = []
- for id_link in component.input_id_links:
- if id_link in key_bits:
- component_key_bits.extend(key_bits[id_link])
- key_bits[component.id] = list(set(component_key_bits))
-
- return key_bits
-
- def input_impossible_constraints_with_extensions(self, number_of_rounds=None, initial_round=None, middle_round=None, final_round=None):
-
- if number_of_rounds is None:
- number_of_rounds = self._cipher.number_of_rounds
-
- cp_constraints = []
- cp_declarations = [f'array[0..{bit_size - 1}] of var 0..2: {input_};'
- for input_, bit_size in zip(self._cipher.inputs, self._cipher.inputs_bit_size)]
- cipher = self._cipher
- inverse_cipher = self.inverse_cipher
-
- key_components, key_ids = self.extract_key_schedule()
- constant_components, constant_ids = self.extract_constants()
-
- forward_components = []
- for component in self._cipher.get_all_components():
- comp_r = self.get_component_round(component.id)
- if comp_r >= initial_round - 1 and comp_r <= middle_round - 1 or comp_r > final_round - 1:
- forward_components.append(component)
- components_to_direct = []
- for component in forward_components:
- for id_link in component.input_id_links:
- input_component = self.get_component_from_id(id_link, cipher)
- if input_component not in key_ids + constant_ids + forward_components + components_to_direct and input_component != None:
- components_to_direct.append(input_component)
- forward_components.extend(components_to_direct)
- forward_components.extend(key_components)
- forward_components.extend(constant_components)
-
- backward_components = []
- for component in inverse_cipher.get_all_components():
- comp_r = self.get_component_round(component.id)
- if comp_r < initial_round - 1 or comp_r >= middle_round - 1 and comp_r <= final_round - 1:
- backward_components.append(component)
- components_to_invert = []
- for component in backward_components:
- for id_link in component.input_id_links:
- input_component = self.get_component_from_id(id_link, inverse_cipher)
- if input_component not in key_ids + constant_ids + backward_components + components_to_invert and input_component != None:
- components_to_invert.append(input_component)
- backward_components.extend(components_to_invert)
-
- for component in forward_components:
- output_id_link = component.id
- output_size = int(component.output_bit_size)
- if 'output' in component.type:
- cp_declarations.append(f'array[0..{output_size - 1}] of var 0..2: {output_id_link};')
- cp_constraints.append(f'constraint count({output_id_link},2) < {output_size};')
- elif CONSTANT not in component.type:
- cp_declarations.append(f'array[0..{output_size - 1}] of var 0..2: {output_id_link};')
-
- for component in backward_components:
- output_id_link = component.id
- output_size = int(component.output_bit_size)
- if 'output' in component.type:
- cp_declarations.append(f'array[0..{output_size - 1}] of var 0..2: inverse_{output_id_link};')
- cp_constraints.append(f'constraint count(inverse_{output_id_link},2) < {output_size};')
- if self.get_component_round(component.id) == final_round - 1 or self.get_component_round(component.id) == initial_round - 2:
- cp_constraints.append(f'constraint count(inverse_{output_id_link},1) > 0;')
- elif CONSTANT not in component.type:
- cp_declarations.append(f'array[0..{output_size - 1}] of var 0..2: inverse_{output_id_link};')
-
- cp_constraints.append(f'constraint count(plaintext,2) < {self._cipher.output_bit_size};')
-
- for component in self._cipher.get_all_components():
- if CIPHER_OUTPUT in component.type:
- cp_constraints.append(f'constraint count({component.id},2) < {self._cipher.output_bit_size};')
-
- return cp_declarations, cp_constraints
-
- def input_impossible_constraints(self, number_of_rounds=None, middle_round=None):
-
- if number_of_rounds is None:
- number_of_rounds = self._cipher.number_of_rounds
-
- cp_constraints = []
- cp_declarations = [f'array[0..{bit_size - 1}] of var 0..2: {input_};'
- for input_, bit_size in zip(self._cipher.inputs, self._cipher.inputs_bit_size)]
- cipher = self._cipher
- inverse_cipher = self.inverse_cipher
- forward_components = []
- for r in range(middle_round):
- forward_components.extend(self._cipher.get_components_in_round(r))
- backward_components = []
- for r in range(number_of_rounds - middle_round + 1):
- backward_components.extend(inverse_cipher.get_components_in_round(r))
- cp_declarations.extend([f'array[0..{bit_size - 1}] of var 0..2: inverse_{input_};' for input_, bit_size in zip(inverse_cipher.inputs, inverse_cipher.inputs_bit_size)])
- for component in forward_components:
- output_id_link = component.id
- output_size = int(component.output_bit_size)
- if 'output' in component.type:
- cp_declarations.append(f'array[0..{output_size - 1}] of var 0..2: {output_id_link};')
- elif CIPHER_OUTPUT in component.type:
- cp_declarations.append(f'array[0..{output_size - 1}] of var 0..2: {output_id_link};')
- cp_constraints.append(f'constraint count({output_id_link},2) < {output_size};')
- elif CONSTANT not in component.type:
- cp_declarations.append(f'array[0..{output_size - 1}] of var 0..2: {output_id_link};')
- for component in backward_components:
- output_id_link = component.id
- output_size = int(component.output_bit_size)
- if 'output' in component.type:
- cp_declarations.append(f'array[0..{output_size - 1}] of var 0..2: inverse_{output_id_link};')
- elif CIPHER_OUTPUT in component.type:
- cp_declarations.append(f'array[0..{output_size - 1}] of var 0..2: inverse_{output_id_link};')
- cp_constraints.append(f'constraint count(inverse_{output_id_link},2) < {output_size};')
- cp_constraints.append(f'constraint count(inverse_{output_id_link},1) > 0;')
- elif CONSTANT not in component.type:
- cp_declarations.append(f'array[0..{output_size - 1}] of var 0..2: inverse_{output_id_link};')
- cp_constraints.append('constraint count(plaintext,1) > 0;')
-
- return cp_declarations, cp_constraints
-
- def is_cross_round_component(self, component, discarded_ids):
- component_round = self.get_component_round(component.id)
- for input_id in component.input_id_links:
- if input_id not in discarded_ids and self.get_component_round(input_id) != component_round:
- return True
- return False
-
- def link_constraints_for_trail_with_extensions(self, components_to_link):
- linking_constraints = []
- for pairs in components_to_link:
- linking_constraints.append(f'constraint {pairs[0]} = inverse_{pairs[1]};')
-
- return linking_constraints
-
- def _parse_solver_output(self, output_to_parse, number_of_rounds, initial_round, middle_round, final_round):
- components_values, memory, time = self.parse_solver_information(output_to_parse, True, True)
- all_components = [*self._cipher.inputs]
- for r in list(range(initial_round - 1, middle_round)) + list(range(final_round, number_of_rounds)):
- all_components.extend([component.id for component in [*self._cipher.get_components_in_round(r)]])
- for r in list(range(initial_round - 1)) + list(range(middle_round - 1, final_round)):
- all_components.extend(['inverse_' + component.id for component in [*self.inverse_cipher.get_components_in_round(number_of_rounds - r - 1)]])
- all_components.extend(['inverse_' + id_link for id_link in [*self.inverse_cipher.inputs]])
- all_components.extend(['inverse_' + id_link for id_link in [*self._cipher.inputs]])
- for component_id in all_components:
- solution_number = 1
- for j, string in enumerate(output_to_parse):
- if f'{component_id}' in string and 'inverse_' not in component_id + string:
- value = self.format_component_value(component_id, string)
- component_solution = {}
- component_solution['value'] = value
- self.add_solution_to_components_values(component_id, component_solution, components_values, j,
- output_to_parse, solution_number, string)
- elif f'{component_id}' in string and 'inverse_' in component_id:
- value = self.format_component_value(component_id, string)
- component_solution = {}
- component_solution['value'] = value
- self.add_solution_to_components_values(component_id, component_solution, components_values, j,
- output_to_parse, solution_number, string)
- elif '----------' in string:
- solution_number += 1
-
- return time, memory, components_values
-
- def set_inverse_component_id_in_constraints(self, component, inverse_variables, inverse_constraints):
- for v in range(len(inverse_variables)):
- start = 0
- while component.id in inverse_variables[v][start:]:
- new_start = inverse_variables[v].index(component.id, start)
- inverse_variables[v] = inverse_variables[v][:new_start] + 'inverse_' + inverse_variables[v][new_start:]
- start = new_start + 9
- for c in range(len(inverse_constraints)):
- start = 0
- while component.id in inverse_constraints[c][start:]:
- new_start = inverse_constraints[c].index(component.id, start)
- inverse_constraints[c] = inverse_constraints[c][:new_start] + 'inverse_' + inverse_constraints[c][new_start:]
- start = new_start + 9
-
- return inverse_variables, inverse_constraints
- def solve(self, model_type, solver_name=None, number_of_rounds=None, initial_round=None, middle_round=None, final_round=None, processes_=None, timeout_in_seconds_=None, all_solutions_=False, solve_external = False):
- cipher_name = self.cipher_id
- input_file_path = f'{cipher_name}_Mzn_{model_type}_{solver_name}.mzn'
- command = self.get_command_for_solver_process(input_file_path, model_type, solver_name, processes_, timeout_in_seconds_)
- solver_process = subprocess.run(command, stdout=subprocess.PIPE, stderr=subprocess.PIPE, encoding="utf-8")
- os.remove(input_file_path)
- if solver_process.returncode >= 0:
- solutions = []
- solver_output = solver_process.stdout.splitlines()
- if model_type in ['deterministic_truncated_xor_differential',
- 'deterministic_truncated_xor_differential_one_solution',
- 'impossible_xor_differential',
- 'impossible_xor_differential_one_solution',
- 'impossible_xor_differential_attack']:
- solve_time, memory, components_values = self._parse_solver_output(solver_output, number_of_rounds, initial_round, middle_round, final_round)
- total_weight = 0
- else:
- solve_time, memory, components_values, total_weight = self._parse_solver_output(solver_output, number_of_rounds, initial_round, middle_round, final_round)
- if components_values == {}:
- solution = convert_solver_solution_to_dictionary(self.cipher_id, model_type, solver_name,
- solve_time, memory,
- components_values, total_weight)
- if 'UNSATISFIABLE' in solver_output[0]:
- solution['status'] = 'UNSATISFIABLE'
- else:
- solution['status'] = 'SATISFIABLE'
- solutions.append(solution)
- else:
- self.add_solutions_from_components_values(components_values, memory, model_type, solutions, solve_time,
- solver_name, solver_output, 0, solve_external)
- if model_type in ['xor_differential_one_solution',
- 'xor_linear_one_solution',
- 'deterministic_truncated_one_solution',
- 'impossible_xor_differential_one_solution']:
- return solutions[0]
- else:
- return solutions
\ No newline at end of file
+ return enumerate_impossible_xor_differential_trails(self, number_of_active_key_bits, number_of_active_pt_bits,
+ number_of_active_ct_bits, solver_name)
\ No newline at end of file
diff --git a/claasp/cipher_modules/models/cp/mzn_models/mzn_wordwise_deterministic_truncated_xor_differential_model.py b/claasp/cipher_modules/models/cp/mzn_models/mzn_wordwise_deterministic_truncated_xor_differential_model.py
index b6824079..34f4d7da 100644
--- a/claasp/cipher_modules/models/cp/mzn_models/mzn_wordwise_deterministic_truncated_xor_differential_model.py
+++ b/claasp/cipher_modules/models/cp/mzn_models/mzn_wordwise_deterministic_truncated_xor_differential_model.py
@@ -22,14 +22,14 @@
import itertools
import subprocess
-from claasp.cipher_modules.models.cp.mzn_models.mzn_deterministic_truncated_xor_differential_model import MznDeterministicTruncatedXorDifferentialModel, solve_satisfy
+from claasp.cipher_modules.models.cp.mzn_models.mzn_bitwise_deterministic_truncated_xor_differential_model import MznBitwiseDeterministicTruncatedXorDifferentialModel, solve_satisfy
from claasp.cipher_modules.models.utils import write_model_to_file, convert_solver_solution_to_dictionary
from claasp.name_mappings import (CONSTANT, INTERMEDIATE_OUTPUT, CIPHER_OUTPUT, LINEAR_LAYER, SBOX, MIX_COLUMN,
WORD_OPERATION, DETERMINISTIC_TRUNCATED_XOR_DIFFERENTIAL)
from claasp.cipher_modules.models.cp.solvers import MODEL_DEFAULT_PATH, SOLVER_DEFAULT
-class MznWordwiseDeterministicTruncatedXorDifferentialModel(MznDeterministicTruncatedXorDifferentialModel):
+class MznWordwiseDeterministicTruncatedXorDifferentialModel(MznBitwiseDeterministicTruncatedXorDifferentialModel):
def __init__(self, cipher):
super().__init__(cipher)
diff --git a/claasp/cipher_modules/models/milp/milp_model.py b/claasp/cipher_modules/models/milp/milp_model.py
index 5b2b9726..fba5fbcf 100644
--- a/claasp/cipher_modules/models/milp/milp_model.py
+++ b/claasp/cipher_modules/models/milp/milp_model.py
@@ -352,7 +352,7 @@ def solve(self, model_type, solver_name=SOLVER_DEFAULT, external_solver_name=Non
os.remove(f"{solution_file_path}")
else:
objective_value = None
- components_values = None
+ components_values = {}
solver_name_in_solution = solver_name
status, milp_time, milp_memory = self._solve_with_internal_solver()
if status == 'SATISFIABLE':
diff --git a/claasp/cipher_modules/models/milp/milp_models/milp_impossible_xor_differential_model.py b/claasp/cipher_modules/models/milp/milp_models/milp_impossible_xor_differential_model.py
new file mode 100644
index 00000000..04c08a98
--- /dev/null
+++ b/claasp/cipher_modules/models/milp/milp_models/milp_impossible_xor_differential_model.py
@@ -0,0 +1,88 @@
+
+# ****************************************************************************
+# Copyright 2023 Technology Innovation Institute
+#
+# This program is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# This program is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program. If not, see .
+# ****************************************************************************
+
+"""
+The search methods presented in this class differ from those of the classes
+:py:class:`Milp Bitwise Impossible Xor Differential Model
+`
+
+and :py:class:`Milp Wordwise Impossible Xor Differential Model
+`.
+
+Indeed, this class implements the framework proposed by `Cui et al.` which uses
+infeasibility of a XOR DIFFERENTIAL model to detect an impossible differential trail.
+"""
+
+from claasp.cipher_modules.models.milp import solvers
+from claasp.cipher_modules.models.milp.milp_models.milp_xor_differential_model import MilpXorDifferentialModel
+from claasp.cipher_modules.models.utils import enumerate_impossible_xor_differential_trails
+
+class MilpImpossibleXorDifferentialModel(MilpXorDifferentialModel):
+ def __init__(self, cipher, n_window_heuristic=None, verbose=False):
+ super().__init__(cipher, n_window_heuristic, verbose)
+
+ def find_one_impossible_xor_differential_trail(self, number_of_active_key_bits=1, number_of_active_pt_bits=1, number_of_active_ct_bits=1, solver_name=solvers.SOLVER_DEFAULT):
+ """
+ Returns one impossible XOR differential trail.
+
+ INPUTS:
+
+ - ``fixed_values`` -- *list of dict*, the variables to be fixed in
+ standard format (see :py:meth:`~GenericModel.set_fixed_variables`)
+ - ``solver_name`` -- *str*, the solver to call
+
+ EXAMPLE::
+
+ # to retrieve one of the trails of Table 2 from https://eprint.iacr.org/2016/689
+ sage: from claasp.ciphers.block_ciphers.lblock_block_cipher import LBlockBlockCipher
+ sage: lblock = LBlockBlockCipher(number_of_rounds=16)
+ sage: from claasp.cipher_modules.models.milp.milp_models.milp_impossible_xor_differential_model import MilpImpossibleXorDifferentialModel
+ sage: milp = MilpImpossibleXorDifferentialModel(lblock)
+ sage: trail = milp.find_one_impossible_xor_differential_trail(1,0,0) # doctest: +SKIP
+ ...
+
+ """
+
+ return enumerate_impossible_xor_differential_trails(self, number_of_active_key_bits, number_of_active_pt_bits,
+ number_of_active_ct_bits, solver_name,
+ output_only_one_solution=True)
+
+ def find_all_impossible_xor_differential_trails(self, number_of_active_key_bits=1, number_of_active_pt_bits=1, number_of_active_ct_bits=1, solver_name=solvers.SOLVER_DEFAULT):
+ """
+ Returns all impossible XOR differential trails.
+
+ INPUTS:
+
+ - ``fixed_values`` -- *list of dict*, the variables to be fixed in
+ standard format (see :py:meth:`~GenericModel.set_fixed_variables`)
+ - ``solver_name`` -- *str*, the solver to call
+
+ EXAMPLE::
+
+ # to retrieve the trails of Table 2 from https://eprint.iacr.org/2016/689
+ sage: from claasp.ciphers.block_ciphers.lblock_block_cipher import LBlockBlockCipher
+ sage: lblock = LBlockBlockCipher(number_of_rounds=16)
+ sage: from claasp.cipher_modules.models.milp.milp_models.milp_impossible_xor_differential_model import MilpImpossibleXorDifferentialModel
+ sage: milp = MilpImpossibleXorDifferentialModel(lblock)
+ sage: trails = milp.find_all_impossible_xor_differential_trails(1,0,0) # doctest: +SKIP
+ ...
+
+ """
+
+ return enumerate_impossible_xor_differential_trails(self, number_of_active_key_bits, number_of_active_pt_bits,
+ number_of_active_ct_bits, solver_name)
\ No newline at end of file
diff --git a/claasp/cipher_modules/models/sat/cms_models/cms_impossible_xor_differential_model.py b/claasp/cipher_modules/models/sat/cms_models/cms_impossible_xor_differential_model.py
new file mode 100644
index 00000000..4e21e428
--- /dev/null
+++ b/claasp/cipher_modules/models/sat/cms_models/cms_impossible_xor_differential_model.py
@@ -0,0 +1,88 @@
+
+# ****************************************************************************
+# Copyright 2023 Technology Innovation Institute
+#
+# This program is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# This program is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program. If not, see .
+# ****************************************************************************
+
+"""
+The search methods presented in this class differ from those of the classes
+:py:class:`Cms Bitwise Impossible Xor Differential Model
+`
+
+and :py:class:`Cms Wordwise Impossible Xor Differential Model
+`.
+
+Indeed, this class implements the framework proposed by `Cui et al.` which uses
+infeasibility of a XOR DIFFERENTIAL model to detect an impossible differential trail.
+"""
+
+from claasp.cipher_modules.models.sat import solvers
+from claasp.cipher_modules.models.sat.cms_models.cms_xor_differential_model import CmsSatXorDifferentialModel
+from claasp.cipher_modules.models.utils import enumerate_impossible_xor_differential_trails
+
+class CmsSatImpossibleXorDifferentialModel(CmsSatXorDifferentialModel):
+ def __init__(self, cipher, counter='sequential', compact=False):
+ super().__init__(cipher, counter, compact)
+
+ def find_one_impossible_xor_differential_trail(self, number_of_active_key_bits=1, number_of_active_pt_bits=1, number_of_active_ct_bits=1, solver_name=solvers.SOLVER_DEFAULT):
+ """
+ Returns one impossible XOR differential trail.
+
+ INPUTS:
+
+ - ``fixed_values`` -- *list of dict*, the variables to be fixed in
+ standard format (see :py:meth:`~GenericModel.set_fixed_variables`)
+ - ``solver_name`` -- *str*, the solver to call
+
+ EXAMPLE::
+
+ # to retrieve one of the trails of Table 2 from https://eprint.iacr.org/2016/689
+ sage: from claasp.ciphers.block_ciphers.lblock_block_cipher import LBlockBlockCipher
+ sage: lblock = LBlockBlockCipher(number_of_rounds=16)
+ sage: from claasp.cipher_modules.models.sat.cms_models.cms_impossible_xor_differential_model import CmsSatImpossibleXorDifferentialModel
+ sage: cms = CmsSatImpossibleXorDifferentialModel(lblock)
+ sage: trail = cms.find_one_impossible_xor_differential_trail(1,0,0) # doctest: +SKIP
+ ...
+
+ """
+
+ return enumerate_impossible_xor_differential_trails(self, number_of_active_key_bits, number_of_active_pt_bits,
+ number_of_active_ct_bits, solver_name,
+ output_only_one_solution=True)
+
+ def find_all_impossible_xor_differential_trails(self, number_of_active_key_bits=1, number_of_active_pt_bits=1, number_of_active_ct_bits=1, solver_name=solvers.SOLVER_DEFAULT):
+ """
+ Returns all impossible XOR differential trails.
+
+ INPUTS:
+
+ - ``fixed_values`` -- *list of dict*, the variables to be fixed in
+ standard format (see :py:meth:`~GenericModel.set_fixed_variables`)
+ - ``solver_name`` -- *str*, the solver to call
+
+ EXAMPLE::
+
+ # to retrieve the trails of Table 2 from https://eprint.iacr.org/2016/689
+ sage: from claasp.ciphers.block_ciphers.lblock_block_cipher import LBlockBlockCipher
+ sage: lblock = LBlockBlockCipher(number_of_rounds=16)
+ sage: from claasp.cipher_modules.models.sat.cms_models.cms_impossible_xor_differential_model import CmsSatImpossibleXorDifferentialModel
+ sage: cms = CmsSatImpossibleXorDifferentialModel(lblock)
+ sage: trails = cms.find_all_impossible_xor_differential_trails(1,0,0) # doctest: +SKIP
+ ...
+
+ """
+
+ return enumerate_impossible_xor_differential_trails(self, number_of_active_key_bits, number_of_active_pt_bits,
+ number_of_active_ct_bits, solver_name)
\ No newline at end of file
diff --git a/claasp/cipher_modules/models/sat/cms_models/cms_xor_differential_model.py b/claasp/cipher_modules/models/sat/cms_models/cms_xor_differential_model.py
index 43fd9239..195a1eff 100644
--- a/claasp/cipher_modules/models/sat/cms_models/cms_xor_differential_model.py
+++ b/claasp/cipher_modules/models/sat/cms_models/cms_xor_differential_model.py
@@ -96,9 +96,9 @@ def build_xor_differential_trail_model(self, weight=-1, fixed_variables=[]):
operation = component.description[0]
if component.type not in component_types or (
WORD_OPERATION == component.type and operation not in operation_types):
- variables, constraints = component.cms_xor_differential_propagation_constraints(self)
- else:
print(f'{component.id} not yet implemented')
+ else:
+ variables, constraints = component.cms_xor_differential_propagation_constraints(self)
self._variables_list.extend(variables)
self._model_constraints.extend(constraints)
diff --git a/claasp/cipher_modules/models/sat/sat_models/sat_impossible_xor_differential_model.py b/claasp/cipher_modules/models/sat/sat_models/sat_impossible_xor_differential_model.py
new file mode 100644
index 00000000..ec9e9cc4
--- /dev/null
+++ b/claasp/cipher_modules/models/sat/sat_models/sat_impossible_xor_differential_model.py
@@ -0,0 +1,90 @@
+
+# ****************************************************************************
+# Copyright 2023 Technology Innovation Institute
+#
+# This program is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# This program is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program. If not, see .
+# ****************************************************************************
+
+"""
+The search methods presented in this class differ from those of the classes
+:py:class:`Sat Bitwise Impossible Xor Differential Model
+`
+
+and :py:class:`Sat Wordwise Impossible Xor Differential Model
+`.
+
+Indeed, this class implements the framework proposed by `Cui et al.` which uses
+infeasibility of a XOR DIFFERENTIAL model to detect an impossible differential trail.
+"""
+
+from claasp.cipher_modules.models.sat import solvers
+from claasp.cipher_modules.models.sat.sat_models.sat_xor_differential_model import SatXorDifferentialModel
+from claasp.cipher_modules.models.utils import enumerate_impossible_xor_differential_trails
+
+
+class SatImpossibleXorDifferentialModel(SatXorDifferentialModel):
+ def __init__(self, cipher, counter='sequential', compact=False):
+ super().__init__(cipher, counter, compact)
+
+ def find_one_impossible_xor_differential_trail(self, number_of_active_key_bits=1, number_of_active_pt_bits=1, number_of_active_ct_bits=1, solver_name=solvers.SOLVER_DEFAULT):
+ """
+ Returns one impossible XOR differential trail.
+
+ INPUTS:
+
+ - ``fixed_values`` -- *list of dict*, the variables to be fixed in
+ standard format (see :py:meth:`~GenericModel.set_fixed_variables`)
+ - ``solver_name`` -- *str*, the solver to call
+
+ EXAMPLE::
+
+ # to retrieve one of the trails of Table 2 from https://eprint.iacr.org/2016/689
+ sage: from claasp.ciphers.block_ciphers.lblock_block_cipher import LBlockBlockCipher
+ sage: lblock = LBlockBlockCipher(number_of_rounds=16)
+ sage: from claasp.cipher_modules.models.sat.sat_models.sat_impossible_xor_differential_model import SatImpossibleXorDifferentialModel
+ sage: sat = SatImpossibleXorDifferentialModel(lblock)
+ sage: trail = sat.find_one_impossible_xor_differential_trail(1,0,0) # doctest: +SKIP
+ ...
+
+ """
+
+ return enumerate_impossible_xor_differential_trails(self, number_of_active_key_bits, number_of_active_pt_bits,
+ number_of_active_ct_bits, solver_name,
+ output_only_one_solution=True)
+
+ def find_all_impossible_xor_differential_trails(self, number_of_active_key_bits=1, number_of_active_pt_bits=1, number_of_active_ct_bits=1, solver_name=solvers.SOLVER_DEFAULT):
+ """
+ Returns all impossible XOR differential trails.
+
+ INPUTS:
+
+ - ``fixed_values`` -- *list of dict*, the variables to be fixed in
+ standard format (see :py:meth:`~GenericModel.set_fixed_variables`)
+ - ``solver_name`` -- *str*, the solver to call
+
+ EXAMPLE::
+
+ # to retrieve the trails of Table 2 from https://eprint.iacr.org/2016/689
+ sage: from claasp.ciphers.block_ciphers.lblock_block_cipher import LBlockBlockCipher
+ sage: lblock = LBlockBlockCipher(number_of_rounds=16)
+ sage: from claasp.cipher_modules.models.sat.sat_models.sat_impossible_xor_differential_model import SatImpossibleXorDifferentialModel
+ sage: sat = SatImpossibleXorDifferentialModel(lblock)
+ sage: trails = sat.find_all_impossible_xor_differential_trails(1,0,0) # doctest: +SKIP
+ ...
+
+ """
+
+ return enumerate_impossible_xor_differential_trails(self, number_of_active_key_bits, number_of_active_pt_bits,
+ number_of_active_ct_bits, solver_name)
+
diff --git a/claasp/cipher_modules/models/smt/smt_models/smt_impossible_xor_differential_model.py b/claasp/cipher_modules/models/smt/smt_models/smt_impossible_xor_differential_model.py
new file mode 100644
index 00000000..78bdb299
--- /dev/null
+++ b/claasp/cipher_modules/models/smt/smt_models/smt_impossible_xor_differential_model.py
@@ -0,0 +1,89 @@
+
+# ****************************************************************************
+# Copyright 2023 Technology Innovation Institute
+#
+# This program is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# This program is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program. If not, see .
+# ****************************************************************************
+
+"""
+The search methods presented in this class differ from those of the classes
+:py:class:`Smt Bitwise Impossible Xor Differential Model
+`
+
+and :py:class:`Smt Wordwise Impossible Xor Differential Model
+`.
+
+Indeed, this class implements the framework proposed by `Cui et al.` which uses
+infeasibility of a XOR DIFFERENTIAL model to detect an impossible differential trail.
+"""
+
+from claasp.cipher_modules.models.smt import solvers
+from claasp.cipher_modules.models.smt.smt_models.smt_xor_differential_model import SmtXorDifferentialModel
+from claasp.cipher_modules.models.utils import enumerate_impossible_xor_differential_trails
+
+
+class SmtImpossibleXorDifferentialModel(SmtXorDifferentialModel):
+ def __init__(self, cipher, counter='sequential'):
+ super().__init__(cipher, counter)
+
+ def find_one_impossible_xor_differential_trail(self, number_of_active_key_bits=1, number_of_active_pt_bits=1, number_of_active_ct_bits=1, solver_name=solvers.SOLVER_DEFAULT):
+ """
+ Returns one impossible XOR differential trail.
+
+ INPUTS:
+
+ - ``fixed_values`` -- *list of dict*, the variables to be fixed in
+ standard format (see :py:meth:`~GenericModel.set_fixed_variables`)
+ - ``solver_name`` -- *str*, the solver to call
+
+ EXAMPLE::
+
+ # to retrieve one of the trails of Table 2 from https://eprint.iacr.org/2016/689
+ sage: from claasp.ciphers.block_ciphers.lblock_block_cipher import LBlockBlockCipher
+ sage: lblock = LBlockBlockCipher(number_of_rounds=16)
+ sage: from claasp.cipher_modules.models.smt.smt_models.smt_impossible_xor_differential_model import SmtImpossibleXorDifferentialModel
+ sage: smt = SmtImpossibleXorDifferentialModel(lblock)
+ sage: trail = smt.find_one_impossible_xor_differential_trail(1,0,0) # doctest: +SKIP
+ ...
+
+ """
+
+ return enumerate_impossible_xor_differential_trails(self, number_of_active_key_bits, number_of_active_pt_bits,
+ number_of_active_ct_bits, solver_name,
+ output_only_one_solution=True)
+
+ def find_all_impossible_xor_differential_trails(self, number_of_active_key_bits=1, number_of_active_pt_bits=1, number_of_active_ct_bits=1, solver_name=solvers.SOLVER_DEFAULT):
+ """
+ Returns all impossible XOR differential trails.
+
+ INPUTS:
+
+ - ``fixed_values`` -- *list of dict*, the variables to be fixed in
+ standard format (see :py:meth:`~GenericModel.set_fixed_variables`)
+ - ``solver_name`` -- *str*, the solver to call
+
+ EXAMPLE::
+
+ # to retrieve the trails of Table 2 from https://eprint.iacr.org/2016/689
+ sage: from claasp.ciphers.block_ciphers.lblock_block_cipher import LBlockBlockCipher
+ sage: lblock = LBlockBlockCipher(number_of_rounds=16)
+ sage: from claasp.cipher_modules.models.smt.smt_models.smt_impossible_xor_differential_model import SmtImpossibleXorDifferentialModel
+ sage: smt = SmtImpossibleXorDifferentialModel(lblock)
+ sage: trails = smt.find_all_impossible_xor_differential_trails(1,0,0) # doctest: +SKIP
+ ...
+
+ """
+
+ return enumerate_impossible_xor_differential_trails(self, number_of_active_key_bits, number_of_active_pt_bits,
+ number_of_active_ct_bits, solver_name)
\ No newline at end of file
diff --git a/claasp/cipher_modules/models/utils.py b/claasp/cipher_modules/models/utils.py
index d15a87ac..53b91392 100644
--- a/claasp/cipher_modules/models/utils.py
+++ b/claasp/cipher_modules/models/utils.py
@@ -21,11 +21,13 @@
import sys
import math
from copy import deepcopy
+from itertools import combinations, product
import numpy as np
-from claasp.name_mappings import CONSTANT, CIPHER_OUTPUT, INTERMEDIATE_OUTPUT, WORD_OPERATION, LINEAR_LAYER, SBOX, MIX_COLUMN, \
- INPUT_KEY, INPUT_PLAINTEXT, INPUT_MESSAGE, INPUT_STATE
+from claasp.name_mappings import CONSTANT, CIPHER_OUTPUT, INTERMEDIATE_OUTPUT, WORD_OPERATION, LINEAR_LAYER, SBOX, \
+ MIX_COLUMN, \
+ INPUT_KEY, INPUT_PLAINTEXT, INPUT_MESSAGE, INPUT_STATE, IMPOSSIBLE_XOR_DIFFERENTIAL
def add_arcs(arcs, component, curr_input_bit_ids, input_bit_size, intermediate_output_arcs, previous_output_bit_ids):
@@ -144,6 +146,34 @@ def integer_to_bit_list(int_value, list_length, endianness='little'):
return binary_value
+def bit_list_to_integer(bit_list, endianness='big'):
+ """
+ Return the integer value represented by the bit list.
+
+ INPUT:
+
+ - ``bit_list`` -- **list** of integers (0s and 1s); the list of bits to convert
+ - ``endianness`` -- **string** (default: `big`); the endianness of the list
+
+ * ``endianness='big'``, the bit list will be interpreted with the MSB indexed by 0
+ * ``endianness='little'``, the bit list will be interpreted with the LSB indexed by 0
+
+ EXAMPLES::
+
+ sage: from claasp.cipher_modules.models.utils import bit_list_to_integer
+ sage: bit_list_to_integer([0, 0, 1, 0, 1], 'big')
+ 5
+ """
+
+ if endianness == 'big':
+ binary_string = ''.join(map(str, bit_list))
+ elif endianness == 'little':
+ binary_string = ''.join(map(str, bit_list[::-1]))
+ else:
+ raise ValueError("Endianness must be 'big' or 'little'")
+
+ return int(binary_string, 2)
+
def print_components_values(solution):
"""
@@ -315,6 +345,36 @@ def set_fixed_variables(component_id, constraint_type, bit_positions, bit_values
'bit_values': bit_values
}
+def set_components_variables_to_one(component_id, component_size, bit_positions):
+ """
+ Return a dictionary.
+
+ The dictionary has the information needed to fix specific output bits of a component to 1 and the rest is all 0.
+
+ INPUT:
+
+ - ``component_id`` -- **string**; the id of the component
+ - ``bit_positions`` -- **list of int**; the positions of the bits to be fixed to 1
+ - ``component_size`` -- **int**; the total size of the component
+
+
+ EXAMPLES::
+
+ sage: from claasp.cipher_modules.models.utils import set_components_variables_to_one
+ sage: set_components_variables_to_one('key', 32, [0, 2, 12])
+ {'bit_positions': range(0, 32),
+ 'bit_values': array([1, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0,
+ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]),
+ 'component_id': 'key',
+ 'constraint_type': 'equal'}
+
+ """
+
+ component_bits = np.zeros(component_size, dtype=int)
+ component_bits[bit_positions] = 1
+ return set_fixed_variables(component_id=component_id, constraint_type='equal', bit_positions=range(component_size),
+ bit_values=component_bits)
+
def write_model_to_file(model_to_write, file_name):
"""
@@ -880,3 +940,52 @@ def differential_linear_checker_for_block_cipher_single_key(
count = np.count_nonzero(parities == 0)
corr = 2*count/number_of_samples*1.0-1
return corr
+
+def _convert_impossible_xor_differential_solution_to_dictionnary(trail, solving_time, components_list):
+ """
+ Converts a XOR differential solution into an impossible XOR differential solution dictionary.
+ """
+ from copy import deepcopy
+ solution = deepcopy(trail)
+ solution['solving_time_seconds'] = solving_time
+ for component in components_list:
+ solution['components_values'][component['component_id']] = {}
+ value = hex(bit_list_to_integer(component['bit_values']))[2:].zfill(len(component['bit_positions']) // 4)
+ solution['components_values'][component['component_id']]['value'] = value
+ solution['model_type'] = IMPOSSIBLE_XOR_DIFFERENTIAL
+ solution['test_name'] = 'find_one_impossible_xor_differential_trail'
+ solution['status'] = 'SATISFIABLE'
+
+ return solution
+
+def enumerate_impossible_xor_differential_trails(model, number_of_active_key_bits, number_of_active_pt_bits, number_of_active_ct_bits, solver_name, output_only_one_solution=False):
+
+ pt_size = model._cipher.inputs_bit_size[model._cipher.inputs.index(INPUT_PLAINTEXT)]
+ key_size = model._cipher.inputs_bit_size[model._cipher.inputs.index(INPUT_KEY)]
+ ct_id = [c.id for c in model._cipher.get_all_components() if c.type == 'cipher_output'][0]
+
+ key_combinations = combinations(range(key_size), number_of_active_key_bits)
+ pt_combinations = combinations(range(pt_size), number_of_active_pt_bits)
+ ct_combinations = combinations(range(model._cipher.output_bit_size), number_of_active_ct_bits)
+
+ solutions_list = []
+ solving_time = 0
+
+ for key_bits, pt_bits, ct_bits in product(key_combinations, pt_combinations, ct_combinations):
+ key_vars = set_components_variables_to_one(INPUT_KEY, key_size, list(key_bits))
+ pt_vars = set_components_variables_to_one(INPUT_PLAINTEXT, pt_size, list(pt_bits))
+ ct_vars = set_components_variables_to_one(ct_id, model._cipher.output_bit_size, list(ct_bits))
+
+ trail = model.find_one_xor_differential_trail(fixed_values=[key_vars, pt_vars, ct_vars],
+ solver_name=solver_name)
+
+ solving_time += trail['solving_time_seconds']
+
+ if trail['status'] == 'UNSATISFIABLE':
+ solution = _convert_impossible_xor_differential_solution_to_dictionnary(trail, solving_time,
+ [key_vars, pt_vars, ct_vars])
+ if output_only_one_solution:
+ return solution
+ solutions_list.append(solution)
+
+ return solutions_list
\ No newline at end of file
diff --git a/claasp/editor.py b/claasp/editor.py
index af507cf0..2bd696d6 100644
--- a/claasp/editor.py
+++ b/claasp/editor.py
@@ -18,7 +18,11 @@
from copy import deepcopy
+from itertools import chain
+import networkx as nx
+
+from claasp.cipher_modules.graph_generator import create_networkx_graph_from_input_ids
from claasp.components.or_component import OR
from claasp.components.and_component import AND
from claasp.components.xor_component import XOR
@@ -44,7 +48,7 @@
from claasp.components.variable_rotate_component import VariableRotate
from claasp.components.word_permutation_component import WordPermutation
from claasp.components.intermediate_output_component import IntermediateOutput
-from claasp.name_mappings import INTERMEDIATE_OUTPUT, CIPHER_OUTPUT, CONSTANT, INPUT_KEY, LINEAR_LAYER
+from claasp.name_mappings import INTERMEDIATE_OUTPUT, CIPHER_OUTPUT, CONSTANT, INPUT_KEY, LINEAR_LAYER, INPUT_PLAINTEXT
cipher_round_not_found_error = "Error! The cipher has no round: please run self.add_round() before adding any " \
"component. "
@@ -1729,6 +1733,67 @@ def remove_round_component(cipher, round_id, component):
def remove_round_component_from_id(cipher, round_id, component_id):
cipher.rounds.remove_round_component_from_id(round_id, component_id)
+def get_key_schedule(cipher):
+ """
+ Return the key schedule, if any, as a Cipher object.
+
+ INPUT:
+
+ - ``cipher`` -- **Cipher object**; an instance of the object cipher
+
+ EXAMPLES::
+
+ sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
+ sage: speck = SpeckBlockCipher(number_of_rounds=4)
+ sage: speck_key_schedule = speck.get_key_schedule()
+ sage: speck_key_schedule.print_as_python_dictionary()
+ cipher = {
+ ...
+ 'cipher_rounds' : [
+ # round 0
+ ...
+ # round 1
+ [
+ {
+ # round = 1 - round component = 0
+ 'id': 'constant_1_0',
+ 'type': 'constant',
+ 'input_bit_size': 0,
+ 'input_id_link': [''],
+ 'input_bit_positions': [[]],
+ 'output_bit_size': 16,
+ 'description': ['0x0000'],
+ },
+ ...
+ ],
+ # round 2
+ ...
+ # round 3
+ ...
+ ],
+ 'cipher_reference_code': None,
+ }
+ """
+
+ if INPUT_KEY not in cipher.inputs:
+ raise Exception("The primitive does not have a key schedule.")
+
+ graph_cipher = create_networkx_graph_from_input_ids(cipher)
+ key_schedule_component_ids = set(nx.dfs_tree(graph_cipher, source=INPUT_KEY)) - set(nx.dfs_tree(graph_cipher, source=INPUT_PLAINTEXT))
+ constants_ids = set(chain.from_iterable(graph_cipher.predecessors(i) for i in key_schedule_component_ids))
+
+ cipher_with_only_key_schedule = deepcopy(cipher)
+ for input in set(cipher_with_only_key_schedule.inputs) - {INPUT_KEY}:
+ index = cipher_with_only_key_schedule.inputs.index(input)
+ cipher_with_only_key_schedule.inputs.pop(index)
+ cipher_with_only_key_schedule.inputs_bit_size.pop(index)
+
+ for cipher_round in cipher.rounds_as_list:
+ for component in cipher_round.components:
+ if component.id not in key_schedule_component_ids.union(constants_ids):
+ cipher_with_only_key_schedule .remove_round_component_from_id(cipher_round.id, component.id)
+
+ return cipher_with_only_key_schedule
def sort_cipher(cipher):
"""
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 18d15a89..5817229c 100644
--- a/tests/unit/cipher_modules/models/cp/mzn_model_test.py
+++ b/tests/unit/cipher_modules/models/cp/mzn_model_test.py
@@ -8,8 +8,8 @@
from claasp.cipher_modules.models.cp.mzn_models.mzn_xor_differential_model_arx_optimized import \
MznXorDifferentialModelARXOptimized
from claasp.cipher_modules.models.cp.mzn_models.mzn_cipher_model_arx_optimized import MznCipherModelARXOptimized
-from claasp.cipher_modules.models.cp.mzn_models.mzn_deterministic_truncated_xor_differential_model_arx_optimized \
- import MznDeterministicTruncatedXorDifferentialModelARXOptimized
+from claasp.cipher_modules.models.cp.mzn_models.mzn_bitwise_deterministic_truncated_xor_differential_model_arx_optimized \
+ import MznBitwiseDeterministicTruncatedXorDifferentialModelARXOptimized
@pytest.mark.filterwarnings("ignore::DeprecationWarning:")
@@ -84,7 +84,7 @@ def test_fix_variables_value_constraints():
f'plaintext_y2+plaintext_y3>0;'
raiden = RaidenBlockCipher(number_of_rounds=1)
- mzn = MznDeterministicTruncatedXorDifferentialModelARXOptimized(raiden)
+ mzn = MznBitwiseDeterministicTruncatedXorDifferentialModelARXOptimized(raiden)
mzn.build_deterministic_truncated_xor_differential_trail_model()
fixed_variables = [{'component_id': 'key',
diff --git a/tests/unit/cipher_modules/models/cp/mzn_models/mzn_bitwise_deterministic_truncated_xor_differential_model_arx_optimized_test.py b/tests/unit/cipher_modules/models/cp/mzn_models/mzn_bitwise_deterministic_truncated_xor_differential_model_arx_optimized_test.py
new file mode 100644
index 00000000..6d2fbafd
--- /dev/null
+++ b/tests/unit/cipher_modules/models/cp/mzn_models/mzn_bitwise_deterministic_truncated_xor_differential_model_arx_optimized_test.py
@@ -0,0 +1,9 @@
+from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
+from claasp.cipher_modules.models.cp.mzn_models.mzn_bitwise_deterministic_truncated_xor_differential_model_arx_optimized \
+ import MznBitwiseDeterministicTruncatedXorDifferentialModelARXOptimized
+
+
+def test_build_bitwise_deterministic_truncated_xor_differential_trail_model():
+ speck = SpeckBlockCipher(number_of_rounds=22)
+ mzn = MznBitwiseDeterministicTruncatedXorDifferentialModelARXOptimized(speck)
+ mzn.build_deterministic_truncated_xor_differential_trail_model()
diff --git a/tests/unit/cipher_modules/models/cp/mzn_models/mzn_deterministic_truncated_xor_differential_model_test.py b/tests/unit/cipher_modules/models/cp/mzn_models/mzn_bitwise_deterministic_truncated_xor_differential_model_test.py
similarity index 90%
rename from tests/unit/cipher_modules/models/cp/mzn_models/mzn_deterministic_truncated_xor_differential_model_test.py
rename to tests/unit/cipher_modules/models/cp/mzn_models/mzn_bitwise_deterministic_truncated_xor_differential_model_test.py
index 07c281c7..394b82a8 100644
--- a/tests/unit/cipher_modules/models/cp/mzn_models/mzn_deterministic_truncated_xor_differential_model_test.py
+++ b/tests/unit/cipher_modules/models/cp/mzn_models/mzn_bitwise_deterministic_truncated_xor_differential_model_test.py
@@ -1,13 +1,13 @@
from claasp.ciphers.block_ciphers.aes_block_cipher import AESBlockCipher
from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
from claasp.cipher_modules.models.utils import set_fixed_variables, integer_to_bit_list
-from claasp.cipher_modules.models.cp.mzn_models.mzn_deterministic_truncated_xor_differential_model import \
- MznDeterministicTruncatedXorDifferentialModel
+from claasp.cipher_modules.models.cp.mzn_models.mzn_bitwise_deterministic_truncated_xor_differential_model import \
+ MznBitwiseDeterministicTruncatedXorDifferentialModel
def test_build_deterministic_truncated_xor_differential_trail_model():
speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=2)
- mzn = MznDeterministicTruncatedXorDifferentialModel(speck)
+ mzn = MznBitwiseDeterministicTruncatedXorDifferentialModel(speck)
fixed_variables = [set_fixed_variables('key', 'equal', range(64), integer_to_bit_list(0, 64, 'little'))]
mzn.build_deterministic_truncated_xor_differential_trail_model(fixed_variables)
@@ -19,7 +19,7 @@ def test_build_deterministic_truncated_xor_differential_trail_model():
def test_find_all_deterministic_truncated_xor_differential_trails():
speck = SpeckBlockCipher(number_of_rounds=3)
- mzn = MznDeterministicTruncatedXorDifferentialModel(speck)
+ mzn = MznBitwiseDeterministicTruncatedXorDifferentialModel(speck)
plaintext = set_fixed_variables(component_id='plaintext', constraint_type='not_equal',
bit_positions=range(32), bit_values=[0] * 32)
key = set_fixed_variables(component_id='key', constraint_type='equal', bit_positions=range(64), bit_values=[0] * 64)
@@ -44,7 +44,7 @@ def test_find_all_deterministic_truncated_xor_differential_trails():
def test_find_one_deterministic_truncated_xor_differential_trail():
speck = SpeckBlockCipher(number_of_rounds=1)
- mzn = MznDeterministicTruncatedXorDifferentialModel(speck)
+ mzn = MznBitwiseDeterministicTruncatedXorDifferentialModel(speck)
plaintext = set_fixed_variables(component_id='plaintext', constraint_type='not_equal',
bit_positions=range(32), bit_values=[0] * 32)
key = set_fixed_variables(component_id='key', constraint_type='equal', bit_positions=range(64), bit_values=[0] * 64)
diff --git a/tests/unit/cipher_modules/models/cp/mzn_models/mzn_bitwise_impossible_xor_differential_model_test.py b/tests/unit/cipher_modules/models/cp/mzn_models/mzn_bitwise_impossible_xor_differential_model_test.py
new file mode 100644
index 00000000..721c5c6a
--- /dev/null
+++ b/tests/unit/cipher_modules/models/cp/mzn_models/mzn_bitwise_impossible_xor_differential_model_test.py
@@ -0,0 +1,108 @@
+from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
+from claasp.cipher_modules.models.utils import set_fixed_variables, integer_to_bit_list
+from claasp.cipher_modules.models.cp.mzn_models.mzn_bitwise_impossible_xor_differential_model import \
+ MznBitwiseImpossibleXorDifferentialModel
+
+
+def test_build_impossible_xor_differential_trail_with_extensions_model():
+ speck = SpeckBlockCipher(number_of_rounds=6)
+ mzn = MznBitwiseImpossibleXorDifferentialModel(speck)
+ fixed_variables = [set_fixed_variables('key', 'equal', range(64), integer_to_bit_list(0, 64, 'little'))]
+ mzn.build_impossible_xor_differential_trail_with_extensions_model(number_of_rounds=6, fixed_variables=fixed_variables, initial_round=2, middle_round=3, final_round=5, intermediate_components=False)
+
+ assert len(mzn.model_constraints) == 1764
+ assert mzn.model_constraints[99] == 'array[0..31] of var 0..2: inverse_plaintext;'
+ assert mzn.model_constraints[3] == 'array[0..63] of var 0..2: key;'
+ assert mzn.model_constraints[39] == 'array[0..31] of var 0..2: cipher_output_5_12;'
+
+
+def test_build_impossible_xor_differential_trail_model():
+ speck = SpeckBlockCipher(number_of_rounds=5)
+ mzn = MznBitwiseImpossibleXorDifferentialModel(speck)
+ fixed_variables = [set_fixed_variables('key', 'equal', range(64), integer_to_bit_list(0, 64, 'little'))]
+ mzn.build_impossible_xor_differential_trail_model(number_of_rounds=5, fixed_variables=fixed_variables, middle_round=3)
+
+ assert len(mzn.model_constraints) == 1662
+ assert mzn.model_constraints[2] == 'array[0..31] of var 0..2: plaintext;'
+ assert mzn.model_constraints[3] == 'array[0..63] of var 0..2: key;'
+ assert mzn.model_constraints[4] == 'array[0..31] of var 0..2: inverse_cipher_output_4_12;'
+
+
+def test_find_all_impossible_xor_differential_trails():
+ speck = SpeckBlockCipher(number_of_rounds=7)
+ mzn = MznBitwiseImpossibleXorDifferentialModel(speck)
+ plaintext = set_fixed_variables(component_id='plaintext', constraint_type='not_equal',
+ bit_positions=range(32), bit_values=[0] * 32)
+ ciphertext = set_fixed_variables(component_id='inverse_' + speck.get_all_components_ids()[-1], constraint_type='not_equal',
+ bit_positions=range(32), bit_values=[0] * 32)
+ key = set_fixed_variables('key', constraint_type='equal',
+ bit_positions=range(64), bit_values=[0] * 64)
+ trail = mzn.find_all_impossible_xor_differential_trails(7, [plaintext, ciphertext, key], 'Chuffed', 1, 3, 7, False, solve_external = True)
+
+ assert trail[0]['status'] == 'UNSATISFIABLE'
+
+
+def test_find_lowest_complexity_impossible_xor_differential_trail():
+ speck = SpeckBlockCipher(number_of_rounds=6)
+ mzn = MznBitwiseImpossibleXorDifferentialModel(speck)
+ plaintext = set_fixed_variables(component_id='plaintext', constraint_type='not_equal',
+ bit_positions=range(32), bit_values=[0] * 32)
+ ciphertext = set_fixed_variables(component_id='inverse_' + speck.get_all_components_ids()[-1], constraint_type='not_equal',
+ bit_positions=range(32), bit_values=[0] * 32)
+ key = set_fixed_variables('key', constraint_type='equal',
+ bit_positions=range(64), bit_values=[0] * 64)
+ trail = mzn.find_lowest_complexity_impossible_xor_differential_trail(6, [plaintext, ciphertext, key], 'Chuffed', 1, 3, 6, True, solve_external = True)
+
+ assert str(trail['cipher']) == 'speck_p32_k64_o32_r6'
+ assert trail['model_type'] == 'impossible_xor_differential_one_solution'
+ assert trail['solver_name'] == 'Chuffed'
+
+ assert trail['components_values']['plaintext']['value'] == '00000000010000000000000000000000'
+ assert trail['components_values']['inverse_cipher_output_5_12']['value'] == '10000000000000001000000000000010'
+
+ assert trail['components_values']['xor_1_10']['value'] == '2222222100000010'
+ assert trail['components_values']['inverse_rot_2_9']['value'] == '2222222210022222'
+
+
+def test_find_one_impossible_xor_differential_trail():
+ speck = SpeckBlockCipher(number_of_rounds=6)
+ mzn = MznBitwiseImpossibleXorDifferentialModel(speck)
+ plaintext = set_fixed_variables(component_id='plaintext', constraint_type='not_equal',
+ bit_positions=range(32), bit_values=[0] * 32)
+ ciphertext = set_fixed_variables(component_id='inverse_' + speck.get_all_components_ids()[-1], constraint_type='not_equal',
+ bit_positions=range(32), bit_values=[0] * 32)
+ key = set_fixed_variables('key', constraint_type='equal',
+ bit_positions=range(64), bit_values=[0] * 64)
+ trail = mzn.find_one_impossible_xor_differential_trail(6, [plaintext, ciphertext, key], 'Chuffed', 1, 3, 6, True, solve_external = True)
+
+ assert str(trail['cipher']) == 'speck_p32_k64_o32_r6'
+ assert trail['model_type'] == 'impossible_xor_differential_one_solution'
+ assert trail['solver_name'] == 'Chuffed'
+
+ assert trail['components_values']['plaintext']['value'] == '00000000022200000021000000000000'
+ assert trail['components_values']['inverse_cipher_output_5_12']['value'] == '10000000000000001000000000000010'
+
+ assert trail['components_values']['xor_1_10']['value'] == '2222222222100022'
+ assert trail['components_values']['inverse_rot_2_9']['value'] == '2222222210022222'
+
+
+def test_find_one_impossible_xor_differential_trail_with_extensions():
+ speck = SpeckBlockCipher(number_of_rounds=6)
+ mzn = MznBitwiseImpossibleXorDifferentialModel(speck)
+ plaintext = set_fixed_variables(component_id='inverse_plaintext', constraint_type='not_equal',
+ bit_positions=range(32), bit_values=[0] * 32)
+ ciphertext = set_fixed_variables(component_id=speck.get_all_components_ids()[-1], constraint_type='not_equal',
+ bit_positions=range(32), bit_values=[0] * 32)
+ key = set_fixed_variables('key', constraint_type='equal',
+ bit_positions=range(64), bit_values=[0] * 64)
+ trail = mzn.find_one_impossible_xor_differential_trail_with_extensions(6, [plaintext, ciphertext, key], 'Chuffed', 2, 3, 5, True, solve_external = True)
+
+ assert str(trail['cipher']) == 'speck_p32_k64_o32_r6'
+ assert trail['model_type'] == 'impossible_xor_differential_one_solution'
+ assert trail['solver_name'] == 'Chuffed'
+
+ assert trail['components_values']['inverse_plaintext']['value'] == '22222220022222220000100000022200'
+ assert trail['components_values']['inverse_cipher_output_5_12']['value'] == '22222210000000002222221000000011'
+
+ assert trail['components_values']['intermediate_output_2_12']['value'] == '22222222220000002222222222000022'
+ assert trail['components_values']['inverse_intermediate_output_2_12']['value'] == '22222222222222222222222222122222'
diff --git a/tests/unit/cipher_modules/models/cp/mzn_models/mzn_deterministic_truncated_xor_differential_model_arx_optimized_test.py b/tests/unit/cipher_modules/models/cp/mzn_models/mzn_deterministic_truncated_xor_differential_model_arx_optimized_test.py
deleted file mode 100644
index 17e28673..00000000
--- a/tests/unit/cipher_modules/models/cp/mzn_models/mzn_deterministic_truncated_xor_differential_model_arx_optimized_test.py
+++ /dev/null
@@ -1,9 +0,0 @@
-from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
-from claasp.cipher_modules.models.cp.mzn_models.mzn_deterministic_truncated_xor_differential_model_arx_optimized \
- import MznDeterministicTruncatedXorDifferentialModelARXOptimized
-
-
-def test_build_deterministic_truncated_xor_differential_trail_model():
- speck = SpeckBlockCipher(number_of_rounds=22)
- mzn = MznDeterministicTruncatedXorDifferentialModelARXOptimized(speck)
- mzn.build_deterministic_truncated_xor_differential_trail_model()
diff --git a/tests/unit/cipher_modules/models/cp/mzn_models/mzn_impossible_xor_differential_model_test.py b/tests/unit/cipher_modules/models/cp/mzn_models/mzn_impossible_xor_differential_model_test.py
index f71a21e3..c91e8b67 100644
--- a/tests/unit/cipher_modules/models/cp/mzn_models/mzn_impossible_xor_differential_model_test.py
+++ b/tests/unit/cipher_modules/models/cp/mzn_models/mzn_impossible_xor_differential_model_test.py
@@ -1,108 +1,27 @@
+from claasp.ciphers.block_ciphers.lblock_block_cipher import LBlockBlockCipher
from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
-from claasp.cipher_modules.models.utils import set_fixed_variables, integer_to_bit_list
from claasp.cipher_modules.models.cp.mzn_models.mzn_impossible_xor_differential_model import \
- MznImpossibleXorDifferentialModel
-
-
-def test_build_impossible_xor_differential_trail_with_extensions_model():
- speck = SpeckBlockCipher(number_of_rounds=6)
- mzn = MznImpossibleXorDifferentialModel(speck)
- fixed_variables = [set_fixed_variables('key', 'equal', range(64), integer_to_bit_list(0, 64, 'little'))]
- mzn.build_impossible_xor_differential_trail_with_extensions_model(number_of_rounds=6, fixed_variables=fixed_variables, initial_round=2, middle_round=3, final_round=5, intermediate_components=False)
-
- assert len(mzn.model_constraints) == 1764
- assert mzn.model_constraints[99] == 'array[0..31] of var 0..2: inverse_plaintext;'
- assert mzn.model_constraints[3] == 'array[0..63] of var 0..2: key;'
- assert mzn.model_constraints[39] == 'array[0..31] of var 0..2: cipher_output_5_12;'
-
-
-def test_build_impossible_xor_differential_trail_model():
- speck = SpeckBlockCipher(number_of_rounds=5)
- mzn = MznImpossibleXorDifferentialModel(speck)
- fixed_variables = [set_fixed_variables('key', 'equal', range(64), integer_to_bit_list(0, 64, 'little'))]
- mzn.build_impossible_xor_differential_trail_model(number_of_rounds=5, fixed_variables=fixed_variables, middle_round=3)
-
- assert len(mzn.model_constraints) == 1662
- assert mzn.model_constraints[2] == 'array[0..31] of var 0..2: plaintext;'
- assert mzn.model_constraints[3] == 'array[0..63] of var 0..2: key;'
- assert mzn.model_constraints[4] == 'array[0..31] of var 0..2: inverse_cipher_output_4_12;'
-
-
-def test_find_all_impossible_xor_differential_trails():
- speck = SpeckBlockCipher(number_of_rounds=7)
- mzn = MznImpossibleXorDifferentialModel(speck)
- plaintext = set_fixed_variables(component_id='plaintext', constraint_type='not_equal',
- bit_positions=range(32), bit_values=[0] * 32)
- ciphertext = set_fixed_variables(component_id='inverse_' + speck.get_all_components_ids()[-1], constraint_type='not_equal',
- bit_positions=range(32), bit_values=[0] * 32)
- key = set_fixed_variables('key', constraint_type='equal',
- bit_positions=range(64), bit_values=[0] * 64)
- trail = mzn.find_all_impossible_xor_differential_trails(7, [plaintext, ciphertext, key], 'Chuffed', 1, 3, 7, False, solve_external = True)
-
- assert trail[0]['status'] == 'UNSATISFIABLE'
-
-
-def test_find_lowest_complexity_impossible_xor_differential_trail():
- speck = SpeckBlockCipher(number_of_rounds=6)
- mzn = MznImpossibleXorDifferentialModel(speck)
- plaintext = set_fixed_variables(component_id='plaintext', constraint_type='not_equal',
- bit_positions=range(32), bit_values=[0] * 32)
- ciphertext = set_fixed_variables(component_id='inverse_' + speck.get_all_components_ids()[-1], constraint_type='not_equal',
- bit_positions=range(32), bit_values=[0] * 32)
- key = set_fixed_variables('key', constraint_type='equal',
- bit_positions=range(64), bit_values=[0] * 64)
- trail = mzn.find_lowest_complexity_impossible_xor_differential_trail(6, [plaintext, ciphertext, key], 'Chuffed', 1, 3, 6, True, solve_external = True)
-
- assert str(trail['cipher']) == 'speck_p32_k64_o32_r6'
- assert trail['model_type'] == 'impossible_xor_differential_one_solution'
- assert trail['solver_name'] == 'Chuffed'
-
- assert trail['components_values']['plaintext']['value'] == '00000000010000000000000000000000'
- assert trail['components_values']['inverse_cipher_output_5_12']['value'] == '10000000000000001000000000000010'
-
- assert trail['components_values']['xor_1_10']['value'] == '2222222100000010'
- assert trail['components_values']['inverse_rot_2_9']['value'] == '2222222210022222'
+ MznImpossibleXorDifferentialModel
+from claasp.name_mappings import IMPOSSIBLE_XOR_DIFFERENTIAL, INPUT_KEY, INPUT_PLAINTEXT
def test_find_one_impossible_xor_differential_trail():
- speck = SpeckBlockCipher(number_of_rounds=6)
+ speck = SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=8)
mzn = MznImpossibleXorDifferentialModel(speck)
- plaintext = set_fixed_variables(component_id='plaintext', constraint_type='not_equal',
- bit_positions=range(32), bit_values=[0] * 32)
- ciphertext = set_fixed_variables(component_id='inverse_' + speck.get_all_components_ids()[-1], constraint_type='not_equal',
- bit_positions=range(32), bit_values=[0] * 32)
- key = set_fixed_variables('key', constraint_type='equal',
- bit_positions=range(64), bit_values=[0] * 64)
- trail = mzn.find_one_impossible_xor_differential_trail(6, [plaintext, ciphertext, key], 'Chuffed', 1, 3, 6, True, solve_external = True)
+ trail = mzn.find_one_impossible_xor_differential_trail(1, 0, 0)
- assert str(trail['cipher']) == 'speck_p32_k64_o32_r6'
- assert trail['model_type'] == 'impossible_xor_differential_one_solution'
- assert trail['solver_name'] == 'Chuffed'
+ assert str(trail['cipher']) == 'speck_p8_k16_o8_r8'
+ assert trail['model_type'] == IMPOSSIBLE_XOR_DIFFERENTIAL
+ assert trail['solver_name'] == 'chuffed'
+ assert trail['status'] == 'SATISFIABLE'
+ assert trail['components_values'][INPUT_KEY]['value'][1:] == '000'
+ assert trail['components_values'][INPUT_PLAINTEXT]['value'] == '00'
+ assert trail['components_values']['cipher_output_7_12']['value'] == '00'
- assert trail['components_values']['plaintext']['value'] == '00000000022200000021000000000000'
- assert trail['components_values']['inverse_cipher_output_5_12']['value'] == '10000000000000001000000000000010'
-
- assert trail['components_values']['xor_1_10']['value'] == '2222222222100022'
- assert trail['components_values']['inverse_rot_2_9']['value'] == '2222222210022222'
-
-def test_find_one_impossible_xor_differential_trail_with_extensions():
- speck = SpeckBlockCipher(number_of_rounds=6)
+def test_find_all_impossible_xor_differential_trails():
+ speck = SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=8)
mzn = MznImpossibleXorDifferentialModel(speck)
- plaintext = set_fixed_variables(component_id='inverse_plaintext', constraint_type='not_equal',
- bit_positions=range(32), bit_values=[0] * 32)
- ciphertext = set_fixed_variables(component_id=speck.get_all_components_ids()[-1], constraint_type='not_equal',
- bit_positions=range(32), bit_values=[0] * 32)
- key = set_fixed_variables('key', constraint_type='equal',
- bit_positions=range(64), bit_values=[0] * 64)
- trail = mzn.find_one_impossible_xor_differential_trail_with_extensions(6, [plaintext, ciphertext, key], 'Chuffed', 2, 3, 5, True, solve_external = True)
+ trails = mzn.find_all_impossible_xor_differential_trails(1, 0, 0)
- assert str(trail['cipher']) == 'speck_p32_k64_o32_r6'
- assert trail['model_type'] == 'impossible_xor_differential_one_solution'
- assert trail['solver_name'] == 'Chuffed'
-
- assert trail['components_values']['inverse_plaintext']['value'] == '22222220022222220000100000022200'
- assert trail['components_values']['inverse_cipher_output_5_12']['value'] == '22222210000000002222221000000011'
-
- assert trail['components_values']['intermediate_output_2_12']['value'] == '22222222220000002222222222000022'
- assert trail['components_values']['inverse_intermediate_output_2_12']['value'] == '22222222222222222222222222122222'
+ assert len(trails) == 2
\ No newline at end of file
diff --git a/tests/unit/cipher_modules/models/milp/milp_models/milp_impossible_xor_differential_model_test.py b/tests/unit/cipher_modules/models/milp/milp_models/milp_impossible_xor_differential_model_test.py
new file mode 100644
index 00000000..0cd41920
--- /dev/null
+++ b/tests/unit/cipher_modules/models/milp/milp_models/milp_impossible_xor_differential_model_test.py
@@ -0,0 +1,26 @@
+from claasp.cipher_modules.models.milp.milp_models.milp_impossible_xor_differential_model import \
+ MilpImpossibleXorDifferentialModel
+from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
+from claasp.name_mappings import IMPOSSIBLE_XOR_DIFFERENTIAL, INPUT_KEY, INPUT_PLAINTEXT
+
+
+def test_find_one_impossible_xor_differential_trail():
+ speck = SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=8)
+ milp = MilpImpossibleXorDifferentialModel(speck)
+ trail = milp.find_one_impossible_xor_differential_trail(1, 0, 0)
+
+ assert str(trail['cipher']) == 'speck_p8_k16_o8_r8'
+ assert trail['model_type'] == IMPOSSIBLE_XOR_DIFFERENTIAL
+ assert trail['solver_name'] == 'GLPK'
+ assert trail['status'] == 'SATISFIABLE'
+ assert trail['components_values'][INPUT_KEY]['value'][1:] == '000'
+ assert trail['components_values'][INPUT_PLAINTEXT]['value'] == '00'
+ assert trail['components_values']['cipher_output_7_12']['value'] == '00'
+
+
+def test_find_all_impossible_xor_differential_trails():
+ speck = SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=8)
+ milp = MilpImpossibleXorDifferentialModel(speck)
+ trails = milp.find_all_impossible_xor_differential_trails(1, 0, 0)
+
+ assert len(trails) == 2
\ No newline at end of file
diff --git a/tests/unit/cipher_modules/models/sat/cms_models/cms_impossible_xor_differential_model_test.py b/tests/unit/cipher_modules/models/sat/cms_models/cms_impossible_xor_differential_model_test.py
new file mode 100644
index 00000000..4732993f
--- /dev/null
+++ b/tests/unit/cipher_modules/models/sat/cms_models/cms_impossible_xor_differential_model_test.py
@@ -0,0 +1,26 @@
+from claasp.cipher_modules.models.sat.cms_models.cms_impossible_xor_differential_model import \
+ CmsSatImpossibleXorDifferentialModel
+from claasp.ciphers.block_ciphers.lblock_block_cipher import LBlockBlockCipher
+from claasp.name_mappings import IMPOSSIBLE_XOR_DIFFERENTIAL, INPUT_KEY, INPUT_PLAINTEXT
+
+
+def test_find_one_impossible_xor_differential_trail():
+ lblock = LBlockBlockCipher(number_of_rounds=16)
+ cms = CmsSatImpossibleXorDifferentialModel(lblock)
+ trail = cms.find_one_impossible_xor_differential_trail(1, 0, 0)
+
+ assert str(trail['cipher']) == 'lblock_p64_k80_o64_r16'
+ assert trail['model_type'] == IMPOSSIBLE_XOR_DIFFERENTIAL
+ assert trail['solver_name'] == 'CRYPTOMINISAT_EXT'
+ assert trail['status'] == 'SATISFIABLE'
+ assert trail['components_values'][INPUT_KEY]['value'][:-3] == '00000000000000000'
+ assert trail['components_values'][INPUT_PLAINTEXT]['value'] == '0000000000000000'
+ assert trail['components_values']['cipher_output_15_19']['value'] == '0000000000000000'
+
+
+def test_find_all_impossible_xor_differential_trails():
+ lblock = LBlockBlockCipher(number_of_rounds=16)
+ cms = CmsSatImpossibleXorDifferentialModel(lblock)
+ trails = cms.find_all_impossible_xor_differential_trails(1, 0, 0)
+
+ assert len(trails) == 4
\ No newline at end of file
diff --git a/tests/unit/cipher_modules/models/sat/sat_models/sat_impossible_xor_differential_model_test.py b/tests/unit/cipher_modules/models/sat/sat_models/sat_impossible_xor_differential_model_test.py
new file mode 100644
index 00000000..18a51163
--- /dev/null
+++ b/tests/unit/cipher_modules/models/sat/sat_models/sat_impossible_xor_differential_model_test.py
@@ -0,0 +1,33 @@
+from claasp.ciphers.block_ciphers.lblock_block_cipher import LBlockBlockCipher
+from claasp.cipher_modules.models.sat.sat_models.sat_impossible_xor_differential_model import \
+ SatImpossibleXorDifferentialModel
+from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
+from claasp.name_mappings import IMPOSSIBLE_XOR_DIFFERENTIAL, INPUT_KEY, INPUT_PLAINTEXT
+
+
+def test_find_one_impossible_xor_differential_trail():
+ lblock = LBlockBlockCipher(number_of_rounds=16)
+ sat = SatImpossibleXorDifferentialModel(lblock)
+ trail = sat.find_one_impossible_xor_differential_trail(1, 0, 0)
+
+ assert str(trail['cipher']) == 'lblock_p64_k80_o64_r16'
+ assert trail['model_type'] == IMPOSSIBLE_XOR_DIFFERENTIAL
+ assert trail['solver_name'] == 'CRYPTOMINISAT_EXT'
+ assert trail['status'] == 'SATISFIABLE'
+ assert trail['components_values'][INPUT_KEY]['value'][:-3] == '00000000000000000'
+ assert trail['components_values'][INPUT_PLAINTEXT]['value'] == '0000000000000000'
+ assert trail['components_values']['cipher_output_15_19']['value'] == '0000000000000000'
+
+
+def test_find_all_impossible_xor_differential_trails():
+ lblock = LBlockBlockCipher(number_of_rounds=16)
+ sat = SatImpossibleXorDifferentialModel(lblock)
+ trails = sat.find_all_impossible_xor_differential_trails(1, 0, 0)
+
+ assert len(trails) == 4
+
+ speck = SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=8)
+ sat = SatImpossibleXorDifferentialModel(speck)
+ trails = sat.find_all_impossible_xor_differential_trails(1, 0, 0)
+
+ assert len(trails) == 2
\ No newline at end of file
diff --git a/tests/unit/cipher_modules/models/smt/smt_models/smt_impossible_xor_differential_model_test.py b/tests/unit/cipher_modules/models/smt/smt_models/smt_impossible_xor_differential_model_test.py
new file mode 100644
index 00000000..1c1f1782
--- /dev/null
+++ b/tests/unit/cipher_modules/models/smt/smt_models/smt_impossible_xor_differential_model_test.py
@@ -0,0 +1,26 @@
+from claasp.ciphers.block_ciphers.lblock_block_cipher import LBlockBlockCipher
+from claasp.cipher_modules.models.smt.smt_models.smt_impossible_xor_differential_model import \
+ SmtImpossibleXorDifferentialModel
+from claasp.name_mappings import IMPOSSIBLE_XOR_DIFFERENTIAL, INPUT_KEY, INPUT_PLAINTEXT
+
+
+def test_find_one_impossible_xor_differential_trail():
+ lblock = LBlockBlockCipher(number_of_rounds=16)
+ smt = SmtImpossibleXorDifferentialModel(lblock)
+ trail = smt.find_one_impossible_xor_differential_trail(1, 0, 0)
+
+ assert str(trail['cipher']) == 'lblock_p64_k80_o64_r16'
+ assert trail['model_type'] == IMPOSSIBLE_XOR_DIFFERENTIAL
+ assert trail['solver_name'] == 'Z3_EXT'
+ assert trail['status'] == 'SATISFIABLE'
+ assert trail['components_values'][INPUT_KEY]['value'][:-3] == '00000000000000000'
+ assert trail['components_values'][INPUT_PLAINTEXT]['value'] == '0000000000000000'
+ assert trail['components_values']['cipher_output_15_19']['value'] == '0000000000000000'
+
+
+def test_find_all_impossible_xor_differential_trails():
+ lblock = LBlockBlockCipher(number_of_rounds=16)
+ smt = SmtImpossibleXorDifferentialModel(lblock)
+ trails = smt.find_all_impossible_xor_differential_trails(1, 0, 0)
+
+ assert len(trails) == 4
\ No newline at end of file
diff --git a/tests/unit/editor_test.py b/tests/unit/editor_test.py
index aea128eb..25dac4d8 100644
--- a/tests/unit/editor_test.py
+++ b/tests/unit/editor_test.py
@@ -46,6 +46,21 @@ def test_remove_key_schedule():
'output_bit_size': 16,
'description': ['ROTATE', 7]}
+def test_get_key_schedule():
+ speck = SpeckBlockCipher(number_of_rounds=4)
+ removed_key_speck = speck.remove_key_schedule()
+ key_schedule_speck = speck.get_key_schedule()
+
+ assert set(removed_key_speck.get_all_components_ids()).symmetric_difference(set(key_schedule_speck.get_all_components_ids())) == set(speck.get_all_components_ids())
+ assert key_schedule_speck.component_from(1, 0).as_python_dictionary() == {'id': 'constant_1_0',
+ 'type': 'constant',
+ 'input_bit_size': 0,
+ 'input_id_link': [''],
+ 'input_bit_positions': [[]],
+ 'output_bit_size': 16,
+ 'description': ['0x0000']}
+
+
def test_remove_permutations():
present = PresentBlockCipher()