cascada.linear.chmodel module

Manage bit-vector models of linear characteristics.

ChModel

Represent bit-vector models of linear characteristics over bit-vector functions.

EncryptionChModel

Represent linear characteristic models of encryption functions.
class cascada.linear.chmodel.ChModel(func, mask_type, input_mask_names, prefix='mx', external_var2mask=None, op_model_class2options=None)[source]

Bases: cascada.abstractproperty.chmodel.ChModel

Represent bit-vector models of linear characteristics over bit-vector functions.

Internally, this class is a subclass of abstractproperty.chmodel.ChModel, where the Property is a LinearMask type and the probability of the characteristic here considered is the product of the absolute linear correlation of the linear approximations \((\Delta_{x_{i}} \mapsto \Delta_{x_{i+1}})\) composing the characteristic (see linear.characteristic.Characteristic).

To handle the propagation of masks through branching subroutines (i.e., \(x \mapsto (x, x)\)), the SSA of the BvFunction is computed with the initialization argument replace_multiuse_vars set to True and the new free masks are wrapped in LinearModelFreeBranch objects (see also SSA and LinearModelFreeBranch).

If the SSA of the BvFunction contains external Variable objects and their LinearMask objects are not provided in the initialization through external_var2mask, these free external masks are wrapped in LinearMask objects.

Linear characteristic models of functions with unused input vars is currently not supported.

>>> from cascada.bitvector.core import Variable
>>> from cascada.linear.mask import LinearMask
>>> from cascada.linear.chmodel import ChModel
>>> from cascada.primitives import speck
>>> Speck32_KS = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64).key_schedule
>>> Speck32_KS.set_num_rounds(2)
>>> ch_model = ChModel(Speck32_KS, LinearMask, ["mk0", "mk1", "mk2"])
>>> ch_model  
ChModel(func=SpeckKeySchedule_2R,
        input_mask=[LinearMask(mk0), LinearMask(mk1), LinearMask(mk2)],
        output_mask=[LinearMask(mk2_out), LinearMask(mx3_out), LinearMask(mx8_out)],
        assign_outmask2op_model=[(LinearMask(mk2__0), LinearModelFreeBranch(LinearMask(mk2))),
            (LinearMask(mk2__1), LinearModelFreeBranch(LinearMask(mk2))),
            (LinearMask(mx1), LinearModelBvAdd([LinearMask(mk1 >>> 7), LinearMask(mk2__0)])),
            (LinearMask(mx3), LinearModelBvXor([LinearMask(mk2__1 <<< 2), LinearMask(mx1)])),
            (LinearMask(mx3__0), LinearModelFreeBranch(LinearMask(mx3))),
            (LinearMask(mx3__1), LinearModelFreeBranch(LinearMask(mx3))),
            (LinearMask(mx5), LinearModelBvAdd([LinearMask(mk0 >>> 7), LinearMask(mx3__0)])),
            (LinearMask(mx8), LinearModelBvXor([LinearMask(mx3__1 <<< 2), LinearMask(mx5)])),
            (LinearMask(mk2_out), LinearModelId(LinearMask(mk2 ^ mk2__0 ^ mk2__1))),
            (LinearMask(mx3_out), LinearModelId(LinearMask(mx3 ^ mx3__0 ^ mx3__1))),
            (LinearMask(mx8_out), LinearModelId(LinearMask(mx8)))])
>>> ch_model.ssa  
SSA(input_vars=[mk0, mk1, mk2],
    output_vars=[mk2_out, mx3_out, mx8_out],
    assignments=[(mx0, mk1 >>> 7), (mk2__0, Id(mk2)), (mk2__1, Id(mk2)), (mk2__2, Id(mk2)),
            (mx1, mx0 + mk2__0), (mx2, mk2__1 <<< 2), (mx3, mx2 ^ mx1),
        (mx4, mk0 >>> 7), (mx3__0, Id(mx3)), (mx3__1, Id(mx3)), (mx3__2, Id(mx3)),
            (mx5, mx4 + mx3__0), (mx6, mx5 ^ 0x0001), (mx7, mx3__1 <<< 2), (mx8, mx7 ^ mx6),
        (mk2_out, Id(mk2__2)), (mx3_out, Id(mx3__2)), (mx8_out, Id(mx8))])
