arxpy.smt.search_differential module

Search for characteristics by modeling the search as a SMT problem.

class arxpy.smt.search_differential.DerMode[source]

Bases: enum.Enum

Represent the different constraints available for the derivative weights of a characteristic.

Default

no additional constraint is added

ProbabilityOne

fix all derivative weights to zero

Valid

only the validity constraint is added (weight is ignored)

XDCA_Approx

for the weights of XDCA, the precision is set to 0

class arxpy.smt.search_differential.ChSearchMode[source]

Bases: enum.Enum

Represent the different options for searching BvCharacteristic.

A characteristic is said to be valid if its weight \(w = - \log_2(p)\), where p is the probability of the characteristic, is lower than the bit-size of the input difference.

A derivative weight is said to be non-exact if its weight does not match its exact weight.

FirstCh

returns the 1st characteristic found by iteratively searching with increasing weight. The characteristic found is returned as a ChFound object, but it may not have optimal theoretical weight if it contains a non-exact derivative weight or it may be empirically invalid. If no characteristic is found, None is returned.

FirstChValid

similar to FirstCh, but if the characteristic found is empirically invalid (after computing its empirical weight), the search continues.

Optimal

similar to FirstCh, but several characteristics are found to ensure that the one returned has the optimal theoretical weight. (only differs from FirstCh if there is a non-exact derivative weight).

OptimalDifferential

similar to Optimal, but once a characteristic is found, only characteristics with different input/output differences are searched.

AllOptimal

similar to Optimal, but the search never stops.

TopDifferentials

searches for MAX_CH_FOUND characteristics (as in FirstCh) and return the differentials obtained by gathering those characteristics.

AllValid

a non-stop search of valid characteristics with no additional constraints.

class arxpy.smt.search_differential.SkChSearchMode[source]

Bases: enum.Enum

Represent the different options for searching SingleKeyCh.

The options are the same as ChSearchMode, but SkChFound objects are returned instead of ChFound.

class arxpy.smt.search_differential.RkChSearchMode[source]

Bases: enum.Enum

Represent the different options for searching RelatedKeyCh.

A related-key characteristic is said to be valid if its encryption weight is lower than the bit-size of the plaintext difference and its key schedule weight is lower than the bit-size of the master-key difference.

FirstMinSum

returns the 1st related-key characteristic found by iteratively searching with increasing weight, where the weight is taken as the sum of the key schedule weight and the encryption weight. The characteristic found is returned as a RkChFound object, but it may not have optimal theoretical weight if it it contains a non-exact derivative weight or it may be empirically invalid. If no characteristic is found, None is returned.

FirstMinSumValid

similar to FirstMinSum, but if the characteristic found is empirically invalid (after computing its empirical weight), the search continues.

OptimalMinSum

similar to FirstMinSum, but several characteristics are found to ensure that the one returned has the optimal theoretical weight. (only differs from FirstMinSum if there is a non-exact derivative weight).

OptimalMinSumDifferential

similar to OptimalMinSum, but once a characteristic is found, only characteristics with different input/output differences are searched. (to ensure optimality).

FirstValidKeyMinEnc

similar to FirstMinSum, but the weight is taken as the encryption weight and the key schedule weight is restricted to be smaller than the key size.

FirstValidKeyMinEncValid

similar to FirstMinSumValid, but the weight is defined as FirstValidKeyMinEnc.

OptimalValidKeyMinEnc

similar to OptimalMinSum, but the weight is defined as FirstValidKeyMinEnc.

OptimalValidKeyMinEncDifferential

similar to OptimalMinSumDifferential, but the weight is defined as FirstValidKeyMinEnc.

FirstFixEncMinKey

similar to FirstMinSum, but the weight is taken as the key schedule weight and the encryption weight is fixed to a given value.

FirstFixEncMinKeyValid

similar to FirstMinSumValid, but the weight is defined as FirstFixEncMinKey.

OptimalFixEncMinKey

similar to OptimalMinSum, but the weight is defined as FirstFixEncMinKey.

OptimalFixEncMinKeyDifferential

similar to OptimalMinSumDifferential, but the weight is defined as FirstFixEncMinKey.

AllOptimalMinSum

