Mzn model

class MznModel(cipher, window_size_list=None, probability_weight_per_round=None, sat_or_milp='sat')

Bases: object

add_comment(comment)

Write a ‘comment’ at the beginning of the model.

INPUT:

  • comment – string; string with the comment to be added

add_constraint_from_str(str_constraint)
add_output_comment(comment)
add_solution_to_components_values(component_id, component_solution, components_values, j, output_to_parse, solution_number, string)
add_solution_to_components_values_internal(component_solution, components_values, component_weight, solution_number, component)
add_solutions_from_components_values(components_values, memory, model_type, solutions, solve_time, solver_name, solver_output, total_weight, solve_external)
build_mix_column_truncated_table(component)

Return a model that generates the list of possible input/output couples for the given mix column.

INPUT:

  • component – Component object; the mix column component in Cipher

EXAMPLES:

sage: from claasp.cipher_modules.models.cp.mzn_model import MznModel
sage: from claasp.ciphers.block_ciphers.aes_block_cipher import AESBlockCipher
sage: aes = AESBlockCipher(number_of_rounds=3)
sage: cp = MznModel(aes)
sage: mix_column = aes.component_from(0, 21)
sage: cp.build_mix_column_truncated_table(mix_column)
'array[0..93, 1..8] of int: mix_column_truncated_table_mix_column_0_21 = array2d(0..93, 1..8, [0,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,0,0,1,0,1,1,1,1,0,0,1,1,0,1,1,1,0,0,1,1,1,0,1,1,0,0,1,1,1,1,0,1,0,0,1,1,1,1,1,0,0,0,1,1,1,1,1,1,0,1,0,0,1,1,1,1,0,1,0,1,0,1,1,1,0,1,0,1,1,0,1,1,0,1,0,1,1,1,0,1,0,1,0,1,1,1,1,0,0,1,0,1,1,1,1,1,0,1,1,0,0,1,1,1,0,1,1,0,1,0,1,1,0,1,1,0,1,1,0,1,0,1,1,0,1,1,1,0,0,1,1,0,1,1,1,1,0,1,1,1,0,0,1,1,0,1,1,1,0,1,0,1,0,1,1,1,0,1,1,0,0,1,1,1,0,1,1,1,0,1,1,1,1,0,0,1,0,1,1,1,1,0,1,0,0,1,1,1,1,0,1,1,0,1,1,1,1,1,0,0,0,1,1,1,1,1,0,1,0,1,1,1,1,1,1,0,0,1,1,1,1,1,1,1,1,0,0,0,1,1,1,1,1,0,0,1,0,1,1,1,1,0,0,1,1,0,1,1,1,0,0,1,1,1,0,1,1,0,0,1,1,1,1,0,1,0,0,1,1,1,1,1,1,0,1,0,0,1,1,1,1,0,1,0,1,0,1,1,1,0,1,0,1,1,0,1,1,0,1,0,1,1,1,0,1,0,1,0,1,1,1,1,1,0,1,1,0,0,1,1,1,0,1,1,0,1,0,1,1,0,1,1,0,1,1,0,1,0,1,1,0,1,1,1,1,0,1,1,1,0,0,1,1,0,1,1,1,0,1,0,1,0,1,1,1,0,1,1,1,0,1,1,1,1,0,0,1,0,1,1,1,1,0,1,1,0,1,1,1,1,1,0,1,0,1,1,1,1,1,1,1,1,0,0,0,1,1,1,1,1,0,0,1,0,1,1,1,1,0,0,1,1,0,1,1,1,0,0,1,1,1,0,1,1,0,0,1,1,1,1,1,1,0,1,0,0,1,1,1,1,0,1,0,1,0,1,1,1,0,1,0,1,1,0,1,1,0,1,0,1,1,1,1,1,0,1,1,0,0,1,1,1,0,1,1,0,1,0,1,1,0,1,1,0,1,1,1,1,0,1,1,1,0,0,1,1,0,1,1,1,0,1,1,1,0,1,1,1,1,0,1,1,0,1,1,1,1,1,1,1,1,0,0,0,1,1,1,1,1,0,0,1,0,1,1,1,1,0,0,1,1,0,1,1,1,0,0,1,1,1,1,1,1,0,1,0,0,1,1,1,1,0,1,0,1,0,1,1,1,0,1,0,1,1,1,1,1,0,1,1,0,0,1,1,1,0,1,1,0,1,1,1,1,0,1,1,1,0,1,1,1,0,1,1,1,1,1,1,1,1,0,0,0,1,1,1,1,1,0,0,1,0,1,1,1,1,0,0,1,1,1,1,1,1,0,1,0,0,1,1,1,1,0,1,0,1,1,1,1,1,0,1,1,0,1,1,1,1,0,1,1,1,1,1,1,1,1,0,0,0,1,1,1,1,1,0,0,1,1,1,1,1,1,0,1,0,1,1,1,1,1,0,1,1,1,1,1,1,1,1,0,0,1,1,1,1,1,1,0,1,1,1,1,1,1,1,1,0,1,1,1,1,1,1,1,1]);'
calculate_bit_positions(bit_positions, input_length)
calculate_bit_values(bit_values, input_length)
calculate_input_bit_positions(word_index, input_name_1, input_name_2, new_input_bit_positions_1, new_input_bit_positions_2)
property cipher
property cipher_id
find_possible_number_of_active_sboxes(weight)

