Smt xor linear model

class SmtXorLinearModel(cipher, counter='sequential')

Bases: SmtModel

branch_xor_linear_constraints()

Return a variable list and SMT-LIB list asserts for branch in XOR LINEAR model.

INPUT:

  • None

EXAMPLES:

sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_linear_model import SmtXorLinearModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: smt = SmtXorLinearModel(speck)
sage: smt.branch_xor_linear_constraints()
['(assert (not (xor plaintext_0_o rot_0_0_0_i)))',
 '(assert (not (xor plaintext_1_o rot_0_0_1_i)))',
 ...
 '(assert (not (xor xor_2_10_14_o cipher_output_2_12_30_i)))',
 '(assert (not (xor xor_2_10_15_o cipher_output_2_12_31_i)))']
build_xor_linear_trail_model(weight=- 1, fixed_variables=[])

Build the model for the search of xor differential trails.

INPUT:

  • weight – integer (default: -1); if set to non-negative integer, fixes the xor trail search to a specific weight

  • fixed_variables – list (default: []); dictionaries contain 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_positions’: [0, 1, 2, 3], | ‘binary_value’: [0, 0, 0, 0] | } | ]

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_linear_model import SmtXorLinearModel
sage: speck = SpeckBlockCipher(number_of_rounds=1)
sage: smt = SmtXorLinearModel(speck)
sage: smt.build_xor_linear_trail_model()
calculate_component_weight(component, out_suffix, output_values_dict)
property cipher_id
cipher_input_variables()

Return the list of input variables.

INPUT:

  • None

EXAMPLES:

sage: from claasp.cipher_modules.models.smt.smt_model import SmtModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: smt = SmtModel(speck)
sage: smt.cipher_input_variables()
['plaintext_0',
 'plaintext_1',
 ...
 'key_62',
 'key_63']
cipher_input_xor_linear_variables()

Return the list of input variables.

INPUT:

  • None

EXAMPLES:

sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_linear_model import SmtXorLinearModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: smt = SmtXorLinearModel(speck)
sage: smt.cipher_input_xor_linear_variables()
['plaintext_0_o',
 'plaintext_1_o',
 ...
 'key_62_o',
 'key_63_o']
find_all_xor_linear_trails_with_fixed_weight(fixed_weight, fixed_values=[], solver_name='Z3_EXT')

Return a list of solutions containing all the XOR linear trails having weight equal to fixed_weight. By default, the search removes the key schedule, if any. By default, the weight corresponds to the negative base-2 logarithm of the correlation of the trail.

INPUT:

  • fixed_weight – integer; the weight to be fixed

  • fixed_values – list (default: []); they can be created using set_fixed_variables method

  • solver_name – string (default: Z3_EXT); the name of the solver

See also

SMT standard of Cipher

EXAMPLES:

sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_linear_model import SmtXorLinearModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: smt = SmtXorLinearModel(speck)
sage: trails = smt.find_all_xor_linear_trails_with_fixed_weight(1)
sage: len(trails)
4

# including the key schedule in the model
sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_linear_model import SmtXorLinearModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: from claasp.cipher_modules.models.utils import set_fixed_variables
sage: speck = SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=4)
sage: smt = SmtXorLinearModel(speck)
sage: key = set_fixed_variables('key', 'not_equal', list(range(16)), [0] * 16)
sage: trails = smt.find_all_xor_linear_trails_with_fixed_weight(2, fixed_values=[key]) # long
sage: len(trails)
8
find_all_xor_linear_trails_with_weight_at_most(min_weight, max_weight, fixed_values=[], solver_name='Z3_EXT')

Return a list of solutions. By default, the search removes the key schedule, if any.

The list contains all the XOR linear trails having the weight lying in the interval [min_weight, max_weight].

INPUT:

  • min_weight – integer; the weight from which to start the search

  • max_weight – integer; the weight at which the search stops

  • fixed_values – list (default: []); they can be created using set_fixed_variables method

  • solver_name – string (default: Z3_EXT); the name of the solver

See also

SMT standard of Cipher

EXAMPLES:

sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_linear_model import SmtXorLinearModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: smt = SmtXorLinearModel(speck)
sage: trails = smt.find_all_xor_linear_trails_with_weight_at_most(0, 2) # long # doctest: +SKIP
sage: len(trails) # doctest: +SKIP
187

# including the key schedule in the model
sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_linear_model import SmtXorLinearModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: from claasp.cipher_modules.models.utils import set_fixed_variables
sage: speck = SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=4)
sage: smt = SmtXorLinearModel(speck)
sage: key = set_fixed_variables('key', 'not_equal', list(range(16)), [0] * 16)
sage: trails = smt.find_all_xor_linear_trails_with_weight_at_most(0, 3, fixed_values=[key])
sage: len(trails)
73
find_lowest_weight_xor_linear_trail(fixed_values=[], solver_name='Z3_EXT')

Return the solution representing a XOR LINEAR trail with the lowest possible weight. By default, the search removes the key schedule, if any. By default, the weight corresponds to the negative base-2 logarithm of the correlation of the trail.

Note

There could be more than one trail with the lowest weight. In order to find all the lowest weight trail, run find_all_xor_linear_trails_with_fixed_weight()

INPUT:

  • fixed_values – list (default: []); they can be created using set_fixed_variables method

  • solver_name – string (default: Z3_EXT); the name of the solver

See also

SMT standard of Cipher

EXAMPLES:

sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_linear_model import SmtXorLinearModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: smt = SmtXorLinearModel(speck)
sage: trail = smt.find_lowest_weight_xor_linear_trail()
sage: trail['total_weight']
1.0

# including the key schedule in the model
sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_linear_model import SmtXorLinearModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: from claasp.cipher_modules.models.utils import set_fixed_variables
sage: speck = SpeckBlockCipher(block_bit_size=16, key_bit_size=32, number_of_rounds=4)
sage: smt = SmtXorLinearModel(speck)
sage: key = set_fixed_variables('key', 'not_equal', list(range(32)), [0] * 32)
sage: trail = smt.find_lowest_weight_xor_linear_trail(fixed_values=[key])
sage: trail['total_weight']
3.0
find_one_xor_linear_trail(fixed_values=[], solver_name='Z3_EXT')

Return the solution representing a XOR linear trail. By default, the search removes the key schedule, if any. By default, the weight corresponds to the negative base-2 logarithm of the correlation of the trail.

The solution probability is almost always lower than the one of a random guess of the longest input.

INPUT:

  • fixed_values – list (default: []); they can be created using set_fixed_variables method

  • solver_name – string (default: Z3_EXT); the name of the solver

See also

SMT standard of Cipher

EXAMPLES:

sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_linear_model import SmtXorLinearModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=4)
sage: smt = SmtXorLinearModel(speck)
sage: smt.find_one_xor_linear_trail() #random
{'cipher_id': 'speck_p32_k64_o32_r4',
 'model_type': 'xor_linear',
 'solver_name': 'Z3_EXT',
 'solving_time_seconds': 0.06,
 'memory_megabytes': 19.65,
 ...
 'total_weight': 67,
 'building_time_seconds': 0.003168344497680664}

sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_linear_model import SmtXorLinearModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: from claasp.cipher_modules.models.utils import set_fixed_variables
sage: speck = SpeckBlockCipher(block_bit_size=32, key_bit_size=64, number_of_rounds=4)
sage: smt = SmtXorLinearModel(speck)
sage: key = set_fixed_variables('key', 'not_equal', list(range(64)), [0] * 64)
sage: smt.find_one_xor_linear_trail(fixed_values=[key]) #random
find_one_xor_linear_trail_with_fixed_weight(fixed_weight, fixed_values=[], solver_name='Z3_EXT')

Return the solution representing a XOR linear trail whose weight is fixed_weight. By default, the search removes the key schedule, if any. By default, the weight corresponds to the negative base-2 logarithm of the correlation of the trail.

INPUT:

  • fixed_weight – integer; the weight to be fixed

  • fixed_values – list (default: []); can be created using set_fixed_variables method

  • solver_name – string (default: cryptominisat); the name of the solver

See also

SAT Solvers

EXAMPLES:

sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_linear_model import SmtXorLinearModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: smt = SmtXorLinearModel(speck)
sage: trail = smt.find_one_xor_linear_trail_with_fixed_weight(7)
sage: trail['total_weight']
7.0

