Advanced Usage

Before searching for characteristics or zero-probability properties over a large number of rounds of a cryptographic primitive, CASCADA provides a set of tools to run a fine-grained search over a small number of rounds and check the results. Additionally, if you are implementing a new primitive or a new property model, CASCADA also includes several tests to check cipher implementations and property models.

In this tutorial we will see how to check the bit-vector implementation of a primitive, the property models of a bit-vector operations, a characteristic model, and a characteristic obtained in the search.

Checking the bit-vector implementation of a primitive

If you are using one of the primitives included in CASCADA (see Primitives implemented) you can skip this section. Otherwise, you can check that the primitive is correct by evaluating it with some test vectors. For example, you can evaluate the cipher Speck32/64 with a test vector as follows:

>>> from cascada.primitives import speck
>>> Speck32 = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64)
>>> plaintext = (0x6574, 0x694c)
>>> key = (0x1918, 0x1110, 0x0908, 0x0100)
>>> Speck32(plaintext, key) == (0xa868, 0x42f2)
True

For a round-based primitive including add_round_outputs calls, you can also check the automatic round splitting of the SSA form:

>>> SpeckCipher.set_num_rounds(2)
>>> SpeckCipher.set_round_keys(symbolic_prefix="k")
>>> ssa_2rounds = SpeckCipher.encryption.to_ssa(["p0", "p1"], "x")
>>> ssa_2rounds
SSA(input_vars=[p0, p1], output_vars=[x7_out, x9_out], external_vars=[k0, k1],
    assignments=[(x0, p0 >>> 7), (x1, x0 + p1), (x2, x1 ^ k0), (x3, p1 <<< 2), (x4, x3 ^ x2),
        (x5, x2 >>> 7), (x6, x5 + x4), (x7, x6 ^ k1), (x8, x4 <<< 2), (x9, x8 ^ x7), (x7_out, Id(x7)), (x9_out, Id(x9))])
>>> ssa_round1, ssa_round2 = ssa_2rounds.split(ssa_2rounds.get_round_separators())
>>> ssa_round1
SSA(input_vars=[p0, p1], output_vars=[x2_out, x4_out], external_vars=[k0],
    assignments=[(x0, p0 >>> 7), (x1, x0 + p1), (x2, x1 ^ k0), (x3, p1 <<< 2), (x4, x3 ^ x2), (x2_out, Id(x2)), (x4_out, Id(x4))])
>>> ssa_round2
SSA(input_vars=[x2, x4], output_vars=[x7_out, x9_out], external_vars=[k1],
    assignments=[(x5, x2 >>> 7), (x6, x5 + x4), (x7, x6 ^ k1), (x8, x4 <<< 2), (x9, x8 ^ x7), (x7_out, Id(x7)), (x9_out, Id(x9))])

Here we can see the SSA of each round corresponds exactly to a round of Speck, that the external variables are the round keys, and that the composition of ssa_round1 and ssa_round2 results in ssa_2rounds. Checking the SSA form of the cipher is beneficial as this is the main internal representation used by CASCADA. Moreover, the SSA form might differ from the original implementation (while still being functionally equivalent), as redundant assignments are removed and additional transformations might be performed (more on that later).

Additionally, you can use the tests in smt/tests/test_primitives_eval.py (by adding your primitive to the list LIST_PRIMITIVES) or in smt/tests/test_primitives_smt.py, or read more about implementing primitives in Adding a primitive, cascada.bitvector.ssa and blockcipher.

Checking the property model of a bit-vector operation

If you are using one the primitives included in CASCADA or only property models included in CASCADA, you can skip this section.

If you implement a new property model from the generic models WeakModel, BranchNumberModel or WDTModel, then you can check the weights and the model error. For example, for a WDTModel:

