Cms xor linear model¶

CMS XOR LINEAR model of a cipher¶

The target of this class is to override the methods of the superclass Sat Xor Linear Model to take the advantage given by the handling of XOR clauses in CryptoMiniSat SAT solver. Therefore, the internal format for SAT CNF clauses follows 4 rules (3 from the superclass + 1):

every variable is a string with no spaces nor dashes;

if a literal is a negation of a variable, a dash is prepended to the variable;

the separator for literals is a space;

the string 'x ' is prepended to a clause representing a XOR.

Note that only methods that do not need to introduce new variables to handle XOR operations were overridden.

For any further information, visit CryptoMiniSat - XOR clauses.

class CmsSatXorLinearModel(cipher, counter='sequential', compact=False)¶

Bases: SatXorLinearModel

branch_xor_linear_constraints()¶

Return lists of variables and clauses for branch in XOR LINEAR model.

See also

CMS XOR LINEAR model for the format.

INPUT:

None

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.cms_models.cms_xor_linear_model import CmsSatXorLinearModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: sat = CmsSatXorLinearModel(speck)
sage: sat.branch_xor_linear_constraints()
['x -plaintext_0_o rot_0_0_0_i',
 'x -plaintext_1_o rot_0_0_1_i',
 'x -plaintext_2_o rot_0_0_2_i',
 ...
 'x -xor_2_10_13_o cipher_output_2_12_29_i',
 'x -xor_2_10_14_o cipher_output_2_12_30_i',
 'x -xor_2_10_15_o cipher_output_2_12_31_i']

build_generic_sat_model_from_dictionary(component_and_model_types)¶

build_xor_linear_trail_model(weight=- 1, fixed_variables=[])¶

Build the linear model.

INPUT:

weight – integer (default: -1)
fixed_variables – list (default: [])

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: from claasp.cipher_modules.models.sat.cms_models.cms_xor_linear_model import CmsSatXorLinearModel
sage: speck = SpeckBlockCipher(number_of_rounds=22)
sage: cms = CmsSatXorLinearModel(speck)
sage: cms.build_xor_linear_trail_model()
...

calculate_component_weight(component, out_suffix, output_values_dict)¶

property cipher_id¶

