arxpy.smt.search_impossible module

Search for impossible differentials (ID) by modeling the search as a SMT problem.

class arxpy.smt.search_impossible.KeySetting

Bases: enum.Enum

Represent the different types of ID of block ciphers.

class arxpy.smt.search_impossible.SearchMode

Bases: enum.Enum

Represent the different options for searching ID

FirstID

returns the first ID found by iteratively searching with increasing number of active bits. The ID found is returned as a IDFound object. If none is found, None is returned.

AllID

similar to FirstID, but the search is not stopped after the first ID, and all found ID are printed.

class arxpy.smt.search_impossible.ActivationMode

Bases: enum.Enum

Represent the different options to consider when activating.

Default

no restrictions

SingleBit

activates at most one bit in each word

MSBbit

activates at most the MSB in each word

Zero

all words are set to zero

arxpy.smt.search_impossible.generate_active_bvlists(list_width, num_active_bits, active_bits_mode)

Generate all bitvector list with given width, number of active bits and activation mode.

>>> list(generate_active_bvlists([2, 2], 1, active_bits_mode=ActivationMode.Default))
[[0b01, 0b00], [0b10, 0b00], [0b00, 0b01], [0b00, 0b10]]
>>> list(generate_active_bvlists([2, 2], 1, active_bits_mode=ActivationMode.SingleBit))
[[0b01, 0b00], [0b00, 0b01]]

class arxpy.smt.search_impossible.IDFound(ch, input_diff_found, output_diff_found)

Bases: object

Represent (non-symbolic) ID found over a BvCharacteristic.

ch

the associated symbolic differential characteristic

input_diff

a list, where the i-th element is a pair containing the i-th input symbolic difference and its value

output_diff

a list, where the i-th element is a pair containing the i-th output symbolic difference and its value

>>> from arxpy.bitvector.operation import BvComp
>>> from arxpy.differential.difference import XorDiff, RXDiff
>>> from arxpy.differential.characteristic import BvCharacteristic
>>> from arxpy.primitives.chaskey import ChaskeyPi
>>> from arxpy.smt.search_impossible import SearchID
>>> ChaskeyPi.set_rounds(1)
>>> ch = BvCharacteristic(ChaskeyPi, XorDiff, ["dv0", "dv1", "dv2", "dv3"])
>>> search_problem = SearchID(ch)
>>> id_found = search_problem.solve(2)
>>> id_found.input_diff  
[[XorDiff(dv0), XorDiff(0x00000001)], [XorDiff(dv1), XorDiff(0x00000000)],
[XorDiff(dv2), XorDiff(0x00000000)], [XorDiff(dv3), XorDiff(0x00000000)]]
>>> id_found.output_diff  
[[XorDiff(d7), XorDiff(0x00000001)], [XorDiff(d12), XorDiff(0x00000000)],
[XorDiff(d13), XorDiff(0x00000000)], [XorDiff(d9), XorDiff(0x00000000)]]
>>> print(id_found)  
{'input_diff': [[dv0, 0x00000001], [dv1, 0x00000000], [dv2, 0x00000000], [dv3, 0x00000000]],
'output_diff': [[d7, 0x00000001], [d12, 0x00000000], [d13, 0x00000000], [d9, 0x00000000]]}
>>> ch = BvCharacteristic(ChaskeyPi, RXDiff, ["dv0", "dv1", "dv2", "dv3"])
>>> search_problem = SearchID(ch)
>>> id_found = search_problem.solve(2)
>>> id_found.input_diff  
[[RXDiff(dv0), RXDiff(0x00000001)], [RXDiff(dv1), RXDiff(0x00000000)],
[RXDiff(dv2), RXDiff(0x00000000)], [RXDiff(dv3), RXDiff(0x00000000)]]
>>> id_found.output_diff  
[[RXDiff(d7), RXDiff(0x00000001)], [RXDiff(d12), RXDiff(0x00000000)],
[RXDiff(d13), RXDiff(0x00000000)], [RXDiff(d9), RXDiff(0x00000000)]]
>>> print(id_found)  
{'input_diff': [[dv0, 0x00000001], [dv1, 0x00000000], [dv2, 0x00000000], [dv3, 0x00000000]],
'output_diff': [[d7, 0x00000001], [d12, 0x00000000], [d13, 0x00000000], [d9, 0x00000000]]}