similar to OptimalMinSum, but the search never stops.

AllValid

a non-stop search of valid characteristics with no additional constraints.

exception arxpy.smt.search_differential.ExactWeightError[source]

Bases: Exception

The exception raised in ChFound.check_empirical_weight and similar functions.

class arxpy.smt.search_differential.ChFound(ch, ch_weight, der_weights, model, aux_model=None)[source]

Bases: object

Represent (non-symbolic) characteristics found.

ch

the associated symbolic characteristic

ch_weight

a Constant denoting the the characteristic weight

der_weights

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

input_diff

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

nonlinear_diffs

aa list, where the i-th element is a pair containing the i-th non-linear 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_differential import SearchCh
>>> ChaskeyPi.set_rounds(1)
>>> ch = BvCharacteristic(ChaskeyPi, XorDiff, ["dv0", "dv1", "dv2", "dv3"])
>>> search_problem = SearchCh(ch)
>>> ch_found = search_problem.solve(0)
>>> ch_found.ch_weight
0b0000000
>>> ch_found.der_weights
[[w0w1w2, 0b0000000], [w3, 0b00000]]
>>> ch_found.input_diff  
[[XorDiff(dv0), XorDiff(...)], [XorDiff(dv1), XorDiff(...)],
[XorDiff(dv2), XorDiff(...)], [XorDiff(dv3), XorDiff(...)]]
>>> ch_found.nonlinear_diffs  
[[XorDiff(d0), XorDiff(...)], [XorDiff(d4), XorDiff(...)],
[XorDiff(d7), XorDiff(...)], [XorDiff(d10), XorDiff(...)]]
>>> ch_found.output_diff  
[[XorDiff(d7), XorDiff(...)], [XorDiff(d12), XorDiff(...)],
[XorDiff(d13), XorDiff(...)], [XorDiff(d9), XorDiff(...)]]
>>> print(ch_found)  
{'ch_weight': 0,
 'der_weights': [[w0w1w2, 0], [w3, 0]],
 'exact_weight': 0,
 'input_diff': [[dv0, ...], [dv1, ...], [dv2, ...], [dv3, ...]],
 'nonlinear_diffs': [[d0, ...], [d4, ...], [d7, ...], [d10, ...]],
 'output_diff': [[d7, ...], [d12, ...], [d13, ...], [d9, ...]]}
>>> ch = BvCharacteristic(ChaskeyPi, RXDiff, ["dv0", "dv1", "dv2", "dv3"])
>>> ic = [BvComp(0, d.val) for d in ch.input_diff]
>>> ic += [BvComp(0, d[1].val) for d in ch.output_diff]
>>> search_problem = SearchCh(ch, allow_zero_input_diff=True, initial_constraints=ic)
>>> ch_found = search_problem.solve(5)
>>> ch_found.ch_weight
0x05
>>> ch_found.der_weights
[[w0, 0b000001011], [w1, 0b000001011], [w2, 0b000001011], [w3, 0b000001011]]
>>> ch_found.input_diff  
[[RXDiff(dv0), RXDiff(0x00000000)], [RXDiff(dv1), RXDiff(0x00000000)],
[RXDiff(dv2), RXDiff(0x00000000)], [RXDiff(dv3), RXDiff(0x00000000)]]
>>> ch_found.nonlinear_diffs  
[[RXDiff(d0), RXDiff(0x00000000)], [RXDiff(d4), RXDiff(0x00000000)],
[RXDiff(d7), RXDiff(0x00000000)], [RXDiff(d10), RXDiff(0x00000000)]]
>>> ch_found.output_diff  
[[RXDiff(d7), RXDiff(0x00000000)], [RXDiff(d12), RXDiff(0x00000000)],
[RXDiff(d13), RXDiff(0x00000000)], [RXDiff(d9), RXDiff(0x00000000)]]
>>> print(ch_found)  
{'ch_weight': 5,
 'der_weights': [[w0, 1.375], [w1, 1.375], [w2, 1.375], [w3, 1.375]],
 'exact_weight': 5.66...,
 'input_diff': [[dv0, 0x00000000], [dv1, 0x00000000], [dv2, 0x00000000], [dv3, 0x00000000]],
 'nonlinear_diffs': [[d0, 0x00000000], [d4, 0x00000000], [d7, 0x00000000], [d10, 0x00000000]],
 'output_diff': [[d7, 0x00000000], [d12, 0x00000000], [d13, 0x00000000], [d9, 0x00000000]]}