find_all_xor_linear_trails_with_fixed_weight(fixed_weight, fixed_values=[], solver_name='CRYPTOMINISAT_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: CRYPTOMINISAT_EXT); the name of the solver

See also

SAT Solvers

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_linear_model import SatXorLinearModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: sat = SatXorLinearModel(speck)
sage: trails = sat.find_all_xor_linear_trails_with_fixed_weight(1)
sage: len(trails) == 4
True

# including the key schedule in the model
sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_linear_model import SatXorLinearModel
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: sat = SatXorLinearModel(speck)
sage: key = set_fixed_variables('key', 'not_equal', list(range(16)), [0] * 16)
sage: trails = sat.find_all_xor_linear_trails_with_fixed_weight(2, fixed_values=[key])
sage: len(trails) == 8
True

find_all_xor_linear_trails_with_weight_at_most(min_weight, max_weight, fixed_values=[], solver_name='CRYPTOMINISAT_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: []); can be created using set_fixed_variables method
solver_name – string (default: CRYPTOMINISAT_EXT); the name of the solver

See also

SAT Solvers

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_linear_model import SatXorLinearModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: sat = SatXorLinearModel(speck)
sage: trails = sat.find_all_xor_linear_trails_with_weight_at_most(0, 2) # long
sage: len(trails) == 187
True

# including the key schedule in the model
sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_linear_model import SatXorLinearModel
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: sat = SatXorLinearModel(speck)
sage: key = set_fixed_variables('key', 'not_equal', list(range(16)), [0] * 16)
sage: trails = sat.find_all_xor_linear_trails_with_weight_at_most(0, 3, fixed_values=[key]) # long
sage: len(trails) == 73
True

find_lowest_weight_xor_linear_trail(fixed_values=[], solver_name='CRYPTOMINISAT_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: []); can be created using set_fixed_variables method
solver_name – string (default: CRYPTOMINISAT_EXT); the name of the solver

See also

SAT Solvers

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_linear_model import SatXorLinearModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: sat = SatXorLinearModel(speck)
sage: trail = sat.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.sat.sat_models.sat_xor_linear_model import SatXorLinearModel
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: sat = SatXorLinearModel(speck)
sage: key = set_fixed_variables('key', 'not_equal', list(range(32)), [0] * 32)
sage: trail = sat.find_lowest_weight_xor_linear_trail(fixed_values=[key])
sage: trail['total_weight']
3.0

find_one_xor_linear_trail(fixed_values=[], solver_name='CRYPTOMINISAT_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: CRYPTOMINISAT_EXT); the name of the solver

See also

SAT Solvers

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_linear_model import SatXorLinearModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=4)
sage: sat = SatXorLinearModel(speck)
sage: sat.find_one_xor_linear_trail() # random
{'cipher_id': 'speck_p32_k64_o32_r4',
 'model_type': 'xor_linear',
 'solver_name': 'cryptominisat',
 'solving_time_seconds': 0.01,
 'memory_megabytes': 7.2,
 ...
 'status': 'SATISFIABLE',
 'building_time_seconds': 0.010079622268676758}

# including the key schedule in the model
sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_linear_model import SatXorLinearModel
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(number_of_rounds=4)
sage: sat = SatXorLinearModel(speck)
sage: key = set_fixed_variables('key', 'not_equal', list(range(64)), [0] * 64)
sage: sat.find_one_xor_linear_trail(fixed_values=[key]) # random

find_one_xor_linear_trail_with_fixed_weight(fixed_weight, fixed_values=[], solver_name='CRYPTOMINISAT_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_EXT); the name of the solver

See also

SAT Solvers

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_linear_model import SatXorLinearModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: sat = SatXorLinearModel(speck)
sage: trail = sat.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.sat.sat_models.sat_xor_linear_model import SatXorLinearModel
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: sat = SatXorLinearModel(speck)
sage: key = set_fixed_variables('key', 'not_equal', list(range(16)), [0] * 16)
sage: trail = sat.find_one_xor_linear_trail_with_fixed_weight(3, fixed_values=[key])
sage: trail['total_weight']
3.0

static fix_variables_value_constraints(fixed_variables=[])¶

Return lists of variables and clauses for fixing variables in CIPHER model.

See also

SAT standard of Cipher for the format.

INPUT:

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

EXAMPLES:

sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: from claasp.cipher_modules.models.sat.sat_model import SatModel
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: sat = SatModel(speck)
sage: fixed_variables = [{
....:    'component_id': 'plaintext',
....:    'constraint_type': 'equal',
....:    'bit_positions': [0, 1, 2, 3],
....:    'bit_values': [1, 0, 1, 1]
....: }, {
....:    'component_id': 'ciphertext',
....:    'constraint_type': 'not_equal',
....:    'bit_positions': [0, 1, 2, 3],
....:    'bit_values': [1, 1, 1, 0]
....: }]
sage: SatModel.fix_variables_value_constraints(fixed_variables)
['plaintext_0',
 '-plaintext_1',
 'plaintext_2',
 'plaintext_3',
 '-ciphertext_0 -ciphertext_1 -ciphertext_2 ciphertext_3']

static fix_variables_value_xor_linear_constraints(fixed_variables=[])¶

Return lists variables and clauses for fixing variables in XOR LINEAR model.

See also

SAT standard of Cipher for the format

INPUT:

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

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_linear_model import SatXorLinearModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: sat = SatXorLinearModel(speck)
sage: fixed_variables = [{
....:    'component_id': 'plaintext',
....:    'constraint_type': 'equal',
....:    'bit_positions': [0, 1, 2, 3],
....:    'bit_values': [1, 0, 1, 1]
....: }, {
....:    'component_id': 'ciphertext',
....:    'constraint_type': 'not_equal',
....:    'bit_positions': [0, 1, 2, 3],
....:    'bit_values': [1, 1, 1, 0]
....: }]
sage: SatXorLinearModel.fix_variables_value_xor_linear_constraints(fixed_variables)
['plaintext_0_o',
 '-plaintext_1_o',
 'plaintext_2_o',
 'plaintext_3_o',
 '-ciphertext_0_o -ciphertext_1_o -ciphertext_2_o ciphertext_3_o']

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.sat.sat_model import SatModel
sage: speck = SpeckBlockCipher(number_of_rounds=4)
sage: sat = SatModel(speck)
sage: sat.model_constraints('xor_differential')
Traceback (most recent call last):
...
ValueError: No model generated

property sboxes_ddt_templates¶

property sboxes_lat_templates¶

solve(model_type, solver_name='CRYPTOMINISAT_EXT', options=None)¶

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

Note

Two types of solvers can be chosen: external or internal. In the following list of inputs, allowed SAT solvers are listed. Those ending with _sage will not create a subprocess nor additional files and will work completely embedded in Sage. Remaining solvers are allowed, but they need to be installed in the system.

INPUT:

model_type – string; the model for which we want a solution. Available values are:
- 'cipher'
- 'xor_differential'
- 'xor_linear'
solver_name – string (default: cryptominisat); the name of the solver

See also

SAT Solvers

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.sat_models.sat_cipher_model import SatCipherModel
sage: from claasp.ciphers.block_ciphers.tea_block_cipher import TeaBlockCipher
sage: tea = TeaBlockCipher(number_of_rounds=32)
sage: sat = SatCipherModel(tea)
sage: sat.build_cipher_model()
sage: sat.solve('cipher') # random
{'cipher_id': 'tea_p64_k128_o64_r32',
 'model_type': 'tea_p64_k128_o64_r32',
 'solver_name': 'CRYPTOMINISAT_EXT',
 ...
  'intermediate_output_31_15': {'value': '8ca8d5de0906f08e', 'weight': 0, 'sign': 1},
  'cipher_output_31_16': {'value': '8ca8d5de0906f08e', 'weight': 0, 'sign': 1}},
 'total_weight': 0,
 'status': 'SATISFIABLE'}}

weight_constraints(weight)¶

Return lists of variables and constraints that fix the total weight of the trail to a specific value.

INPUT:

weight – integer; the total weight of the trail

EXAMPLES:

sage: from claasp.cipher_modules.models.sat.sat_models.sat_xor_differential_model import SatXorDifferentialModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=3)
sage: sat = SatXorDifferentialModel(speck)
sage: sat.build_xor_differential_trail_model()
sage: sat.weight_constraints(7)
(['dummy_hw_0_0_0',
  'dummy_hw_0_0_1',
  'dummy_hw_0_0_2',
  ...
  '-dummy_hw_0_77_6 dummy_hw_0_78_6',
  '-hw_modadd_2_7_14 -dummy_hw_0_77_6',
  '-hw_modadd_2_7_15 -dummy_hw_0_78_6'])

weight_xor_linear_constraints(weight)¶

Cms xor linear model¶

CMS XOR LINEAR model of a cipher¶

Table of Contents

Previous topic

Next topic

This Page