mask_type

the mask type (currently only LinearMask is supported); alias of abstractproperty.chmodel.ChModel.prop_type.

input_mask

a list of LinearMask objects containing the (symbolic) input mask (alias of abstractproperty.chmodel.ChModel.input_prop).

output_mask

a list of LinearMask objects containing the (symbolic) output mask (alias of abstractproperty.chmodel.ChModel.output_prop).

external_var2mask

a collections.OrderedDict mapping the external variables of abstractproperty.chmodel.ChModel.ssa to their associated (symbolic or constant) LinearMask objects (alias of abstractproperty.chmodel.ChModel.external_var2prop).

assign_outmask2op_model

a collections.OrderedDict mapping the output LinearMask \(\Delta_{x_{i+1}}\) of the non-trivial assignment \(x_{i+1} \leftarrow f_i(x_i)\) to the linear.opmodel.OpModel of this assignment (alias of abstractproperty.chmodel.ChModel.assign_outprop2op_model).

var2mask

a collections.OrderedDict mapping each variable in abstractproperty.chmodel.ChModel.ssa to its associated LinearMask object (alias of abstractproperty.chmodel.ChModel.var2prop).

vrepr()[source]

Return an executable string representation.

See also abstractproperty.chmodel.ChModel.vrepr.

>>> from cascada.bitvector.core import Variable
>>> from cascada.linear.mask import LinearMask
>>> from cascada.linear.chmodel import ChModel
>>> from cascada.primitives import speck
>>> Speck32_KS = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64).key_schedule
>>> Speck32_KS.set_num_rounds(2)
>>> ch_model = ChModel(Speck32_KS, LinearMask, ["mk0", "mk1", "mk2"])
>>> ch_model.vrepr()  
"ChModel(func=SpeckKeySchedule.set_num_rounds_and_return(2), mask_type=LinearMask,
         input_mask_names=['mk0', 'mk1', 'mk2'], prefix='mx')"
validity_assertions()[source]

Return the validity constraint as a list of assertions.

See also abstractproperty.chmodel.ChModel.validity_assertions.

>>> from functools import reduce
>>> from cascada.bitvector.core import Variable
>>> from cascada.bitvector.operation import BvAnd
>>> from cascada.linear.mask import LinearMask
>>> from cascada.linear.chmodel import ChModel
>>> from cascada.primitives import speck
>>> Speck32_KS = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64).key_schedule
>>> Speck32_KS.set_num_rounds(2)
>>> ch_model = ChModel(Speck32_KS, LinearMask, ["mk0", "mk1", "mk2"])
>>> assertions = ch_model.validity_assertions()
>>> for a in assertions: print(a)  
((~((mx1 ^ (mk1 >>> 7)) | (mx1 ^ mk2__0)) | _tmp5b87dfbff36ecd792bff9b4a837080cc) == 0xffff) &
    ((_tmp5b87dfbff36ecd792bff9b4a837080cc ^ (_tmp5b87dfbff36ecd792bff9b4a837080cc >> 0x0001) ^
    ((mx1 ^ (mk1 >>> 7) ^ mk2__0) >> 0x0001)) == 0x0000)
((mk2__1 <<< 2) == mx1) & ((mk2__1 <<< 2) == mx3)
((~((mx5 ^ (mk0 >>> 7)) | (mx5 ^ mx3__0)) | _tmp496354c626556f9b918d51527d988998) == 0xffff) &
    ((_tmp496354c626556f9b918d51527d988998 ^ (_tmp496354c626556f9b918d51527d988998 >> 0x0001) ^
    ((mx5 ^ (mk0 >>> 7) ^ mx3__0) >> 0x0001)) == 0x0000)
