Minizinc cipher model

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

Bases: MinizincModel

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)
build_cipher_model(fixed_variables=[])

Build the cipher model.

INPUT:

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

See also

set_fixed_variables()

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: from claasp.cipher_modules.models.minizinc.minizinc_models.minizinc_cipher_model import MinizincCipherModel
sage: speck = SpeckBlockCipher(number_of_rounds=22)
sage: minizinc = MinizincCipherModel(speck)
sage: minizinc.build_cipher_model()
...
property cipher
property cipher_id
fix_variables_value_constraints(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.minizinc.minizinc_models.minizinc_xor_differential_model import MinizincXorDifferentialModel
sage: from claasp.ciphers.block_ciphers.raiden_block_cipher import RaidenBlockCipher
sage: raiden = RaidenBlockCipher(number_of_rounds=1)
sage: minizinc = MinizincXorDifferentialModel(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(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(fixed_variables)[0]
'constraint plaintext_y0+plaintext_y1+plaintext_y2+plaintext_y3>0;'
property model_constraints

Return the model specified by model_type.

If the key refers to one of the available solver, Otherwise will raise a KeyError exception.

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.minizinc.minizinc_model import MinizincModel
sage: speck = SpeckBlockCipher(number_of_rounds=4)
sage: minizinc = MinizincModel(speck)
sage: minizinc.model_constraints('xor_differential')
Traceback (most recent call last):
...
ValueError: No model generated
output_probability_per_round()
solve(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.minizinc.minizinc_models.minizinc_xor_differential_model import MinizincXorDifferentialModel
sage: speck = SpeckBlockCipher(number_of_rounds=5, block_bit_size=32, key_bit_size=64)
sage: minizinc = MinizincXorDifferentialModel(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('Xor')
sage: result.statistics['nSolutions']
1
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: ``)