check_empirical_weight(verbose_lvl=0, filename=None)

Check the empirical weight is math.inf.

If the empirical weight is not math.inf, an ExactWeightError exception is raised.

If filename is not None, the output will be printed to the given file rather than the to stdout.

The argument verbose_lvl can also take the values 1 and 2 for a more detailed output.

vrepr()

Return a verbose dictionary-like representation of the ID.

>>> from arxpy.differential.difference import XorDiff
>>> from arxpy.differential.characteristic import BvCharacteristic
>>> from arxpy.primitives.chaskey import ChaskeyPi
>>> from arxpy.smt.search_impossible import SearchID
>>> ChaskeyPi.set_rounds(1)
>>> ch = BvCharacteristic(ChaskeyPi, XorDiff, ["dv0", "dv1", "dv2", "dv3"])
>>> search_problem = SearchID(ch)
>>> id_found = search_problem.solve(2)
>>> print(id_found.vrepr())  
{'input_diff': [[XorDiff(Variable('dv0', width=32)), XorDiff(Constant(0b00000000000000000000000000000001, width=32))],
[XorDiff(Variable('dv1', width=32)), XorDiff(Constant(0b00000000000000000000000000000000, width=32))],
[XorDiff(Variable('dv2', width=32)), XorDiff(Constant(0b00000000000000000000000000000000, width=32))],
[XorDiff(Variable('dv3', width=32)), XorDiff(Constant(0b00000000000000000000000000000000, width=32))]],
'output_diff': [[XorDiff(Variable('d7', width=32)), XorDiff(Constant(0b00000000000000000000000000000001, width=32))],
[XorDiff(Variable('d12', width=32)), XorDiff(Constant(0b00000000000000000000000000000000, width=32))],
[XorDiff(Variable('d13', width=32)), XorDiff(Constant(0b00000000000000000000000000000000, width=32))],
[XorDiff(Variable('d9', width=32)), XorDiff(Constant(0b00000000000000000000000000000000, width=32))]]}

srepr()

Return a short representation of the ID.

class arxpy.smt.search_impossible.SkIDFound(ch, input_diff_found, output_diff_found)

Bases: arxpy.smt.search_impossible.IDFound

Represent (non-symbolic) single-key ID found over a SingleKeyCh.

See also IDFound.

>>> from arxpy.differential.difference import XorDiff
>>> from arxpy.differential.characteristic import SingleKeyCh
>>> from arxpy.smt.search_impossible import SearchSkID
>>> from arxpy.primitives import speck
>>> Speck32 = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64)
>>> Speck32.set_rounds(1)
>>> ch = SingleKeyCh(Speck32, XorDiff)
>>> search_problem = SearchSkID(ch)
>>> id_found = search_problem.solve(2)
>>> id_found.input_diff
[[XorDiff(dp0), XorDiff(0x0001)], [XorDiff(dp1), XorDiff(0x0000)]]
>>> id_found.output_diff
[[XorDiff(dx2), XorDiff(0x0001)], [XorDiff(dx4), XorDiff(0x0000)]]
>>> print(id_found)
{'input_diff': [[dp0, 0x0001], [dp1, 0x0000]], 'output_diff': [[dx2, 0x0001], [dx4, 0x0000]]}

check_empirical_weight(verbose_lvl=0, filename=None)

Check the empirical weight is math.inf for many keys.

If the empirical weight is not math.inf for some key, an ExactWeightError exception is raised.

If filename is not None, the output will be printed to the given file rather than the to stdout.

The argument verbose_lvl can also take the values 1 and 2 for a more detailed output.

class arxpy.smt.search_impossible.RkIDFound(rkch, key_input_diff_found, enc_input_diff_found, enc_output_diff_found)

Bases: object

Represent (non-symbolic) related-key ID found over a RelatedKeyCh.

rkch

the associated symbolic RelatedKeyCh

key_id_found

a IDFound denoting the ID over the key schedule

enc_id_found

a IDFound denoting the ID over the encryption