((mx3__1 <<< 2) == mx5) & ((mx3__1 <<< 2) == mx8)
(mk2 ^ mk2__0 ^ mk2__1) == mk2_out
(mx3 ^ mx3__0 ^ mx3__1) == mx3_out
mx8 == mx8_out
>>> validity_constraint = reduce(BvAnd, assertions)
>>> validity_constraint  
((~((mx1 ^ (mk1 >>> 7)) | (mx1 ^ mk2__0)) | ...
pr_one_assertions()[source]

Return the probability-one constraint as a list of assertions.

See also abstractproperty.chmodel.ChModel.pr_one_assertions.

>>> from cascada.bitvector.core import Variable
>>> from cascada.linear.mask import LinearMask
>>> from cascada.linear.chmodel import ChModel
>>> from cascada.primitives import speck
>>> Speck32_KS = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64).key_schedule
>>> Speck32_KS.set_num_rounds(2)
>>> ch_model = ChModel(Speck32_KS, LinearMask, ["mk0", "mk1", "mk2"])
>>> for a in ch_model.pr_one_assertions(): print(a)  
(~((mx1 ^ (mk1 >>> 7)) | (mx1 ^ mk2__0)) == 0xffff) & (((mx1 ^ (mk1 >>> 7) ^ mk2__0)[:1]) == 0b000000000000000)
((mk2__1 <<< 2) == mx1) & ((mk2__1 <<< 2) == mx3)
(~((mx5 ^ (mk0 >>> 7)) | (mx5 ^ mx3__0)) == 0xffff) & (((mx5 ^ (mk0 >>> 7) ^ mx3__0)[:1]) == 0b000000000000000)
((mx3__1 <<< 2) == mx5) & ((mx3__1 <<< 2) == mx8)
(mk2 ^ mk2__0 ^ mk2__1) == mk2_out
(mx3 ^ mx3__0 ^ mx3__1) == mx3_out
mx8 == mx8_out
weight_assertions(ch_weight_variable, assign_weight_variables, truncate=True)[source]

Return the weight constraint as a list of assertions.

See also abstractproperty.chmodel.ChModel.weight_assertions.

>>> from cascada.bitvector.core import Variable
>>> from cascada.linear.mask import LinearMask
>>> from cascada.linear.chmodel import ChModel
>>> from cascada.primitives import speck
>>> Speck32_KS = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64).key_schedule
>>> Speck32_KS.set_num_rounds(2)
>>> cm = ChModel(Speck32_KS, LinearMask, ["mk0", "mk1", "mk2"])
>>> cwv = Variable("w", cm.weight_width())
>>> omvs = [Variable(f"w{i}", om.weight_width()) for i, om in enumerate(cm.assign_outmask2op_model.values())]
>>> for a in cm.weight_assertions(cwv, omvs): print(a)  
w0 == 0b0
w1 == 0b0
(PopCount(_tmp5b87dfbff36ecd792bff9b4a837080cc[14:]) == w2) & ((_tmp5b87dfbff36ecd792bff9b4a837080cc ^
    (_tmp5b87dfbff36ecd792bff9b4a837080cc >> 0x0001) ^ ((mx1 ^ (mk1 >>> 7) ^ mk2__0) >> 0x0001)) == 0x0000)
w3 == 0b0
w4 == 0b0
w5 == 0b0
(PopCount(_tmp496354c626556f9b918d51527d988998[14:]) == w6) & ((_tmp496354c626556f9b918d51527d988998 ^
    (_tmp496354c626556f9b918d51527d988998 >> 0x0001) ^ ((mx5 ^ (mk0 >>> 7) ^ mx3__0) >> 0x0001)) == 0x0000)
w7 == 0b0
w8 == 0b0
w9 == 0b0
w10 == 0b0
w == ((0b0 :: w2) + (0b0 :: w6))
max_weight(truncate=True)[source]

Return the maximum value the ch. weight variable can achieve in weight_assertions.

See also abstractproperty.chmodel.ChModel.max_weight.

>>> from cascada.bitvector.core import Variable
>>> from cascada.linear.mask import LinearMask
>>> from cascada.linear.chmodel import ChModel
>>> from cascada.primitives import speck
>>> Speck32_KS = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64).key_schedule
>>> Speck32_KS.set_num_rounds(2)
>>> cm = ChModel(Speck32_KS, LinearMask, ["mk0", "mk1", "mk2"])
>>> cm.max_weight(), cm.weight_width(), cm.num_frac_bits()
(30, 5, 0)
error()[source]