get_exact_weight()[source]

Return the exact weight of the characteristic found.

check_empirical_weight(verbose_lvl=0, filename=None)[source]

Check the exact weight of the model matches its empirical weight.

If the exact weight doesn’t match, the exception ExactWeightError 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()[source]

Return a verbose dictionary-like representation of the characteristic.

>>> from arxpy.differential.difference import XorDiff
>>> from arxpy.differential.characteristic import BvCharacteristic
>>> from arxpy.primitives.chaskey import ChaskeyPi
>>> from arxpy.smt.search_differential import SearchCh
>>> ChaskeyPi.set_rounds(1)
>>> ch = BvCharacteristic(ChaskeyPi, XorDiff, ["dv0", "dv1", "dv2", "dv3"])
>>> search_problem = SearchCh(ch)
>>> ch_found = search_problem.solve(0)
>>> print(ch_found.vrepr())  
{'ch_weight': Constant(0b0000000, width=7),
'exact_weight': 0,
'input_diff': [[XorDiff(Variable('dv0', width=32)), XorDiff(Constant(..., width=32))],
    [XorDiff(Variable('dv1', width=32)), XorDiff(Constant(..., width=32))],
    [XorDiff(Variable('dv2', width=32)), XorDiff(Constant(..., width=32))],
    [XorDiff(Variable('dv3', width=32)), XorDiff(Constant(..., width=32))]],
'output_diff': [[XorDiff(Variable('d7', width=32)), XorDiff(Constant(..., width=32))],
    [XorDiff(Variable('d12', width=32)), XorDiff(Constant(..., width=32))],
    [XorDiff(Variable('d13', width=32)), XorDiff(Constant(..., width=32))],
    [XorDiff(Variable('d9', width=32)), XorDiff(Constant(..., width=32))]],
'nonlinear_diffs': [[XorDiff(Variable('d0', width=32)), XorDiff(Constant(..., width=32))],
    [XorDiff(Variable('d4', width=32)), XorDiff(Constant(..., width=32))],
    [XorDiff(Variable('d7', width=32)), XorDiff(Constant(..., width=32))],
    [XorDiff(Variable('d10', width=32)), XorDiff(Constant(..., width=32))]],
'der_weights': [[Variable('w0w1w2', width=7), Constant(0b0000000, width=7)],
    [Variable('w3', width=5), Constant(0b00000, width=5)]]}
srepr()[source]

Return a short representation of the characteristic.

class arxpy.smt.search_differential.SkChFound(ch, ch_weight, der_weights, model)[source]

Bases: arxpy.smt.search_differential.ChFound

Represent (non-symbolic) single-key characteristics found.

See also ChFound.

>>> from arxpy.differential.difference import XorDiff
>>> from arxpy.differential.characteristic import SingleKeyCh
>>> from arxpy.smt.search_differential import SearchSkCh
>>> 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 = SearchSkCh(ch)
>>> ch_found = search_problem.solve(0)
>>> ch_found.ch_weight
0x0
>>> ch_found.der_weights
[[w0, 0x0]]
>>> ch_found.input_diff  
[[XorDiff(dp0), XorDiff(...)], [XorDiff(dp1), XorDiff(...)]]
>>> ch_found.nonlinear_diffs  
[[XorDiff(dx1), XorDiff(...)]]
>>> ch_found.output_diff  
[[XorDiff(dx2), XorDiff(...)], [XorDiff(dx4), XorDiff(...)]]
>>> print(ch_found)  
{'ch_weight': 0,
 'der_weights': [[w0, 0]],
 'exact_weight': 0,
 'input_diff': [[dp0, ...], [dp1, ...]],
 'nonlinear_diffs': [[dx1, ...]],
 'output_diff': [[dx2, ...], [dx4, ...]]}
check_empirical_weight(verbose_lvl=0, filename=None)[source]

Check the exact weight of the model matches one weight of the empirical weight distribution.