>>> from arxpy.differential.difference import XorDiff
>>> from arxpy.differential.characteristic import RelatedKeyCh
>>> from arxpy.smt.search_impossible import SearchRkID
>>> from arxpy.primitives import speck
>>> Speck32 = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64)
>>> Speck32.set_rounds(1)
>>> rkch = RelatedKeyCh(Speck32, XorDiff)
>>> search_problem = SearchRkID(rkch)
>>> rkid_found = search_problem.solve(2)
>>> rkid_found.key_id_found.input_diff
[[XorDiff(dmk0), XorDiff(0x0001)]]
>>> rkid_found.enc_id_found.input_diff
[[XorDiff(dp0), XorDiff(0x0000)], [XorDiff(dp1), XorDiff(0x0000)]]
>>> rkid_found.enc_id_found.output_diff
[[XorDiff(dx2), XorDiff(0x0001)], [XorDiff(dx4), XorDiff(0x0000)]]
>>> print(rkid_found)
{'enc_id_found': {'input_diff': [[dp0, 0x0000], [dp1, 0x0000]],
                  'output_diff': [[dx2, 0x0001], [dx4, 0x0000]]},
 'key_id_found': {'input_diff': [[dmk0, 0x0001]], 'output_diff': []}}

check_empirical_weight(verbose_lvl=0, filename=None)

Check the empirical weight is math.inf for many keys.

If the empirical weight is not math.inf for some key, an ExactWeightError exception is raised.

If filename is not None, the output will be printed to the given file rather than the to stdout.

The argument verbose_lvl can also take the values 1 and 2 for a more detailed output.

vrepr()

Return a verbose dictionary-like representation of the ID.

See also IDFound.vrepr.

srepr()

Return a short representation of the ID.

class arxpy.smt.search_impossible.SearchID(ch, initial_constraints=None)

Bases: arxpy.smt.search_differential.SearchCh

Represent the problem of finding an ID over a BvCharacteristic.

Parameters

ch (BvCharacteristic) – a symbolic characteristic of a BvFunction

See also SearchCh.

>>> from arxpy.bitvector.core import Variable
>>> from arxpy.differential.difference import XorDiff
>>> from arxpy.differential.characteristic import BvCharacteristic
>>> from arxpy.smt.search_impossible import SearchID
>>> from arxpy.primitives.chaskey import ChaskeyPi
>>> ChaskeyPi.set_rounds(1)
>>> ch = BvCharacteristic(ChaskeyPi, XorDiff, ["dv0", "dv1", "dv2", "dv3"])
>>> search_problem = SearchID(ch)
>>> search_problem.formula_size()
142
>>> search_problem.error()
0
>>> print(search_problem.hrepr(False))
assert 0x00000000 == ((~(... << ...) ^ (d0 << 0x00000001)) & (~(... << ...) ^ (dv1 << 0x00000001)) & ((dv0 << 0x00000001) ^ d0 ^ dv0 ^ dv1))
assert 0x00000000 == ((~(... << ...) ^ (d4 << 0x00000001)) & (~(... << ...) ^ (dv3 << 0x00000001)) & ((dv2 << 0x00000001) ^ d4 ^ dv2 ^ dv3))
assert 0x00000000 == ((~(... << ...) ^ (d7 << 0x00000001)) & (~(... << ...) ^ ((... ^ ...) << 0x00000001)) & (((d0 <<< 16) << 0x00000001) ^ d7 ^ ... ^ ... ^ (... <<< ...)))
assert 0x00000000 == ((~(... << ...) ^ (d10 << 0x00000001)) & (~(... << ...) ^ (d4 << 0x00000001)) & (((d0 ^ (... <<< ...)) << 0x00000001) ^ d10 ^ d4 ^ ... ^ ...))
assert 0b0 == w
check-unsat

hrepr(full_repr=False)

Return a human readable representing of the SMT problem.

If full_repr is False, the short string representation srepr is used.

extend(id_found, solver_name, check, verbose_level, filename)

Extend the ID by appending a characteristic with probability one.

solve(initial_active_bits, solver_name='btor', search_mode=<SearchMode.FirstID: 1>, input_diff_mode=<ActivationMode.Default: 1>, output_diff_mode=<ActivationMode.Default: 1>, to_extend=False, check=False, verbose_level=0, filename=None)

Solve the SMT problem associated to the search of an ID over a BvCharacteristic.

Parameters

• initial_active_bits (int) – the initial number of active bits in the input and output

• solver_name (str) – the name of the solver (according to pySMT) to be used

• search_mode (SearchMode) – one of the search modes available