Return the maximum difference between weight_assertions and the exact weight.

See also abstractproperty.chmodel.ChModel.error.

>>> from cascada.bitvector.core import Variable
>>> from cascada.linear.mask import LinearMask
>>> from cascada.linear.chmodel import ChModel
>>> from cascada.primitives import speck
>>> Speck32_KS = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64).key_schedule
>>> Speck32_KS.set_num_rounds(2)
>>> ChModel(Speck32_KS, LinearMask, ["mk0", "mk1", "mk2"]).error()
0
signature(sig_type)[source]

Return the signature of the characteristic model.

See also abstractproperty.chmodel.ChModel.signature.

>>> from cascada.bitvector.core import Variable
>>> from cascada.linear.mask import LinearMask
>>> from cascada.linear.chmodel import ChModel, ChModelSigType
>>> from cascada.primitives import speck
>>> Speck32_KS = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64).key_schedule
>>> Speck32_KS.set_num_rounds(2)
>>> ch_model = ChModel(Speck32_KS, LinearMask, ["mk0", "mk1", "mk2"])
>>> ch_model.signature(ChModelSigType.Unique)
[mk2, mk1, mk2__0, mx3, mk0, mx3__0, mk2_out, mx3_out, mx8_out]
>>> ch_model.signature(ChModelSigType.InputOutput)
[mk0, mk1, mk2, mk2_out, mx3_out, mx8_out]
split(mask_separators)[source]

Split into multiple ChModel objects given the list of mask separators.

See also abstractproperty.chmodel.ChModel.split.

>>> from cascada.bitvector.core import Variable
>>> from cascada.linear.mask import LinearMask
>>> from cascada.linear.chmodel import ChModel, ChModelSigType
>>> from cascada.primitives import speck
>>> Speck32_KS = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64).key_schedule
>>> Speck32_KS.set_num_rounds(2)
>>> ch_model = ChModel(Speck32_KS, LinearMask, ["mk0", "mk1", "mk2"])
>>> tuple(ch_model.ssa.assignments.items())  
((mx0, mk1 >>> 7), (mk2__0, Id(mk2)), (mk2__1, Id(mk2)), (mk2__2, Id(mk2)),
    (mx1, mx0 + mk2__0), (mx2, mk2__1 <<< 2), (mx3, mx2 ^ mx1),
(mx4, mk0 >>> 7), (mx3__0, Id(mx3)), (mx3__1, Id(mx3)), (mx3__2, Id(mx3)),
    (mx5, mx4 + mx3__0), (mx6, mx5 ^ 0x0001), (mx7, mx3__1 <<< 2), (mx8, mx7 ^ mx6),
(mk2_out, Id(mk2__2)), (mx3_out, Id(mx3__2)), (mx8_out, Id(mx8)))
>>> mask_separators = [ (LinearMask(Variable("mx2", width=16)), LinearMask(Variable("mx3", width=16))), ]
>>> for cm in ch_model.split(mask_separators): print(cm)  
ChModel(func=SpeckKeySchedule_2R_0S,
        input_mask=[LinearMask(mk0), LinearMask(mk1), LinearMask(mk2)],
        output_mask=[LinearMask(mk0_out), LinearMask(mx3_out), LinearMask(mk2__2_out)],
        assign_outmask2op_model=[(LinearMask(mk2__0), LinearModelFreeBranch(LinearMask(mk2))),
            (LinearMask(mk2__1), LinearModelFreeBranch(LinearMask(mk2))),
            (LinearMask(mx1), LinearModelBvAdd([LinearMask(mk1 >>> 7), LinearMask(mk2__0)])),
            (LinearMask(mx3), LinearModelBvXor([LinearMask(mk2__1 <<< 2), LinearMask(mx1)])),
            (LinearMask(mk0_out), LinearModelId(LinearMask(mk0))),
            (LinearMask(mx3_out), LinearModelId(LinearMask(mx3))),
            (LinearMask(mk2__2_out), LinearModelId(LinearMask(mk2 ^ mk2__0 ^ mk2__1)))])