If the exact weight doesn’t match, the exception ExactWeightError 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_differential.RkChFound(rkch, key_schedule_problem, encryption_problem, model)[source]

Bases: object

Represent (non-symbolic) related-key characteristics found.

rkch

the associated symbolic RelatedKeyCh

key_ch_found

a ChFound denoting the key schedule characteristic found

enc_ch_found

a ChFound denoting the encryption characteristic found

>>> from arxpy.differential.difference import XorDiff
>>> from arxpy.differential.characteristic import RelatedKeyCh
>>> from arxpy.smt.search_differential import SearchRkCh
>>> from arxpy.primitives.lea import LeaCipher
>>> LeaCipher.set_rounds(1)
>>> rkch = RelatedKeyCh(LeaCipher, XorDiff)
>>> search_problem = SearchRkCh(rkch)
>>> rkch_found = search_problem.solve(0, 0, solver_name="btor")
>>> rkch_found.key_ch_found.ch_weight
0b0000000
>>> rkch_found.key_ch_found.input_diff  
[[XorDiff(dmk0), XorDiff(...)], [XorDiff(dmk1), XorDiff(...)],
[XorDiff(dmk2), XorDiff(...)], [XorDiff(dmk3), XorDiff(...)]]
>>> rkch_found.key_ch_found.output_diff  
[[XorDiff(dk1), XorDiff(...)], [XorDiff(dk3), XorDiff(...)],
[XorDiff(dk5), XorDiff(...)], [XorDiff(dk3), XorDiff(...)],
[XorDiff(dk7), XorDiff(...)], [XorDiff(dk3), XorDiff(...)]]
>>> rkch_found.enc_ch_found.ch_weight
0b0000000
>>> rkch_found.enc_ch_found.input_diff  
[[XorDiff(dp0), XorDiff(...)], [XorDiff(dp1), XorDiff(...)],
[XorDiff(dp2), XorDiff(...)], [XorDiff(dp3), XorDiff(...)]]
>>> rkch_found.enc_ch_found.output_diff  
[[XorDiff(dx3), XorDiff(...)], [XorDiff(dx7), XorDiff(...)],
[XorDiff(dx11), XorDiff(...)], [XorDiff(dp0), XorDiff(...)]]
>>> print(rkch_found)  
{'enc_ch_found': {'ch_weight': 0,
                  'der_weights': [[w0w1w2, 0]],
                  'exact_weight': 0,
                  'input_diff': [[dp0, ...], [dp1, ...], [dp2, ...], [dp3, ...]],
                  'nonlinear_diffs': [[dx2, ...], [dx6, ...], [dx10, ...]],
                  'output_diff': [[dx3, ...], [dx7, ...], [dx11, ...], [dp0, ...]]},
 'key_ch_found': {'ch_weight': 0,
                  'der_weights': [[wk0, ...], [wk1, ...], [wk2, ...], [wk3, ...]],
                  'exact_weight': ...,
                  'input_diff': [[dmk0, ...], [dmk1, ...], [dmk2, ...], [dmk3, ...]],
                  'nonlinear_diffs': [[dk0, ...], [dk2, ...], [dk4, ...], [dk6, ...]],
                  'output_diff': [[dk1, ...], [dk3, ...], [dk5, ...], [dk3, ...], [dk7, ...], [dk3, ...]]}}
check_empirical_weight(verbose_lvl=0, filename=None)[source]

Check the exact weight of the model match its empirical weight.

Check both the exact weight of the key schedule characteristic and the encryption characteristic found match their empirical weights.

See also ChFound.check_empirical_weight and SkChFound.check_empirical_weight.

vrepr()[source]

Return a verbose dictionary-like representation of the characteristic.

See also ChFound.vrepr.

srepr()[source]

Return a short representation of the characteristic.

class arxpy.smt.search_differential.SearchCh(ch, der_mode=<DerMode.Default: 1>, weight_prefix='w', allow_zero_input_diff=False, initial_constraints=None, env=None)[source]

Bases: object

Represent the SMT problem of finding a BvCharacteristic with conditions on the weight.

