Cms cipher model

CMS cipher model of a cipher

The target of this class is to override the methods of the superclass Sat Cipher 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 CmsSatCipherModel(cipher, counter='sequential', compact=False)

Bases: SatCipherModel

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.cipher_modules.models.sat.cms_models.cms_cipher_model import CmsSatCipherModel
sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=22)
sage: cms = CmsSatCipherModel(speck)
sage: cms.build_cipher_model()

build_generic_sat_model_from_dictionary(fixed_variables, component_and_model_types)

calculate_component_weight(component, out_suffix, output_values_dict)

property cipher_id

find_missing_bits(fixed_values=[], solver_name='CRYPTOMINISAT_EXT')

Return the solution representing a generic flow of the cipher from plaintext and key to ciphertext.

INPUT:

• 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.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher
sage: speck = SpeckBlockCipher(number_of_rounds=22)
sage: from claasp.cipher_modules.models.sat.sat_models.sat_cipher_model import SatCipherModel
sage: sat = SatCipherModel(speck)
sage: from claasp.cipher_modules.models.utils import set_fixed_variables, integer_to_bit_list
sage: ciphertext = set_fixed_variables(
....:         component_id=speck.get_all_components_ids()[-1],
....:         constraint_type='equal',
....:         bit_positions=range(32),
....:         bit_values=integer_to_bit_list(endianness='big', list_length=32, int_value=0xaffec7ed))
sage: sat.find_missing_bits(fixed_values=[ciphertext]) # random
{'cipher_id': 'speck_p32_k64_o32_r22',
 'model_type': 'cipher',
 'solver_name': 'CRYPTOMINISAT_EXT',
 ...
  'intermediate_output_21_11': {'value': '1411'},
  'cipher_output_21_12': {'value': 'affec7ed'}},
 'total_weight': None,
 'status': 'SATISFIABLE',
 'building_time_seconds': 0.019376516342163086}

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']

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'])