Smt model

SMT standard of Cipher

The target of this class is to build, solve and retrieve the solution of an SMT CNF representing some attacks on ciphers, e.g. the generic cipher inversion or the search for XOR differential trails (for SAT CNFs see the correspondent class Sat Model). SMT-LIB is the chosen standard.

This module is able to use many different SMT solvers.

For any further information, refer to the file claasp.cipher_modules.models.smt.solvers.py and to the section Available SMT solvers.

class SmtModel(cipher, counter='sequential')

Bases: object

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

mathsat_parser(output_to_parse)
yices_parser(output_to_parse)
z3_parser(output_to_parse)