Parameters

  • ch (BvCharacteristic) – a symbolic characteristic of a BvFunction

  • der_mode (DerMode) – one of the modes available for the derivative weights

  • weight_prefix (str) – the prefix to label weight variables

  • allow_zero_input_diff (bool) – if True, allow the input difference to be zero

  • initial_constraints (list) – a list of constraints (given as Term) to add to the SMT problem

  • env (pysmt.environment.Environment) – if None, a new pySMT environment is created

>>> from arxpy.bitvector.core import Variable
>>> from arxpy.differential.difference import XorDiff
>>> from arxpy.differential.characteristic import BvCharacteristic
>>> from arxpy.primitives.chaskey import ChaskeyPi
>>> ChaskeyPi.set_rounds(1)
>>> ch = BvCharacteristic(ChaskeyPi, XorDiff, ["dv0", "dv1", "dv2", "dv3"])
>>> search_problem = SearchCh(ch)
>>> search_problem.formula_size()
2804
>>> search_problem.error()
0
>>> print(search_problem.hrepr(False))
assert ~(0x00000000000000000000000000000000 == (dv0 :: dv1 :: dv2 :: dv3))
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 w0w1w2 == (PopCountSum3(~((d0 ^ ~...) & (dv1 ^ ~...))[30:], ~((d4 ^ ~...) & (dv3 ^ ~...))[30:], ~((d7 ^ ~...) & (~... ^ ... ^ ...))[30:]))
assert w3 == PopCount(~((d10 ^ ~...) & (d4 ^ ~...))[30:])
assert w == (w0w1w2 + (0b00 :: w3))
minimize w
>>> search_problem.solve(0).ch_weight
0b0000000
solve(initial_weight, solver_name='btor', search_mode=<ChSearchMode.Optimal: 3>, check=False, return_generator=False, verbose_level=0, filename=None)[source]

Solve the SMT problem associated to the search of a valid BvCharacteristic.

Parameters

  • initial_weight (int) – the initial weight for starting the iterative search

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

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

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

  • return_generator (bool) – if True, return a Python generator with the characteristics found (only valid in AllOptimal)

  • 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.

formula_size(measure=None)[source]

Return the size of the underlying SMT problem.

See pysmt.oracles.SizeOracle for choosing the measure.

hrepr(full_repr=False, minimize_constraint=True)[source]

Return a human readable representing of the SMT problem.

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

error()[source]

Return an upper bound of the weight error of the SMT problem.

class arxpy.smt.search_differential.SearchSkCh(skch, der_mode=<DerMode.Default: 1>, allow_zero_input_diff=False, initial_constraints=None)[source]

Bases: arxpy.smt.search_differential.SearchCh

Represent the problem of finding a SingleKeyCh with conditions on the weight.

Parameters

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

  • der_mode (DerMode) – one of the modes available for the derivative weights

  • allow_zero_input_diff (bool) – if True, allow the input difference to be zero

See also SearchCh.

>>> from arxpy.differential.difference import XorDiff
>>> from arxpy.differential.characteristic import SingleKeyCh
>>> from arxpy.smt.search_differential import SearchSkCh
>>> 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 = SearchSkCh(ch)
>>> search_problem.formula_size()
349
>>> search_problem.error()
0
>>> print(search_problem.hrepr(False))
assert ~(0x00000000 == (dp0 :: dp1))
assert 0x0000 == ((~(... << ...) ^ (dx1 << 0x0001)) & (~(... << ...) ^ ((... >>> ...) << 0x0001)) & ((dp1 << 0x0001) ^ dx1 ^ dp1 ^ (... >>> ...)))
assert w0 == PopCount(~((dx1 ^ ~...) & (~... ^ (... >>> ...)))[14:])
assert w == w0
minimize w
>>> search_problem.solve(0).ch_weight
0x0
solve(initial_weight, solver_name='btor', search_mode=<SkChSearchMode.Optimal: 3>, check=False, return_generator=False, verbose_level=0, filename=None)[source]

Solve the SMT problem associated to the search of a valid SingleKeyCh.

See also SearchCh.solve.

class arxpy.smt.search_differential.SearchRkCh(rkch, key_der_mode=<DerMode.Default: 1>, enc_der_mode=<DerMode.Default: 1>, allow_zero_key_input_diff=False, allow_zero_enc_input_diff=True, initial_key_constraints=None, initial_enc_constraints=None)[source]