• input_diff_mode (ActivationMode) – the diff-mode for the input difference

• output_diff_mode (ActivationMode) – the diff-mode for the output difference

• check (bool) – if True, IDFound.check_empirical_weight will be called after an ID is found. If it is not valid, the search will continue.

• verbose_level (int) – an integer between 0 (no verbose) and 3 (full verbose).

• filename (str) – if not None, the output will be printed to the given file rather than the to stdout.

class arxpy.smt.search_impossible.SearchSkID(skch, initial_constraints=None)

Bases: arxpy.smt.search_impossible.SearchID

Represent the problem of finding an single-key ID over a SingleKeyCh.

Parameters

skch (SingleKeyCh) – a symbolic single-key characteristic of a Cipher

See also SearchID.

>>> from arxpy.differential.difference import XorDiff
>>> from arxpy.differential.characteristic import SingleKeyCh
>>> from arxpy.smt.search_impossible import SearchSkID
>>> from arxpy.primitives import speck
>>> Speck32 = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64)
>>> Speck32.set_rounds(1)
>>> ch = SingleKeyCh(Speck32, XorDiff)
>>> search_problem = SearchSkID(ch)
>>> search_problem.formula_size()
35
>>> search_problem.error()
0
>>> print(search_problem.hrepr(False))
assert 0x0000 == ((~(... << ...) ^ (dx1 << 0x0001)) & (~(... << ...) ^ ((... >>> ...) << 0x0001)) & ((dp1 << 0x0001) ^ dx1 ^ dp1 ^ (... >>> ...)))
assert 0b0 == w
check-unsat
>>> print(search_problem.solve(2))
{'input_diff': [[dp0, 0x0001], [dp1, 0x0000]], 'output_diff': [[dx2, 0x0001], [dx4, 0x0000]]}

extend(id_found, solver_name, check, verbose_level, filename)

Extend the ID by appending a characteristic with probability one.

class arxpy.smt.search_impossible.SearchRkID(rkch, initial_key_constraints=None, initial_enc_constraints=None)

Bases: arxpy.smt.search_differential.SearchRkCh

Represent the problem of finding a related-key ID over a RelatedKeyCh.

Parameters

rkch (RelatedKeyCh) – a symbolic related-key characteristic of a Cipher

See also SearchID.

>>> from arxpy.differential.difference import XorDiff
>>> from arxpy.differential.characteristic import RelatedKeyCh
>>> from arxpy.smt.search_impossible import SearchRkID
>>> from arxpy.primitives import speck
>>> Speck32 = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64)
>>> Speck32.set_rounds(1)
>>> ch = RelatedKeyCh(Speck32, XorDiff)
>>> search_problem = SearchRkID(ch)
>>> search_problem.formula_size()
38
>>> print(search_problem.hrepr(False))
assert 0b0 == wk
assert 0x0000 == ((~(... << ...) ^ (dx1 << 0x0001)) & (~(... << ...) ^ ((... >>> ...) << 0x0001)) & ((dp1 << 0x0001) ^ dx1 ^ dp1 ^ (... >>> ...)))
assert 0b0 == w
check-unsat
>>> print(search_problem.solve(2))
{'enc_id_found': {'input_diff': [[dp0, 0x0000], [dp1, 0x0000]],
                  'output_diff': [[dx2, 0x0001], [dx4, 0x0000]]},
 'key_id_found': {'input_diff': [[dmk0, 0x0001]], 'output_diff': []}}

hrepr(full_repr=False)

Return a human readable representing of the SMT problem.

See also SearchID.hrepr.

solve(initial_active_bits, solver_name='btor', search_mode=<SearchMode.FirstID: 1>, key_input_diff_mode=<ActivationMode.Default: 1>, enc_input_diff_mode=<ActivationMode.Default: 1>, enc_output_diff_mode=<ActivationMode.Default: 1>, to_extend=False, check=False, verbose_level=0, filename=None)

Solve the SMT problem associated to the search of an ID over a RelatedKeyCh.

Parameters

• initial_active_bits (int) – the initial number of active bits in the input and output

• solver_name (str) – the name of the solver (according to pySMT) to be used

• search_mode (SearchMode) – one of the search modes available

• key_input_diff_mode (ActivationMode) – the diff-mode for the master key difference

• enc_input_diff_mode (ActivationMode) – the diff-mode for the plaintext difference