>>> from decimal import Decimal
>>> from math import inf
>>> from cascada.bitvector.core import Variable, Constant
>>> from cascada.bitvector.secondaryop import LutOperation
>>> from cascada.differential.difference import XorDiff
>>> from cascada.differential.opmodel import log2_decimal, get_wdt_model
>>> class Sbox3b(LutOperation): lut = [Constant(i, 3) for i in (0, 1, 2, 3, 4, 6, 7, 5)]
>>> ddt = [(8, 0, 0, 0, 0, 0, 0, 0), (0, 4, 4, 0, 0, 0, 0, 0), (0, 0, 4, 4, 0, 0, 0, 0), (0, 4, 0, 4, 0, 0, 0, 0),
...     (0, 0, 0, 0, 2, 2, 2, 2), (0, 0, 0, 0, 2, 2, 2, 2), (0, 0, 0, 0, 2, 2, 2, 2), (0, 0, 0, 0, 2, 2, 2, 2)]
>>> wdt_dec = tuple([tuple(inf if x == 0 else -log2_decimal(x/Decimal(2**3)) for x in row) for row in ddt])
>>> wdt_dec
((Decimal('0'), inf, inf, inf, inf, inf, inf, inf),
(inf, Decimal('1'), Decimal('1'), inf, inf, inf, inf, inf),
(inf, inf, Decimal('1'), Decimal('1'), inf, inf, inf, inf),
(inf, Decimal('1'), inf, Decimal('1'), inf, inf, inf, inf),
(inf, inf, inf, inf, Decimal('2'), Decimal('2'), Decimal('2'), Decimal('2')),
(inf, inf, inf, inf, Decimal('2'), Decimal('2'), Decimal('2'), Decimal('2')),
(inf, inf, inf, inf, Decimal('2'), Decimal('2'), Decimal('2'), Decimal('2')),
(inf, inf, inf, inf, Decimal('2'), Decimal('2'), Decimal('2'), Decimal('2')))
>>> XorWDTModelSbox3b = get_wdt_model(Sbox3b, XorDiff, wdt_dec)
>>> XorWDTModelSbox3b(XorDiff(Variable("a", 3))).error()
0
>>> wdt_bv = [[None for _ in range(2**3)] for _ in range(2**3)]
>>> for i in range(2**3):
...    for j in range(2**3):
...        f = XorWDTModelSbox3b(XorDiff(Constant(i, 3)))
...        if f.validity_constraint(XorDiff(Constant(j, 3))):
...            wdt_bv[i][j] = f.bv_weight(XorDiff(Constant(j, 3)))
>>> wdt_bv
[[0b00, None, None, None, None, None, None, None],
[None, 0b01, 0b01, None, None, None, None, None],
[None, None, 0b01, 0b01, None, None, None, None],
[None, 0b01, None, 0b01, None, None, None, None],
[None, None, None, None, 0b10, 0b10, 0b10, 0b10],
[None, None, None, None, 0b10, 0b10, 0b10, 0b10],
[None, None, None, None, 0b10, 0b10, 0b10, 0b10],
[None, None, None, None, 0b10, 0b10, 0b10, 0b10]]

We can see that the error is 0 as the bit-vector weights from wdt_bv match the decimal weights from wdt_dec. However, if the decimal weights provided to get_wdt_model are not integers, you should check the error and the bit-vector weights to choose the best trade-off for the precision (more fractional bits give to less error but more complex models).

If you implement a new property model (not derived from WeakModel, BranchNumberModel or WDTModel), then the CASCADA modules differential.tests.test_opmodel and linear.tests.test_opmodel provide the class TestOpModelGeneric to test the constraints of a differential or linear model by sampling all inputs of small wordsize. An example of how to use this class is the method TestOpModelsSmallWidth.test_*_models_slow from these modules, or the method TestOpModelsSmallWidth.test_Xor_models_slow from smt/tests/test_simon_rf (which might be easier to understand). Additionally, you can check the error and the symbolic expressions of the constraints of the model similar to the docstrings of smt/tests/test_simon_rf, differential.opmodel and linear.opmodel. You can read more about property models in abstractproperty.opmodel.

Checking a characteristic model