Bases: object

Represent the problem of finding an RelatedKeyCh with conditions on the weight.

Parameters

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

  • key_der_mode (DerMode) – the derivative mode for the key schedule characteristic

  • enc_der_mode (DerMode) – the derivative mode for the encryption characteristic

  • allow_zero_key_input_diff (bool) – if True, allow the input difference of the key schedule to be zero

  • allow_zero_enc_input_diff (bool) – if True, allow the input difference of the encryption to be zero

See also SearchCh.

>>> from arxpy.differential.difference import XorDiff
>>> from arxpy.differential.characteristic import RelatedKeyCh
>>> from arxpy.smt.search_differential import SearchRkCh
>>> from arxpy.primitives.lea import LeaCipher
>>> LeaCipher.set_rounds(1)
>>> rkch = RelatedKeyCh(LeaCipher, XorDiff)
>>> search_problem = SearchRkCh(rkch)
>>> search_problem.formula_size()
50495
>>> search_problem.key_schedule_problem.error(), search_problem.encryption_problem.error()
(4.199250014423123, 0)
>>> print(search_problem.hrepr(False))
assert ~(0x00000000000000000000000000000000 == (dmk0 :: dmk1 :: dmk2 :: dmk3))
assert 0x00000000 == (((... << ...) & (... << ...) & ~(... ^ ...) & (~(... << ...) | (~... ^ ... ^ ...))) | (~(... << ...) & ~(... << ...) & (dk0 ^ dmk0)))
assert wk0_tmp_0lz == LeadingZeros(~((~... & ~...) << 0x00000001))
assert wk0_tmp_1rev == Reverse((~dk0 & ~dmk0) << 0x00000001)
assert wk0_tmp_2rev == Reverse(~(... >> ...) & ((... & ...) << 0x00000001) & (~(... ^ ...) >> 0x00000001))
assert wk0_tmp_3rev == Reverse(wk0_tmp_2rev ^ wk0_tmp_1rev ^ (wk0_tmp_1rev + wk0_tmp_2rev))
assert wk0_tmp_4rev == Reverse((((... & ...) + (... & ...)) & ~(... | ...)) | ((... & ... & (... >> ...)) - ((... + ...) & (... | ...))))
assert wk0 == (((PopCountDiff((... & ...) | (... << ...), (... & ...) ^ ... ^ ...)) :: 0b000) - (0b00 :: ((0b0 :: PopCount(...)) + (PopCount(...) :: 0b0))))
assert 0x00000000 == (((... << ...) & (... << ...) & ~(... ^ ...) & (~(... << ...) | (~... ^ ... ^ ...))) | (~(... << ...) & ~(... << ...) & (dk2 ^ dmk1)))
assert wk1_tmp_0lz == LeadingZeros(~((~... & ~...) << 0x00000001))
assert wk1_tmp_1rev == Reverse((~dk2 & ~dmk1) << 0x00000001)
assert wk1_tmp_2rev == Reverse(~(... >> ...) & ((... & ...) << 0x00000001) & (~(... ^ ...) >> 0x00000001))
assert wk1_tmp_3rev == Reverse(wk1_tmp_2rev ^ wk1_tmp_1rev ^ (wk1_tmp_1rev + wk1_tmp_2rev))
assert wk1_tmp_4rev == Reverse((((... & ...) + (... & ...)) & ~(... | ...)) | ((... & ... & (... >> ...)) - ((... + ...) & (... | ...))))
assert wk1 == (((PopCountDiff((... & ...) | (... << ...), (... & ...) ^ ... ^ ...)) :: 0b000) - (0b00 :: ((0b0 :: PopCount(...)) + (PopCount(...) :: 0b0))))
assert 0x00000000 == (((... << ...) & (... << ...) & ~(... ^ ...) & (~(... << ...) | (~... ^ ... ^ ...))) | (~(... << ...) & ~(... << ...) & (dk4 ^ dmk2)))
assert wk2_tmp_0lz == LeadingZeros(~((~... & ~...) << 0x00000001))
assert wk2_tmp_1rev == Reverse((~dk4 & ~dmk2) << 0x00000001)
assert wk2_tmp_2rev == Reverse(~(... >> ...) & ((... & ...) << 0x00000001) & (~(... ^ ...) >> 0x00000001))
assert wk2_tmp_3rev == Reverse(wk2_tmp_2rev ^ wk2_tmp_1rev ^ (wk2_tmp_1rev + wk2_tmp_2rev))
assert wk2_tmp_4rev == Reverse((((... & ...) + (... & ...)) & ~(... | ...)) | ((... & ... & (... >> ...)) - ((... + ...) & (... | ...))))
assert wk2 == (((PopCountDiff((... & ...) | (... << ...), (... & ...) ^ ... ^ ...)) :: 0b000) - (0b00 :: ((0b0 :: PopCount(...)) + (PopCount(...) :: 0b0))))
assert (0b0000000000000000000000000000000 == ((... & ... & ~... & (~... | (... ^ ...))) | (~... & ~... & ((dk6[:1]) ^ (dmk3[:1]))))) & ((dk6[0]) == (dmk3[0]))
assert wk3_tmp_0lz == LeadingZeros(~((~... & ~...) << 0b0000000000000000000000000000001))
assert wk3_tmp_1rev == Reverse((~(dk6[:1]) & ~(dmk3[:1])) << 0b0000000000000000000000000000001)
assert wk3_tmp_2rev == Reverse(~(... >> ...) & ((... & ...) << 0b0000000000000000000000000000001) & (~(... ^ ...) >> 0b0000000000000000000000000000001))
assert wk3_tmp_3rev == Reverse(wk3_tmp_2rev ^ wk3_tmp_1rev ^ (wk3_tmp_1rev + wk3_tmp_2rev))
assert wk3_tmp_4rev == Reverse((((... & ...) + (... & ...)) & ~(... | ...)) | ((... & ... & (... >> ...)) - ((... + ...) & (... | ...))))
assert wk3 == (((PopCountDiff((... & ...) | (... << ...), (... & ...) ^ ... ^ ...)) :: 0b000) - (0b00 :: ((0b0 :: PopCount(...)) + (PopCount(...) :: 0b0))))
assert wk == (((0b0 :: wk0) + (0b0 :: wk1) + (0b0 :: wk2) + (0b00 :: wk3))[:3])
assert 0x00000000 == ((~(... << ...) ^ (dx2 << 0x00000001)) & (~(... << ...) ^ ((... ^ ...) << 0x00000001)) & (((dp0 ^ (... <<< ...)) << 0x00000001) ^ dx2 ^ dp0 ^ (... <<< ...) ^ dp1 ^ (... <<< ...)))
assert 0x00000000 == ((~(... << ...) ^ (dx6 << 0x00000001)) & (~(... << ...) ^ ((... ^ ...) << 0x00000001)) & (((dp1 ^ (... <<< ...)) << 0x00000001) ^ dx6 ^ dp1 ^ (... <<< ...) ^ dp2 ^ (... <<< ...)))
assert 0x00000000 == ((~(... << ...) ^ (dx10 << 0x00000001)) & (~(... << ...) ^ ((... ^ ...) << 0x00000001)) & (((dp2 ^ (... <<< ...)) << 0x00000001) ^ dx10 ^ dp2 ^ (... <<< ...) ^ dp3 ^ (... <<< ...)))
assert w0w1w2 == (PopCountSum3(~((dx10 ^ ~...) & (~... ^ ... ^ ...))[30:], ~((dx2 ^ ~...) & (~... ^ ... ^ ...))[30:], ~((dx6 ^ ~...) & (~... ^ ... ^ ...))[30:]))
assert w == w0w1w2
minimize wk, w
>>> rkch_found = search_problem.solve(0, 0, solver_name="btor")
>>> rkch_found.key_ch_found.ch_weight, rkch_found.enc_ch_found.ch_weight
(0b0000000, 0b0000000)
formula_size(measure=None)[source]

