Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
46 changes: 29 additions & 17 deletions claasp/cipher_modules/models/cp/mzn_model.py
Original file line number Diff line number Diff line change
Expand Up @@ -17,32 +17,33 @@
# ****************************************************************************


import os
import math
import itertools
import math
import os
import subprocess

from copy import deepcopy

from sage.crypto.sbox import SBox

from datetime import timedelta

from minizinc import Instance, Model, Solver, Status
from sage.crypto.sbox import SBox

from claasp.cipher_modules.component_analysis_tests import branch_number
from claasp.cipher_modules.models.cp.minizinc_utils import usefulfunctions
from claasp.cipher_modules.models.cp.solvers import CP_SOLVERS_INTERNAL, CP_SOLVERS_EXTERNAL, MODEL_DEFAULT_PATH, \
SOLVER_DEFAULT
from claasp.name_mappings import SBOX, CIPHER_OUTPUT, CONSTANT, INTERMEDIATE_OUTPUT, LINEAR_LAYER, MIX_COLUMN, \
WORD_OPERATION

from claasp.cipher_modules.models.utils import write_model_to_file, convert_solver_solution_to_dictionary
from claasp.name_mappings import SBOX
from claasp.cipher_modules.models.cp.solvers import CP_SOLVERS_INTERNAL, CP_SOLVERS_EXTERNAL, MODEL_DEFAULT_PATH, SOLVER_DEFAULT

solve_satisfy = 'solve satisfy;'
constraint_type_error = 'Constraint type not defined'


class MznModel:

def __init__(self, cipher, window_size_list=None, probability_weight_per_round=None, sat_or_milp='sat'):
def __init__(self, cipher, sat_or_milp='sat'):
self._cipher = cipher
self.initialise_model()
if sat_or_milp not in ['sat', 'milp']:
Expand All @@ -66,17 +67,8 @@ def __init__(self, cipher, window_size_list=None, probability_weight_per_round=N
self.mzn_carries_output_directives = []
self.input_postfix = "x"
self.output_postfix = "y"
self.window_size_list = window_size_list
self.probability_weight_per_round = probability_weight_per_round
self.carries_vars = []
if probability_weight_per_round and len(probability_weight_per_round) != self._cipher.number_of_rounds:
raise ValueError("probability_weight_per_round size must be equal to cipher_number_of_rounds")

self.probability_modadd_vars_per_round = [[] for _ in range(self._cipher.number_of_rounds)]

if window_size_list and len(window_size_list) != self._cipher.number_of_rounds:
raise ValueError("window_size_list size must be equal to cipher_number_of_rounds")


def initialise_model(self):
self._variables_list = []
Expand Down Expand Up @@ -158,6 +150,26 @@ def add_solution_to_components_values_internal(self, component_solution, compone
component_solution['weight'] = component_weight
components_values[f'solution{solution_number}'][f'{component}'] = component_solution

def build_generic_cp_model_from_dictionary(self, component_and_model_types):
self._variables_list = []
self._model_constraints = []

component_types = [CIPHER_OUTPUT, CONSTANT, INTERMEDIATE_OUTPUT, LINEAR_LAYER, MIX_COLUMN, SBOX, WORD_OPERATION]
operation_types = ['AND', 'MODADD', 'MODSUB', 'NOT', 'OR', 'ROTATE', 'SHIFT', 'SHIFT_BY_VARIABLE_AMOUNT', 'XOR']

for component_and_model_type in component_and_model_types:
component = component_and_model_type["component_object"]
model_type = component_and_model_type["model_type"]
operation = component.description[0]
if component.type not in component_types or (
WORD_OPERATION == component.type and operation not in operation_types):
print(f'{component.id} not yet implemented')
else:
cp_continuous_differential_propagation_constraints = getattr(component, model_type)
variables, constraints = cp_continuous_differential_propagation_constraints(self)
self._model_constraints.extend(constraints)
self._variables_list.extend(variables)

def build_mix_column_truncated_table(self, component):
"""
Return a model that generates the list of possible input/output couples for the given mix column.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -23,8 +23,8 @@

class MznCipherModelARXOptimized(MznModel):

def __init__(self, cipher, window_size_list=None, probability_weight_per_round=None, sat_or_milp='sat'):
super().__init__(cipher, window_size_list, probability_weight_per_round, sat_or_milp)
def __init__(self, cipher, sat_or_milp='sat'):
super().__init__(cipher, sat_or_milp)

def build_cipher_model(self, fixed_variables=[]):
"""
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -24,8 +24,8 @@

class MznDeterministicTruncatedXorDifferentialModelARXOptimized(MznModel):

def __init__(self, cipher, window_size_list=None, probability_weight_per_round=None, sat_or_milp='sat'):
super().__init__(cipher, window_size_list, probability_weight_per_round, sat_or_milp)
def __init__(self, cipher, sat_or_milp='sat'):
super().__init__(cipher, sat_or_milp)

def build_deterministic_truncated_xor_differential_trail_model(self, fixed_variables=[]):
"""
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -29,8 +29,15 @@ def __init__(
self, cipher, window_size_list=None, probability_weight_per_round=None, sat_or_milp='sat',
include_word_operations_mzn_file=True
):
self.window_size_list = window_size_list
self.probability_weight_per_round = probability_weight_per_round
self.include_word_operations_mzn_file = include_word_operations_mzn_file
super().__init__(cipher, window_size_list, probability_weight_per_round, sat_or_milp)
super().__init__(cipher, sat_or_milp)
if probability_weight_per_round and len(probability_weight_per_round) != self._cipher.number_of_rounds:
raise ValueError("probability_weight_per_round size must be equal to cipher_number_of_rounds")

if window_size_list and len(window_size_list) != self._cipher.number_of_rounds:
raise ValueError("window_size_list size must be equal to cipher_number_of_rounds")

@staticmethod
def _create_minizinc_1d_array_from_list(mzn_list):
Expand Down
58 changes: 58 additions & 0 deletions tests/unit/cipher_modules/models/cp/mzn_model_test.py
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,8 @@
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.utils import set_fixed_variables, integer_to_bit_list
from minizinc import Model, Solver, Instance, Status


@pytest.mark.filterwarnings("ignore::DeprecationWarning:")
Expand Down Expand Up @@ -111,3 +113,59 @@ def test_model_constraints():
speck = SpeckBlockCipher(number_of_rounds=4)
mzn = MznModel(speck)
mzn.model_constraints()

def test_build_generic_cp_model_from_dictionary():

speck = SpeckBlockCipher(number_of_rounds=3)
model = MznXorDifferentialModelARXOptimized(speck)
component_and_model_types = []

for component in speck.get_all_components():
component_and_model_types.append({
"component_object": component,
"model_type": "minizinc_xor_differential_propagation_constraints"
})

model.build_generic_cp_model_from_dictionary(component_and_model_types)

#Caso especial para ARX
model.init_constraints()

fixed_variables = []

fixed_variables.append(
set_fixed_variables(
component_id="plaintext",
constraint_type="equal",
bit_positions=list(range(32)),
bit_values=integer_to_bit_list(0x00400000, 32, 'big')
)
)

fixed_variables.append(
set_fixed_variables(
component_id="key",
constraint_type="equal",
bit_positions=list(range(64)),
bit_values=[0] * 64
)
)

fixed_variables.append(
set_fixed_variables(
component_id="cipher_output_2_12",
constraint_type="equal",
bit_positions=list(range(32)),
bit_values=integer_to_bit_list(0x8000840a, 32, 'big')
)
)

constraints = model.fix_variables_value_constraints_for_ARX(fixed_variables)

result = model.solve_for_ARX(solver_name="cp-sat")

assert result.status in {
Status.SATISFIED,
Status.OPTIMAL_SOLUTION,
Status.ALL_SOLUTIONS,
}
Loading