• enc_output_diff_mode (ActivationMode) – the diff-mode for the ciphertext difference

• check (bool) – if True, IDFound.check_empirical_weight will be called after an ID is found. If it is not valid, the search will continue.

• verbose_level (int) – an integer between 0 (no verbose) and 3 (full verbose).

• filename (str) – if not None, the output will be printed to the given file rather than the to stdout.

arxpy.smt.search_impossible.round_based_search_ID(cipher, diff_type, initial_active_bits, solver_name, start_round, end_round, search_mode, input_diff_mode, output_diff_mode, check, verbose_level, filename, to_extend=False)

Find single-key impossible differentials over multiple rounds.

Parameters

• cipher (Cipher) – an (iterated) cipher

• diff_type (Difference) – a type of difference

• initial_active_bits (int) – the initial number of active bits for starting the iterative search

• solver_name (str) – the name of the solver (according to pySMT) to be used

• start_round (int) – the minimum number of rounds to consider

• end_round (int) – the maximum number of rounds to consider

• search_mode (SearchMode) – one of the search modes available

• input_diff_mode – (ActivationMode): the diff-mode for the input difference

• output_diff_mode – (ActivationMode): the diff-mode for the output difference

• check (bool) – if True, check_empirical_weight will be called after an ID is found.

• verbose_level (int) – an integer between 0 (no verbose) and 3 (full verbose).

• filename (str) – if not None, the output will be printed to the given file rather than the to stdout.

• from arxpy.differential.difference import XorDiff, RXDiff (>>>) –

• from arxpy.smt.search_impossible import round_based_search_ID, KeySetting, SearchMode, ActivationMode (>>>) –

• from arxpy.primitives import speck (>>>) –

• Speck32 = speck.get_Speck_instance (>>>) –

• round_based_search_ID(Speck32, XorDiff, 2, "btor", 1, 2, SearchMode.FirstID, (>>>) –

• ActivationMode.Default, ActivationMode.Default, False, 0, None) # doctest (..) – +ELLIPSIS

• rounds (Num) – 1

• found (ID) –

• 0000 -> 0001 0000 (0001) –

• <BLANKLINE> –

• rounds – 2

• found –

• 0000 -> 0001 0000 –

arxpy.smt.search_impossible.round_based_search_RkID(cipher, diff_type, initial_active_bits, solver_name, start_round, end_round, search_mode, key_input_diff_mode, enc_input_diff_mode, enc_output_diff_mode, check, verbose_level, filename, to_extend=False)

Find related-key impossible differentials over multiple rounds.

Parameters

• cipher (Cipher) – an (iterated) cipher

• diff_type (Difference) – a type of difference

• initial_active_bits (int) – the initial number of active bits for starting the iterative search

• solver_name (str) – the name of the solver (according to pySMT) to be used

• start_round (int) – the minimum number of rounds to consider

• end_round (int) – the maximum number of rounds to consider

• search_mode (SearchMode) – one of the search modes available

• key_input_diff_mode – (ActivationMode): the diff-mode for the master key difference

• enc_input_diff_mode – (ActivationMode): the diff-mode for the plaintext difference

• enc_output_diff_mode – (ActivationMode): the diff-mode for the ciphertext difference

• check (bool) – if True, check_empirical_weight will be called after an ID is found.

• verbose_level (int) – an integer between 0 (no verbose) and 3 (full verbose).

• filename (str) – if not None, the output will be printed to the given file rather than the to stdout.

• from arxpy.differential.difference import XorDiff, RXDiff (>>>) –

• from arxpy.smt.search_impossible import round_based_search_RkID, KeySetting, SearchMode, ActivationMode (>>>) –

• from arxpy.primitives import speck (>>>) –

• Speck32 = speck.get_Speck_instance (>>>) –

• round_based_search_RkID(Speck32, XorDiff, 2, "btor", 1, 2, SearchMode.FirstID, ActivationMode.Default, (>>>) –

• ActivationMode.Default, ActivationMode.Default, False, 0, None) # doctest (..) – +ELLIPSIS

• rounds (Num) – 1

• found (ID) –

• K – 0001 -> | E: 0000 0000 -> 0001 0000

• <BLANKLINE> –

• rounds – 2

• found –

• K – 0001 0000 -> | E: 0000 0000 -> 0001 0000