Return the size of the underlying SMT problem.

See also SearchCh.formula_size.

hrepr(full_repr=False, minimize_constraint=True)[source]

Return a human readable representing of the SMT problem.

See also SearchCh.hrepr.

solve(initial_ew, initial_kw, solver_name='btor', search_mode=<RkChSearchMode.OptimalMinSum: 3>, check=False, verbose_level=0, filename=None, return_generator=False)[source]

Solve the SMT problem associated to the search a valid RelatedKeyCh.

Parameters

  • initial_ew (int) – the initial encryption weight for starting the iterative search

  • initial_kw (int) – the initial key schedule weight for starting the iterative search

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

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

  • check (bool) – if True, RkChFound.check_empirical_weight will be called after a characteristic 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_differential.round_based_search_SkCh(cipher, diff_type, initial_weight, solver_name, start_round, end_round, der_mode, search_mode, check, verbose_level, filename, fix_input_diff=None, fix_output_diff=None, fix_round_inputs=None, return_best=None)[source]

Find valid single-key characteristics over consecutive rounds.

Parameters

  • cipher (Cipher) – an (iterated) cipher

  • diff_type (Difference) – a type of difference

  • initial_weight (int) – the initial weight 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

  • der_mode (DerMode) – one of the modes available for the derivative weights

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

  • check (bool) – if True, SkChFound.check_empirical_weight will be called after a characteristic 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.