ChModel(func=SpeckKeySchedule_2R_1S,
        input_mask=[LinearMask(mk0), LinearMask(mx3), LinearMask(mk2__2)],
        output_mask=[LinearMask(mk2_out), LinearMask(mx3_out), LinearMask(mx8_out)],
        assign_outmask2op_model=[(LinearMask(mx3__0), LinearModelFreeBranch(LinearMask(mx3))),
            (LinearMask(mx3__1), LinearModelFreeBranch(LinearMask(mx3))),
            (LinearMask(mx5), LinearModelBvAdd([LinearMask(mk0 >>> 7), LinearMask(mx3__0)])),
            (LinearMask(mx8), LinearModelBvXor([LinearMask(mx3__1 <<< 2), LinearMask(mx5)])),
            (LinearMask(mk2_out), LinearModelId(LinearMask(mk2__2))),
            (LinearMask(mx3_out), LinearModelId(LinearMask(mx3 ^ mx3__0 ^ mx3__1))),
            (LinearMask(mx8_out), LinearModelId(LinearMask(mx8)))])
get_round_separators()[source]

Return the round separators if func is a RoundBasedFunction.

See also abstractproperty.chmodel.ChModel.get_round_separators.

>>> from cascada.linear.mask import LinearMask
>>> from cascada.linear.chmodel import ChModel
>>> from cascada.primitives import speck
>>> Speck32_KS = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64).key_schedule
>>> Speck32_KS.set_num_rounds(2)
>>> ch_model = ChModel(Speck32_KS, LinearMask, ["mk0", "mk1", "mk2"])
>>> sub_cms = ch_model.split(ch_model.get_round_separators())
>>> for cm in sub_cms: print(cm)  
ChModel(func=SpeckKeySchedule_2R_0S,
        input_mask=[LinearMask(mk0), LinearMask(mk1), LinearMask(mk2)],
        output_mask=[LinearMask(mk0_out), LinearMask(mx3_out), LinearMask(mk2__2_out)],
        assign_outmask2op_model=[(LinearMask(mk2__0), LinearModelFreeBranch(LinearMask(mk2))),
            (LinearMask(mk2__1), LinearModelFreeBranch(LinearMask(mk2))),
            (LinearMask(mx1), LinearModelBvAdd([LinearMask(mk1 >>> 7), LinearMask(mk2__0)])),
            (LinearMask(mx3), LinearModelBvXor([LinearMask(mk2__1 <<< 2), LinearMask(mx1)])),
            (LinearMask(mk0_out), LinearModelId(LinearMask(mk0))),
            (LinearMask(mx3_out), LinearModelId(LinearMask(mx3))),
            (LinearMask(mk2__2_out), LinearModelId(LinearMask(mk2 ^ mk2__0 ^ mk2__1)))])
ChModel(func=SpeckKeySchedule_2R_1S,
        input_mask=[LinearMask(mk0), LinearMask(mx3), LinearMask(mk2__2)],
        output_mask=[LinearMask(mk2_out), LinearMask(mx3_out), LinearMask(mx8_out)],
        assign_outmask2op_model=[(LinearMask(mx3__0), LinearModelFreeBranch(LinearMask(mx3))),
            (LinearMask(mx3__1), LinearModelFreeBranch(LinearMask(mx3))),
            (LinearMask(mx5), LinearModelBvAdd([LinearMask(mk0 >>> 7), LinearMask(mx3__0)])),
            (LinearMask(mx8), LinearModelBvXor([LinearMask(mx3__1 <<< 2), LinearMask(mx5)])),
            (LinearMask(mk2_out), LinearModelId(LinearMask(mk2__2))),
            (LinearMask(mx3_out), LinearModelId(LinearMask(mx3 ^ mx3__0 ^ mx3__1))),
            (LinearMask(mx8_out), LinearModelId(LinearMask(mx8)))])
class cascada.linear.chmodel.EncryptionChModel(cipher, mask_type, op_model_class2options=None)[source]

Bases: cascada.abstractproperty.chmodel.EncryptionChModel, cascada.linear.chmodel.ChModel

Represent linear characteristic models of encryption functions.