Return a set whose numbers are the possible numbers of active S-boxes.

INPUT:

  • weight – integer; the fixed weight that must be able to be obtained with the found numbers of active S-boxes

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.midori_block_cipher import MidoriBlockCipher
sage: from claasp.cipher_modules.models.cp.mzn_model import MznModel
sage: midori = MidoriBlockCipher()
sage: cp = MznModel(midori)
sage: model = cp.find_possible_number_of_active_sboxes(9)
sage: model
{3, 4}
fix_variables_value_constraints(fixed_variables=[], step='full_model')

Return a list of CP constraints that fix the input variables to a specific value.

INPUT:

  • fixed_variables – list (default: []); dictionaries containing name, bit_size, value (as integer) for the variables that need to be fixed to a certain value:

    {

    ‘component_id’: ‘plaintext’,

    ‘constraint_type’: ‘equal’/’not_equal’

    ‘bit_size’: 32,

    ‘value’: 753

    }

  • step – string (default: full_model)

EXAMPLES:

sage: from claasp.cipher_modules.models.cp.mzn_model import MznModel
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 = MznModel(speck)
sage: cp.fix_variables_value_constraints([set_fixed_variables('plaintext', 'equal', range(4), integer_to_bit_list(5, 4, 'big'))])
['constraint plaintext[0] = 0 /\\ plaintext[1] = 1 /\\ plaintext[2] = 0 /\\ plaintext[3] = 1;']
sage: cp.fix_variables_value_constraints([set_fixed_variables('plaintext', 'not_equal', list(range(4)), integer_to_bit_list(5, 4, 'big'))])
['constraint plaintext[0] != 0 \\/ plaintext[1] != 1 \\/ plaintext[2] != 0 \\/ plaintext[3] != 1;']
fix_variables_value_constraints_for_ARX(fixed_variables=[])

Return a list of constraints that fix the input variables to a specific value.

INPUT:

  • fixed_variables – list (default: []); the variables to be fixed in standard format

See also

set_fixed_variables()

EXAMPLES:

sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_xor_differential_model_arx_optimized import MznXorDifferentialModelARXOptimized
sage: from claasp.ciphers.block_ciphers.raiden_block_cipher import RaidenBlockCipher
sage: raiden = RaidenBlockCipher(number_of_rounds=1)
sage: minizinc = MznXorDifferentialModelARXOptimized(raiden)
sage: minizinc.build_xor_differential_trail_model()
sage: fixed_variables = [{
....:     'component_id': 'key',
....:     'constraint_type': 'equal',
....:     'bit_positions': [0, 1, 2, 3],
....:     'bit_values': [0, 1, 0, 1]
....: }]
sage: minizinc.fix_variables_value_constraints_for_ARX(fixed_variables)[0]
'constraint key_y0 = 0;'

sage: fixed_variables = [{ 'component_id': 'plaintext',
....:     'constraint_type': 'sum',
....:     'bit_positions': [0, 1, 2, 3],
....:     'operator': '>',
....:     'value': '0' }]
sage: minizinc.fix_variables_value_constraints_for_ARX(fixed_variables)[0]
'constraint plaintext_y0+plaintext_y1+plaintext_y2+plaintext_y3>0;'
property float_and_lat_values
format_component_value(component_id, string)
get_command_for_solver_process(input_file_path, model_type, solver_name, num_of_processors, timelimit)
get_mix_column_all_inputs(input_bit_positions_1, input_id_link_1, numb_of_inp_1)
get_total_weight(string_total_weight)
initialise_model()
property model_constraints

Return the model specified by model_type.

INPUT:

  • model_type – string; the model to retrieve

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: from claasp.cipher_modules.models.cp.mzn_model import MznModel
sage: speck = SpeckBlockCipher(number_of_rounds=4)
sage: cp = MznModel(speck)
sage: cp.model_constraints()
Traceback (most recent call last):
...
ValueError: No model generated
output_probability_per_round()
parse_solver_information(output_to_parse, truncated=False, solve_external=True)
set_component_solution_value(component_solution, truncated, value)
solve(model_type, solver_name='chuffed', solve_external=False, timeout_in_seconds_=None, processes_=None, nr_solutions_=None, random_seed_=None, all_solutions_=False, intermediate_solutions_=False, free_search_=False, optimisation_level_=None)