See also SearchSkCh.solve.

>>> from arxpy.differential.difference import XorDiff
>>> from arxpy.smt.search_differential import SkChSearchMode, DerMode, round_based_search_SkCh
>>> from arxpy.primitives import speck
>>> Speck32 = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64)
>>> round_based_search_SkCh(Speck32, XorDiff, 0, "btor", 1, 2,
...                         DerMode.Default, SkChSearchMode.Optimal, True, 0, None)  
Num rounds: 1
Best characteristic found:
(weight 0) ... -> ...

Num rounds: 2
Best characteristic found:
(weight 1) ... -> ...
arxpy.smt.search_differential.round_based_search_RkCh(cipher, diff_type, initial_ew, initial_kw, solver_name, start_round, end_round, key_der_mode, enc_der_mode, allow_zero_enc_input_diff, search_mode, check, verbose_level, filename, allow_zero_key_input_diff=False, fix_key_input_diff=None, fix_enc_input_diff=None, fix_enc_output_diff=None, fix_enc_round_inputs=None, return_best=None)[source]

Find valid related-key characteristics over consecutive rounds.

Parameters

  • cipher (Cipher) – an (iterated) cipher

  • diff_type (Difference) – a type of difference

  • initial_ew (int) – the initial encryption weight for starting the iterative search

  • initial_kw (int) – the initial key schedule weight 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

  • key_der_mode (DerMode) – the derivative mode for the key schedule characteristic

  • enc_der_mode (DerMode) – the derivative mode for the encryption characteristic

  • allow_zero_enc_input_diff (bool) – if True, allow the input difference of the encryption to be zero

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

  • check (bool) – if True, RkChFound.check_empirical_weight will be called after a characteristic 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.

  • allow_zero_key_input_diff (bool) – if True, allow the input difference of the key schedule to be zero.

See also SearchRkCh.solve.

>>> from arxpy.differential.difference import XorDiff, RXDiff
>>> from arxpy.smt.search_differential import RkChSearchMode, DerMode, round_based_search_RkCh
>>> from arxpy.primitives import speck
>>> Speck32 = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64)
>>> round_based_search_RkCh(Speck32, XorDiff, 0, 0, "btor",
...                         4, 5, DerMode.Default, DerMode.Default, True,
...                         RkChSearchMode.OptimalMinSum, True, 0, None)  
Num rounds: 4
Best related-key characteristic found:
K: (weight 0) ... -> ... | E: (weight 0) ... -> ...

Num rounds: 5
Best related-key characteristic found:
K: (weight 0) ... -> ... | E: (weight 1) ... -> ...
>>> round_based_search_RkCh(Speck32, RXDiff, 0, 0, "btor",
...                         2, 3, DerMode.Default, DerMode.Default, True,
...                         RkChSearchMode.FirstMinSumValid, True, 0, None, True)  
Num rounds: 2
Best related-key characteristic found:
K: (weight 1) ... -> ... | E: (weight 2) ... -> ...

Num rounds: 3
Best related-key characteristic found:
K: (weight 2) ... -> ... | E: (weight 4) ... -> ...