# including the key schedule in the model
sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_linear_model import SmtXorLinearModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: from claasp.cipher_modules.models.utils import set_fixed_variables
sage: speck = SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=4)
sage: smt = SmtXorLinearModel(speck)
sage: key = set_fixed_variables('key', 'not_equal', list(range(16)), [0] * 16)
sage: trail = smt.find_one_xor_linear_trail_with_fixed_weight(3, fixed_values=[key])
sage: trail['total_weight']
3.0
fix_variables_value_constraints(fixed_variables=[])

Return a list of SMT-LIB asserts for fixing variables in CIPHER and XOR DIFFERENTIAL model.

INPUT:

  • fixed_variables – list (default: []); variables in default format

EXAMPLES:

sage: from claasp.cipher_modules.models.smt.smt_model import SmtModel
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(number_of_rounds=3)
sage: smt = SmtModel(speck)
sage: smt.fix_variables_value_constraints([set_fixed_variables('plaintext', 'equal', range(4), integer_to_bit_list(5, 4, 'big'))])
['(assert (not plaintext_0))',
 '(assert plaintext_1)',
 '(assert (not plaintext_2))',
 '(assert plaintext_3)']
sage: smt.fix_variables_value_constraints([set_fixed_variables('plaintext', 'not_equal', range(4), integer_to_bit_list(5, 4, 'big'))])
['(assert (or plaintext_0 (not plaintext_1) plaintext_2 (not plaintext_3)))']
fix_variables_value_xor_linear_constraints(fixed_variables=[])

Return a variable list and SMT-LIB list asserts for fixing variables in XOR LINEAR model.

INPUT:

  • fixed_variables – list (default: []); variables in default format

EXAMPLES:

sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_linear_model import SmtXorLinearModel
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(number_of_rounds=3)
sage: smt = SmtXorLinearModel(speck)
sage: smt.fix_variables_value_xor_linear_constraints([set_fixed_variables('plaintext', 'equal', range(4), integer_to_bit_list(5, 4, 'big'))])
['(assert (not plaintext_0_o))',
 '(assert plaintext_1_o)',
 '(assert (not plaintext_2_o))',
 '(assert plaintext_3_o)']
sage: smt.fix_variables_value_xor_linear_constraints([set_fixed_variables('plaintext', 'not_equal', range(4), integer_to_bit_list(5, 4, 'big'))])
['(assert (or plaintext_0_o (not plaintext_1_o) plaintext_2_o (not plaintext_3_o)))']
get_xor_probability_constraints(bit_ids, template)
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.smt.smt_model import SmtModel
sage: speck = SpeckBlockCipher(number_of_rounds=4)
sage: smt = SmtModel(speck)
sage: smt.model_constraints()
Traceback (most recent call last):
...
ValueError: No model generated
property sboxes_ddt_templates
property sboxes_lat_templates
solve(model_type, solver_name='Z3_EXT')

Return the solution of the model using the solver_name SMT solver.

INPUT:

  • model_type – string; the model for which we want a solution. Available values are:

    • 'cipher'

    • 'xor_differential'

    • 'xor_linear'

  • solver_name – string (default: Z3_EXT); the name of the solver

See also

SMT standard of Cipher

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: from claasp.cipher_modules.models.smt.smt_model import SmtModel
sage: speck = SpeckBlockCipher(number_of_rounds=4)
sage: smt = SmtModel(speck)
sage: smt.solve('xor_differential') # random
{'cipher_id': 'speck_p32_k64_o32_r4',
 'model_type': 'xor_differential',
 'solver_name': 'Z3_EXT',
 'solving_time_seconds': 0.0,
 'memory_megabytes': 0.09,
 'components_values': {},
 'total_weight': None}
update_constraints_for_equal_type(bit_positions, bit_values, component_id, constraints, out_suffix='')
update_constraints_for_not_equal_type(bit_positions, bit_values, component_id, constraints, out_suffix='')
weight_constraints(weight)

Return a variable list and SMT-LIB list asserts representing the fixing of the total weight to the input value.

INPUT:

  • weight – integer; represents the total weight of the trail

weight_xor_linear_constraints(weight)