Before checking the characteristics found in the search, it is better to check first the representation of a characteristic model (i.e., the symbolic characteristic associated with any characteristics found) and its error.

For a round-based primitive including add_round_outputs calls, you can print for example the XorDiff differential.chmodel.EncryptionChModel of each round and its underlying SSA form as follows:

>>> from cascada.differential.difference import XorDiff
>>> from cascada.differential.chmodel import EncryptionChModel
>>> from cascada.primitives import speck
>>> Speck32 = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64)
>>> Speck32.set_num_rounds(2)
>>> ch_model_2rounds = EncryptionChModel(Speck32, XorDiff)
>>> ch_model_2rounds.error()
0
>>> ch_model_round1, ch_model_round2 = ch_model_2rounds.split(ch_model_2rounds.get_round_separators())
>>> ch_model_round1.ssa
SSA(input_vars=[dp0, dp1], output_vars=[dx2_out, dx4_out], external_vars=[dk0],
    assignments=[(dx0, dp0 >>> 7), (dx1, dx0 + dp1), (dx2, dx1 ^ dk0), (dx3, dp1 <<< 2), (dx4, dx3 ^ dx2), (dx2_out, Id(dx2)), (dx4_out, Id(dx4))])
>>> ch_model_round1
ChModel(func=SpeckEncryption_2R_0S, input_diff=[XorDiff(dp0), XorDiff(dp1)],
    output_diff=[XorDiff(dx2_out), XorDiff(dx4_out)],
    external_var2diff=[(dk0, XorDiff(0x0000))],
    assign_outdiff2op_model=[(XorDiff(dx1), XorModelBvAdd([XorDiff(dp0 >>> 7), XorDiff(dp1)])),
                             (XorDiff(dx2_out), XorModelId(XorDiff(dx1))),
                             (XorDiff(dx4_out), XorModelId(XorDiff((dp1 <<< 2) ^ dx1)))])
>>> ch_model_round2.ssa
SSA(input_vars=[dx2, dx4], output_vars=[dx7_out, dx9_out], external_vars=[dk1],
    assignments=[(dx5, dx2 >>> 7), (dx6, dx5 + dx4), (dx7, dx6 ^ dk1), (dx8, dx4 <<< 2), (dx9, dx8 ^ dx7), (dx7_out, Id(dx7)), (dx9_out, Id(dx9))])
>>> ch_model_round2
ChModel(func=SpeckEncryption_2R_1S, input_diff=[XorDiff(dx2), XorDiff(dx4)],
    output_diff=[XorDiff(dx7_out), XorDiff(dx9_out)],
    external_var2diff=[(dk1, XorDiff(0x0000))],
    assign_outdiff2op_model=[(XorDiff(dx6), XorModelBvAdd([XorDiff(dx2 >>> 7), XorDiff(dx4)])),
                             (XorDiff(dx7_out), XorModelId(XorDiff(dx6))),
                             (XorDiff(dx9_out), XorModelId(XorDiff((dx4 <<< 2) ^ dx6)))])

Excluding the trivial transitions with XorModelId, we can check that there is only one non-trivial transition per round that corresponds to the propagation of the modular addition: (XorDiff(dx1), XorModelBvAdd([XorDiff(dp0 >>> 7), XorDiff(dp1)])) in the first round, and (XorDiff(dx6), XorModelBvAdd([XorDiff(dx2 >>> 7), XorDiff(dx4)])) in the second round. You can also check the difference associated to each intermediate variable from the attribute var2diff of the characteristic model.

Checking the underlying SSA is particularly important for linear characteristics, as this SSA differs from the SSA of the original primitive; the underlying SSA is computed with the initialization argument replace_multiuse_vars=True. (see linear.chmodel.ChModel).

We can also see here that the characteristic model of the two rounds ch_model_2rounds has error 0, as the model XorModelBvAdd has also error 0. This error is important as it will affect the optimality of the characteristics found in the search and the speed when computing the empirical weights.

You can read more about characteristic models in abstractproperty.chmodel.