Return the solution of the model.

INPUT:

  • model_type – string; the model to solve:

    • ‘cipher’

    • ‘xor_differential’

    • ‘xor_differential_one_solution’

    • ‘xor_linear’

    • ‘xor_linear_one_solution’

    • ‘deterministic_truncated_xor_differential’

    • ‘deterministic_truncated_xor_differential_one_solution’

    • ‘impossible_xor_differential’

  • solver_name – string (default: None); the name of the solver. Available values are:

    • 'Chuffed'

    • 'Gecode'

    • 'COIN-BC'

  • num_of_processors – integer; the number of processors to be used

  • timelimit – integer; time limit to output a result

EXAMPLES:

sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_xor_differential_model import MznXorDifferentialModel
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 = MznXorDifferentialModel(speck)
sage: fixed_variables = [set_fixed_variables('key', 'equal', list(range(64)), integer_to_bit_list(0, 64, 'little')), set_fixed_variables('plaintext', 'not_equal', list(range(32)), integer_to_bit_list(0, 32, 'little'))]
sage: cp.build_xor_differential_trail_model(-1, fixed_variables)
sage: cp.solve('xor_differential', 'chuffed') # random
[{'cipher_id': 'speck_p32_k64_o32_r4',
   ...
  'total_weight': '5.0'}]
solve_for_ARX(solver_name=None, timeout_in_seconds_=30, processes_=4, nr_solutions_=None, random_seed_=None, all_solutions_=False, intermediate_solutions_=False, free_search_=False, optimisation_level_=None)

Solve the model passed in str_model_path by using MiniZinc and str_solver.

INPUT:

  • model_type – string; the type of the model that has been solved

  • solver_name – string (default: None); name of the solver to be used together with MiniZinc

  • timeout_in_seconds_ – integer (default: 30); time in seconds to interrupt the solving process

  • processes_ – integer (default: 4); set the number of processes the solver can use. (Only available when the -p flag is supported by the solver)

  • nr_solutions_ – integer (default: None); the requested number of solution. (Only available on satisfaction problems and when the -n flag is supported by the solver)

  • random_seed_ – integer (default: None); set the random seed for solver. (Only available when the -r flag is supported by the solver)

  • intermediate_solutions_ – boolean (default: False); request the solver to output any intermediate solutions that are found during the solving process. (Only available on optimisation problems and when the -a flag is supported by the solver)

  • all_solutions_ – boolean (default: False); request to solver to find all solutions. (Only available on satisfaction problems and when the -a flag is supported by the solver)

  • free_search – boolean (default: False); allow the solver to ignore the search definition within the instance (Only available when the -f flag is supported by the solver)

  • optimisation_level_ – integer (default: None); set the MiniZinc compiler optimisation level

    • 0: Disable optimisation

    • 1: Single pass optimisation (default)

    • 2: Flatten twice to improve flattening decisions

    • 3: Perform root-node-propagation

    • 4: Probe bounds of all variables at the root node

    • 5: Probe values of all variables at the root node

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: from claasp.cipher_modules.models.cp.mzn_models.mzn_xor_differential_model_arx_optimized import MznXorDifferentialModelARXOptimized
sage: speck = SpeckBlockCipher(number_of_rounds=5, block_bit_size=32, key_bit_size=64)
sage: minizinc = MznXorDifferentialModelARXOptimized(speck)
sage: bit_positions = [i for i in range(speck.output_bit_size)]
sage: bit_positions_key = list(range(64))
sage: fixed_variables = [{ 'component_id': 'plaintext',
....:     'constraint_type': 'sum',
....:     'bit_positions': bit_positions,
....:     'operator': '>',
....:     'value': '0' }]
sage: fixed_variables.append({ 'component_id': 'key',
....:     'constraint_type': 'sum',
....:     'bit_positions': bit_positions_key,
....:     'operator': '=',
....:     'value': '0' })
sage: minizinc.build_xor_differential_trail_model(-1, fixed_variables)
sage: result = minizinc.solve_for_ARX('Xor')
sage: result.statistics['nSolutions']
1
solver_names(verbose=False)
weight_constraints(weight)

Return a list of CP constraints that fix the total weight to a specific value.

INPUT:

  • weight – integer; a specific weight. If set to non-negative integer, fixes the XOR trail weight

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: from claasp.cipher_modules.models.cp.mzn_model import MznModel
sage: speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=4)
sage: cp = MznModel(speck)
sage: cp.weight_constraints(10)
(['constraint weight = 1000;'], [])
write_minizinc_model_to_file(file_path, prefix='')

Write the MiniZinc model into a file inside file_path.

INPUT:

  • file_path – string; the path of the file that will contain the model

  • prefix – str (default: ``)