Given a Cipher, an EncryptionChModel is a bit-vector model (see ChModel) of a linear characteristic over the Cipher.encryption (where the Cipher.key_schedule is ignored and round key masks are set to LinearMask objects containing Variable objects).

See also linear.characteristic.EncryptionCharacteristic.

In an EncryptionChModel, the plaintext masks start with the prefix "mp", the intermediate and output masks start with the prefix "mx", and the round key masks (the masks of the external variables of the encryption SSA) start with the prefix "mk".

>>> from cascada.bitvector.core import Variable
>>> from cascada.linear.mask import LinearMask
>>> from cascada.linear.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 = EncryptionChModel(Speck32, LinearMask)
>>> ch_model  
EncryptionChModel(cipher=SpeckCipher_2R,
    input_mask=[LinearMask(mp0), LinearMask(mp1)],
    output_mask=[LinearMask(mx7_out), LinearMask(mx9_out)],
    external_var2mask=[(mk0, LinearMask(mk0)), (mk1, LinearMask(mk1))],
    assign_outmask2op_model=[(LinearMask(mp1__0), LinearModelFreeBranch(LinearMask(mp1))),
        (LinearMask(mx1), LinearModelBvAdd([LinearMask(mp0 >>> 7), LinearMask(mp1__0)])),
        (LinearMask(mx2), LinearModelBvXor([LinearMask(mx1), LinearMask(mk0)])),
        (LinearMask(mx2__0), LinearModelFreeBranch(LinearMask(mx2))),
        (LinearMask(mx4), LinearModelBvXor([LinearMask((mp1 ^ mp1__0) <<< 2), LinearMask(mx2__0)])),
        (LinearMask(mx4__0), LinearModelFreeBranch(LinearMask(mx4))),
        (LinearMask(mx6), LinearModelBvAdd([LinearMask((mx2 ^ mx2__0) >>> 7), LinearMask(mx4__0)])),
        (LinearMask(mx7), LinearModelBvXor([LinearMask(mx6), LinearMask(mk1)])),
        (LinearMask(mx7__0), LinearModelFreeBranch(LinearMask(mx7))),
        (LinearMask(mx9), LinearModelBvXor([LinearMask((mx4 ^ mx4__0) <<< 2), LinearMask(mx7__0)])),
        (LinearMask(mx7_out), LinearModelId(LinearMask(mx7 ^ mx7__0))),
        (LinearMask(mx9_out), LinearModelId(LinearMask(mx9)))])
>>> ch_model.ssa  
SSA(input_vars=[mp0, mp1], output_vars=[mx7_out, mx9_out], external_vars=[mk0, mk1],
assignments=[(mx0, mp0 >>> 7), (mp1__0, Id(mp1)), (mp1__1, Id(mp1)),
    (mx1, mx0 + mp1__0), (mx2, mx1 ^ mk0), (mx3, mp1__1 <<< 2), (mx2__0, Id(mx2)), (mx2__1, Id(mx2)),
        (mx4, mx3 ^ mx2__0), (mx5, mx2__1 >>> 7), (mx4__0, Id(mx4)), (mx4__1, Id(mx4)),
    (mx6, mx5 + mx4__0), (mx7, mx6 ^ mk1), (mx8, mx4__1 <<< 2), (mx7__0, Id(mx7)), (mx7__1, Id(mx7)),
        (mx9, mx8 ^ mx7__0), (mx7_out, Id(mx7__1)), (mx9_out, Id(mx9))])
vrepr()[source]

Return an executable string representation.

See also abstractproperty.chmodel.EncryptionChModel.vrepr.

>>> from cascada.bitvector.core import Variable
>>> from cascada.linear.mask import LinearMask
>>> from cascada.linear.chmodel import EncryptionChModel
>>> from cascada.primitives import speck
>>> Speck32 = speck.get_Speck_instance(speck.SpeckInstance.speck_32_64)
>>> Speck32.set_num_rounds(2)
>>> EncryptionChModel(Speck32, LinearMask).vrepr()
'EncryptionChModel(cipher=SpeckCipher.set_num_rounds_and_return(2), mask_type=LinearMask)'