diff --git a/claasp/cipher_modules/models/smt/smt_models/smt_xor_quasidifferential_model.py b/claasp/cipher_modules/models/smt/smt_models/smt_xor_quasidifferential_model.py new file mode 100644 index 000000000..dbacb41a9 --- /dev/null +++ b/claasp/cipher_modules/models/smt/smt_models/smt_xor_quasidifferential_model.py @@ -0,0 +1,2788 @@ +# **************************************************************************** +# Copyright 2023 Technology Innovation Institute +# +# This program is free software: you can redistribute it and/or modify +# it under the terms of the GNU General Public License as published by +# the Free Software Foundation, either version 3 of the License, or +# (at your option) any later version. +# +# This program is distributed in the hope that it will be useful, +# but WITHOUT ANY WARRANTY; without even the implied warranty of +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +# GNU General Public License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . +# **************************************************************************** + +import time +from collections import defaultdict + +from claasp.cipher_modules.models.smt import solvers +from claasp.cipher_modules.models.smt.smt_model import SmtModel +from claasp.cipher_modules.models.smt.utils import constants, utils +from claasp.cipher_modules.models.utils import get_single_key_scenario_format_for_fixed_values, set_component_solution + +from claasp.name_mappings import ( + CIPHER_OUTPUT, + CONSTANT, + INPUT_KEY, + INPUT_PLAINTEXT, + INTERMEDIATE_OUTPUT, + LINEAR_LAYER, + MIX_COLUMN, + PERMUTATION_COMPONENT, + SBOX, + WORD_OPERATION, + XOR_QUASIDIFFERENTIAL, +) + + +class SmtXorQuasidifferentialModel(SmtModel): + """ + SMT model of the XOR quasidifferential trails of a cipher [BR2022]_. + + Theorem, Definition and Equation numbers quoted in this module refer to [BR2022]_. + + Where ``SmtXorDifferentialModel`` searches differential characteristics, and so reports a + probability averaged over all keys, this model searches quasidifferential trails: a + characteristic together with a MASK on every intermediate state. Summing the signed correlation + of the trails of one differential gives its probability for a FIXED key (Theorem 4.1), which can + differ substantially from the average. + + The trail whose masks are all zero IS the differential characteristic, with the same weight, so + the lowest weight found here always equals the one the differential model finds. + + INPUT: + + - ``cipher`` -- **Cipher object**; the cipher to model + - ``counter`` -- **string** (default: `sequential`); the weight counter to use. ``"parallel"`` + is not supported, as in ``SmtXorDifferentialModel``. + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: speck = SpeckBlockCipher(number_of_rounds=2) + sage: smt = SmtXorQuasidifferentialModel(speck) + sage: smt.cipher_id + 'speck_p32_k64_o32_r2' + """ + + def __init__(self, cipher, counter="sequential"): + """ + Build the model, and map once which components read each wire bit. + + INPUT: + + - ``cipher`` -- **Cipher object**; the cipher to model + - ``counter`` -- **string** (default: `sequential`); the weight counter to use + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: smt = SmtXorQuasidifferentialModel(SpeckBlockCipher(number_of_rounds=2)) + + Bit 16 of the plaintext is read by two components, so it is a fork: + + sage: smt._wire_consumers[('plaintext', 16)] + [('modadd_0_1', 0), ('rot_0_3', 0)] + """ + super().__init__(cipher, counter) + self.sboxes_qdt_templates = {} + self.sboxes_qdt_matrices = {} + + # The input and output difference of each S-box, once a characteristic is given: {sbox_id: + # (a, b)}. An S-box appears here only if the characteristic decides both of its differences. + # An S-box whose differences are not decided is left out, and writes out its full table. + self.sbox_differences = {} + + # Which components read each wire bit, and which ids are read at all. A consumer is recorded + # once per READ, not once per component: see _component_wire_reads. + self._wire_consumers = defaultdict(list) + self._consumed_component_ids = set() + + for component in cipher.all_components(): + for source_id, position, read_index in self._component_wire_reads(component): + self._consumed_component_ids.add(source_id) + self._wire_consumers[(source_id, position)].append((component.id, read_index)) + + def build_xor_quasidifferential_trail_model(self, weight=-1, fixed_variables=[]): + """ + Build the SMT model of the quasidifferential trails. + + INPUT: + + - ``weight`` -- **integer** (default: `-1`); bound the total weight to at most this value. + ``-1`` leaves it unbounded. + - ``fixed_variables`` -- **list** (default: `[]`); DIFFERENCE constraints, built with + ``set_fixed_variables``. Masks cannot be fixed this way: see + ``estimate_fixed_key_probability``. + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: speck = SpeckBlockCipher(number_of_rounds=2) + sage: smt = SmtXorQuasidifferentialModel(speck) + sage: smt.build_xor_quasidifferential_trail_model() + sage: smt.model_constraints[0] + '(set-option :print-success false)' + + A wire read by two components gets one branch mask per reader, tied to the source by an XOR: + + sage: any('qdt_plaintext_16_to_modadd_0_1' in constraint + ....: for constraint in smt.model_constraints) + True + """ + self._variables_list = [] + + if fixed_variables == []: + fixed_variables = get_single_key_scenario_format_for_fixed_values(self._cipher) + + constraints = self.fix_variables_value_constraints(fixed_variables) + + # Work out each S-box's input and output difference from the values the caller already + # fixed. The S-box can then leave every transition that disagrees with them out of the + # model, nearly all of them, instead of writing them down for the solver to rule out one by + # one. + self.sbox_differences = self._sbox_differences_from(self._known_differences(fixed_variables)) + + component_types = ( + CIPHER_OUTPUT, + CONSTANT, + INTERMEDIATE_OUTPUT, + LINEAR_LAYER, + MIX_COLUMN, + PERMUTATION_COMPONENT, + SBOX, + WORD_OPERATION, + ) + operation_types = ("AND", "MODADD", "MODSUB", "NOT", "OR", "ROTATE", "SHIFT", "XOR") + + for component in self._cipher.all_components(): + operation = component.description[0] + + if component.type not in component_types or ( + component.type == WORD_OPERATION and operation not in operation_types + ): + print(f"{component.id} not yet implemented") + continue + + try: + variables, component_constraints = component.smt_xor_quasidifferential_propagation_constraints(self) + except NotImplementedError: + print(f"{component.id} not yet implemented") + continue + + self._variables_list.extend(variables) + constraints.extend(component_constraints) + + if weight != -1: + counter_variables, weight_constraints = self.weight_constraints(weight) + self._variables_list.extend(counter_variables) + constraints.extend(weight_constraints) + + fork_variables, fork_constraints = self._fork_constraints() + self._variables_list.extend(fork_variables) + constraints.extend(fork_constraints) + constraints.extend(self._unread_input_mask_constraints()) + constraints.extend(self._terminal_tap_mask_constraints()) + self._variables_list.extend(self.cipher_input_variables()) + self._variables_list.extend(f"qdt_{variable_name}" for variable_name in self.cipher_input_variables()) + self._declarations_builder() + self._model_constraints = constants.MODEL_PREFIX + self._declarations + constraints + constants.MODEL_SUFFIX + + def _input_wires(self, component): + """ + Return the source of each input bit of ``component``, in the order it reads them. + + Each source is a ``(source_id, bit_position)`` pair. + + INPUT: + + - ``component`` -- **Component object**; a component of the cipher + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.xor_cipher import XorCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = XorCipher(word_bit_size=2, number_of_inputs=2) + sage: smt = SmtXorQuasidifferentialModel(cipher) + sage: smt._input_wires(cipher.component_from_id('xor_0_0')) + [('plaintext', 0), ('plaintext', 1), ('key', 0), ('key', 1)] + """ + return [(source_id, position) for source_id, position, _ in self._component_wire_reads(component)] + + def _difference_bit_map(self, component): + """ + Return which input bit each output bit of a bit-moving component copies. + + Entry ``i`` is the position in ``_input_wires`` that output bit ``i`` copies, or ``None`` if + the component forces output bit ``i`` to zero, as a shift does. + + The whole result is ``None`` for a component that does more than move bits, an S-box above + all, whose output difference does not follow from its input difference at all. + + Difference and mask both travel along this same map, so both directions of the propagation + read it: forward looks up where an output bit came from, backward where an input bit went. + + Each case mirrors that component's own ``smt_constraints``, so the two cannot drift apart. + + INPUT: + + - ``component`` -- **Component object**; a component of the cipher + + EXAMPLES: + + A rotation by one, on two bits, swaps them:: + + sage: from claasp.ciphers.single_component_ciphers.rotate_cipher import RotateCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = RotateCipher(bit_size=2, rotation_amount=1) + sage: smt = SmtXorQuasidifferentialModel(cipher) + sage: smt._difference_bit_map(cipher.component_from_id('rot_0_0')) + [1, 0] + + An S-box does more than move bits, so it is refused:: + + sage: from claasp.ciphers.block_ciphers.rectangle_block_cipher import RectangleBlockCipher + sage: rectangle = RectangleBlockCipher(number_of_rounds=1) + sage: smt = SmtXorQuasidifferentialModel(rectangle) + sage: smt._difference_bit_map(rectangle.component_from_id('sbox_0_1')) is None + True + """ + positions = list(range(len(self._input_wires(component)))) + output_bit_size = component.output_bit_size + + if component.type in (CIPHER_OUTPUT, INTERMEDIATE_OUTPUT): + # These only concatenate the bits they read. + return positions if len(positions) == output_bit_size else None + + if component.type == PERMUTATION_COMPONENT: + return list(component._bit_perm()) + + if component.type != WORD_OPERATION: + return None + + operation = component.description[0] + + if operation == "NOT": + # Theorem 3.2 (4): a translation leaves the difference alone. + return positions if len(positions) == output_bit_size else None + + if operation == "ROTATE": + rotation = component.description[1] + return positions[-rotation:] + positions[:-rotation] + + if operation == "SHIFT": + return self._shift_bit_map(output_bit_size, component.description[1]) + + return None + + @staticmethod + def _shift_bit_map(output_bit_size, shift_amount): + """ + Return the bit map of a shift by ``shift_amount``, as ``_difference_bit_map`` describes it. + + A positive amount shifts right and a negative one left; the vacated bits are forced to zero + and map to ``None``. + + INPUT: + + - ``output_bit_size`` -- **integer**; the number of bits shifted + - ``shift_amount`` -- **integer**; the shift amount, negative for a left shift + + EXAMPLES:: + + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: SmtXorQuasidifferentialModel._shift_bit_map(4, 1) + [None, 0, 1, 2] + sage: SmtXorQuasidifferentialModel._shift_bit_map(4, -1) + [1, 2, 3, None] + """ + bit_map = [None] * output_bit_size + + if shift_amount < 0: + shift_amount = -shift_amount + for index in range(output_bit_size - shift_amount): + bit_map[index] = shift_amount + index + else: + for index in range(output_bit_size - shift_amount): + bit_map[shift_amount + index] = index + + return bit_map + + def _wire_bit(self, known, source_id, position): + """ + Return bit ``position`` of ``source_id``'s difference, or ``None`` when not yet known. + + INPUT: + + - ``known`` -- **dictionary**; a ``_known_differences`` map + - ``source_id`` -- **string**; the id of a cipher input or of a component + - ``position`` -- **integer**; the bit position in ``source_id`` + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.xor_cipher import XorCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: smt = SmtXorQuasidifferentialModel(XorCipher(word_bit_size=2, number_of_inputs=2)) + sage: smt._wire_bit({'plaintext': [1, None]}, 'plaintext', 0) + 1 + sage: smt._wire_bit({'plaintext': [1, None]}, 'key', 0) is None + True + """ + bits = known.get(source_id) + return None if bits is None else bits[position] + + def _learn(self, known, id_, positions_and_bits): + """ + Record difference bits of ``id_``, and say whether any were new. + + A bit already recorded with the other value means the fixed values contradict each other, + which is raised rather than dropped. + + INPUT: + + - ``known`` -- **dictionary**; a ``_known_differences`` map, updated in place + - ``id_`` -- **string**; the id of a cipher input or of a component + - ``positions_and_bits`` -- **iterable**; the ``(position, bit)`` pairs to record; a + ``None`` bit is skipped + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.xor_cipher import XorCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: smt = SmtXorQuasidifferentialModel(XorCipher(word_bit_size=2, number_of_inputs=2)) + sage: known = {} + sage: smt._learn(known, 'plaintext', [(0, 1)]), known + (True, {'plaintext': [1, None]}) + sage: smt._learn(known, 'plaintext', [(0, 1)]) + False + """ + bits = known.setdefault(id_, [None] * self._bit_size_of(id_)) + changed = False + + for position, bit in positions_and_bits: + if bit is None: + continue + + if bits[position] is None: + bits[position] = bit + changed = True + elif bits[position] != bit: + raise ValueError( + f"{id_} bit {position}: the fixed values force both " + f"{bits[position]} and {bit}, so they contradict each other" + ) + + return changed + + def _propagate_forward(self, component, known): + """ + Work out ``component``'s output difference from its inputs. + + Return whether anything was learned. + + Only components whose output difference follows from their input difference. An S-box's does + not, which is the whole reason its difference has to come from the fixed values instead. + + INPUT: + + - ``component`` -- **Component object**; a component of the cipher + - ``known`` -- **dictionary**; a ``_known_differences`` map, updated in place + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.xor_cipher import XorCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = XorCipher(word_bit_size=2, number_of_inputs=2) + sage: smt = SmtXorQuasidifferentialModel(cipher) + sage: known = {'plaintext': [1, 0], 'key': [1, 1]} + sage: smt._propagate_forward(cipher.component_from_id('xor_0_0'), known) + True + sage: known['xor_0_0'] + [0, 1] + """ + if component.type == CONSTANT: + # A constant is the same in both members of the pair. + return self._learn(known, component.id, [(position, 0) for position in range(component.output_bit_size)]) + + wires = self._input_wires(component) + input_bits = [self._wire_bit(known, source_id, position) for source_id, position in wires] + output_bit_size = component.output_bit_size + + if component.type == WORD_OPERATION and component.description[0] == "XOR": + learned = [] + + for position in range(output_bit_size): + operands = input_bits[position::output_bit_size] + + if None not in operands: + learned.append((position, sum(operands) % 2)) + + return self._learn(known, component.id, learned) + + bit_map = self._difference_bit_map(component) + + if bit_map is None or None in input_bits: + return False + + return self._learn( + known, + component.id, + [(position, 0 if source is None else input_bits[source]) for position, source in enumerate(bit_map)], + ) + + def _propagate_backward(self, component, known): + """ + Work out ``component``'s input differences from its output. + + Return whether anything was learned. + + This is the direction an S-box layer needs: the caller fixes a round output, and the S-box + output differences are only reachable by pulling that back through the linear layer above + them. + + INPUT: + + - ``component`` -- **Component object**; a component of the cipher + - ``known`` -- **dictionary**; a ``_known_differences`` map, updated in place + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.rotate_cipher import RotateCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = RotateCipher(bit_size=2, rotation_amount=1) + sage: smt = SmtXorQuasidifferentialModel(cipher) + sage: known = {'rot_0_0': [1, 0]} + sage: smt._propagate_backward(cipher.component_from_id('rot_0_0'), known) + True + sage: known['plaintext'] + [0, 1] + """ + output_bits = known.get(component.id) + + if output_bits is None: + return False + + wires = self._input_wires(component) + + if component.type == WORD_OPERATION and component.description[0] == "XOR": + return self._xor_backward(component, wires, output_bits, known) + + bit_map = self._difference_bit_map(component) + + if bit_map is None: + return False + + changed = False + + for position, source in enumerate(bit_map): + if source is None or output_bits[position] is None: + continue + + source_id, source_position = wires[source] + changed |= self._learn(known, source_id, [(source_position, output_bits[position])]) + + return changed + + def _xor_backward(self, component, wires, output_bits, known): + """ + Solve an XOR for its one unknown operand, bit position by bit position. + + The XOR is given by its ``_input_wires`` and its known output difference. A position whose + operands are all known teaches nothing, and one with two or more unknowns is not determined, + so only the single-unknown case is used. + + INPUT: + + - ``component`` -- **Component object**; an XOR component of the cipher + - ``wires`` -- **list**; the ``_input_wires`` of ``component`` + - ``output_bits`` -- **list**; the output difference of ``component``, ``None`` where + unknown + - ``known`` -- **dictionary**; a ``_known_differences`` map, updated in place + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.xor_cipher import XorCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = XorCipher(word_bit_size=2, number_of_inputs=2) + sage: smt = SmtXorQuasidifferentialModel(cipher) + sage: xor = cipher.component_from_id('xor_0_0') + sage: known = {'xor_0_0': [0, 1], 'key': [1, 1]} + sage: smt._xor_backward(xor, smt._input_wires(xor), known['xor_0_0'], known) + True + sage: known['plaintext'] + [1, 0] + """ + output_bit_size = component.output_bit_size + changed = False + + for position in range(output_bit_size): + if output_bits[position] is None: + continue + + column = list(range(position, len(wires), output_bit_size)) + unknown = [index for index in column if self._wire_bit(known, *wires[index]) is None] + + if len(unknown) != 1: + continue + + parity = output_bits[position] + + for index in column: + if index != unknown[0]: + parity ^= self._wire_bit(known, *wires[index]) + + source_id, source_position = wires[unknown[0]] + changed |= self._learn(known, source_id, [(source_position, parity)]) + + return changed + + def _known_differences(self, fixed_variables): + """ + Return the difference of every wire that ``fixed_variables`` already settles. + + The result is ``{id: [bit, ...]}``, with ``None`` where a bit is still unknown. + + The fixed values are the starting point. From there differences are pushed forward and + pulled backward through the components that only move or combine bits, until nothing more is + learned. Nothing is guessed: a bit is recorded only where the wiring forces it, so a + characteristic that leaves wires undecided simply leaves them undecided here. + + INPUT: + + - ``fixed_variables`` -- **list**; difference constraints, built with + ``set_fixed_variables`` + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.xor_cipher import XorCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: from claasp.cipher_modules.models.utils import set_fixed_variables + sage: cipher = XorCipher(word_bit_size=2, number_of_inputs=2) + sage: smt = SmtXorQuasidifferentialModel(cipher) + sage: fixed = [set_fixed_variables('plaintext', 'equal', range(2), [1, 0]), + ....: set_fixed_variables('key', 'equal', range(2), [1, 1])] + sage: smt._known_differences(fixed)['xor_0_0'] + [0, 1] + + Fixing the output instead works just as well, since the XOR is also pulled backward: + + sage: fixed = [set_fixed_variables('xor_0_0', 'equal', range(2), [0, 1]), + ....: set_fixed_variables('key', 'equal', range(2), [1, 1])] + sage: smt._known_differences(fixed)['plaintext'] + [1, 0] + """ + known = {} + cipher_ids = set(self._cipher.inputs) | {component.id for component in self._cipher.all_components()} + + for fixed in fixed_variables: + if fixed.get("constraint_type") != "equal" or fixed["component_id"] not in cipher_ids: + continue + + self._learn( + known, fixed["component_id"], zip(fixed["bit_positions"], (int(bit) for bit in fixed["bit_values"])) + ) + + changed = True + + while changed: + changed = False + + for component in self._cipher.all_components(): + changed |= self._propagate_forward(component, known) + changed |= self._propagate_backward(component, known) + + return known + + def _sbox_differences_from(self, known): + """ + Collect the S-boxes from ``known``, as ``{sbox_id: (a, b)}``. + + There is one entry per S-box whose input difference ``a`` and output difference ``b`` are + both known. ``known`` is the map of wire differences that ``_known_differences`` builds. + + Only S-boxes need this. An S-box is modelled from a table, one case for each transition it + allows, and fixing ``a`` and ``b`` keeps only the few cases that agree with them. Every + other component is modelled from a formula, so it is small already. + + An S-box that the characteristic does not decide is left out, and keeps its whole table. + That is slower to solve but just as correct, which is why this is safe to do automatically. + + INPUT: + + - ``known`` -- **dictionary**; a ``_known_differences`` map + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.rectangle_block_cipher import RectangleBlockCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: smt = SmtXorQuasidifferentialModel(RectangleBlockCipher(number_of_rounds=1)) + sage: smt._sbox_differences_from({}) + {} + """ + differences = {} + + for component in self._cipher.all_components(): + if component.type != SBOX: + continue + + output_bits = known.get(component.id) + + if output_bits is None or None in output_bits: + continue + + input_bits = [ + self._wire_bit(known, source_id, position) for source_id, position in self._input_wires(component) + ] + + if None in input_bits: + continue + + differences[component.id] = (self._bits_to_integer(input_bits), self._bits_to_integer(output_bits)) + + return differences + + @staticmethod + def _bits_to_integer(bits): + """ + The integer of a bit list, bit 0 being the most significant. + + INPUT: + + - ``bits`` -- **list**; the bits, each one ``0`` or ``1`` + + EXAMPLES:: + + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: SmtXorQuasidifferentialModel._bits_to_integer([1, 0, 1, 1]) + 11 + """ + value = 0 + + for bit in bits: + value = (value << 1) | bit + + return value + + def _qdt_local_weight_variables(self, component, max_weight): + """ + The local weight indicators ``hw_qdt__`` of a component. + + INPUT: + + - ``component`` -- **Component object**; a component of the cipher + - ``max_weight`` -- **integer**; the highest local weight the component can have + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.xor_cipher import XorCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = XorCipher(word_bit_size=2, number_of_inputs=2) + sage: smt = SmtXorQuasidifferentialModel(cipher) + sage: smt._qdt_local_weight_variables(cipher.component_from_id('xor_0_0'), 3) + ['hw_qdt_xor_0_0_0', 'hw_qdt_xor_0_0_1', 'hw_qdt_xor_0_0_2'] + """ + return [f"hw_qdt_{component.id}_{i}" for i in range(int(max_weight))] + + def _qdt_weight_constraints(self, weight_variables, weight): + """ + Thermometer encoding of ``weight``: the first ``weight`` indicators true, the others false. + + INPUT: + + - ``weight_variables`` -- **list**; the local weight indicators of a component + - ``weight`` -- **integer**; the local weight to encode + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.xor_cipher import XorCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = XorCipher(word_bit_size=2, number_of_inputs=2) + sage: smt = SmtXorQuasidifferentialModel(cipher) + sage: smt._qdt_weight_constraints(['hw_0', 'hw_1', 'hw_2'], 2) + ['hw_0', 'hw_1', '(not hw_2)'] + """ + return [variable if i < weight else utils.smt_not(variable) for i, variable in enumerate(weight_variables)] + + def calculate_component_weight(self, component, out_suffix, output_values_dict): + """ + Calculate the local quasidifferential weight. + + Generalized to any component that declares hw_qdt_{component.id}_* weight-bit variables + (currently: Sbox, via a thermometer encoding; And, via a single per-bit OR indicator -- see + And.smt_xor_quasidifferential_propagation_constraints). For components with no such + variables (XOR, LinearLayer, ...) the sum is naturally 0, since none match the prefix. + + INPUT: + + - ``component`` -- **Component object**; a component of the cipher + - ``out_suffix`` -- **string**; the suffix of the output variables, unused here + - ``output_values_dict`` -- **dictionary**; the solver assignment, from variable name to + value + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: speck = SpeckBlockCipher(number_of_rounds=2) + sage: smt = SmtXorQuasidifferentialModel(speck) + sage: xor = speck.component_from_id('xor_0_2') + sage: smt.calculate_component_weight(xor, '', {}) + 0 + """ + prefix = f"hw_qdt_{component.id}_" + return sum(value for variable, value in output_values_dict.items() if variable.startswith(prefix)) + + @staticmethod + def get_qdt_transitions(weights): + """ + Flatten a QDT weight table into explicit transitions. + + INPUT: + + - ``weights`` -- **dictionary**; a weight table, as built by ``generate_weight_tables``: + ``weights[(b, a)][weight_loss]`` is the list of the ``(v, u)`` mask pairs of the + differential ``a -> b`` having that weight loss + + OUTPUT: + + - **list**; one dictionary per transition, with keys ``"a"``, ``"u"``, ``"b"``, ``"v"`` and + ``"weight"`` + + EXAMPLES:: + + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: weights = {(0x2, 0x1): {1: [(0x3, 0x4)]}} + sage: SmtXorQuasidifferentialModel.get_qdt_transitions(weights) + [{'a': 1, 'b': 2, 'u': 4, 'v': 3, 'weight': 1}] + """ + transitions = [] + + for (b, a), weight_dict in weights.items(): + for weight_loss, mask_pairs in weight_dict.items(): + for v, u in mask_pairs: + transitions.append({"a": a, "u": u, "b": b, "v": v, "weight": weight_loss}) + + return transitions + + @staticmethod + def _component_wire_reads(component): + """ + Yield ``(source_id, position, read_index)`` for every input bit a component reads. + + The bits come in the order the component's constraints use them. + + ``read_index`` counts how many times THIS component has already read THIS bit. A component + may read the same wire bit more than once -- DES's expansion feeds 16 bits of + ``permutation_0_0`` into both halves of ``xor_0_7`` -- and each read is a separate branch of + the copy map, so each needs its own mask variable. Keying a branch by consumer id alone + gives the two reads one name, and ``_fork_constraints`` then emits it twice inside one + ``xor``, where it cancels: the branch drops out of the source relation entirely. + + ``__init__``, ``_qdt_input_bit_ids`` and ``_read_component_input_mask`` all walk the reads + through this one generator, so the three stay aligned by construction. + + INPUT: + + - ``component`` -- **Component object**; a component of the cipher + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.xor_cipher import XorCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = XorCipher(word_bit_size=2, number_of_inputs=2) + sage: list(SmtXorQuasidifferentialModel._component_wire_reads(cipher.component_from_id('xor_0_0'))) + [('plaintext', 0, 0), ('plaintext', 1, 0), ('key', 0, 0), ('key', 1, 0)] + """ + reads_so_far = defaultdict(int) + + for input_id, bit_positions in zip(component.input_id_links, component.input_bit_positions): + for position in bit_positions: + read_index = reads_so_far[(input_id, position)] + reads_so_far[(input_id, position)] += 1 + yield input_id, position, read_index + + @staticmethod + def _branch_mask_id(source_id, position, consumer_id, read_index): + """ + Return the name of the branch mask of one read of a forked wire bit. + + It is the mask through which ``consumer_id``'s ``read_index``-th read of ``source_id`` bit + ``position`` sees the wire. The first read keeps the plain ``_to_`` form. + + INPUT: + + - ``source_id`` -- **string**; the id of the wire's source + - ``position`` -- **integer**; the bit position in ``source_id`` + - ``consumer_id`` -- **string**; the id of the component reading the bit + - ``read_index`` -- **integer**; how many times ``consumer_id`` read the bit before + + EXAMPLES:: + + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: SmtXorQuasidifferentialModel._branch_mask_id('plaintext', 16, 'modadd_0_1', 0) + 'qdt_plaintext_16_to_modadd_0_1' + + A further read of the same bit by the same component, as in DES: + + sage: SmtXorQuasidifferentialModel._branch_mask_id('permutation_0_0', 63, 'xor_0_7', 1) + 'qdt_permutation_0_0_63_to_xor_0_7_read1' + """ + suffix = "" if read_index == 0 else f"_read{read_index}" + return f"qdt_{source_id}_{position}_to_{consumer_id}{suffix}" + + def qdt_input_bit_id(self, component, source_id, position, read_index=0): + """ + Return the mask variable through which ``component`` reads a wire bit. + + It is the variable of ``component``'s ``read_index``-th read of bit ``position`` of + ``source_id``. + + A wire read exactly once keeps the shared name, which is correct: the XOR of a single branch + mask is that mask. A FORKED wire gets one variable per read, tied to the source by the XOR + constraint in ``_fork_constraints``. + + INPUT: + + - ``component`` -- **Component object**; the component reading the bit + - ``source_id`` -- **string**; the id of the wire's source + - ``position`` -- **integer**; the bit position in ``source_id`` + - ``read_index`` -- **integer** (default: `0`); how many times ``component`` read the bit + before + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: speck = SpeckBlockCipher(number_of_rounds=2) + sage: smt = SmtXorQuasidifferentialModel(speck) + + Bit 16 of the plaintext is read by two components, so each read sees the wire through its + own branch mask: + + sage: smt.qdt_input_bit_id(speck.component_from_id('modadd_0_1'), 'plaintext', 16) + 'qdt_plaintext_16_to_modadd_0_1' + + Bit 0 has a single reader, and keeps the shared name -- the XOR of one branch is that + branch: + + sage: smt.qdt_input_bit_id(speck.component_from_id('rot_0_0'), 'plaintext', 0) + 'qdt_plaintext_0' + """ + consumers = self._wire_consumers.get((source_id, position), ()) + + if len(consumers) <= 1: + return f"qdt_{source_id}_{position}" + + return self._branch_mask_id(source_id, position, component.id, read_index) + + def _fork_constraints(self): + """ + Return the fork constraints: the source mask is the XOR of the branch masks. + + This is the dual of the XOR-of-differences rule at a join point. + + Verified against Equation (4) on the copy map F(x) = (x, x): over all 3-bit combinations, + 512 transitions have a nonzero coefficient, and ALL of them satisfy u = v1 xor v2, while + only 8 satisfy u = v1 = v2. Sharing one variable among consumers -- which is what the plain + qdt_ naming does -- imposes the latter, a constraint 64 times too strong. + + Forks are the normal structure of a cipher, not an edge case: Speck has 96 forked wires at + two rounds and 320 at six, RECTANGLE 172 at a single round. + + INPUT: + + - None + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: smt = SmtXorQuasidifferentialModel(SpeckBlockCipher(number_of_rounds=2)) + sage: variables, constraints = smt._fork_constraints() + sage: len(constraints), len(variables) + (96, 256) + sage: constraints[0] + '(assert (= qdt_plaintext_16 (xor qdt_plaintext_16_to_modadd_0_1 qdt_plaintext_16_to_rot_0_3)))' + """ + variables = [] + constraints = [] + + for (source_id, position), consumers in self._wire_consumers.items(): + if len(consumers) <= 1: + continue + + source = f"qdt_{source_id}_{position}" + branches = [ + self._branch_mask_id(source_id, position, consumer_id, read_index) + for consumer_id, read_index in consumers + ] + variables.extend(branches) + equation = utils.smt_equivalent([source, utils.smt_xor(branches)]) + constraints.append(utils.smt_assert(equation)) + + return variables, constraints + + def _unread_input_mask_constraints(self): + """ + Force to zero the mask of every cipher-input bit that no component reads. + + Such a bit does not influence the cipher, so a trail carrying a non-zero mask on it has + correlation zero -- it is not a trail. Leaving the variable free is also expensive: nothing + in the model constrains it, yet ``_qdt_get_operands`` puts every primary-input mask bit into + the blocking clause, so each of its 2^k assignments would be enumerated as a distinct trail + and summed again by ``estimate_fixed_key_probability``. Speck 8/16 at one round has 12 such + bits, Speck 32/64 at two rounds has 32. + + INPUT: + + - None + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: speck = SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=1) + sage: constraints = SmtXorQuasidifferentialModel(speck)._unread_input_mask_constraints() + sage: len(constraints), constraints[0] + (12, '(assert (not qdt_key_0))') + """ + constraints = [] + + for input_id, bit_size in zip(self._cipher.inputs, self._cipher.inputs_bit_size): + for position in range(bit_size): + if self._wire_consumers.get((input_id, position)): + continue + + constraints.append(utils.smt_assert(utils.smt_not(f"qdt_{input_id}_{position}"))) + + return constraints + + def _terminal_tap_mask_constraints(self): + """ + Force to zero the mask of every IntermediateOutput that no component reads. + + Such a component is an observation point -- it exposes a wire without consuming it -- and is + not a coordinate of the function the trail describes. Theorem 3.2's copy rule still hands it + a fork branch, though (the source mask is the XOR of ALL branches), and leaving that branch + free lets the solver push arbitrary mask into the tap, decoupling a producer's + Theorem-constrained output mask from what the next round reads. On 2-round Speck that admits + a spurious weight-2 trail whose sign cancels the genuine one, turning a fixed-key + probability of 2^-2 into 0. + + CipherOutput is deliberately NOT included: its bits ARE coordinates of the cipher's output + -- in Speck the round output is read by the next round AND exposed, a genuine fan-out -- and + their masks are the boundary masks of Theorem 4.1, which the caller pins through + ``fixed_masks``. An IntermediateOutput that some component does read is likewise a real wire + in the data path and keeps a free mask. + + INPUT: + + - None + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: speck = SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=1) + sage: constraints = SmtXorQuasidifferentialModel(speck)._terminal_tap_mask_constraints() + sage: len(constraints), constraints[0] + (4, '(assert (not qdt_intermediate_output_0_5_0))') + """ + constraints = [] + + for component in self._cipher.all_components(): + if component.type != INTERMEDIATE_OUTPUT: + continue + + if component.id in self._consumed_component_ids: + continue + + constraints.extend( + utils.smt_assert(utils.smt_not(f"qdt_{component.id}_{position}")) + for position in range(component.output_bit_size) + ) + + return constraints + + def _qdt_input_bit_ids(self, component): + """ + Return the QDT mask variables of the inputs of ``component``. + + Forked wires get their per-read branch variables. + + INPUT: + + - ``component`` -- **Component object**; a component of the cipher + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.xor_cipher import XorCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = XorCipher(word_bit_size=2, number_of_inputs=2) + sage: smt = SmtXorQuasidifferentialModel(cipher) + sage: smt._qdt_input_bit_ids(cipher.component_from_id('xor_0_0')) + ['qdt_plaintext_0', 'qdt_plaintext_1', 'qdt_key_0', 'qdt_key_1'] + """ + return [ + self.qdt_input_bit_id(component, input_id, position, read_index) + for input_id, position, read_index in self._component_wire_reads(component) + ] + + def _bit_moving_propagation_constraints(self, component, mask_pairs): + """ + Return the constraints of a component that only moves, copies or drops bits. + + These are NOT, Permutation, Rotate and Shift. + + The difference goes through the component's own differential constraints. On the mask side, + each ``(output, input)`` entry of ``mask_pairs`` ties output mask bit ``output`` to input + mask bit ``input``; an entry ``(None, input)`` forces that input mask bit to zero, because + the map discards the bit. Entries are emitted in the order given. + + INPUT: + + - ``component`` -- **Component object**; a NOT, Permutation, Rotate or Shift component + - ``mask_pairs`` -- **list**; the ``(output, input)`` position pairs tying the masks + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.rotate_cipher import RotateCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = RotateCipher(bit_size=2, rotation_amount=1) + sage: rotate = cipher.component_from_id('rot_0_0') + sage: smt = SmtXorQuasidifferentialModel(cipher) + sage: variables, constraints = smt._bit_moving_propagation_constraints(rotate, [(0, 1), (1, 0)]) + sage: constraints + ['(assert (= rot_0_0_0 plaintext_1))', + '(assert (= rot_0_0_1 plaintext_0))', + '(assert (= qdt_rot_0_0_0 qdt_plaintext_1))', + '(assert (= qdt_rot_0_0_1 qdt_plaintext_0))'] + + An input bit the map discards gets a zero mask: + + sage: smt._bit_moving_propagation_constraints(rotate, [(0, 1), (None, 0)])[1][-1] + '(assert (not qdt_plaintext_0))' + """ + output_bit_ids, diff_constraints = component.smt_xor_differential_propagation_constraints(self) + qdt_input_bit_ids = self._qdt_input_bit_ids(component) + qdt_output_bit_ids = [f"qdt_{bit_id}" for bit_id in output_bit_ids] + mask_constraints = [] + + for output_position, input_position in mask_pairs: + input_mask = qdt_input_bit_ids[input_position] + + if output_position is None: + mask_constraints.append(utils.smt_assert(utils.smt_not(input_mask))) + else: + equation = utils.smt_equivalent([qdt_output_bit_ids[output_position], input_mask]) + mask_constraints.append(utils.smt_assert(equation)) + + return output_bit_ids + qdt_output_bit_ids, diff_constraints + mask_constraints + + def _constrain_weight_exactly(self, weight): + """ + Turn the bound on the total weight into an equality. + + The "total weight <= weight" bound that ``weight_constraints`` imposes becomes "total weight + == weight", for any weight, including the two the sequential counter cannot express. + + ``_sequential_counter_greater_or_equal`` rewrites "at least w" as "at most n - w" over the + negated indicators, so w == n makes its inner dimension zero and it raises ``IndexError`` -- + which is reachable through the public API: on 8-bit Speck at one round the model has few + enough ``hw_`` indicators that asking for weight 4 crashes. Both edge cases have an exact, + cheap encoding: + + - ``weight == n``: "at least all of them" is just all of them; + - ``weight > n``: no assignment has that weight, so the model is unsatisfiable and should + say so rather than raise. + + INPUT: + + - ``weight`` -- **integer**; the exact total weight + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: from claasp.cipher_modules.models.smt.utils import constants + sage: smt = SmtXorQuasidifferentialModel(SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=1)) + sage: smt.build_xor_quasidifferential_trail_model(weight=1) + sage: len([variable for variable in smt._variables_list if variable.startswith('hw_')]) + 4 + + Asking for more weight than there are indicators makes the model unsatisfiable instead of + raising: + + sage: smt._constrain_weight_exactly(5) + sage: smt._model_constraints[-len(constants.MODEL_SUFFIX) - 1] + '(assert false)' + """ + hw_list = [variable_id for variable_id in self._variables_list if variable_id.startswith("hw_")] + + if weight > len(hw_list): + extra = [utils.smt_assert("false")] + elif weight == len(hw_list): + extra = [utils.smt_assert(variable_id) for variable_id in hw_list] + else: + if self._counter == self._sequential_counter: + self._sequential_counter_greater_or_equal(weight, "dummy_hw_1") + return + + self._model_constraints = ( + self._model_constraints[: -len(constants.MODEL_SUFFIX)] + extra + constants.MODEL_SUFFIX + ) + + def find_one_xor_quasidifferential_trail( + self, fixed_values=[], fixed_masks=None, solver_name=solvers.SOLVER_DEFAULT + ): + """ + Find one XOR quasidifferential trail. + + INPUT: + + - ``fixed_values`` -- **list** (default: `[]`); can be created using ``set_fixed_variables`` + method + - ``fixed_masks`` -- **list** (default: `None`); mask constraints, which ``fixed_values`` + cannot express, in the format described in ``estimate_fixed_key_probability``; see + ``boundary_masks`` + - ``solver_name`` -- **string** (default: `Z3_EXT`); the name of the solver + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: speck = SpeckBlockCipher(number_of_rounds=1) + sage: smt = SmtXorQuasidifferentialModel(speck) + sage: trail = smt.find_one_xor_quasidifferential_trail() + sage: trail['total_weight'] >= 0 + True + + Every component reports a mask next to its difference: + + sage: 'mask' in trail['components_values']['cipher_output_0_6'] + True + """ + start_building_time = time.time() + self.build_xor_quasidifferential_trail_model(fixed_variables=fixed_values) + self._apply_fixed_masks(fixed_masks) + end_building_time = time.time() + solution = self.solve(XOR_QUASIDIFFERENTIAL, solver_name=solver_name) + solution["building_time_seconds"] = end_building_time - start_building_time + solution["test_name"] = "find_one_xor_quasidifferential_trail" + return solution + + def find_one_xor_quasidifferential_trail_with_fixed_weight( + self, fixed_weight, fixed_values=[], fixed_masks=None, solver_name=solvers.SOLVER_DEFAULT + ): + """ + Find one XOR quasidifferential trail with a fixed total weight loss. + + INPUT: + + - ``fixed_weight`` -- **integer**; the total weight of the trail + - ``fixed_values`` -- **list** (default: `[]`); can be created using ``set_fixed_variables`` + method + - ``fixed_masks`` -- **list** (default: `None`); mask constraints, which ``fixed_values`` + cannot express, in the format described in ``estimate_fixed_key_probability``; see + ``boundary_masks`` + - ``solver_name`` -- **string** (default: `Z3_EXT`); the name of the solver + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: speck = SpeckBlockCipher(number_of_rounds=3) + sage: smt = SmtXorQuasidifferentialModel(speck) + sage: trail = smt.find_one_xor_quasidifferential_trail_with_fixed_weight(3) + sage: trail['total_weight'] + 3.0 + """ + start_building_time = time.time() + self.build_xor_quasidifferential_trail_model(weight=fixed_weight, fixed_variables=fixed_values) + self._constrain_weight_exactly(fixed_weight) + self._apply_fixed_masks(fixed_masks) + end_building_time = time.time() + solution = self.solve(XOR_QUASIDIFFERENTIAL, solver_name=solver_name) + solution["building_time_seconds"] = end_building_time - start_building_time + solution["test_name"] = "find_one_xor_quasidifferential_trail_with_fixed_weight" + return solution + + def find_lowest_weight_xor_quasidifferential_trail( + self, fixed_values=[], fixed_masks=None, solver_name=solvers.SOLVER_DEFAULT + ): + """ + Return a quasidifferential trail with the lowest total weight loss. + + Mirrors SmtXorDifferentialModel.find_lowest_weight_xor_differential_trail: increases the + weight bound from 0 until a solution is found. + + INPUT: + + - ``fixed_values`` -- **list** (default: `[]`); can be created using ``set_fixed_variables`` + method + - ``fixed_masks`` -- **list** (default: `None`); mask constraints, which ``fixed_values`` + cannot express, in the format described in ``estimate_fixed_key_probability``; see + ``boundary_masks`` + - ``solver_name`` -- **string** (default: `Z3_EXT`); the name of the solver + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: speck = SpeckBlockCipher(number_of_rounds=5) + sage: smt = SmtXorQuasidifferentialModel(speck) + sage: trail = smt.find_lowest_weight_xor_quasidifferential_trail() + sage: trail['total_weight'] + 9.0 + + This is the weight ``SmtXorDifferentialModel`` reports for the same cipher, and it must be: + the lowest-weight trail is the one with all masks zero, which is the differential + characteristic itself. + """ + current_weight = 0 + start_building_time = time.time() + self.build_xor_quasidifferential_trail_model(weight=current_weight, fixed_variables=fixed_values) + self._apply_fixed_masks(fixed_masks) + end_building_time = time.time() + solution = self.solve(XOR_QUASIDIFFERENTIAL, solver_name=solver_name) + solution["building_time_seconds"] = end_building_time - start_building_time + total_time = solution["solving_time_seconds"] + max_memory = solution["memory_megabytes"] + + while solution["total_weight"] is None: + current_weight += 1 + start_building_time = time.time() + self.build_xor_quasidifferential_trail_model(weight=current_weight, fixed_variables=fixed_values) + self._apply_fixed_masks(fixed_masks) + end_building_time = time.time() + solution = self.solve(XOR_QUASIDIFFERENTIAL, solver_name=solver_name) + solution["building_time_seconds"] = end_building_time - start_building_time + total_time += solution["solving_time_seconds"] + max_memory = max((max_memory, solution["memory_megabytes"])) + + solution["solving_time_seconds"] = total_time + solution["memory_megabytes"] = max_memory + solution["test_name"] = "find_lowest_weight_xor_quasidifferential_trail" + return solution + + def _qdt_get_operands(self, solution): + """ + Return the blocking-clause literals of a solution's primary-input boundary. + + Unlike the ordinary differential model's ``get_operands`` (which only needs to block the + primary input DIFFERENCE, since the mask side does not exist there), a quasidifferential + trail's boundary also includes the primary input MASK -- two trails sharing the same input + difference but differing in input mask are genuinely different trails and must not be + treated as duplicates. + + INPUT: + + - ``solution`` -- **dictionary**; a solution returned by ``solve`` + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: smt = SmtXorQuasidifferentialModel(SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=1)) + sage: smt.build_xor_quasidifferential_trail_model(weight=0) + sage: solution = smt.solve('xor_quasidifferential') + sage: len(smt._qdt_get_operands(solution)) + 48 + + Difference and mask of the 8-bit plaintext and of the 16-bit key. + """ + operands = [] + + for input_, bit_len in zip(self._cipher.inputs, self._cipher.inputs_bit_size): + operands.extend(self._excluding_literals(input_, solution["components_values"][input_], bit_len)) + + return operands + + @staticmethod + def _excluding_literals(variable_prefix, values, bit_len): + """ + Return the blocking-clause literals that exclude a difference and a mask. + + They exclude the difference and the mask recorded in ``values`` on the ``bit_len`` bits + named ``_`` and ``qdt__``, most significant bit + first. + + INPUT: + + - ``variable_prefix`` -- **string**; the id whose bits are named + - ``values`` -- **dictionary**; a component solution, with a ``value`` and, optionally, a + ``mask`` entry + - ``bit_len`` -- **integer**; the bit size of ``variable_prefix`` + + EXAMPLES:: + + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: SmtXorQuasidifferentialModel._excluding_literals('x', {'value': '0x2', 'mask': '0x1'}, 2) + ['(not x_0)', 'x_1', 'qdt_x_0', '(not qdt_x_1)'] + """ + literals = [] + + for prefix, value in ( + (variable_prefix, int(values["value"], 16)), + (f"qdt_{variable_prefix}", int(values.get("mask", "0x0"), 16)), + ): + # Excluding a value means forcing its complement, bit by bit. + complement = value ^ ((1 << bit_len) - 1) + literals.extend( + SmtXorQuasidifferentialModel._value_literals([f"{prefix}_{j}" for j in range(bit_len)], complement) + ) + + return literals + + @staticmethod + def _value_literals(bit_ids, value): + """ + Return the literals forcing ``bit_ids`` to spell ``value``, most significant bit first. + + INPUT: + + - ``bit_ids`` -- **list**; the variable names, most significant bit first + - ``value`` -- **integer**; the value to spell + + EXAMPLES:: + + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: SmtXorQuasidifferentialModel._value_literals(['x_0', 'x_1', 'x_2'], 5) + ['x_0', '(not x_1)', 'x_2'] + """ + size = len(bit_ids) + return [ + bit_id if (value >> (size - 1 - index)) & 1 else utils.smt_not(bit_id) + for index, bit_id in enumerate(bit_ids) + ] + + def _is_nonlinear_component(self, component): + """ + Return whether ``component`` adds degrees of freedom to a quasidifferential trail. + + These are the components whose specific (difference, mask) transition must be blocked when + enumerating distinct trails. + + These are exactly the components with a nontrivial QDT: Sbox, AND, OR, MODADD and MODSUB. + Every other currently-implemented component (XOR, NOT, LinearLayer, Permutation, Rotate, + Shift, MixColumn, CipherOutput, IntermediateOutput, Constant) is deterministic given its + inputs on both the difference and the mask side, so blocking it would be redundant. + + INPUT: + + - ``component`` -- **Component object**; a component of the cipher + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: speck = SpeckBlockCipher(number_of_rounds=2) + sage: smt = SmtXorQuasidifferentialModel(speck) + sage: smt._is_nonlinear_component(speck.component_from_id('modadd_0_1')) + True + sage: smt._is_nonlinear_component(speck.component_from_id('rot_0_0')) + False + """ + if SBOX in component.type: + return True + + if component.type == WORD_OPERATION and component.description[0] in ("AND", "MODADD", "MODSUB", "OR"): + return True + + return False + + def _blocking_clause_operands(self, solution): + """ + Return the literals of a blocking clause excluding exactly the trail in ``solution``. + + They are the primary input boundary (difference AND mask, via ``_qdt_get_operands``) plus + every nonlinear component's own difference and mask. + + INPUT: + + - ``solution`` -- **dictionary**; a solution returned by ``solve`` + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: smt = SmtXorQuasidifferentialModel(SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=1)) + sage: smt.build_xor_quasidifferential_trail_model(weight=0) + sage: solution = smt.solve('xor_quasidifferential') + sage: len(smt._blocking_clause_operands(solution)) + 56 + + The 48 literals of the primary inputs, plus difference and mask of the one 4-bit modular + addition. + """ + operands = self._qdt_get_operands(solution) + + for component in self._cipher.all_components(): + if self._is_nonlinear_component(component): + operands.extend( + self._excluding_literals( + component.id, solution["components_values"][component.id], component.output_bit_size + ) + ) + + return operands + + def find_all_xor_quasidifferential_trails_with_fixed_weight( + self, fixed_weight, fixed_values=[], fixed_masks=None, solver_name=solvers.SOLVER_DEFAULT + ): + """ + Return all the XOR quasidifferential trails with total weight loss ``fixed_weight``. + + Mirrors SmtXorDifferentialModel.find_all_xor_differential_trails_with_fixed_weight. A + quasidifferential trail is fully determined by its primary-input boundary (difference AND + mask -- see ``_qdt_get_operands``) together with the specific transition chosen at each + NONLINEAR component (Sbox, AND, OR, MODADD, MODSUB -- see ``_is_nonlinear_component``). + Every other component (XOR, LinearLayer, Permutation, Rotate, MixColumn, ...) is fully + deterministic given its inputs, on both the difference and the mask side, so it contributes + no extra degrees of freedom to block on. + + INPUT: + + - ``fixed_weight`` -- **integer**; the total weight of the trails + - ``fixed_values`` -- **list** (default: `[]`); can be created using ``set_fixed_variables`` + method + - ``fixed_masks`` -- **list** (default: `None`); mask constraints, which ``fixed_values`` + cannot express, in the format described in ``estimate_fixed_key_probability``; see + ``boundary_masks`` + - ``solver_name`` -- **string** (default: `Z3_EXT`); the name of the solver + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: speck = SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=1) + sage: smt = SmtXorQuasidifferentialModel(speck) + sage: trails = smt.find_all_xor_quasidifferential_trails_with_fixed_weight(0) + sage: len(trails) + 96 + + Ninety-six trails at weight 0 on one round of 8-bit Speck: they share the characteristic and + differ in their masks, which is what makes a trail finer than a characteristic. + """ + solutions, _ = self._solutions_at_weight(fixed_weight, fixed_values, fixed_masks or [], solver_name, None, None) + + for solution in solutions: + solution["test_name"] = "find_all_xor_quasidifferential_trails_with_fixed_weight" + + return solutions + + def find_all_xor_quasidifferential_trails_with_weight_at_most( + self, max_weight, min_weight=0, fixed_values=[], fixed_masks=None, solver_name=solvers.SOLVER_DEFAULT + ): + """ + Return all the XOR quasidifferential trails with weight in ``[min_weight, max_weight]``. + + Mirrors SmtXorDifferentialModel.find_all_xor_differential_trails_with_weight_at_most. + + INPUT: + + - ``max_weight`` -- **integer**; the highest total weight of the trails + - ``min_weight`` -- **integer** (default: `0`); the lowest total weight of the trails + - ``fixed_values`` -- **list** (default: `[]`); can be created using ``set_fixed_variables`` + method + - ``fixed_masks`` -- **list** (default: `None`); mask constraints, which ``fixed_values`` + cannot express, in the format described in ``estimate_fixed_key_probability``; see + ``boundary_masks`` + - ``solver_name`` -- **string** (default: `Z3_EXT`); the name of the solver + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: speck = SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=1) + sage: smt = SmtXorQuasidifferentialModel(speck) + sage: trails = smt.find_all_xor_quasidifferential_trails_with_weight_at_most(0) + sage: len(trails) + 96 + """ + solutions_list = [] + + for weight in range(min_weight, max_weight + 1): + solutions = self.find_all_xor_quasidifferential_trails_with_fixed_weight( + weight, fixed_values=fixed_values, fixed_masks=fixed_masks, solver_name=solver_name + ) + + for solution in solutions: + solution["test_name"] = "find_all_xor_quasidifferential_trails_with_weight_at_most" + + solutions_list.extend(solutions) + + return solutions_list + + def estimate_fixed_key_probability( + self, + max_weight, + min_weight=0, + fixed_values=[], + fixed_masks=None, + solver_name=solvers.SOLVER_DEFAULT, + key=None, + max_trails_per_weight=None, + timeout_per_weight=None, + ): + """ + Estimate a probability by summing the signed correlations of quasidifferential trails. + + Every trail found with weight in ``[min_weight, max_weight]`` is summed with its SIGNED + correlation ([BR2022]_, Theorem 4.1 / Equation 5). + + ``key`` selects WHICH probability is returned, and the two answers are different quantities: + + - ``key=None`` (default) -- the AVERAGE probability over all keys. A trail's contribution + carries the factor chi_u(k) = (-1)^ for the mask ``u`` on the key input, and + averaging that over all keys kills every trail with a non-zero key mask, so only the + zero-key-mask trails are summed. Exact, and independent of any particular key. + + - ``key=`` -- the FIXED-KEY probability for that key: every trail is summed, each + multiplied by its own chi_u(key) = (-1)^popcount(key_mask & key). + + Without the key factor the sum is neither: it is the fixed-key probability of the all-zero + key, which is why ``key`` has no "just add them all up" setting. On a 6-round Simon + characteristic of weight 12 the three correction trails carry non-zero key masks, and the + fixed-key probability ranges from 2^-12.83 to 2^-11.36 across key classes while the average + stays at 2^-12. + + Each entry of ``"trails"`` records the trail's ``"key_mask"``, so a caller can re-evaluate + the sum for other keys without re-solving. + + signed_correlation = sign * 2**(-weight), summed over all trails. + + INPUT: + + - ``max_weight`` -- **integer**; the highest weight to enumerate + - ``min_weight`` -- **integer** (default: `0`); the lowest weight to enumerate + - ``fixed_values`` -- **list** (default: `[]`); ordinary DIFFERENCE constraints, built with + ``set_fixed_variables`` + - ``fixed_masks`` -- **list** (default: `None`); QDT MASK constraints, which + set_fixed_variables cannot express (it only fixes ordinary difference bits, never + qdt_-prefixed ones). Each entry is a dict: + + | { + | 'component_id': 'plaintext', + | 'bit_positions': range(64), + | 'bit_values': [0] * 64 + | } + + Theorem 4.1 requires the BOUNDARY masks to be zero (u_1 = u_{r+1} = 0) for the sum to + equal the fixed-key probability of a specific differential -- pass those here, typically + for the primary cipher inputs and the cipher output component; ``boundary_masks`` builds + them. With ``None`` the masks come from ``boundary_masks``, because the sum is not a + probability without them. Pass ``[]`` to set no masks. + - ``solver_name`` -- **string** (default: `Z3_EXT`); the name of the solver + - ``key`` -- **integer** (default: `None`); the key whose fixed-key probability is returned, + or ``None`` for the average over all keys + - ``max_trails_per_weight`` -- **integer** (default: `None`); stop enumerating a weight + after this many trails. + - ``timeout_per_weight`` -- **integer** (default: `None`); stop enumerating a weight after + this many seconds. Checked between solver calls, so one slow call can overrun it. + + A weight is reported truncated whenever a bound stopped the loop, even if no further trail + existed: telling the two apart would take the very solver call the bound was there to avoid. + + Masks admit many trails per weight and each one costs a full solve, so on most ciphers the + exhaustive sum does not terminate: those two bounds make the search finish. What they return + is not the same quantity. **Only an exhaustive sum is the fixed-key probability of Theorem + 4.1**; when a bound cuts a weight short the value is the contribution of the trails that + were found and nothing more, and the result says so in ``"truncated"`` and + ``"truncated_weights"``. A truncated sum of a signed series is not even an approximation + with a known direction -- the trails left out can carry either sign. + + This method runs its own build-and-enumerate loop (rather than delegating to + find_all_xor_quasidifferential_trails_with_weight_at_most) precisely so that fixed_masks can + be injected into the model after each rebuild -- the same _model_constraints manipulation + technique already used by the sign cross-validation tests. Nothing outside this file is + modified, so no other model (differential, linear, ...) that shares + fix_variables_value_constraints is affected. + + Inherits the same known scaling limits as the underlying blocking-clause enumeration: + practical mainly when most DIFFERENCES are already fixed (e.g. matching a known differential + characteristic, as in rectangle.py's own reference script), leaving primarily masks to + enumerate. + + Returns a dict with: + + - ``"trails"``: one entry per summed trail, with its ``"sign"``, ``"weight"``, + ``"key_mask"``, ``"key_mask_per_input"`` and signed ``"correlation"``; + - ``"estimated_probability"``: the sum of all signed correlations; + - ``"num_trails"``: how many trails were summed; + - ``"num_trails_found"``: how many trails were found, including the ones that averaging over + the keys discards; + - ``"key"``: the ``key`` argument; + - ``"averaged_over_keys"``: whether ``key`` was ``None``; + - ``"truncated"``: whether a bound cut any weight short, i.e. whether + ``"estimated_probability"`` is a partial sum; + - ``"truncated_weights"``: the weights it cut short. + + EXAMPLES:: + + sage: from claasp.ciphers.toys.toyspn1 import ToySPN1 + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: from claasp.cipher_modules.models.utils import set_fixed_variables, integer_to_bit_list + sage: from claasp.name_mappings import INPUT_KEY, INPUT_PLAINTEXT + sage: toyspn = ToySPN1(number_of_rounds=2) + + The differential 0x02 -> 0x20, with its boundary masks pinned to zero as Theorem 4.1 + requires: + + sage: fixed_values = [ + ....: set_fixed_variables(INPUT_KEY, 'equal', range(6), (0,) * 6), + ....: set_fixed_variables(INPUT_PLAINTEXT, 'equal', range(6), integer_to_bit_list(0x02, 6, 'big')), + ....: set_fixed_variables('cipher_output_1_6', 'equal', range(6), integer_to_bit_list(0x20, 6, 'big')), + ....: ] + sage: fixed_masks = [ + ....: {'component_id': INPUT_PLAINTEXT, 'bit_positions': range(6), 'bit_values': [0] * 6}, + ....: {'component_id': 'cipher_output_1_6', 'bit_positions': range(6), 'bit_values': [0] * 6}, + ....: ] + + Averaged over all keys, only the two zero-key-mask trails survive out of the four found: + + sage: average = SmtXorQuasidifferentialModel(toyspn).estimate_fixed_key_probability( + ....: max_weight=8, fixed_values=fixed_values, fixed_masks=fixed_masks) + sage: average['estimated_probability'] + 0.125 + sage: average['num_trails'], average['num_trails_found'] + (2, 4) + + For a single key all four count, each with its own character, and the answer is a different + number -- twice the average for key 0, and zero for key 2, where the two key-masked trails + cancel the others exactly: + + sage: for key in (0x00, 0x02): + ....: result = SmtXorQuasidifferentialModel(toyspn).estimate_fixed_key_probability( + ....: max_weight=8, fixed_values=fixed_values, fixed_masks=fixed_masks, key=key) + ....: print(key, result['estimated_probability'], result['truncated']) + 0 0.25 False + 2 0.0 False + + Both values are exact: counting over all 64 plaintexts gives 0.25 for key 0 and 0 for key 2. + """ + if fixed_masks is None: + fixed_masks = self.boundary_masks() + + key_input_names = self._key_inputs() + trails = [] + total = 0.0 + num_trails = 0 + num_trails_found = 0 + truncated_weights = [] + + for weight in range(min_weight, max_weight + 1): + solutions, truncated = self._solutions_at_weight( + weight, fixed_values, fixed_masks, solver_name, max_trails_per_weight, timeout_per_weight + ) + + if truncated: + truncated_weights.append(weight) + + num_trails_found += len(solutions) + + for solution in solutions: + trail = self._trail_record(solution, key_input_names, key) + + if trail is None: + continue + + trails.append(trail) + total += trail["correlation"] + num_trails += 1 + + return { + "trails": trails, + "estimated_probability": total, + "num_trails": num_trails, + "num_trails_found": num_trails_found, + "key": key, + "averaged_over_keys": key is None, + "truncated": bool(truncated_weights), + "truncated_weights": truncated_weights, + } + + def boundary_masks(self): + """ + Return the ``fixed_masks`` setting the cipher's input and output masks to zero. + + The masks in between are left free. + + The output end covers every state output of the final round, since a mask left free on any + of them admits trails outside the characteristic. + + INPUT: + + - None + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.rectangle_block_cipher import RectangleBlockCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: rectangle = RectangleBlockCipher(number_of_rounds=3) + sage: masks = SmtXorQuasidifferentialModel(rectangle).boundary_masks() + sage: [entry['component_id'] for entry in masks] + ['plaintext', 'intermediate_output_2_32', 'cipher_output_2_33'] + sage: set(masks[0]['bit_values']) + {0} + """ + if INPUT_PLAINTEXT not in self._cipher.inputs: + raise ValueError( + f"{self._cipher.id}: the input mask cannot be placed automatically, " + f"because this cipher has no {INPUT_PLAINTEXT!r} input " + f"(its inputs are {self._cipher.inputs}). Build fixed_masks by hand." + ) + + block_bit_size = self._cipher.output_bit_size + # Keep the state outputs only. The key schedule has outputs too, and setting their masks to + # zero would lose the round-key masks, which is where weak-key conditions come from. Both + # kinds have the same component type, so the description has to decide: "round_output" or + # "round_key_output". + state_outputs = [ + component.id + for component in self._cipher.all_components() + if component.description[0] in ("round_output", "cipher_output") + and component.output_bit_size == block_bit_size + ] + last_round = int(state_outputs[-1].split("_")[-2]) + component_ids = [INPUT_PLAINTEXT] + [ + output_id for output_id in state_outputs if int(output_id.split("_")[-2]) == last_round + ] + return [ + {"component_id": component_id, "bit_positions": range(block_bit_size), "bit_values": [0] * block_bit_size} + for component_id in component_ids + ] + + def _apply_fixed_masks(self, fixed_masks): + """ + Add the ``fixed_masks`` assertions to the model just built. + + Mask bits need their own assertions, on the ``qdt_`` variables. + + INPUT: + + - ``fixed_masks`` -- **list**; mask constraints, in the format described in + ``estimate_fixed_key_probability``. ``None`` or ``[]`` leaves the model as it is + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.xor_cipher import XorCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: from claasp.cipher_modules.models.smt.utils import constants + sage: smt = SmtXorQuasidifferentialModel(XorCipher(word_bit_size=2, number_of_inputs=2)) + sage: smt.build_xor_quasidifferential_trail_model() + sage: smt._apply_fixed_masks([{'component_id': 'plaintext', 'bit_positions': [0], 'bit_values': [1]}]) + sage: smt.model_constraints[-len(constants.MODEL_SUFFIX) - 1] + '(assert qdt_plaintext_0)' + """ + mask_constraints = self._build_fixed_mask_constraints(fixed_masks or []) + + if mask_constraints: + self._model_constraints = ( + self._model_constraints[: -len(constants.MODEL_SUFFIX)] + mask_constraints + constants.MODEL_SUFFIX + ) + + def _solutions_at_weight( + self, weight, fixed_values, fixed_masks, solver_name, max_trails_per_weight, timeout_per_weight + ): + """ + Return every trail of exactly ``weight``, and whether a bound cut the enumeration short. + + The build-and-enumerate loop lives here, rather than delegating to + find_all_xor_quasidifferential_trails_with_weight_at_most, so that fixed_masks can be + injected into the model after each rebuild -- set_fixed_variables cannot express a mask. + + INPUT: + + - ``weight`` -- **integer**; the total weight of the trails + - ``fixed_values`` -- **list**; can be created using ``set_fixed_variables`` method + - ``fixed_masks`` -- **list**; mask constraints, as in ``estimate_fixed_key_probability`` + - ``solver_name`` -- **string**; the name of the solver + - ``max_trails_per_weight`` -- **integer**; stop after this many trails, or ``None`` + - ``timeout_per_weight`` -- **integer**; stop after this many seconds, or ``None`` + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: from claasp.cipher_modules.models.smt import solvers + sage: speck = SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=1) + sage: model = SmtXorQuasidifferentialModel(speck) + sage: solutions, truncated = model._solutions_at_weight(0, [], [], solvers.SOLVER_DEFAULT, None, None) + sage: len(solutions), truncated + (96, False) + + A bound stops the enumeration, and says so: + + sage: solutions, truncated = model._solutions_at_weight(0, [], [], solvers.SOLVER_DEFAULT, 5, None) + sage: len(solutions), truncated + (5, True) + """ + start_building_time = time.time() + self.build_xor_quasidifferential_trail_model(weight=weight, fixed_variables=fixed_values) + self._constrain_weight_exactly(weight) + self._apply_fixed_masks(fixed_masks) + building_time = time.time() - start_building_time + solutions = [] + started_at = time.time() + solution = self.solve(XOR_QUASIDIFFERENTIAL, solver_name=solver_name) + + while solution["total_weight"] is not None: + solution["building_time_seconds"] = building_time + solutions.append(solution) + + if max_trails_per_weight is not None and len(solutions) >= max_trails_per_weight: + return solutions, True + + if timeout_per_weight is not None and time.time() - started_at >= timeout_per_weight: + return solutions, True + + clause = utils.smt_or(self._blocking_clause_operands(solution)) + self._model_constraints = ( + self._model_constraints[: -len(constants.MODEL_SUFFIX)] + + [utils.smt_assert(clause)] + + constants.MODEL_SUFFIX + ) + solution = self.solve(XOR_QUASIDIFFERENTIAL, solver_name=solver_name) + + return solutions, False + + def _key_inputs(self): + """ + Return the names of the cipher's key inputs. + + They are ``key``, or the one input per round key that ``Cipher.remove_key_schedule()`` + leaves behind, named ``key_0_2``, ``key_1_2`` and so on. + + INPUT: + + - None + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: SmtXorQuasidifferentialModel(SpeckBlockCipher(number_of_rounds=2))._key_inputs() + ['key'] + """ + return [ + input_id + for input_id in self._cipher.inputs + if input_id == INPUT_KEY or input_id.startswith(f"{INPUT_KEY}_") + ] + + def _trail_record(self, solution, key_input_names, key): + """ + Return one entry of ``"trails"``, or ``None`` for a trail the key factor kills. + + Averaging over keys kills every trail whose key mask is non-zero: chi_u averages to 0 unless + u = 0. For a specific key nothing is killed, and the factor is that trail's own character. + + ``key_input_names`` says where to read masks from; ``key`` is the key value, or ``None`` to + average over all keys. Those masks are joined in cipher-input order into the single integer + ``"key_mask"``, while ``"key_mask_per_input"`` keeps them split by input, which is what a + caller needs to state a weak-key condition on one round key. + + INPUT: + + - ``solution`` -- **dictionary**; a solution returned by ``solve`` + - ``key_input_names`` -- **list**; the key inputs, as returned by ``_key_inputs`` + - ``key`` -- **integer**; the key, or ``None`` to average over all keys + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: smt = SmtXorQuasidifferentialModel(SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=1)) + sage: smt.build_xor_quasidifferential_trail_model(weight=0) + sage: solution = smt.solve('xor_quasidifferential') + sage: record = smt._trail_record(solution, ['key'], 0) + sage: sorted(record) + ['correlation', 'key_mask', 'key_mask_per_input', 'sign', 'weight'] + sage: record['weight'] + 0.0 + """ + key_mask = 0 + key_mask_per_input = {} + + for input_id in key_input_names: + size = self._cipher.inputs_bit_size[self._cipher.inputs.index(input_id)] + value = int(solution["components_values"][input_id].get("mask", "0x0"), 16) + key_mask_per_input[input_id] = value + key_mask = (key_mask << size) | value + + if key is None: + key_factor = 0 if key_mask else 1 + else: + key_factor = -1 if bin(key_mask & key).count("1") % 2 else 1 + + if not key_factor: + return None + + sign = self.compute_trail_sign(solution) + weight = solution["total_weight"] + return { + "sign": sign, + "weight": weight, + "key_mask": key_mask, + "key_mask_per_input": key_mask_per_input, + "correlation": key_factor * sign * (2.0 ** (-weight)), + } + + def _build_fixed_mask_constraints(self, fixed_masks): + """ + Turn a ``fixed_masks`` list into SMT assertions on the ``qdt_`` mask variables. + + The format of ``fixed_masks`` is described in ``estimate_fixed_key_probability``. + + This is the mask-side counterpart of fix_variables_value_constraints, kept local to this + file rather than extending that shared method (which is used by the differential, linear and + other models). + + INPUT: + + - ``fixed_masks`` -- **list**; mask constraints, as in ``estimate_fixed_key_probability`` + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.xor_cipher import XorCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = XorCipher(word_bit_size=2, number_of_inputs=2) + sage: smt = SmtXorQuasidifferentialModel(cipher) + sage: smt._build_fixed_mask_constraints([ + ....: {'component_id': 'plaintext', 'bit_positions': range(2), 'bit_values': [1, 0]} + ....: ]) + ['(assert qdt_plaintext_0)', '(assert (not qdt_plaintext_1))'] + """ + constraints = [] + + for entry in fixed_masks: + component_id = entry["component_id"] + bit_positions = entry["bit_positions"] + bit_values = entry["bit_values"] + + for position, value in zip(bit_positions, bit_values): + variable_name = f"qdt_{component_id}_{position}" + + if value: + constraints.append(utils.smt_assert(variable_name)) + else: + constraints.append(utils.smt_assert(utils.smt_not(variable_name))) + + return constraints + + def solve(self, model_type, solver_name=solvers.SOLVER_DEFAULT): + """ + Solve, and attach the raw variable assignment to the solution. + + Branch masks on forked wires belong to no component, so they have no ``components_values`` + entry and ``compute_trail_sign`` has to read them from the assignment. Keeping that + assignment on the model alone makes the sign of a STORED solution wrong: every later + ``solve`` overwrites the single slot, so ``compute_trail_sign(solutions[0])`` would pair + trail 0's differences with the last trail's masks. Carrying it on the solution makes the + argument mean what its name says. + + INPUT: + + - ``model_type`` -- **string**; the model to solve, ``'xor_quasidifferential'`` + - ``solver_name`` -- **string** (default: `Z3_EXT`); the name of the solver + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: speck = SpeckBlockCipher(number_of_rounds=1) + sage: smt = SmtXorQuasidifferentialModel(speck) + sage: smt.build_xor_quasidifferential_trail_model(weight=0) + sage: solution = smt.solve('xor_quasidifferential') + sage: solution['total_weight'] + 0.0 + + The raw assignment travels with the solution, so the sign of a stored trail stays its own: + + sage: 'qdt_variable_assignment' in solution + True + """ + solution = super().solve(model_type, solver_name=solver_name) + + if solution["total_weight"] is None: + solution["qdt_variable_assignment"] = {} + else: + solution["qdt_variable_assignment"] = dict(getattr(self, "_variable2value", {})) + + return solution + + def _parse_solver_output(self, variable2value): + """ + Parse the solver output. + + The ordinary component value contains the XOR difference. The QDT masks are recorded + alongside it (under the "mask" key of each component's solution) so that callers -- notably + the blocking-clause logic in find_all_xor_quasidifferential_trails_with_fixed_weight -- can + distinguish trails that share the same differences but differ in their masks. + + The raw assignment is kept on the model as well: branch masks on forked wires belong to no + component, so they have no ``components_values`` entry and ``_read_component_input_mask`` + has to read them from here. + + INPUT: + + - ``variable2value`` -- **dictionary**; the solver assignment, from variable name to value + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: smt = SmtXorQuasidifferentialModel(SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=1)) + sage: smt.build_xor_quasidifferential_trail_model(weight=0) + sage: solution = smt.solve('xor_quasidifferential') + sage: components, weight = smt._parse_solver_output(solution['qdt_variable_assignment']) + sage: weight, 'mask' in components['plaintext'] + (0, True) + """ + self._variable2value = variable2value + out_suffix = "" + components_solutions = self._get_cipher_inputs_components_solutions(out_suffix, variable2value) + + # The cipher-input entries built by _get_cipher_inputs_components_solutions only carry the + # ordinary difference value; add their QDT mask value too, using the same + # qdt_{input_id}_{position} naming used everywhere else in this model. + for input_id, bit_len in zip(self._cipher.inputs, self._cipher.inputs_bit_size): + if input_id not in components_solutions: + continue + + components_solutions[input_id]["mask"] = self._mask_hex_value(input_id, bit_len, variable2value) + + total_weight = 0 + + for component in self._cipher.all_components(): + hex_value = utils.get_component_hex_value(component, out_suffix, variable2value) + mask_hex_value = self._mask_hex_value(component.id, component.output_bit_size, variable2value) + weight = self.calculate_component_weight(component, out_suffix, variable2value) + component_solution = set_component_solution(hex_value, weight) + component_solution["mask"] = mask_hex_value + components_solutions[f"{component.id}{out_suffix}"] = component_solution + total_weight += weight + + return (components_solutions, total_weight) + + @staticmethod + def _mask_hex_value(identifier, bit_size, variable2value): + """ + Return the mask on ``identifier`` as a hex string, read from a solver assignment. + + ``identifier`` is a cipher input or a component, and the mask is read from its + ``qdt__`` variables. Bits the assignment does not mention are 0. + + INPUT: + + - ``identifier`` -- **string**; the id of a cipher input or of a component + - ``bit_size`` -- **integer**; the bit size of ``identifier`` + - ``variable2value`` -- **dictionary**; the solver assignment, from variable name to value + + EXAMPLES:: + + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: SmtXorQuasidifferentialModel._mask_hex_value('xor_0_0', 2, {'qdt_xor_0_0_0': 1, 'qdt_xor_0_0_1': 0}) + '0x2' + """ + value = 0 + + for position in range(bit_size): + value = (value << 1) | variable2value.get(f"qdt_{identifier}_{position}", 0) + + hex_digits = bit_size // 4 + (bit_size % 4 != 0) + return f"{value:#0{hex_digits + 2}x}" + + # TRAIL SIGN (post-processing on an already-solved trail) + # + # Everything above finds trails and their WEIGHT (-log2|correlation|). This section computes the + # SIGN of the correlation for an already-solved trail, mirroring rectangle.py's compute_sign, + # common.py's compute_sign_speck, and simon_32.py's correlation_sign_and -- but as pure Python + # post-processing on a solved `solution` dict, exactly like those reference scripts do, rather + # than as new SMT constraints (sign never affects the weight-based SAT search itself, only the + # final numeric correlation once a trail is found). + # + # Per Definition 4.1, a trail's correlation is the PRODUCT of each component's local D^Fi + # coefficient, so the sign is the product of each component's local sign. Only SBOX, AND, MODADD + # (Theorem 5.1 / 5.2's proofs) and CONSTANT (Theorem 3.2 (4)'s chi_v(t) factor) contribute a + # sign other than +1; every other currently-implemented component (XOR of data branches, + # LinearLayer, Permutation, Rotate, MixColumn, CipherOutput, IntermediateOutput) is a pure + # linear or identity map with a delta-function (always-nonnegative) correlation (Theorem 3.2 + # (5)), contributing +1. + + def compute_trail_sign(self, solution): + """ + Compute the overall correlation sign of an already-solved quasidifferential trail. + + The trail is a solution as returned, e.g., by ``find_one_xor_quasidifferential_trail`` or + ``find_one_xor_quasidifferential_trail_with_fixed_weight``. + + Returns +1 or -1. + + Reads the mask assignment carried by ``solution`` itself, so a solution stored earlier -- + one element of the list returned by + ``find_all_xor_quasidifferential_trails_with_fixed_weight``, say -- still gets its own sign + and not the latest solve's. + + INPUT: + + - ``solution`` -- **dictionary**; a solution returned by ``solve`` + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: speck = SpeckBlockCipher(number_of_rounds=1) + sage: smt = SmtXorQuasidifferentialModel(speck) + sage: smt.build_xor_quasidifferential_trail_model(weight=0) + sage: solution = smt.solve('xor_quasidifferential') + sage: smt.compute_trail_sign(solution) + 1 + """ + assignment = solution.get("qdt_variable_assignment") + previous_assignment = getattr(self, "_variable2value", None) + + if assignment is not None: + self._variable2value = assignment + + try: + return self._compute_trail_sign(solution) + finally: + if assignment is not None: + self._variable2value = previous_assignment + + def _compute_trail_sign(self, solution): + """ + Return the sign of a solved trail, read with the assignment the model holds. + + See ``compute_trail_sign``. + + INPUT: + + - ``solution`` -- **dictionary**; a solution returned by ``solve`` + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: smt = SmtXorQuasidifferentialModel(SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=1)) + sage: smt.build_xor_quasidifferential_trail_model(weight=0) + sage: solution = smt.solve('xor_quasidifferential') + sage: smt._compute_trail_sign(solution) in (-1, 1) + True + """ + components_solutions = solution["components_values"] + sign = 1 + + for component in self._cipher.all_components(): + local_sign = self._local_sign_rule(component) + + if local_sign is not None: + sign *= local_sign(component, components_solutions) + + return sign + + def _local_sign_rule(self, component): + """ + Return the rule giving the local sign of ``component``, or ``None`` if it has none. + + A pure linear map or the identity contributes +1 and drops out of the product. + + INPUT: + + - ``component`` -- **Component object**; a component of the cipher + + EXAMPLES:: + + sage: from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: speck = SpeckBlockCipher(number_of_rounds=2) + sage: smt = SmtXorQuasidifferentialModel(speck) + sage: smt._local_sign_rule(speck.component_from_id('modadd_0_1')).__name__ + '_modadd_local_sign' + sage: smt._local_sign_rule(speck.component_from_id('rot_0_0')) is None + True + """ + if SBOX in component.type: + return self._sbox_local_sign + + if CONSTANT in component.type: + return self._constant_local_sign + + if component.type != WORD_OPERATION: + return None + + return { + "AND": self._and_local_sign, + "MODADD": self._modadd_local_sign, + "MODSUB": self._modsub_local_sign, + "NOT": self._not_local_sign, + "OR": self._or_local_sign, + }.get(component.description[0]) + + @staticmethod + def _parity(value): + """ + Parity of the number of set bits of ``value``. + + INPUT: + + - ``value`` -- **integer**; a non-negative integer + + EXAMPLES:: + + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: SmtXorQuasidifferentialModel._parity(0b1011) + 1 + """ + return bin(value).count("1") % 2 + + def _bit_size_of(self, id_): + """ + Return the bit size of a cipher input or of a component's output, given its id. + + INPUT: + + - ``id_`` -- **string**; the id of a cipher input or of a component + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.xor_cipher import XorCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = XorCipher(word_bit_size=2, number_of_inputs=2) + sage: smt = SmtXorQuasidifferentialModel(cipher) + sage: smt._bit_size_of('plaintext'), smt._bit_size_of('xor_0_0') + (2, 2) + """ + for input_id, input_bit_size in zip(self._cipher.inputs, self._cipher.inputs_bit_size): + if input_id == id_: + return input_bit_size + + for component in self._cipher.all_components(): + if component.id == id_: + return component.output_bit_size + + raise ValueError(f"{id_}: unknown cipher input or component id") + + def _read_component_input_integer(self, component, field, components_solutions): + """ + Reconstruct the full input integer of a component, difference or mask. + + The integer is the difference "value" or the QDT "mask". It is built by reading the + requested bits from its upstream producers' (or primary inputs') already-solved hex + value/mask, in the same order used everywhere else in this model to build input bit ids + (_generate_input_ids, _qdt_input_bit_ids): for each (input_id, bit_positions) pair in + component.input_id_links / component.input_bit_positions, in order, each position in + bit_positions in order (position 0 = MSB of the upstream id's own value/mask). + + For ``field="mask"`` on a FORKED wire the value must come from this component's own BRANCH + variable, not from the producer's mask: the producer's mask is the XOR of all branches, + while the component's constraints were written over its own branch. Using the producer's + value there yields a transition the solver never asserted -- for an sbox, one whose QDT + coefficient may be zero. + + INPUT: + + - ``component`` -- **Component object**; a component of the cipher + - ``field`` -- **string**; ``'value'`` for the difference, ``'mask'`` for the mask + - ``components_solutions`` -- **dictionary**; the ``components_values`` of a solution, with + a ``value`` and a ``mask`` entry per id + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.xor_cipher import XorCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = XorCipher(word_bit_size=2, number_of_inputs=2) + sage: smt = SmtXorQuasidifferentialModel(cipher) + sage: solution = {'plaintext': {'value': '0x2'}, 'key': {'value': '0x1'}} + sage: smt._read_component_input_integer(cipher.component_from_id('xor_0_0'), 'value', solution) + 9 + + The plaintext bits ``10`` followed by the key bits ``01``. + """ + if field == "mask": + return self._read_component_input_mask(component) + + result = 0 + + for input_id, bit_positions in zip(component.input_id_links, component.input_bit_positions): + upstream_size = self._bit_size_of(input_id) + upstream_value = int(components_solutions[input_id][field], 16) + + for position in bit_positions: + bit = (upstream_value >> (upstream_size - 1 - position)) & 1 + result = (result << 1) | bit + + return result + + def _read_component_input_mask(self, component): + """ + Reconstruct a component's input MASK from the solver's variable assignment. + + On forked wires the branch variable is used. + + Reads ``self._variable2value``, populated by ``_parse_solver_output``, because branch + variables have no ``components_values`` entry of their own: they belong to no component. + + INPUT: + + - ``component`` -- **Component object**; a component of the cipher + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.xor_cipher import XorCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = XorCipher(word_bit_size=2, number_of_inputs=2) + sage: smt = SmtXorQuasidifferentialModel(cipher) + sage: smt._variable2value = {'qdt_plaintext_0': 1, 'qdt_plaintext_1': 0, 'qdt_key_0': 0, 'qdt_key_1': 1} + sage: smt._read_component_input_mask(cipher.component_from_id('xor_0_0')) + 9 + """ + variable2value = getattr(self, "_variable2value", None) + + if not variable2value: + raise ValueError( + f"{component.id}: no solver assignment available for mask " + f"reconstruction -- _parse_solver_output must run first." + ) + + result = 0 + + for input_id, position, read_index in self._component_wire_reads(component): + variable = self.qdt_input_bit_id(component, input_id, position, read_index) + result = (result << 1) | variable2value.get(variable, 0) + + return result + + def _read_component_input_operands(self, component, field, components_solutions, num_operands, word_size): + """ + Like ``_read_component_input_integer``, but split into ``num_operands`` integers. + + Each one has ``word_size`` bits (one per AND/MODADD operand), matching the same + [:word_size], [word_size:2*word_size], ... slicing convention used by And/ModAdd's own + smt_xor_quasidifferential_propagation_constraints. + + Delegates the reconstruction to _read_component_input_integer, which on forked wires reads + the component's own BRANCH mask rather than the producer's -- see the note there. + + INPUT: + + - ``component`` -- **Component object**; a component of the cipher + - ``field`` -- **string**; ``'value'`` for the difference, ``'mask'`` for the mask + - ``components_solutions`` -- **dictionary**; the ``components_values`` of a solution, with + a ``value`` and a ``mask`` entry per id + - ``num_operands`` -- **integer**; the number of operands + - ``word_size`` -- **integer**; the bit size of each operand + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.xor_cipher import XorCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = XorCipher(word_bit_size=2, number_of_inputs=2) + sage: smt = SmtXorQuasidifferentialModel(cipher) + sage: solution = {'plaintext': {'value': '0x2'}, 'key': {'value': '0x1'}} + sage: smt._read_component_input_operands(cipher.component_from_id('xor_0_0'), 'value', solution, 2, 2) + [2, 1] + """ + full_value = self._read_component_input_integer(component, field, components_solutions) + total_bits = num_operands * word_size + mask = (1 << word_size) - 1 + return [(full_value >> (total_bits - (index + 1) * word_size)) & mask for index in range(num_operands)] + + def _sbox_local_sign(self, component, components_solutions): + """ + Return the sign of the S-box's QDT coefficient at the solved (a, u, b, v) point. + + It is looked up directly from the cached deinterleaved QDT matrix (see + Sbox.smt_xor_quasidifferential_propagation_constraints, which populates + model.sboxes_qdt_matrices). + + INPUT: + + - ``component`` -- **Component object**; a component of the cipher + - ``components_solutions`` -- **dictionary**; the ``components_values`` of a solution, with + a ``value`` and a ``mask`` entry per id + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.sbox_cipher import SboxCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = SboxCipher(bit_size=2, lookup_table=[0, 1, 3, 2]) + sage: sbox = cipher.component_from_id('sbox_0_0') + sage: smt = SmtXorQuasidifferentialModel(cipher) + sage: _ = sbox.smt_xor_quasidifferential_propagation_constraints(smt) + sage: smt._variable2value = {'qdt_plaintext_0': 0, 'qdt_plaintext_1': 0} + sage: smt._sbox_local_sign(sbox, {'plaintext': {'value': '0x1'}, 'sbox_0_0': {'value': '0x1', 'mask': '0x0'}}) + 1 + """ + cache_key = str(component.description) + qdt = self.sboxes_qdt_matrices.get(cache_key) + + if qdt is None: + raise ValueError( + f"{component.id}: no cached QDT matrix found for sign " + f"lookup -- was smt_xor_quasidifferential_propagation_constraints " + f"called for this sbox before solving?" + ) + + n = component.input_bit_size + m = component.output_bit_size + a = self._read_component_input_integer(component, "value", components_solutions) + u = self._read_component_input_integer(component, "mask", components_solutions) + b = int(components_solutions[component.id]["value"], 16) + v = int(components_solutions[component.id]["mask"], 16) + coefficient = qdt[(2**m) * b + v, (2**n) * a + u] + + if coefficient == 0: + raise ValueError( + f"{component.id}: the solved (a={a:#x}, u={u:#x}, " + f"b={b:#x}, v={v:#x}) transition has a zero QDT " + f"coefficient -- this should never happen for a valid " + f"SAT solution." + ) + + return 1 if coefficient > 0 else -1 + + def _two_operand_values(self, component, components_solutions): + """ + Return ``(a, b, c, u, v, w, word_size)`` of a solved two-operand word operation. + + They are the input differences, output difference, input masks and output mask. The sign + rules of AND, OR, MODADD and MODSUB all start from these. + + INPUT: + + - ``component`` -- **Component object**; a component of the cipher + - ``components_solutions`` -- **dictionary**; the ``components_values`` of a solution, with + a ``value`` and a ``mask`` entry per id + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.and_cipher import AndCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = AndCipher(word_bit_size=2, number_of_inputs=2) + sage: smt = SmtXorQuasidifferentialModel(cipher) + sage: smt._variable2value = {'qdt_plaintext_0': 0, 'qdt_plaintext_1': 1, 'qdt_key_0': 1, 'qdt_key_1': 0} + sage: solution = {'plaintext': {'value': '0x3'}, 'key': {'value': '0x1'}, + ....: 'and_0_0': {'value': '0x1', 'mask': '0x3'}} + sage: smt._two_operand_values(cipher.component_from_id('and_0_0'), solution) + (3, 1, 1, 1, 2, 3, 2) + """ + if component.description[1] != 2: + raise NotImplementedError( + f"{component.id}: sign computation for {component.description[0]} is only implemented for 2 operands." + ) + + word_size = component.output_bit_size + a, b = self._read_component_input_operands(component, "value", components_solutions, 2, word_size) + u, v = self._read_component_input_operands(component, "mask", components_solutions, 2, word_size) + c = int(components_solutions[component.id]["value"], 16) + w = int(components_solutions[component.id].get("mask", "0x0"), 16) + return a, b, c, u, v, w, word_size + + def _and_local_sign(self, component, components_solutions): + """ + Sign of a solved AND transition (Theorem 5.1). + + INPUT: + + - ``component`` -- **Component object**; a component of the cipher + - ``components_solutions`` -- **dictionary**; the ``components_values`` of a solution, with + a ``value`` and a ``mask`` entry per id + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.and_cipher import AndCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = AndCipher(word_bit_size=2, number_of_inputs=2) + sage: smt = SmtXorQuasidifferentialModel(cipher) + sage: smt._variable2value = {'qdt_plaintext_0': 0, 'qdt_plaintext_1': 1, 'qdt_key_0': 1, 'qdt_key_1': 0} + sage: solution = {'plaintext': {'value': '0x3'}, 'key': {'value': '0x1'}, + ....: 'and_0_0': {'value': '0x1', 'mask': '0x3'}} + sage: smt._and_local_sign(cipher.component_from_id('and_0_0'), solution) + 1 + """ + a, b, c, u, v, _, word_size = self._two_operand_values(component, components_solutions) + return self._and_sign_word(a, b, c, u, v, word_size) + + def _modadd_local_sign(self, component, components_solutions): + """ + Sign of a solved MODADD transition (Theorem 5.2). + + INPUT: + + - ``component`` -- **Component object**; a component of the cipher + - ``components_solutions`` -- **dictionary**; the ``components_values`` of a solution, with + a ``value`` and a ``mask`` entry per id + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.modadd_cipher import ModaddCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = ModaddCipher(word_bit_size=2, number_of_inputs=2, modulus=4) + sage: smt = SmtXorQuasidifferentialModel(cipher) + sage: smt._variable2value = {'qdt_plaintext_0': 0, 'qdt_plaintext_1': 0, 'qdt_key_0': 0, 'qdt_key_1': 0} + sage: solution = {'plaintext': {'value': '0x0'}, 'key': {'value': '0x0'}, + ....: 'modadd_0_0': {'value': '0x0', 'mask': '0x0'}} + sage: smt._modadd_local_sign(cipher.component_from_id('modadd_0_0'), solution) + 1 + """ + a, b, c, u, v, w, word_size = self._two_operand_values(component, components_solutions) + return self._modadd_sign_word(a, b, c, u, v, w, word_size) + + def _not_local_sign(self, component, components_solutions): + """ + Return the local sign of a solved NOT, chi_v(t) with t = all-ones. + + NOT is the affine map x -> x xor 1, so by Theorem 3.2 (4) its only contribution is the sign + factor (-1)^(v . 1) = (-1)^popcount(v), where v is the component's output mask. Differences + and masks themselves pass through unchanged (see + Not.smt_xor_quasidifferential_propagation_constraints). + + INPUT: + + - ``component`` -- **Component object**; a component of the cipher + - ``components_solutions`` -- **dictionary**; the ``components_values`` of a solution, with + a ``value`` and a ``mask`` entry per id + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.not_cipher import NotCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = NotCipher(bit_size=2) + sage: smt = SmtXorQuasidifferentialModel(cipher) + sage: component = cipher.component_from_id('not_0_0') + sage: smt._not_local_sign(component, {'not_0_0': {'mask': '0x1'}}) + -1 + sage: smt._not_local_sign(component, {'not_0_0': {'mask': '0x3'}}) + 1 + """ + v = int(components_solutions[component.id]["mask"], 16) + return -1 if self._parity(v) else 1 + + def _or_local_sign(self, component, components_solutions): + """ + Sign of a solved OR transition: AND's sign times (-1)^(u + v + w). + + INPUT: + + - ``component`` -- **Component object**; a component of the cipher + - ``components_solutions`` -- **dictionary**; the ``components_values`` of a solution, with + a ``value`` and a ``mask`` entry per id + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.or_cipher import OrCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = OrCipher(word_bit_size=2, number_of_inputs=2) + sage: smt = SmtXorQuasidifferentialModel(cipher) + sage: smt._variable2value = {'qdt_plaintext_0': 0, 'qdt_plaintext_1': 1, 'qdt_key_0': 0, 'qdt_key_1': 0} + sage: solution = {'plaintext': {'value': '0x0'}, 'key': {'value': '0x0'}, + ....: 'or_0_0': {'value': '0x0', 'mask': '0x0'}} + sage: smt._or_local_sign(cipher.component_from_id('or_0_0'), solution) + -1 + + One input mask bit is set, so the parity of ``u + v + w`` is odd. + """ + a, b, c, u, v, w, word_size = self._two_operand_values(component, components_solutions) + return self._or_sign_word(a, b, c, u, v, w, word_size) + + def _modsub_local_sign(self, component, components_solutions): + """ + Sign of a solved MODSUB transition, computed as MODADD with permuted roles. + + INPUT: + + - ``component`` -- **Component object**; a component of the cipher + - ``components_solutions`` -- **dictionary**; the ``components_values`` of a solution, with + a ``value`` and a ``mask`` entry per id + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.modsub_cipher import ModsubCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = ModsubCipher(word_bit_size=2, number_of_inputs=2, modulus=4) + sage: smt = SmtXorQuasidifferentialModel(cipher) + sage: smt._variable2value = {'qdt_plaintext_0': 0, 'qdt_plaintext_1': 0, 'qdt_key_0': 0, 'qdt_key_1': 0} + sage: solution = {'plaintext': {'value': '0x0'}, 'key': {'value': '0x0'}, + ....: 'modsub_0_0': {'value': '0x0', 'mask': '0x0'}} + sage: smt._modsub_local_sign(cipher.component_from_id('modsub_0_0'), solution) + 1 + """ + a, b, c, u, v, w, word_size = self._two_operand_values(component, components_solutions) + + # z = x - y is x = z + y, so MODSUB(a, b, c, u, v, w) is MODADD with the roles of the first + # input and the output swapped. + return self._modadd_sign_word(c, b, a, w, v, u, word_size) + + @staticmethod + def _or_sign_word(a, b, c, u, v, w, word_size): + """ + Word-level sign of a bitwise-OR quasidifferential transition. + + OR is AND conjugated by complementation (x1 | x2 = ~(~x1 & ~x2)). Complementation does not + change differences, so OR's validity conditions and |coefficients| -- and hence its WEIGHT + -- are IDENTICAL to AND's; only the sign differs, by the translation factors of Theorem 3.2 + (4). + + Verified by exhaustive brute force of Equation (4) on the 1-bit case (all 64 combinations: + same validity, same absolute value, sign ratio exactly (-1)^(u+v+w) per bit), then + cross-checked at word level against the per-bit tensor product over 200000 random 4-bit + vectors (8403 valid transitions, 0 mismatches). + + Note that unlike AND's sign, OR's DOES depend on the output mask w. + + INPUT: + + - ``a`` -- **integer**; the difference of the first input + - ``b`` -- **integer**; the difference of the second input + - ``c`` -- **integer**; the difference of the output + - ``u`` -- **integer**; the mask of the first input + - ``v`` -- **integer**; the mask of the second input + - ``w`` -- **integer**; the mask of the output + - ``word_size`` -- **integer**; the bit size of each operand + + EXAMPLES:: + + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: SmtXorQuasidifferentialModel._or_sign_word(0, 0, 0, 1, 0, 0, 1) + -1 + """ + base = SmtXorQuasidifferentialModel._and_sign_word(a, b, c, u, v, word_size) + correction_parity = ( + SmtXorQuasidifferentialModel._parity(u) + + SmtXorQuasidifferentialModel._parity(v) + + SmtXorQuasidifferentialModel._parity(w) + ) % 2 + return base * ((-1) ** correction_parity) + + def _constant_local_sign(self, component, components_solutions): + """ + Return the local sign of a solved constant, chi_v(t) = (-1)^(v . t). + + This is Theorem 3.2 (4), the translation-sign factor for a constant addition. The constant's + own difference contribution is always 0 (see + Constant.smt_xor_quasidifferential_propagation_constraints), so only its mask v and its + known value t matter here. + + INPUT: + + - ``component`` -- **Component object**; a component of the cipher + - ``components_solutions`` -- **dictionary**; the ``components_values`` of a solution, with + a ``value`` and a ``mask`` entry per id + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.constant_cipher import ConstantCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = ConstantCipher(output_bit_size=3, value=2) + sage: constant = cipher.component_from_id('constant_0_0') + sage: constant.description + ['0b010'] + sage: smt = SmtXorQuasidifferentialModel(cipher) + + The mask ``0b010`` sees the one set bit of the constant, so the sign flips; the mask + ``0b001`` does not see it: + + sage: smt._constant_local_sign(constant, {'constant_0_0': {'mask': '0x2'}}) + -1 + sage: smt._constant_local_sign(constant, {'constant_0_0': {'mask': '0x1'}}) + 1 + """ + + # Base 0 reads both forms CLAASP uses for constants: '0x...' and '0b...'. Base 16 would + # accept '0b010' silently, as 0xb010. + t = int(component.description[0], 0) + v = int(components_solutions[component.id]["mask"], 16) + return -1 if self._parity(t & v) else 1 + + @staticmethod + def _and_sign_word(a, b, c, u, v, word_size): + """ + Return the word-level sign of a bitwise-AND quasidifferential transition. + + It follows [BR2022]_, Theorem 5.1 and its proof in Appendix A.3, applied bit-independently + across the whole word via Theorem 3.2 (2) ("boxed maps": the sign of the word-level + transition is the product of the per-bit signs, since each bit's AND is an independent + sub-function acting on its own disjoint pair of input bits). + + Transliterated from simon_32.py's correlation_sign_and (the paper authors' own reference + implementation) and verified against a direct brute-force evaluation of Equation (4) for the + 1-bit case (29 valid transitions, 0 mismatches) before being encoded here. + + INPUT: + + - ``a`` -- **integer**; the difference of the first input + - ``b`` -- **integer**; the difference of the second input + - ``c`` -- **integer**; the difference of the output + - ``u`` -- **integer**; the mask of the first input + - ``v`` -- **integer**; the mask of the second input + - ``word_size`` -- **integer**; the bit size of each operand + + EXAMPLES:: + + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: SmtXorQuasidifferentialModel._and_sign_word(0, 0, 0, 0, 0, 2) + 1 + sage: SmtXorQuasidifferentialModel._and_sign_word(0, 0, 0, 1, 1, 1) + -1 + """ + mask = (1 << word_size) - 1 + comp_a = a ^ mask + comp_b = b ^ mask + comp_c = c ^ mask + term1 = ((comp_a & u) ^ (c & v)) & ((comp_b & v) ^ (c & u)) + term2 = (u & v) & (c ^ (a & b & comp_c)) + p = SmtXorQuasidifferentialModel._parity(term1) + q = SmtXorQuasidifferentialModel._parity(term2) + return -1 if (p ^ q) else 1 + + @staticmethod + def _modadd_sign_word(a, b, c, u, v, w, word_size): + """ + Return the word-level sign of a modular-addition quasidifferential transition. + + It follows [BR2022]_, Theorem 5.2, computed via the same AND-sign formula applied to the + primed variables (a' = b xor c, b' = a xor c, c' = M+(a xor b xor c), u' = u xor w, v' = v + xor w) -- since MODADD's theory is derived via CCZ-equivalence to a quadratic function + "nearly the same as bitwise-and" (paper, Section 5.2 / Appendix A.4). + + Transliterated from common.py's compute_sign_speck (the paper authors' own reference + implementation), using the SAME u' = u xor w / v' = v xor w substitution already used, and + already verified, for the validity/weight constraints in + ModAdd.smt_xor_quasidifferential_propagation_constraints -- NOT compute_sign_speck's extra + inter-round rotation logic, which is specific to how Speck wires masks between rounds and is + already handled separately by claasp's own Rotate components. + + INPUT: + + - ``a`` -- **integer**; the difference of the first input + - ``b`` -- **integer**; the difference of the second input + - ``c`` -- **integer**; the difference of the output + - ``u`` -- **integer**; the mask of the first input + - ``v`` -- **integer**; the mask of the second input + - ``w`` -- **integer**; the mask of the output + - ``word_size`` -- **integer**; the bit size of each operand + + EXAMPLES:: + + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: SmtXorQuasidifferentialModel._modadd_sign_word(0, 0, 0, 0, 0, 0, 2) + 1 + """ + mask = (1 << word_size) - 1 + abc_xor = a ^ b ^ c + shifted_left = (abc_xor << 1) & mask + c_prime = (abc_xor ^ shifted_left) >> 1 + a_prime = b ^ c + b_prime = a ^ c + u_prime = u ^ w + v_prime = v ^ w + return SmtXorQuasidifferentialModel._and_sign_word(a_prime, b_prime, c_prime, u_prime, v_prime, word_size) diff --git a/claasp/cipher_modules/models/smt/utils/utils.py b/claasp/cipher_modules/models/smt/utils/utils.py index 1a8aff918..69b5f918e 100644 --- a/claasp/cipher_modules/models/smt/utils/utils.py +++ b/claasp/cipher_modules/models/smt/utils/utils.py @@ -14,7 +14,8 @@ # You should have received a copy of the GNU General Public License # along with this program. If not, see . # **************************************************************************** - +import numpy as np +import pickle # ------------------------ # # - Build formulae - # @@ -182,9 +183,9 @@ def smt_carry(x, y, previous_carry): """ Return a list of strings. - The list represents the Boolean equality ``carry = Or(And(x, y), And(x, previous_carry), And(y, previous_carry))`` - in SMT-LIB standard. It represents the general form of a carry when performing modular addition between two - bitvectors. + The list represents the Boolean equality + ``carry = Or(And(x, y), And(x, previous_carry), And(y, previous_carry))`` in SMT-LIB standard. It + represents the general form of a carry when performing modular addition between two bitvectors. INPUT: @@ -242,3 +243,381 @@ def get_component_hex_value(component, out_suffix, variable2value): hex_value = f"{value:#0{hex_digits + 2}x}" return hex_value + + +def interleave_bits(x, y, n): + """ + Interleave the bits of x and y. + + INPUT: + + - ``x`` -- **integer**; the value whose bits land on the even positions + - ``y`` -- **integer**; the value whose bits land on the odd positions + - ``n`` -- **integer**; the bit size of ``x`` and ``y`` + + EXAMPLES:: + + sage: from claasp.cipher_modules.models.smt.utils.utils import interleave_bits + sage: interleave_bits(0b11, 0b00, 2), interleave_bits(0b00, 0b11, 2) + (5, 10) + + The bits of ``x`` land on the even positions, those of ``y`` on the odd ones. + """ + z = 0 + + for i in range(n): + z |= (x & (1 << i)) << i | (y & (1 << i)) << (i + 1) + + return z + + +def to_quasidifferential_basis(x): + """ + Transform x into the quasidifferential basis. + + INPUT: + + - ``x`` -- **NumPy array**; a vector whose length is a power of 4 + + EXAMPLES:: + + sage: import numpy as np + sage: from claasp.cipher_modules.models.smt.utils.utils import to_quasidifferential_basis + sage: to_quasidifferential_basis(np.array([1, 0, 0, 0], dtype=float)).tolist() + [1.0, 0.0, 1.0, 0.0] + sage: to_quasidifferential_basis(np.array([1, 0], dtype=float)) + Traceback (most recent call last): + ... + ValueError: Input length must be divisible by 4. + """ + if len(x) == 1: + return x + + if len(x) % 4 != 0: + raise ValueError("Input length must be divisible by 4.") + + block_length = len(x) // 4 + + x_00 = to_quasidifferential_basis(x[:block_length]) + x_01 = to_quasidifferential_basis(x[block_length : 2 * block_length]) + x_10 = to_quasidifferential_basis(x[2 * block_length : 3 * block_length]) + x_11 = to_quasidifferential_basis(x[3 * block_length :]) + + return np.concatenate([x_00 + x_11, x_01 + x_10, x_00 - x_11, x_01 - x_10]) + + +def interleaved_transition_matrix(sbox_function, n, m): + """ + Build the interleaved transition matrix of ``sbox_function``. + + This is the NumPy equivalent of the Sage implementation. + + INPUT: + + - ``sbox_function`` -- **function**; the S-box, from integer to integer + - ``n`` -- **integer**; the input bit size of the S-box + - ``m`` -- **integer**; the output bit size of the S-box + + EXAMPLES:: + + sage: from claasp.cipher_modules.models.smt.utils.utils import interleaved_transition_matrix + sage: interleaved_transition_matrix(lambda x: x, 1, 1).tolist() + [[1.0, 0.0, 0.0, 0.0], [0.0, 1.0, 0.0, 0.0], [0.0, 0.0, 1.0, 0.0], [0.0, 0.0, 0.0, 1.0]] + """ + size_rows = 2 ** (2 * m) + size_cols = 2 ** (2 * n) + + transition_matrix = np.zeros((size_rows, size_cols), dtype=np.float64) + + for x in range(2**n): + for y in range(2**n): + i = interleave_bits(x, y, n) + j = interleave_bits(sbox_function(x), sbox_function(y), m) + + transition_matrix[j, i] = 1 + + return transition_matrix + + +def quasidifferential_transition_matrix(sbox_function, n, m): + """ + Compute the quasidifferential transition matrix of ``sbox_function``. + + INPUT: + + - ``sbox_function`` -- **function**; the S-box, from integer to integer + - ``n`` -- **integer**; the input bit size of the S-box + - ``m`` -- **integer**; the output bit size of the S-box + + EXAMPLES:: + + sage: from claasp.cipher_modules.models.smt.utils.utils import quasidifferential_transition_matrix + sage: quasidifferential_transition_matrix(lambda x: x ^^ 1, 1, 1).tolist() + [[1.0, 0.0, 0.0, 0.0], [0.0, 1.0, 0.0, 0.0], [0.0, 0.0, -1.0, 0.0], [0.0, 0.0, 0.0, -1.0]] + + The one-bit NOT, still in the interleaved order. + """ + quasidifferential_matrix = interleaved_transition_matrix(sbox_function, n, m) + + # Transform columns. + for i in range(2 ** (2 * n)): + quasidifferential_matrix[:, i] = to_quasidifferential_basis(quasidifferential_matrix[:, i]) + + # Transform rows. + for i in range(2 ** (2 * m)): + quasidifferential_matrix[i, :] = to_quasidifferential_basis(quasidifferential_matrix[i, :]) + + return quasidifferential_matrix / (2**n) + + +def _diff_target_indices(n, m, a, b, u, v): + """ + Target position with the DIFFERENCE as the major index. + + INPUT: + + - ``n`` -- **integer**; the input bit size of the S-box + - ``m`` -- **integer**; the output bit size of the S-box + - ``a`` -- **integer**; the input difference + - ``b`` -- **integer**; the output difference + - ``u`` -- **integer**; the input mask + - ``v`` -- **integer**; the output mask + + EXAMPLES:: + + sage: from claasp.cipher_modules.models.smt.utils.utils import _diff_target_indices + sage: _diff_target_indices(2, 2, 1, 2, 3, 0) + (8, 7) + """ + return 2**m * b + v, 2**n * a + u + + +def _mask_target_indices(n, m, a, b, u, v): + """ + Target position with the MASK as the major index. + + INPUT: + + - ``n`` -- **integer**; the input bit size of the S-box + - ``m`` -- **integer**; the output bit size of the S-box + - ``a`` -- **integer**; the input difference + - ``b`` -- **integer**; the output difference + - ``u`` -- **integer**; the input mask + - ``v`` -- **integer**; the output mask + + EXAMPLES:: + + sage: from claasp.cipher_modules.models.smt.utils.utils import _mask_target_indices + sage: _mask_target_indices(2, 2, 1, 2, 3, 0) + (2, 13) + """ + return 2**m * v + b, 2**n * u + a + + +def _fill_deinterleaved_block(deinterleaved_matrix, qdt_matrix, n, m, u, v, target_indices): + """ + Copy into ``deinterleaved_matrix`` the block of ``qdt_matrix`` selected by ``u`` and ``v``. + + ``u`` is the input mask and ``v`` the output mask; each entry is placed at the position given by + ``target_indices``. + + INPUT: + + - ``deinterleaved_matrix`` -- **NumPy array**; the matrix to fill, updated in place + - ``qdt_matrix`` -- **NumPy array**; the interleaved quasidifferential transition matrix + - ``n`` -- **integer**; the input bit size of the S-box + - ``m`` -- **integer**; the output bit size of the S-box + - ``u`` -- **integer**; the input mask + - ``v`` -- **integer**; the output mask + - ``target_indices`` -- **function**; either ``_diff_target_indices`` or + ``_mask_target_indices`` + + EXAMPLES:: + + sage: import numpy as np + sage: from claasp.cipher_modules.models.smt.utils.utils import ( + ....: _diff_target_indices, _fill_deinterleaved_block, quasidifferential_transition_matrix) + sage: qdt = quasidifferential_transition_matrix(lambda x: x ^^ 1, 1, 1) + sage: block = np.zeros((4, 4)) + sage: _fill_deinterleaved_block(block, qdt, 1, 1, 1, 1, _diff_target_indices) + sage: block.tolist() + [[0.0, 0.0, 0.0, 0.0], [0.0, -1.0, 0.0, 0.0], [0.0, 0.0, 0.0, 0.0], [0.0, 0.0, 0.0, -1.0]] + """ + for a in range(2**n): + source_col = interleave_bits(a, u, n) + + for b in range(2**m): + source_row = interleave_bits(b, v, m) + target_row, target_col = target_indices(n, m, a, b, u, v) + + deinterleaved_matrix[target_row, target_col] = qdt_matrix[source_row, source_col] + + +def deinterleave_qdt_matrix(qdt_matrix, n, m, primary: str = "diff"): + """ + Convert an interleaved QDT matrix to the requested ordering. + + ``primary`` selects which of the two quantities is used as the major index of the result: + ``"diff"`` (the default, expected by the quasidifferential SMT model) or ``"mask"``. + + INPUT: + + - ``qdt_matrix`` -- **NumPy array**; the interleaved quasidifferential transition matrix + - ``n`` -- **integer**; the input bit size of the S-box + - ``m`` -- **integer**; the output bit size of the S-box + - ``primary`` -- **string** (default: `diff`); the major index of the result, either ``'diff'`` + or ``'mask'`` + + EXAMPLES:: + + sage: from claasp.cipher_modules.models.smt.utils.utils import deinterleave_qdt_matrix, quasidifferential_transition_matrix + sage: qdt = quasidifferential_transition_matrix(lambda x: x ^^ 1, 1, 1) + sage: deinterleave_qdt_matrix(qdt, 1, 1).tolist() + [[1.0, 0.0, 0.0, 0.0], [0.0, -1.0, 0.0, 0.0], [0.0, 0.0, 1.0, 0.0], [0.0, 0.0, 0.0, -1.0]] + sage: deinterleave_qdt_matrix(qdt, 1, 1, primary='mask').tolist() + [[1.0, 0.0, 0.0, 0.0], [0.0, 1.0, 0.0, 0.0], [0.0, 0.0, -1.0, 0.0], [0.0, 0.0, 0.0, -1.0]] + sage: deinterleave_qdt_matrix(qdt, 1, 1, primary='other') + Traceback (most recent call last): + ... + ValueError: primary must be either 'diff' or 'mask'. + + With the difference as the major index, the one-bit NOT has coefficient ``-1`` exactly where the + output mask is 1: the sign factor ``(-1)^v``. + """ + if primary == "diff": + target_indices = _diff_target_indices + elif primary == "mask": + target_indices = _mask_target_indices + else: + raise ValueError("primary must be either 'diff' or 'mask'.") + + deinterleaved_matrix = np.zeros_like(qdt_matrix) + + for u in range(2**n): + for v in range(2**m): + _fill_deinterleaved_block(deinterleaved_matrix, qdt_matrix, n, m, u, v, target_indices) + + return deinterleaved_matrix + + +def check_qdt_feasibility(qdt_matrix): + """ + Check that the non-zero coefficients of a quasidifferential transition matrix are powers of two. + + The weight of a transition is ``-log2|coefficient|``, and the SMT model encodes it as a + thermometer of Boolean indicators, so it must be an integer. A coefficient of 3/8 has weight + 1.415 and would be recorded as 1 -- a silently optimistic weight, pooled with the genuine + weight-1 transitions, and a correlation of 2^-1 instead of 3/8 in the sum of Theorem 4.1. + + This mirrors ``claasp.components.sbox_component.check_table_feasibility``, which already refuses + a DDT with a non-power-of-two entry for the SAT, SMT and MILP differential models. The two + checks are NOT equivalent: a power-of-two DDT can still yield a non-power-of-two QDT, since a + mask-carrying cell sums +-1 over a power-of-two number of terms and may land anywhere in + between. Of 31 random 4-bit permutations whose DDT is all powers of two, 14 had a QDT cell that + is not. + + INPUT: + + - ``qdt_matrix`` -- a NumPy array of quasidifferential coefficients + + OUTPUT: + + - None; raises ``ValueError`` when a non-zero coefficient is not a power of two + + EXAMPLES:: + + sage: import numpy as np + sage: from claasp.cipher_modules.models.smt.utils.utils import check_qdt_feasibility + sage: check_qdt_feasibility(np.array([[1, 1/2], [0, 1/4]], dtype=float)) + sage: check_qdt_feasibility(np.array([[3/8]], dtype=float)) + Traceback (most recent call last): + ... + ValueError: The S-box QDT of the cipher contains 0.375 which is not a power of two. Currently, SMT cannot handle it. + """ + magnitudes = np.unique(np.abs(qdt_matrix[qdt_matrix != 0])) + exponents = np.log2(magnitudes) + offending = magnitudes[np.abs(exponents - np.round(exponents)) > 1e-9] + + if offending.size: + raise ValueError( + f"The S-box QDT of the cipher contains {offending[0]} which is not a " + f"power of two. Currently, SMT cannot handle it." + ) + + +def _weight_table_for_differential(qdt_matrix, n, m, b, a): + """ + Return the weight table of a single differential transition (``a`` -> ``b``) of the QDT. + + The result maps each weight loss to the list of ``(v, u)`` mask pairs achieving it. An empty + dictionary means the differential admits no valid quasidifferential transition. + + INPUT: + + - ``qdt_matrix`` -- **NumPy array**; the quasidifferential transition matrix, deinterleaved with + the difference as the major index + - ``n`` -- **integer**; the input bit size of the S-box + - ``m`` -- **integer**; the output bit size of the S-box + - ``b`` -- **integer**; the output difference + - ``a`` -- **integer**; the input difference + + EXAMPLES:: + + sage: from claasp.cipher_modules.models.smt.utils.utils import ( + ....: _weight_table_for_differential, deinterleave_qdt_matrix, quasidifferential_transition_matrix) + sage: qdt = deinterleave_qdt_matrix(quasidifferential_transition_matrix(lambda x: x ^^ 1, 1, 1), 1, 1) + sage: _weight_table_for_differential(qdt, 1, 1, 0, 0) + {0: [(0, 0), (1, 1)]} + sage: _weight_table_for_differential(qdt, 1, 1, 1, 0) + {} + """ + table = {} + + for v in range(2**m): + for u in range(2**n): + coefficient = qdt_matrix[2**m * b + v, 2**n * a + u] + + if coefficient == 0: + continue + + w_loss = int(-np.log2(abs(coefficient))) + table.setdefault(w_loss, []).append((v, u)) + + return table + + +def generate_weight_tables(qdt_matrix, n, m): + """ + Return the weight tables of the quasidifferential transition matrix. + + They are indexed by differential transition: + + {(b, a): {weight_loss: [(v, u), ...], ...}, ...} + + Every ``(b, a)`` pair is present, mapping to an empty dictionary when the differential admits no + valid transition. + + INPUT: + + - ``qdt_matrix`` -- **NumPy array**; the quasidifferential transition matrix, deinterleaved with + the difference as the major index + - ``n`` -- **integer**; the input bit size of the S-box + - ``m`` -- **integer**; the output bit size of the S-box + + EXAMPLES:: + + sage: from claasp.cipher_modules.models.smt.utils.utils import ( + ....: deinterleave_qdt_matrix, generate_weight_tables, quasidifferential_transition_matrix) + sage: qdt = deinterleave_qdt_matrix(quasidifferential_transition_matrix(lambda x: x ^^ 1, 1, 1), 1, 1) + sage: generate_weight_tables(qdt, 1, 1) + {(0, 0): {0: [(0, 0), (1, 1)]}, (0, 1): {}, (1, 0): {}, (1, 1): {0: [(0, 0), (1, 1)]}} + """ + check_qdt_feasibility(qdt_matrix) + + weights = {} + + for b in range(2**m): + for a in range(2**n): + weights[(b, a)] = _weight_table_for_differential(qdt_matrix, n, m, b, a) + + return weights diff --git a/claasp/components/and_component.py b/claasp/components/and_component.py index b4afd98eb..9dc19f19c 100644 --- a/claasp/components/and_component.py +++ b/claasp/components/and_component.py @@ -128,6 +128,7 @@ class And(MultiInputNonlinearLogicalOperator): sage: print(component3.description) # 6 total bits / output_bit_size 2 = 3 operands ['AND', 3] """ + def __init__( self, current_round_number, @@ -396,7 +397,7 @@ def sat_constraints(self): output_bit_ids = self._generate_output_ids() constraints = [] for i, output_bit_id in enumerate(output_bit_ids): - constraints.extend(sat_utils.cnf_and(output_bit_id, input_bit_ids[i::self.output_bit_size])) + constraints.extend(sat_utils.cnf_and(output_bit_id, input_bit_ids[i :: self.output_bit_size])) return output_bit_ids, constraints @@ -425,8 +426,10 @@ def smt_constraints(self): output_bit_ids = self._generate_output_ids() constraints = [] for i, output_bit_id in enumerate(output_bit_ids): - operation = smt_utils.smt_and(input_bit_ids[i::self.output_bit_size]) + operation = smt_utils.smt_and(input_bit_ids[i :: self.output_bit_size]) equation = smt_utils.smt_equivalent((output_bit_id, operation)) constraints.append(smt_utils.smt_assert(equation)) return output_bit_ids, constraints + + \ No newline at end of file diff --git a/claasp/components/cipher_output_component.py b/claasp/components/cipher_output_component.py index 819d9b45e..fad448785 100644 --- a/claasp/components/cipher_output_component.py +++ b/claasp/components/cipher_output_component.py @@ -50,6 +50,7 @@ class CipherOutput(Component): sage: print(component.description) ['cipher_output'] """ + def __init__( self, current_round_number, @@ -290,29 +291,23 @@ def cp_continuous_differential_propagation_constraints(self, model): component_id = self.id ninputs = self.input_bit_size num_links = len(self.input_id_links) - + cp_declarations = [] cp_constraints = [] - + for i in range(num_links): link_size = len(self.input_bit_positions[i]) - cp_declarations.append( - f"array[0..{link_size - 1}] of var -1.0..1.0: x{i+1}_{component_id};" - ) - - cp_declarations.append( - f"array[0..{ninputs - 1}] of var -1.0..1.0: {component_id};" - ) - + cp_declarations.append(f"array[0..{link_size - 1}] of var -1.0..1.0: x{i + 1}_{component_id};") + + cp_declarations.append(f"array[0..{ninputs - 1}] of var -1.0..1.0: {component_id};") + output_idx = 0 for i in range(num_links): link_size = len(self.input_bit_positions[i]) for j in range(link_size): - cp_constraints.append( - f"constraint {component_id}[{output_idx}] = x{i+1}_{component_id}[{j}];" - ) + cp_constraints.append(f"constraint {component_id}[{output_idx}] = x{i + 1}_{component_id}[{j}];") output_idx += 1 - + return cp_declarations, cp_constraints def get_byte_based_vectorized_python_code(self, params): @@ -743,3 +738,68 @@ def smt_xor_linear_mask_propagation_constraints(self, model=None): constraints.append(smt_utils.smt_assert(equation)) return output_bit_ids + input_bit_ids, constraints + + def smt_xor_quasidifferential_propagation_constraints( + self, + model, + ): + """ + Return SMT constraints for CIPHER OUTPUT quasidifferential propagation. + + A cipher output (and, unless overridden for fork-handling, + an intermediate output -- see IntermediateOutput) is a pure + copy of its input. For an identity map, Theorem 3.2 (5) gives + trivial propagation for BOTH the difference and the mask: + b = a and u = v, with weight 0. + + NOTE: if this component's input wire is also consumed + elsewhere (a "fork" in the cipher's data-flow graph), the + mask-propagation rule is NOT plain equality but an + XOR-combination of all the branches' masks (the dual of the + XOR-of-differences rule at a join point). The input mask read + here is then this component's own branch mask, given by + ``model._qdt_input_bit_ids``, and the model ties the branches to + the source in ``SmtXorQuasidifferentialModel._fork_constraints``. + + INPUT: + + - ``model`` -- **model object**; a ``SmtXorQuasidifferentialModel`` instance + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.constant_cipher import ConstantCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = ConstantCipher(output_bit_size=3, value=2) + sage: output = cipher.component_from_id('cipher_output_0_1') + sage: variables, constraints = output.smt_xor_quasidifferential_propagation_constraints(SmtXorQuasidifferentialModel(cipher)) + sage: constraints + ['(assert (= cipher_output_0_1_0 constant_0_0_0))', + '(assert (= cipher_output_0_1_1 constant_0_0_1))', + '(assert (= cipher_output_0_1_2 constant_0_0_2))', + '(assert (= qdt_cipher_output_0_1_0 qdt_constant_0_0_0))', + '(assert (= qdt_cipher_output_0_1_1 qdt_constant_0_0_1))', + '(assert (= qdt_cipher_output_0_1_2 qdt_constant_0_0_2))'] + """ + + input_bit_ids = self._generate_input_ids() + output_bit_ids = self._generate_output_ids() + + qdt_input_bit_ids = model._qdt_input_bit_ids(self) + qdt_output_bit_ids = [f"qdt_{bit_id}" for bit_id in output_bit_ids] + + constraints = [] + + for output_bit_id, input_bit_id in zip(output_bit_ids, input_bit_ids): + equation = smt_utils.smt_equivalent([output_bit_id, input_bit_id]) + constraints.append(smt_utils.smt_assert(equation)) + + for output_bit_id, input_bit_id in zip(qdt_output_bit_ids, qdt_input_bit_ids): + equation = smt_utils.smt_equivalent([output_bit_id, input_bit_id]) + constraints.append(smt_utils.smt_assert(equation)) + + variables = output_bit_ids + qdt_output_bit_ids + + return ( + variables, + constraints, + ) diff --git a/claasp/components/constant_component.py b/claasp/components/constant_component.py index 4b1d93130..349e512df 100644 --- a/claasp/components/constant_component.py +++ b/claasp/components/constant_component.py @@ -97,6 +97,7 @@ class Constant(Component): sage: print(component.description) ['0b0001000'] """ + def __init__(self, current_round_number, current_round_number_of_components, output_bit_size, value): component_id = f"{CONSTANT}_{current_round_number}_{current_round_number_of_components}" component_type = CONSTANT @@ -208,17 +209,12 @@ def cp_continuous_differential_propagation_constraints(self, model): """ size = self.output_bit_size - cp_declarations = [ - f"array[0..{size - 1}] of var -1.0..1.0: {self.id};" - ] + cp_declarations = [f"array[0..{size - 1}] of var -1.0..1.0: {self.id};"] - cp_constraints = [ - f"constraint {self.id}[{i}] = -1.0;" - for i in range(size) - ] + cp_constraints = [f"constraint {self.id}[{i}] = -1.0;" for i in range(size)] return cp_declarations, cp_constraints - + def cp_deterministic_truncated_xor_differential_trail_constraints(self): return self.cp_xor_differential_propagation_constraints() @@ -769,3 +765,58 @@ def smt_xor_linear_mask_propagation_constraints(self, model=None): output_bit_ids = self._generate_output_ids(suffix=constants.OUTPUT_BIT_ID_SUFFIX) return output_bit_ids, [] + + def smt_xor_quasidifferential_propagation_constraints( + self, + model, + ): + """ + Return SMT constraints for CONSTANT quasidifferential propagation. + + Per Beyne & Rijmen, Theorem 3.2 (4): for a translation + F(x) = x + t (a constant is exactly such a translation), + + D^F_(v,b),(u,a) = chi_v(t) * delta_v(u) * delta_b(a) + + This factors into: + + - the difference contributed by a constant is always 0 + (identical to smt_xor_differential_propagation_constraints); + - the mask v is a FREE parameter: it never affects the local + weight (which is always 0 regardless of v), only the sign + chi_v(t) of the correlation. This weight-based search does + not track signs, so v is simply left unconstrained here -- + exactly as smt_xor_linear_mask_propagation_constraints + already does for the ordinary linear model. Leaving it free + (rather than e.g. fixing it to 0) keeps it available for + any later sign/key-dependence analysis (cf. + generic_with_constant_sign_linear_constraints in + xor_component.py, and Section 4.4 of the paper). + + INPUT: + + - ``model`` -- **model object**; a ``SmtXorQuasidifferentialModel`` instance + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.constant_cipher import ConstantCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = ConstantCipher(output_bit_size=3, value=2) + sage: constant = cipher.component_from_id('constant_0_0') + sage: variables, constraints = constant.smt_xor_quasidifferential_propagation_constraints(SmtXorQuasidifferentialModel(cipher)) + sage: variables + ['constant_0_0_0', 'constant_0_0_1', 'constant_0_0_2', 'qdt_constant_0_0_0', 'qdt_constant_0_0_1', 'qdt_constant_0_0_2'] + sage: constraints + ['(assert (not constant_0_0_0))', '(assert (not constant_0_0_1))', '(assert (not constant_0_0_2))'] + """ + + output_bit_ids, diff_constraints = self.smt_xor_differential_propagation_constraints(model) + + qdt_output_bit_ids = [f"qdt_{bit_id}" for bit_id in output_bit_ids] + + variables = output_bit_ids + qdt_output_bit_ids + + return ( + variables, + diff_constraints, + ) diff --git a/claasp/components/fsr_component.py b/claasp/components/fsr_component.py index a81f74aad..227f4f571 100644 --- a/claasp/components/fsr_component.py +++ b/claasp/components/fsr_component.py @@ -94,6 +94,7 @@ class Fsr(Component): sage: print(component.output_bit_size) 0 """ + def __init__( self, current_round_number, diff --git a/claasp/components/idea_modmul_component.py b/claasp/components/idea_modmul_component.py index 287f7484b..5eb066daa 100644 --- a/claasp/components/idea_modmul_component.py +++ b/claasp/components/idea_modmul_component.py @@ -50,7 +50,7 @@ class IdeaModmul(Modular): sage: print(component.description) ['IDEA_MODMUL', 2, 5] """ - + def __init__( self, current_round_number, @@ -78,9 +78,7 @@ def algebraic_polynomials(self, model): Not implemented. """ - raise NotImplementedError( - "Algebraic polynomials for idea_modmul are not yet implemented." - ) + raise NotImplementedError("Algebraic polynomials for idea_modmul are not yet implemented.") def cms_constraints(self): """ @@ -90,9 +88,7 @@ def cms_constraints(self): Not implemented. """ - raise NotImplementedError( - "CMS constraints for idea_modmul are not yet implemented." - ) + raise NotImplementedError("CMS constraints for idea_modmul are not yet implemented.") def cp_constraints(self): """ @@ -102,14 +98,12 @@ def cp_constraints(self): Not implemented. """ - raise NotImplementedError( - "CP constraints for idea_modmul are not yet implemented." - ) + raise NotImplementedError("CP constraints for idea_modmul are not yet implemented.") def get_bit_based_vectorized_python_code(self, params): """ Generate Python code for bit-based vectorized modular multiplication. - + INPUT: - ``params`` -- **list**; the parameters for the function @@ -124,7 +118,7 @@ def get_bit_based_vectorized_python_code(self, params): # Retrieve stored parameters num_inputs = self.description[1] modulus = self.description[2] - + return [ f" {self.id} = bit_vector_idea_modmul([{','.join(params)}], " f"{num_inputs}, {self.output_bit_size}, {modulus})" @@ -133,7 +127,7 @@ def get_bit_based_vectorized_python_code(self, params): def get_byte_based_vectorized_python_code(self, params): """ Generate byte-based vectorized Python code for MODMUL evaluation. - + INPUT: - ``params`` -- **string**; the parameters for the function @@ -141,7 +135,7 @@ def get_byte_based_vectorized_python_code(self, params): # Retrieve stored modulus and word_size modulus = self.description[2] word_size = self.output_bit_size - + return [f" {self.id} = byte_vector_idea_modmul({params}, {modulus}, {word_size})"] def sat_constraints(self): @@ -152,9 +146,7 @@ def sat_constraints(self): Not implemented. """ - raise NotImplementedError( - "SAT constraints for idea_modmul are not yet implemented." - ) + raise NotImplementedError("SAT constraints for idea_modmul are not yet implemented.") def smt_constraints(self): """ @@ -164,6 +156,4 @@ def smt_constraints(self): Not implemented. """ - raise NotImplementedError( - "SMT constraints for idea_modmul are not yet implemented." - ) + raise NotImplementedError("SMT constraints for idea_modmul are not yet implemented.") diff --git a/claasp/components/intermediate_output_component.py b/claasp/components/intermediate_output_component.py index d60aa34f1..731b84aa2 100644 --- a/claasp/components/intermediate_output_component.py +++ b/claasp/components/intermediate_output_component.py @@ -74,6 +74,7 @@ class IntermediateOutput(CipherOutput): sage: print(component.description) ['round_output'] """ + def __init__( self, current_round_number, diff --git a/claasp/components/linear_layer_component.py b/claasp/components/linear_layer_component.py index 276a7b8af..1384f99ce 100644 --- a/claasp/components/linear_layer_component.py +++ b/claasp/components/linear_layer_component.py @@ -1151,3 +1151,101 @@ def smt_xor_linear_mask_propagation_constraints(self, model=None): dummy_bit_ids = [dummy_id for output_dummy_ids in outputs_dummy_ids for dummy_id in output_dummy_ids] return input_bit_ids + dummy_bit_ids + output_bit_ids, constraints + + def smt_xor_quasidifferential_propagation_constraints( + self, + model, + ): + """ + Return SMT constraints for LINEAR LAYER quasidifferential propagation. + + Per Beyne & Rijmen, Theorem 3.2 (5): for a linear map L, + + D^L_(v,b),(u,a) = delta_u(L^T(v)) * delta_b(L(a)) + + i.e. difference and mask propagation are two INDEPENDENT + constraint systems for a linear (non-sbox) component: + + - b = L(a): identical to the ordinary XOR-differential model + for this component (``smt_xor_differential_propagation_constraints``); + - u = L^T(v): the same relation used by the existing, tested + ordinary linear-mask-propagation model + (``smt_xor_linear_mask_propagation_constraints``, via + ``sat_generate_ids_for_linear_layer``, which inverts + ``self.description``). We reuse that exact matrix logic + here rather than re-deriving the transpose direction, and + only rename the produced variables to the ``qdt_`` naming + convention used by the quasidifferential model (direct + reference to the upstream component's bit id, instead of + the ``_i``/``_o`` suffix convention used by the ordinary + linear model). + + INPUT: + + - ``model`` -- **model object**; a ``SmtXorQuasidifferentialModel`` instance + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.linear_layer_cipher import LinearLayerCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = LinearLayerCipher(bit_size=2, description=[[1, 1], [0, 1]]) + sage: linear_layer = cipher.component_from_id('linear_layer_0_0') + sage: variables, constraints = linear_layer.smt_xor_quasidifferential_propagation_constraints(SmtXorQuasidifferentialModel(cipher)) + sage: constraints + ['(assert (= linear_layer_0_0_0 plaintext_0))', + '(assert (= linear_layer_0_0_1 (xor plaintext_0 plaintext_1)))', + '(assert (= qdt_plaintext_0 qdt_dummy_0_qdt_linear_layer_0_0_0))', + '(assert (= qdt_plaintext_1 qdt_dummy_1_qdt_linear_layer_0_0_0 qdt_dummy_1_qdt_linear_layer_0_0_1))', + '(assert (= qdt_linear_layer_0_0_0 (xor qdt_dummy_0_qdt_linear_layer_0_0_0 qdt_dummy_1_qdt_linear_layer_0_0_0)))', + '(assert (= qdt_linear_layer_0_0_1 qdt_dummy_1_qdt_linear_layer_0_0_1))'] + """ + + output_bit_ids, diff_constraints = LinearLayer.smt_constraints(self) + + # Mask propagation: u = L^T(v). + # + # Same construction as sat_generate_ids_for_linear_layer / + # smt_xor_linear_mask_propagation_constraints (matrix + # inversion over GF(2)), but seeded directly with the + # qdt_ naming convention instead of the "_i"/"_o" one. + + qdt_input_bit_ids = model._qdt_input_bit_ids(self) + qdt_output_bit_ids = [f"qdt_{bit_id}" for bit_id in output_bit_ids] + + inverse_matrix = Matrix(FiniteField(2), self.description).inverse() + + outputs_dummy_ids = [[] for _ in range(self.output_bit_size)] + inputs_equivalent_ids = [[] for _ in range(self.input_bit_size)] + + for i, qdt_input_bit_id in enumerate(qdt_input_bit_ids): + inputs_equivalent_ids[i] = [qdt_input_bit_id] + for j, qdt_output_bit_id in enumerate(qdt_output_bit_ids): + if inverse_matrix[j][i]: + variable = f"qdt_dummy_{i}_{qdt_output_bit_id}" + inputs_equivalent_ids[i].append(variable) + outputs_dummy_ids[j].append(variable) + + mask_constraints = [] + + for input_equivalent_ids in inputs_equivalent_ids: + equivalence = smt_utils.smt_equivalent(input_equivalent_ids) + mask_constraints.append(smt_utils.smt_assert(equivalence)) + + for i, qdt_output_bit_id in enumerate(qdt_output_bit_ids): + if len(outputs_dummy_ids[i]) == 1: + operation = outputs_dummy_ids[i][0] + else: + operation = smt_utils.smt_xor(outputs_dummy_ids[i]) + equation = smt_utils.smt_equivalent((qdt_output_bit_id, operation)) + mask_constraints.append(smt_utils.smt_assert(equation)) + + dummy_bit_ids = [dummy_id for output_dummy_ids in outputs_dummy_ids for dummy_id in output_dummy_ids] + + variables = output_bit_ids + qdt_output_bit_ids + dummy_bit_ids + + constraints = diff_constraints + mask_constraints + + return ( + variables, + constraints, + ) diff --git a/claasp/components/mix_column_component.py b/claasp/components/mix_column_component.py index 7128ef2f0..c80801f24 100644 --- a/claasp/components/mix_column_component.py +++ b/claasp/components/mix_column_component.py @@ -116,6 +116,7 @@ class MixColumn(LinearLayer): sage: print(component.description[1]) 1 """ + def __init__( self, current_round_number, @@ -1249,3 +1250,48 @@ def smt_xor_linear_mask_propagation_constraints(self, model=None): self.description = original_description result = variables, constraints return result + + def smt_xor_quasidifferential_propagation_constraints( + self, + model, + ): + """ + Return SMT constraints for MIX COLUMN quasidifferential propagation. + + Same pattern used throughout this class for every other model + (differential, linear, MILP, SAT, ...): MixColumn stores its + description as ``[word_matrix, rotation/polynomial, word_size]`` + rather than a plain bit matrix, so ``LinearLayer``'s methods -- + which index ``self.description`` directly as a bit matrix -- + cannot be inherited as-is. We expand to the bit-level matrix via + ``binary_matrix_of_linear_component``, temporarily swap + ``self.description`` to it, delegate to + ``LinearLayer.smt_xor_quasidifferential_propagation_constraints`` + (which already implements Theorem 3.2(5): b = L(a) for the + difference, u = L^T(v) for the mask), and restore the original + description afterwards. + + INPUT: + + - ``model`` -- **model object**; a ``SmtXorQuasidifferentialModel`` instance + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.mix_column_cipher import MixColumnCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = MixColumnCipher(word_size=2, matrix=[[1, 1], [0, 1]], irreducible_polynomial=0x7) + sage: mix_column = cipher.component_from_id('mix_column_0_0') + sage: variables, constraints = mix_column.smt_xor_quasidifferential_propagation_constraints(SmtXorQuasidifferentialModel(cipher)) + sage: len(variables), len(constraints) + (14, 12) + sage: constraints[0] + '(assert (= mix_column_0_0_0 (xor plaintext_0 plaintext_2)))' + """ + matrix = binary_matrix_of_linear_component(self) + matrix_transposed = [[matrix[i][j] for i in range(matrix.nrows())] for j in range(matrix.ncols())] + original_description = deepcopy(self.description) + self.description = matrix_transposed + variables, constraints = super().smt_xor_quasidifferential_propagation_constraints(model) + self.description = original_description + result = variables, constraints + return result diff --git a/claasp/components/modadd_component.py b/claasp/components/modadd_component.py index d848035f9..56e4d11ad 100644 --- a/claasp/components/modadd_component.py +++ b/claasp/components/modadd_component.py @@ -20,6 +20,256 @@ from claasp.cipher_modules.models.smt.utils import utils as smt_utils from claasp.components.modular_component import Modular +def smt_quasidifferential_modadd( + component, + name_prefix, + a_ids, + b_ids, + c_ids, + u_ids, + v_ids, + w_ids, +): + """ + Return the SMT variables and constraints of Theorem 5.2 of Beyne & + Rijmen for a two-operand modular addition, plus the classical + Lipmaa-Moriai differential validity condition. + + Shared by MODADD and MODSUB: modular subtraction reduces EXACTLY to + modular addition with permuted roles (``z = x - y`` is equivalent to + ``x = z + y``), so ModSub calls this with its own arguments swapped + -- see ModSub.smt_xor_quasidifferential_propagation_constraints. + + ``name_prefix`` distinguishes the auxiliary variables of the two + operations (``modadd_`` / ``modsub_``), so that a cipher using both + does not collide. + + The ``M`` and ``M-transpose`` linear maps of Section 5.2 reduce, + bit by bit in claasp's MSB-first ordering (index 0 = MSB), to: + + M_pseudoinverse(t)[0] = false + M_pseudoinverse(t)[q] = t[q] xor t[q-1] for q = 1..n-1 + + M_transpose(t)[0] = false + M_transpose(t)[q] = t[0] xor t[1] xor ... xor t[q-1] for q = 1..n-1 + (prefix XOR of all more-significant bits) + + This was verified EXHAUSTIVELY against the QDT coefficient computed + directly from Equation (4) of the paper, over all 3-bit + (a,b,c,u,v,w) combinations: 6728 valid transitions, 0 false + positives, 0 false negatives, 0 wrong weights. + + INPUT: + + - ``component`` -- **Component object**; the modular addition or subtraction component + - ``name_prefix`` -- **string**; the prefix of the auxiliary variables, ``'modadd_'`` or ``'modsub_'`` + - ``a_ids`` -- **list**; the difference variables of the first addend + - ``b_ids`` -- **list**; the difference variables of the second addend + - ``c_ids`` -- **list**; the difference variables of the sum + - ``u_ids`` -- **list**; the mask variables of the first addend + - ``v_ids`` -- **list**; the mask variables of the second addend + - ``w_ids`` -- **list**; the mask variables of the sum + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.modadd_cipher import ModaddCipher + sage: from claasp.components.modadd_component import smt_quasidifferential_modadd + sage: cipher = ModaddCipher(word_bit_size=2, number_of_inputs=2, modulus=4) + sage: modadd = cipher.component_from_id('modadd_0_0') + sage: variables, constraints = smt_quasidifferential_modadd( + ....: modadd, 'modadd_', + ....: ['plaintext_0', 'plaintext_1'], ['key_0', 'key_1'], ['modadd_0_0_0', 'modadd_0_0_1'], + ....: ['qdt_plaintext_0', 'qdt_plaintext_1'], ['qdt_key_0', 'qdt_key_1'], ['qdt_modadd_0_0_0', 'qdt_modadd_0_0_1']) + sage: len(variables), len(constraints) + (20, 23) + sage: constraints[0] + '(assert (= modadd_aprime_modadd_0_0_0 (xor key_0 modadd_0_0_0)))' + """ + + word_size = component.output_bit_size + + constraints = [] + variables = [] + + def new_named_formula(prefix, index, formula): + variable_name = f"{prefix}_{component.id}_{index}" + equation = smt_utils.smt_equivalent([variable_name, formula]) + constraints.append(smt_utils.smt_assert(equation)) + variables.append(variable_name) + return variable_name + + # a' = b xor c ; b' = a xor c ; c' = M+(a xor b xor c) + + a_prime_ids = [] + b_prime_ids = [] + abc_xor_ids = [] + + for i in range(word_size): + a_prime_ids.append( + new_named_formula(f"{name_prefix}aprime", i, smt_utils.smt_xor([b_ids[i], c_ids[i]])) + ) + b_prime_ids.append( + new_named_formula(f"{name_prefix}bprime", i, smt_utils.smt_xor([a_ids[i], c_ids[i]])) + ) + abc_xor_ids.append( + new_named_formula( + f"{name_prefix}abcxor", + i, + smt_utils.smt_xor([a_ids[i], b_ids[i], c_ids[i]]), + ) + ) + + c_prime_ids = ["false"] * word_size + + for q in range(1, word_size): + c_prime_ids[q] = new_named_formula( + f"{name_prefix}cprime", + q, + smt_utils.smt_xor([abc_xor_ids[q], abc_xor_ids[q - 1]]), + ) + + # u' = u xor w ; v' = v xor w ; w' = M^T(u xor v xor w) + + u_prime_ids = [] + v_prime_ids = [] + uvw_xor_ids = [] + + for i in range(word_size): + u_prime_ids.append( + new_named_formula(f"{name_prefix}uprime", i, smt_utils.smt_xor([u_ids[i], w_ids[i]])) + ) + v_prime_ids.append( + new_named_formula(f"{name_prefix}vprime", i, smt_utils.smt_xor([v_ids[i], w_ids[i]])) + ) + uvw_xor_ids.append( + new_named_formula( + f"{name_prefix}uvwxor", + i, + smt_utils.smt_xor([u_ids[i], v_ids[i], w_ids[i]]), + ) + ) + + w_prime_ids = ["false"] * word_size + prefix_xor = "false" + + for q in range(1, word_size): + prefix_xor = new_named_formula( + f"{name_prefix}wprime", + q, + smt_utils.smt_xor([prefix_xor, uvw_xor_ids[q - 1]]), + ) + w_prime_ids[q] = prefix_xor + + # DIFFERENTIAL VALIDITY (Lipmaa-Moriai). + # + # Theorem 5.2's own conditions constrain the MASK side assuming the + # differential (a, b) -> c is already valid: common.py can omit this + # check because there a, b, c are CONSTANTS taken from a known-good + # characteristic. Here they are variables, so the classical + # modular-addition differential validity must be asserted + # explicitly, otherwise the solver returns "trails" whose true + # correlation is zero. + # + # eq(a<<1, b<<1, c<<1) & (a xor b xor c xor (b<<1)) == 0 + + for i in range(word_size): + + if i == word_size - 1: + # LSB: eq is trivially true (all shifted-in bits are 0), + # so the condition reduces to a xor b xor c == 0. + constraints.append( + smt_utils.smt_assert( + smt_utils.smt_not(smt_utils.smt_xor([a_ids[i], b_ids[i], c_ids[i]])) + ) + ) + else: + bits_equal = smt_utils.smt_and( + [ + smt_utils.smt_equivalent([a_ids[i + 1], b_ids[i + 1]]), + smt_utils.smt_equivalent([a_ids[i + 1], c_ids[i + 1]]), + ] + ) + must_vanish = smt_utils.smt_xor([a_ids[i], b_ids[i], c_ids[i], b_ids[i + 1]]) + constraints.append( + smt_utils.smt_assert( + smt_utils.smt_implies(bits_equal, smt_utils.smt_not(must_vanish)) + ) + ) + + # Validity + local weight, per bit. + + weight_bit_ids = [] + + for i in range(word_size): + + a_p, b_p, c_p = a_prime_ids[i], b_prime_ids[i], c_prime_ids[i] + u_p, v_p, w_p = u_prime_ids[i], v_prime_ids[i], w_prime_ids[i] + + validity_1 = smt_utils.smt_implies( + smt_utils.smt_or([u_p, v_p]), + smt_utils.smt_or([a_p, b_p, w_p]), + ) + constraints.append(smt_utils.smt_assert(validity_1)) + + validity_2 = smt_utils.smt_equivalent( + [ + smt_utils.smt_xor( + [ + smt_utils.smt_and([a_p, u_p]), + smt_utils.smt_and([b_p, v_p]), + ] + ), + smt_utils.smt_and([c_p, w_p]), + ] + ) + constraints.append(smt_utils.smt_assert(validity_2)) + + weight_bit_id = f"hw_qdt_{component.id}_{i}" + weight_bit_ids.append(weight_bit_id) + + if i == 0: + # Third condition of Theorem 5.2, on the most significant bit. + top_bit_validity = smt_utils.smt_or( + [ + smt_utils.smt_and([smt_utils.smt_not(a_p), smt_utils.smt_not(b_p)]), + smt_utils.smt_equivalent( + [ + smt_utils.smt_and([a_p, u_p]), + smt_utils.smt_xor([u_p, v_p]), + ] + ), + ] + ) + constraints.append(smt_utils.smt_assert(top_bit_validity)) + + # The most significant bit does NOT contribute to the weight: + # in modular addition it generates no carry (the classical + # Lipmaa-Moriai exclusion). + # + # Theorem 5.2's "-1" correction term is NOT encoded because it + # is PROVABLY unreachable given the validity conditions: it + # requires a'_0 = u'_0 = 1 and v'_0 = 0, but the second + # condition at bit 0 forces + # (a'_0 & u'_0) xor (b'_0 & v'_0) == c'_0 & w'_0, and + # c'_0 = w'_0 = 0 by construction, so the left-hand side would + # be 1 != 0. Confirmed empirically as well: 0 cases with the + # correction active over all valid 3-bit transitions. + weight_definition = smt_utils.smt_equivalent([weight_bit_id, "false"]) + else: + weight_definition = smt_utils.smt_equivalent( + [ + weight_bit_id, + smt_utils.smt_or([a_p, b_p, w_p]), + ] + ) + + constraints.append(smt_utils.smt_assert(weight_definition)) + output_bit_ids = component._generate_output_ids() + qdt_output_bit_ids = [f"qdt_{bit_id}" for bit_id in output_bit_ids] + + variables = output_bit_ids + qdt_output_bit_ids + variables + weight_bit_ids + + return variables, constraints def cms_modadd(output_ids, input0_ids, input1_ids, carry_ids): # The CMS modular addition between 2 addenda @@ -432,3 +682,67 @@ def smt_constraints(self): ids.extend([output_id for output_ids in outputs_ids for output_id in output_ids]) return ids, constraints + + def smt_xor_quasidifferential_propagation_constraints( + self, + model, + ): + """ + Return SMT constraints for MODADD quasidifferential propagation. + + Implements Theorem 5.2 of Beyne & Rijmen (modular addition mod + 2^n) for the pairwise case only -- this is what Speck actually + uses. ModAdd's n>2-operand chaining (sat_modadd_seq / + smt_modadd_seq) has no equivalent QDT derivation in the paper, + so this raises NotImplementedError rather than guessing; + build_xor_quasidifferential_trail_model catches that and skips + the component with a clear message. + + The constraints themselves live in the module-level function + ``smt_quasidifferential_modadd``, shared with ModSub, which + reduces to modular addition with permuted roles. + + INPUT: + + - ``model`` -- **model object**; a model instance + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.modadd_cipher import ModaddCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = ModaddCipher(word_bit_size=2, number_of_inputs=2, modulus=4) + sage: modadd = cipher.component_from_id('modadd_0_0') + sage: variables, constraints = modadd.smt_xor_quasidifferential_propagation_constraints(SmtXorQuasidifferentialModel(cipher)) + sage: len(variables), len(constraints) + (20, 23) + sage: variables[:4] + ['modadd_0_0_0', 'modadd_0_0_1', 'qdt_modadd_0_0_0', 'qdt_modadd_0_0_1'] + """ + + num_operands = self.description[1] + + if num_operands != 2: + raise NotImplementedError( + f"{self.id}: quasidifferential propagation for MODADD is " + f"only implemented for 2 operands (Theorem 5.2 of " + f"Beyne & Rijmen); got {num_operands}." + ) + + word_size = self.output_bit_size + + input_bit_ids = self._generate_input_ids() + output_bit_ids = self._generate_output_ids() + + qdt_input_bit_ids = model._qdt_input_bit_ids(self) + qdt_output_bit_ids = [f"qdt_{bit_id}" for bit_id in output_bit_ids] + + return smt_quasidifferential_modadd( + self, + "modadd_", + input_bit_ids[:word_size], + input_bit_ids[word_size:], + output_bit_ids, + qdt_input_bit_ids[:word_size], + qdt_input_bit_ids[word_size:], + qdt_output_bit_ids, + ) diff --git a/claasp/components/modmul_component.py b/claasp/components/modmul_component.py index d67ca39e9..02f7b7c59 100644 --- a/claasp/components/modmul_component.py +++ b/claasp/components/modmul_component.py @@ -58,6 +58,7 @@ class ModMul(Modular): sage: print(component3.description) # 6 total bits / output_bit_size 2 = 3 operands ['MODMUL', 3, 4] """ + def __init__( self, current_round_number, diff --git a/claasp/components/modsub_component.py b/claasp/components/modsub_component.py index cb315d913..881679aee 100644 --- a/claasp/components/modsub_component.py +++ b/claasp/components/modsub_component.py @@ -19,7 +19,7 @@ from claasp.cipher_modules.models.sat.utils import utils as sat_utils from claasp.cipher_modules.models.smt.utils import utils as smt_utils from claasp.components.modular_component import Modular - +from claasp.components.modadd_component import smt_quasidifferential_modadd def cp_twoterms(input_1, input_2, out, component_name, input_length, cp_constraints, cp_declarations): cp_declarations.append(f"array[0..{input_length - 1}] of var 0..1:pre_minus_{input_2};") @@ -413,3 +413,91 @@ def smt_constraints(self): constraints.append(smt_utils.smt_assert(equation)) return temp_carry_bit_ids + temp_input_bit_ids + carry_bit_ids + output_bit_ids, constraints + + def smt_xor_quasidifferential_propagation_constraints( + self, + model, + ): + """ + Return SMT constraints for MODSUB quasidifferential propagation. + + Modular subtraction reduces EXACTLY to modular addition with + permuted roles: ``z = x - y`` is equivalent to ``x = z + y``, so + a MODSUB transition with input differences (A, B), output + difference C, input masks (U, V) and output mask W has the same + QDT coefficient as the MODADD transition with input differences + (C, B), output difference A, input masks (W, V) and output mask + U: + + D_MODSUB(A,B,C,U,V,W) == D_MODADD(C,B,A,W,V,U) + + i.e. simply swap A <-> C and U <-> W. + + This was verified by EXHAUSTIVE brute force of Equation (4) + applied directly to modular subtraction and to modular + addition, over all 3-bit (A,B,C,U,V,W) combinations: 6728 valid + transitions compared, 0 mismatches. + + The constraints are therefore ModAdd's own, obtained by calling + the shared ``smt_quasidifferential_modadd`` with the arguments + permuted. Only 2 operands are supported, as for ModAdd. + + INPUT: + + - ``model`` -- **model object**; a model instance + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.modsub_cipher import ModsubCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = ModsubCipher(word_bit_size=2, number_of_inputs=2, modulus=4) + sage: modsub = cipher.component_from_id('modsub_0_0') + sage: variables, constraints = modsub.smt_xor_quasidifferential_propagation_constraints(SmtXorQuasidifferentialModel(cipher)) + sage: len(variables), len(constraints) + (20, 23) + sage: constraints[0] + '(assert (= modsub_aprime_modsub_0_0_0 (xor key_0 plaintext_0)))' + + The first auxiliary variable already shows the swap: for ``z = x - y`` + the shared addition sees ``x = z + y``. + """ + + num_operands = self.description[1] + + if num_operands != 2: + raise NotImplementedError( + f"{self.id}: quasidifferential propagation for MODSUB is " + f"only implemented for 2 operands (Theorem 5.2 of " + f"Beyne & Rijmen, via the reduction to MODADD); " + f"got {num_operands}." + ) + + word_size = self.output_bit_size + + input_bit_ids = self._generate_input_ids() + output_bit_ids = self._generate_output_ids() + + qdt_input_bit_ids = model._qdt_input_bit_ids(self) + qdt_output_bit_ids = [f"qdt_{bit_id}" for bit_id in output_bit_ids] + + # MODSUB's own variables. + modsub_a_ids = input_bit_ids[:word_size] + modsub_b_ids = input_bit_ids[word_size:] + modsub_c_ids = output_bit_ids + + modsub_u_ids = qdt_input_bit_ids[:word_size] + modsub_v_ids = qdt_input_bit_ids[word_size:] + modsub_w_ids = qdt_output_bit_ids + + # Apply the verified permutation to obtain MODADD's roles: + # (a, b, c, u, v, w) = (C, B, A, W, V, U). + return smt_quasidifferential_modadd( + self, + "modsub_", + modsub_c_ids, + modsub_b_ids, + modsub_a_ids, + modsub_w_ids, + modsub_v_ids, + modsub_u_ids, + ) diff --git a/claasp/components/modular_component.py b/claasp/components/modular_component.py index d4a4cc69f..35b886f1a 100644 --- a/claasp/components/modular_component.py +++ b/claasp/components/modular_component.py @@ -107,6 +107,7 @@ class Modular(Component): sage: print(component3.description) # 6 total bits / output_bit_size 2 = 3 operands ['MODADD', 3, 4] """ + def __init__( self, current_round_number, @@ -169,13 +170,19 @@ def cms_xor_linear_mask_propagation_constraints(self, model=None): 'hw_modular_0_0_3_o -modular_0_0_3_o modular_0_0_7_i'] """ input_bit_ids = self._generate_component_input_ids() - lhs_input_bit_ids = input_bit_ids[:self.output_bit_size] - rhs_input_bit_ids = input_bit_ids[self.output_bit_size:] + lhs_input_bit_ids = input_bit_ids[: self.output_bit_size] + rhs_input_bit_ids = input_bit_ids[self.output_bit_size :] output_bit_ids = self._generate_output_ids(suffix=constants.OUTPUT_BIT_ID_SUFFIX) hw_bit_ids = [f"hw_{output_bit_id}" for output_bit_id in output_bit_ids] constraints = [f"-{hw_bit_ids[0]}"] constraints.append(f"x -{hw_bit_ids[1]} {output_bit_ids[0]} {lhs_input_bit_ids[0]} {rhs_input_bit_ids[0]}") - for new_hw_bit_id, output_bit_id, lhs_input_bit_id, rhs_input_bit_id, hw_bit_id, in zip( + for ( + new_hw_bit_id, + output_bit_id, + lhs_input_bit_id, + rhs_input_bit_id, + hw_bit_id, + ) in zip( hw_bit_ids[1:-1], output_bit_ids[1:-1], lhs_input_bit_ids[1:-1], rhs_input_bit_ids[1:-1], hw_bit_ids[2:] ): constraints.append(f"x {new_hw_bit_id} {output_bit_id} {lhs_input_bit_id} {rhs_input_bit_id} -{hw_bit_id}") @@ -311,7 +318,10 @@ def cp_semi_deterministic_truncated_xor_differential_constraints(self): for i in range(num_add): cp_declarations.append(f"array[0..{input_len - 1}] of var 0..2: pre_{output_id_link}_{i};") cp_constraints.extend( - [f"constraint pre_{output_id_link}_{i}[{j}] = {all_inputs[i * input_len + j]};" for j in range(input_len)] + [ + f"constraint pre_{output_id_link}_{i}[{j}] = {all_inputs[i * input_len + j]};" + for j in range(input_len) + ] ) for i in range(num_add, 2 * num_add - 2): @@ -1318,8 +1328,8 @@ def extend_constraints_for_window_size( constraints_.extend(new_constraints) input_bit_ids = self._generate_input_ids() - lhs_input_bit_ids = input_bit_ids[:self.output_bit_size] - rhs_input_bit_ids = input_bit_ids[self.output_bit_size:] + lhs_input_bit_ids = input_bit_ids[: self.output_bit_size] + rhs_input_bit_ids = input_bit_ids[self.output_bit_size :] output_bit_ids = self._generate_output_ids() dummy_bit_ids = [f"dummy_{output_bit_id}" for output_bit_id in output_bit_ids[:-1]] hw_bit_ids = [f"hw_{output_bit_id}" for output_bit_id in output_bit_ids] @@ -1333,10 +1343,17 @@ def extend_constraints_for_window_size( # Trail validity # for hw_bit_id, dummy_bit_id, shifted_id, lhs_input_bit_id, rhs_input_bit_id, output_bit_id in zip( - hw_bit_ids[:-1], dummy_bit_ids, rhs_input_bit_ids[1:], lhs_input_bit_ids[:-1], rhs_input_bit_ids[:-1], output_bit_ids[:-1] + hw_bit_ids[:-1], + dummy_bit_ids, + rhs_input_bit_ids[1:], + lhs_input_bit_ids[:-1], + rhs_input_bit_ids[:-1], + output_bit_ids[:-1], ): constraints.extend( - sat_utils.cnf_lipmaa(hw_bit_id, dummy_bit_id, shifted_id, lhs_input_bit_id, rhs_input_bit_id, output_bit_id) + sat_utils.cnf_lipmaa( + hw_bit_id, dummy_bit_id, shifted_id, lhs_input_bit_id, rhs_input_bit_id, output_bit_id + ) ) constraints.extend(sat_utils.cnf_xor(output_bit_ids[-1], [lhs_input_bit_ids[-1], rhs_input_bit_ids[-1]])) @@ -1400,8 +1417,8 @@ def sat_bitwise_deterministic_truncated_xor_differential_constraints(self): '-carry_modular_0_0_3_0_0 -carry_modular_0_0_3_1_1' """ in_ids_0, in_ids_1 = self._generate_input_double_ids() - lhs_in_ids_0, lhs_in_ids_1 = in_ids_0[:self.output_bit_size], in_ids_1[:self.output_bit_size] - rhs_in_ids_0, rhs_in_ids_1 = in_ids_0[self.output_bit_size:], in_ids_1[self.output_bit_size:] + lhs_in_ids_0, lhs_in_ids_1 = in_ids_0[: self.output_bit_size], in_ids_1[: self.output_bit_size] + rhs_in_ids_0, rhs_in_ids_1 = in_ids_0[self.output_bit_size :], in_ids_1[self.output_bit_size :] out_ids_0, out_ids_1 = self._generate_output_double_ids() carry_ids_0 = [f"carry_{out_id}_0" for out_id in out_ids_0] carry_ids_1 = [f"carry_{out_id}_1" for out_id in out_ids_1] @@ -1626,15 +1643,21 @@ def sat_xor_linear_mask_propagation_constraints(self, model=None): '-hw_modular_0_0_0_o' """ input_bit_ids = self._generate_component_input_ids() - lhs_input_bit_ids = input_bit_ids[:self.output_bit_size] - rhs_input_bit_ids = input_bit_ids[self.output_bit_size:] + lhs_input_bit_ids = input_bit_ids[: self.output_bit_size] + rhs_input_bit_ids = input_bit_ids[self.output_bit_size :] output_bit_ids = self._generate_output_ids(suffix=constants.OUTPUT_BIT_ID_SUFFIX) hw_bit_ids = [f"hw_{output_bit_id}" for output_bit_id in output_bit_ids] constraints = [f"-{hw_bit_ids[0]}"] constraints.extend( sat_utils.cnf_xor(hw_bit_ids[1], [output_bit_ids[0], lhs_input_bit_ids[0], rhs_input_bit_ids[0]]) ) - for hw_bit_id, new_hw_bit_id, output_bit_id, lhs_input_bit_id, rhs_input_bit_id, in zip( + for ( + hw_bit_id, + new_hw_bit_id, + output_bit_id, + lhs_input_bit_id, + rhs_input_bit_id, + ) in zip( hw_bit_ids[2:], hw_bit_ids[1:-1], output_bit_ids[1:-1], lhs_input_bit_ids[1:-1], rhs_input_bit_ids[1:-1] ): constraints.extend( @@ -1674,8 +1697,8 @@ def smt_xor_differential_propagation_constraints(self, model=None): True """ input_bit_ids = self._generate_input_ids() - lhs_input_bit_ids = input_bit_ids[:self.output_bit_size] - rhs_input_bit_ids = input_bit_ids[self.output_bit_size:] + lhs_input_bit_ids = input_bit_ids[: self.output_bit_size] + rhs_input_bit_ids = input_bit_ids[self.output_bit_size :] output_bit_ids = self._generate_output_ids() hw_bit_ids = [f"hw_{output_bit_id}" for output_bit_id in output_bit_ids] constraints = [] @@ -1728,15 +1751,21 @@ def smt_xor_linear_mask_propagation_constraints(self, model=None): '(assert (not hw_modular_0_0_0_o))' """ input_bit_ids = self._generate_component_input_ids() - lhs_input_bit_ids = input_bit_ids[:self.output_bit_size] - rhs_input_bit_ids = input_bit_ids[self.output_bit_size:] + lhs_input_bit_ids = input_bit_ids[: self.output_bit_size] + rhs_input_bit_ids = input_bit_ids[self.output_bit_size :] output_bit_ids = self._generate_output_ids(suffix=constants.OUTPUT_BIT_ID_SUFFIX) hw_bit_ids = [f"hw_{output_bit_id}" for output_bit_id in output_bit_ids] constraints = [smt_utils.smt_assert(smt_utils.smt_not(hw_bit_ids[0]))] operation = smt_utils.smt_xor((output_bit_ids[0], lhs_input_bit_ids[0], rhs_input_bit_ids[0])) equation = smt_utils.smt_equivalent((hw_bit_ids[1], operation)) constraints.append(smt_utils.smt_assert(equation)) - for hw_bit_id, new_hw_bit_id, output_bit_id, lhs_input_bit_id, rhs_input_bit_id, in zip( + for ( + hw_bit_id, + new_hw_bit_id, + output_bit_id, + lhs_input_bit_id, + rhs_input_bit_id, + ) in zip( hw_bit_ids[2:], hw_bit_ids[1:-1], output_bit_ids[1:-1], lhs_input_bit_ids[1:-1], rhs_input_bit_ids[1:-1] ): operation = smt_utils.smt_xor((new_hw_bit_id, output_bit_id, lhs_input_bit_id, rhs_input_bit_id)) diff --git a/claasp/components/multi_input_non_linear_logical_operator_component.py b/claasp/components/multi_input_non_linear_logical_operator_component.py index 8be4b5b2b..23b50b743 100644 --- a/claasp/components/multi_input_non_linear_logical_operator_component.py +++ b/claasp/components/multi_input_non_linear_logical_operator_component.py @@ -63,6 +63,7 @@ class MultiInputNonlinearLogicalOperator(Component): sage: print(component3.description) # 6 total bits / output_bit_size 2 = 3 operands ['AND', 3] """ + def __init__( self, current_round_number, @@ -492,10 +493,10 @@ def sat_bitwise_deterministic_truncated_xor_differential_constraints(self): out_ids_0, out_ids_1 = self._generate_output_double_ids() constraints = [] for i in range(self.output_bit_size): - constraints.extend([f"{out_ids_0[i]} -{in_id}" for in_id in in_ids_0[i::self.output_bit_size]]) - constraints.extend([f"{out_ids_0[i]} -{in_id}" for in_id in in_ids_1[i::self.output_bit_size]]) + constraints.extend([f"{out_ids_0[i]} -{in_id}" for in_id in in_ids_0[i :: self.output_bit_size]]) + constraints.extend([f"{out_ids_0[i]} -{in_id}" for in_id in in_ids_1[i :: self.output_bit_size]]) constraints.append(f"{out_ids_0[i]} -{out_ids_1[i]}") - clause = f"{' '.join(in_ids_0[i::self.output_bit_size])} {' '.join(in_ids_1[i::self.output_bit_size])} -{out_ids_0[i]}" + clause = f"{' '.join(in_ids_0[i :: self.output_bit_size])} {' '.join(in_ids_1[i :: self.output_bit_size])} -{out_ids_0[i]}" constraints.append(clause) return out_ids_0 + out_ids_1, constraints @@ -520,8 +521,8 @@ def sat_xor_differential_propagation_constraints(self, model=None): (['and_0_0_0', 'and_0_0_1', 'hw_and_0_0_0', 'hw_and_0_0_1'],) """ input_bit_ids = self._generate_input_ids() - lhs_input_bit_ids = input_bit_ids[:self.output_bit_size] - rhs_input_bit_ids = input_bit_ids[self.output_bit_size:] + lhs_input_bit_ids = input_bit_ids[: self.output_bit_size] + rhs_input_bit_ids = input_bit_ids[self.output_bit_size :] output_bit_ids = self._generate_output_ids() hw_bit_ids = [f"hw_{output_bit_id}" for output_bit_id in output_bit_ids] constraints = [] @@ -550,8 +551,8 @@ def sat_xor_linear_mask_propagation_constraints(self, model=None): (['and_0_0_0_i', 'and_0_0_1_i', 'and_0_0_2_i', 'and_0_0_3_i', 'and_0_0_0_o', 'and_0_0_1_o', 'hw_and_0_0_0_o', 'hw_and_0_0_1_o'],) """ input_bit_ids = self._generate_component_input_ids() - lhs_input_bit_ids = input_bit_ids[:self.output_bit_size] - rhs_input_bit_ids = input_bit_ids[self.output_bit_size:] + lhs_input_bit_ids = input_bit_ids[: self.output_bit_size] + rhs_input_bit_ids = input_bit_ids[self.output_bit_size :] output_bit_ids = self._generate_output_ids(suffix=constants.OUTPUT_BIT_ID_SUFFIX) hw_bit_ids = [f"hw_{output_bit_id}" for output_bit_id in output_bit_ids] constraints = [] @@ -586,8 +587,8 @@ def smt_xor_differential_propagation_constraints(self, model=None): (['and_0_0_0', 'and_0_0_1', 'hw_and_0_0_0', 'hw_and_0_0_1'],) """ input_bit_ids = self._generate_input_ids() - lhs_input_bit_ids = input_bit_ids[:self.output_bit_size] - rhs_input_bit_ids = input_bit_ids[self.output_bit_size:] + lhs_input_bit_ids = input_bit_ids[: self.output_bit_size] + rhs_input_bit_ids = input_bit_ids[self.output_bit_size :] output_bit_ids = self._generate_output_ids() hw_bit_ids = [f"hw_{output_bit_id}" for output_bit_id in output_bit_ids] constraints = [] @@ -626,8 +627,8 @@ def smt_xor_linear_mask_propagation_constraints(self, model=None): (['and_0_0_0_i', 'and_0_0_1_i', 'and_0_0_2_i', 'and_0_0_3_i', 'and_0_0_0_o', 'and_0_0_1_o', 'hw_and_0_0_0_o', 'hw_and_0_0_1_o'],) """ input_bit_ids = self._generate_component_input_ids() - lhs_input_bit_ids = input_bit_ids[:self.output_bit_size] - rhs_input_bit_ids = input_bit_ids[self.output_bit_size:] + lhs_input_bit_ids = input_bit_ids[: self.output_bit_size] + rhs_input_bit_ids = input_bit_ids[self.output_bit_size :] output_bit_ids = self._generate_output_ids(suffix=constants.OUTPUT_BIT_ID_SUFFIX) hw_bit_ids = [f"hw_{output_bit_id}" for output_bit_id in output_bit_ids] constraints = [] @@ -647,3 +648,143 @@ def smt_xor_linear_mask_propagation_constraints(self, model=None): constraints.append(smt_utils.smt_assert(sop)) return input_bit_ids + output_bit_ids + hw_bit_ids, constraints + + def smt_xor_quasidifferential_propagation_constraints( + self, + model, + ): + """ + Return SMT constraints for quasidifferential propagation of a + bitwise nonlinear logical operator (AND, OR). + + AND is covered by Theorem 5.1 of Beyne & Rijmen. OR is AND + conjugated by complementation (``x1 | x2 = ~(~x1 & ~x2)``), and + since complementation leaves XOR differences unchanged, OR's + validity conditions and the ABSOLUTE VALUES of its QDT + coefficients -- hence its WEIGHT -- are IDENTICAL to AND's. + The two operations therefore share these constraints verbatim. + + Only the SIGN differs, by the translation factors of Theorem + 3.2 (4): per bit a factor ``(-1)^(u + v + w)`` for OR. The sign + is not encoded here -- it never affects the weight-based search + -- but applied in post-processing by + ``SmtXorQuasidifferentialModel.compute_trail_sign``, which + dispatches on the operation. + + This was established by exhaustive brute force of Equation (4) + on the 1-bit case (all 64 combinations: same validity, same + absolute value, sign ratio exactly ``(-1)^(u+v+w)``), and + cross-checked at word level over 200000 random 4-bit vectors + (8403 valid transitions, 0 mismatches). + + Only 2 operands are supported: Theorem 5.1 is stated for a + single pairwise operation, so an n > 2 version would need its + own derivation. This raises ``NotImplementedError`` rather than + guessing; ``build_xor_quasidifferential_trail_model`` catches + that and skips the component with a clear message. + + Per bit i (``a_i``, ``b_i`` -> ``c_i``; masks ``u_i``, ``v_i`` + on the inputs and ``w_i`` on the output): + + c_i => (a_i or b_i) + (u_i or v_i) => (a_i or b_i or w_i) + (a_i and u_i) xor (b_i and v_i) == (c_i and w_i) + + with local weight ``(a_i or b_i or w_i)``: Theorem 5.1's + ``wt(a|b) + wt(w & ~a & ~b)`` reduces to this single per-bit OR, + the two terms being mutually exclusive at each bit position. + + INPUT: + + - ``model`` -- **model object**; a model instance + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.and_cipher import AndCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = AndCipher(word_bit_size=2, number_of_inputs=2) + sage: and_component = cipher.component_from_id('and_0_0') + sage: variables, constraints = and_component.smt_xor_quasidifferential_propagation_constraints(SmtXorQuasidifferentialModel(cipher)) + sage: variables + ['and_0_0_0', 'and_0_0_1', 'qdt_and_0_0_0', 'qdt_and_0_0_1', 'hw_qdt_and_0_0_0', 'hw_qdt_and_0_0_1'] + sage: len(constraints) + 8 + sage: constraints[0] + '(assert (=> and_0_0_0 (or plaintext_0 key_0)))' + sage: constraints[3] + '(assert (= hw_qdt_and_0_0_0 (or plaintext_0 key_0 qdt_and_0_0_0)))' + + OR inherits this method unchanged: same constraints, and only the sign, + applied by the model after solving, differs. + """ + + num_operands = self.description[1] + + if num_operands != 2: + raise NotImplementedError( + f"{self.id}: quasidifferential propagation for " + f"{self.description[0]} is only implemented for 2 operands " + f"(Theorem 5.1 of Beyne & Rijmen); got {num_operands}." + ) + + word_size = self.output_bit_size + + input_bit_ids = self._generate_input_ids() + output_bit_ids = self._generate_output_ids() + + qdt_input_bit_ids = model._qdt_input_bit_ids(self) + qdt_output_bit_ids = [f"qdt_{bit_id}" for bit_id in output_bit_ids] + + a_ids = input_bit_ids[:word_size] + b_ids = input_bit_ids[word_size:] + c_ids = output_bit_ids + + u_ids = qdt_input_bit_ids[:word_size] + v_ids = qdt_input_bit_ids[word_size:] + w_ids = qdt_output_bit_ids + + weight_bit_ids = [f"hw_qdt_{self.id}_{i}" for i in range(word_size)] + + constraints = [] + + for i in range(word_size): + + a, b, c = a_ids[i], b_ids[i], c_ids[i] + u, v, w = u_ids[i], v_ids[i], w_ids[i] + + validity_1 = smt_utils.smt_implies(c, smt_utils.smt_or([a, b])) + constraints.append(smt_utils.smt_assert(validity_1)) + + validity_2 = smt_utils.smt_implies( + smt_utils.smt_or([u, v]), + smt_utils.smt_or([a, b, w]), + ) + constraints.append(smt_utils.smt_assert(validity_2)) + + validity_3 = smt_utils.smt_equivalent( + [ + smt_utils.smt_xor( + [ + smt_utils.smt_and([a, u]), + smt_utils.smt_and([b, v]), + ] + ), + smt_utils.smt_and([c, w]), + ] + ) + constraints.append(smt_utils.smt_assert(validity_3)) + + weight_definition = smt_utils.smt_equivalent( + [ + weight_bit_ids[i], + smt_utils.smt_or([a, b, w]), + ] + ) + constraints.append(smt_utils.smt_assert(weight_definition)) + + variables = output_bit_ids + qdt_output_bit_ids + weight_bit_ids + + return ( + variables, + constraints, + ) diff --git a/claasp/components/not_component.py b/claasp/components/not_component.py index 6a7d388a0..7181b52dc 100644 --- a/claasp/components/not_component.py +++ b/claasp/components/not_component.py @@ -48,6 +48,7 @@ class Not(Component): sage: print(component.description) ['NOT', 0] """ + def __init__( self, current_round_number, @@ -717,3 +718,49 @@ def smt_xor_linear_mask_propagation_constraints(self, model=None): ] result = input_bit_ids + output_bit_ids, constraints return result + + def smt_xor_quasidifferential_propagation_constraints( + self, + model, + ): + """ + Return SMT constraints for NOT quasidifferential propagation. + + NOT is an AFFINE map (x -> x xor 1), not a linear one. Per + Beyne & Rijmen, Theorem 3.2 (4), a translation by a constant t + propagates both differences and masks UNCHANGED, and + contributes only a SIGN factor chi_v(t) = (-1)^(v . t) -- here + t is the all-ones word, so the factor is (-1)^popcount(v). + + The sign is deliberately NOT encoded as an SMT constraint: it + never affects the weight (which is 0 for an affine map), so + constraining it would only slow the search down. It is applied + afterwards by + SmtXorQuasidifferentialModel.compute_trail_sign, exactly as + done for the Constant component. Note that + Not.generic_sign_linear_constraints in this same file computes + the very same parity for the ordinary linear model. + + INPUT: + + - ``model`` -- **model object**; a model instance + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.not_cipher import NotCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = NotCipher(bit_size=2) + sage: not_component = cipher.component_from(0, 0) + sage: smt = SmtXorQuasidifferentialModel(cipher) + sage: variables, constraints = not_component.smt_xor_quasidifferential_propagation_constraints(smt) + sage: len(variables) + 4 + sage: len(constraints) + 4 + """ + + # Theorem 3.2 (4): a translation leaves differences and masks + # unchanged. Its sign factor is applied by compute_trail_sign. + return model._bit_moving_propagation_constraints( + self, [(position, position) for position in range(self.output_bit_size)] + ) diff --git a/claasp/components/or_component.py b/claasp/components/or_component.py index 73a3c60a8..6107b3273 100644 --- a/claasp/components/or_component.py +++ b/claasp/components/or_component.py @@ -55,6 +55,7 @@ class Or(MultiInputNonlinearLogicalOperator): sage: print(component3.description) # 6 total bits / output_bit_size 2 = 3 operands ['OR', 3] """ + def __init__( self, current_round_number, @@ -299,7 +300,7 @@ def sat_constraints(self): output_bit_ids = self._generate_output_ids() constraints = [] for i, output_bit_id in enumerate(output_bit_ids): - constraints.extend(sat_utils.cnf_or(output_bit_id, input_bit_ids[i::self.output_bit_size])) + constraints.extend(sat_utils.cnf_or(output_bit_id, input_bit_ids[i :: self.output_bit_size])) return output_bit_ids, constraints @@ -328,7 +329,7 @@ def smt_constraints(self): output_bit_ids = self._generate_output_ids() constraints = [] for i, output_bit_id in enumerate(output_bit_ids): - operation = smt_utils.smt_or(input_bit_ids[i::self.output_bit_size]) + operation = smt_utils.smt_or(input_bit_ids[i :: self.output_bit_size]) equation = smt_utils.smt_equivalent((output_bit_id, operation)) constraints.append(smt_utils.smt_assert(equation)) diff --git a/claasp/components/permutation_component.py b/claasp/components/permutation_component.py index b15236eb3..17c79410e 100644 --- a/claasp/components/permutation_component.py +++ b/claasp/components/permutation_component.py @@ -70,6 +70,7 @@ class Permutation(Component): sage: print(component.description) [[1, 0], 4] """ + def __init__( self, current_round_number, @@ -91,9 +92,7 @@ def __init__( # Validate that output_bit_size is divisible by word_size if output_bit_size % word_size != 0: - raise ValueError( - f"output_bit_size ({output_bit_size}) must be divisible by word_size ({word_size})" - ) + raise ValueError(f"output_bit_size ({output_bit_size}) must be divisible by word_size ({word_size})") # Validate permutation_description length expected_perm_len = output_bit_size // word_size @@ -110,7 +109,9 @@ def __init__( if perm_set != valid_range: missing = valid_range - perm_set duplicates = [x for x in permutation_description if permutation_description.count(x) > 1] - out_of_range = [x for x in permutation_description if not isinstance(x, int) or x < 0 or x >= expected_perm_len] + out_of_range = [ + x for x in permutation_description if not isinstance(x, int) or x < 0 or x >= expected_perm_len + ] error_parts = [] if out_of_range: @@ -388,6 +389,54 @@ def smt_xor_linear_mask_propagation_constraints(self, model=None): return input_bit_ids + output_bit_ids, constraints + def smt_xor_quasidifferential_propagation_constraints( + self, + model, + ): + """ + Return SMT constraints for PERMUTATION quasidifferential propagation. + + A permutation matrix is orthogonal (P^{-1} = P^T), so by Theorem + 3.2 (5) of Beyne & Rijmen, both the difference and the mask + propagate through the SAME bit permutation: + + b = P(a) (ordinary differential propagation) + u = P^T(v) = P^{-1}(v) = P(u) <=> v = P(u) (mask, self-dual) + + This is exactly the "self-duality of bit-permutations" property + discussed in Section 4.3 of the paper (and directly visible in + this component's own ``smt_xor_linear_mask_propagation_constraints``, + where ``output_mask[i] = input_mask[bit_perm[i]]`` -- the same + ``bit_perm`` used for the ordinary difference). + + INPUT: + + - ``model`` -- **model object**; a ``SmtXorQuasidifferentialModel`` instance + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.permutation_cipher import PermutationCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = PermutationCipher(bit_size=4, permutation_description=[3, 0, 2, 1]) + sage: permutation = cipher.component_from_id('permutation_0_0') + sage: variables, constraints = permutation.smt_xor_quasidifferential_propagation_constraints(SmtXorQuasidifferentialModel(cipher)) + sage: constraints + ['(assert (= permutation_0_0_0 plaintext_1))', + '(assert (= permutation_0_0_1 plaintext_3))', + '(assert (= permutation_0_0_2 plaintext_2))', + '(assert (= permutation_0_0_3 plaintext_0))', + '(assert (= qdt_permutation_0_0_0 qdt_plaintext_1))', + '(assert (= qdt_permutation_0_0_1 qdt_plaintext_3))', + '(assert (= qdt_permutation_0_0_2 qdt_plaintext_2))', + '(assert (= qdt_permutation_0_0_3 qdt_plaintext_0))'] + """ + + # Self-dual: the mask goes through the same bit permutation as + # the difference. + return model._bit_moving_propagation_constraints( + self, list(zip(range(self.output_bit_size), self._bit_perm())) + ) + def cp_constraints(self): """ Return lists of declarations and constraints for PERMUTATION component for CP CIPHER model. @@ -416,8 +465,7 @@ def cp_constraints(self): bit_perm = self._bit_perm() cp_declarations = [] cp_constraints = [ - f"constraint {self.id}[{i}] = {all_inputs[bit_perm[i]]};" - for i in range(self.output_bit_size) + f"constraint {self.id}[{i}] = {all_inputs[bit_perm[i]]};" for i in range(self.output_bit_size) ] return cp_declarations, cp_constraints @@ -514,10 +562,12 @@ def cp_wordwise_deterministic_truncated_xor_differential_constraints(self, model all_inputs_active = [] for id_link, bit_positions in zip(self.input_id_links, self.input_bit_positions): - all_inputs_active.extend([ - f"{id_link}_active[{bit_positions[j * word_size] // word_size}]" - for j in range(len(bit_positions) // word_size) - ]) + all_inputs_active.extend( + [ + f"{id_link}_active[{bit_positions[j * word_size] // word_size}]" + for j in range(len(bit_positions) // word_size) + ] + ) bit_perm = self._bit_perm() cp_constraints = [] @@ -576,20 +626,21 @@ def cp_xor_differential_propagation_first_step_constraints(self, model): all_inputs = [] for id_link, bit_positions in zip(self.input_id_links, self.input_bit_positions): - all_inputs.extend([ - f"{id_link}[{bit_positions[j * model_word_size] // model_word_size}]" - for j in range(len(bit_positions) // model_word_size) - ]) + all_inputs.extend( + [ + f"{id_link}[{bit_positions[j * model_word_size] // model_word_size}]" + for j in range(len(bit_positions) // model_word_size) + ] + ) cp_declarations = [f"array[0..{output_num_words - 1}] of var 0..1: {output_id};"] bit_perm = self._bit_perm() cp_constraints = [] for j in range(output_num_words): - contributing = sorted({ - bit_perm[j * model_word_size + off] // model_word_size - for off in range(model_word_size) - }) + contributing = sorted( + {bit_perm[j * model_word_size + off] // model_word_size for off in range(model_word_size)} + ) contributing_refs = [all_inputs[k] for k in contributing] if len(contributing_refs) == 1: cp_constraints.append(f"constraint {output_id}[{j}] = {contributing_refs[0]};") @@ -626,8 +677,7 @@ def cp_xor_linear_mask_propagation_constraints(self, model=None): ] bit_perm = self._bit_perm() cp_constraints = [ - f"constraint {self.id}_o[{i}]={self.id}_i[{bit_perm[i]}];" - for i in range(self.output_bit_size) + f"constraint {self.id}_o[{i}]={self.id}_i[{bit_perm[i]}];" for i in range(self.output_bit_size) ] return cp_declarations, cp_constraints @@ -668,8 +718,7 @@ def milp_constraints(self, model): variables = [(f"x[{var}]", x[var]) for var in input_vars + output_vars] bit_perm = self._bit_perm() input_vars_permuted = [input_vars[bit_perm[i]] for i in range(len(output_vars))] - constraints = [x[output_var] == x[input_var] - for output_var, input_var in zip(output_vars, input_vars_permuted)] + constraints = [x[output_var] == x[input_var] for output_var, input_var in zip(output_vars, input_vars_permuted)] return variables, constraints @@ -724,8 +773,7 @@ def milp_bitwise_deterministic_truncated_xor_differential_constraints(self, mode bit_perm = self._bit_perm() constraints = [ - x_class[output_var] == x_class[input_vars[bit_perm[i]]] - for i, output_var in enumerate(output_vars) + x_class[output_var] == x_class[input_vars[bit_perm[i]]] for i, output_var in enumerate(output_vars) ] return variables, constraints @@ -791,16 +839,10 @@ def milp_wordwise_deterministic_truncated_xor_differential_constraints(self, mod model_word_size = model.word_size if self.input_bit_size % model_word_size != 0 or self.output_bit_size % model_word_size != 0: - raise ValueError( - f"{self.id}: input/output size must be divisible by model.word_size={model_word_size}" - ) + raise ValueError(f"{self.id}: input/output size must be divisible by model.word_size={model_word_size}") input_tuples, output_tuples = self._get_wordwise_input_output_full_tuples(model) - variables = [ - (f"x[{var}]", x[var]) - for word_tuple in input_tuples + output_tuples - for var in word_tuple - ] + variables = [(f"x[{var}]", x[var]) for word_tuple in input_tuples + output_tuples for var in word_tuple] constraints = [] bit_perm = self._bit_perm() diff --git a/claasp/components/reverse_component.py b/claasp/components/reverse_component.py index b05b45c5d..1893c6020 100644 --- a/claasp/components/reverse_component.py +++ b/claasp/components/reverse_component.py @@ -43,6 +43,7 @@ class Reverse(LinearLayer): sage: print(component.input_bit_size) 4 """ + def __init__( self, current_round_number, diff --git a/claasp/components/rotate_component.py b/claasp/components/rotate_component.py index bf87b922c..50ce5d819 100644 --- a/claasp/components/rotate_component.py +++ b/claasp/components/rotate_component.py @@ -49,6 +49,7 @@ class Rotate(Component): sage: print(component.description) ['ROTATE', -1] """ + def __init__( self, current_round_number, @@ -165,7 +166,6 @@ def cp_constraints(self): return cp_declarations, cp_constraints def cp_continuous_differential_propagation_constraints(self, model): - output_id_link = self.id input_len = self.output_bit_size rot_val = self.description[1] @@ -173,12 +173,8 @@ def cp_continuous_differential_propagation_constraints(self, model): cp_declarations = [] cp_constraints = [] - cp_declarations.append( - f"array[0..{input_len - 1}] of var -1.0..1.0: x1_{output_id_link};" - ) - cp_declarations.append( - f"array[0..{input_len - 1}] of var -1.0..1.0: {output_id_link};" - ) + cp_declarations.append(f"array[0..{input_len - 1}] of var -1.0..1.0: x1_{output_id_link};") + cp_declarations.append(f"array[0..{input_len - 1}] of var -1.0..1.0: {output_id_link};") if rot_val > 0: cp_constraints.append( @@ -190,7 +186,7 @@ def cp_continuous_differential_propagation_constraints(self, model): ) return cp_declarations, cp_constraints - + def cp_deterministic_truncated_xor_differential_trail_constraints(self): return self.cp_constraints() @@ -840,3 +836,49 @@ def smt_xor_linear_mask_propagation_constraints(self, model=None): constraints.append(smt_utils.smt_assert(equation)) return input_bit_ids + output_bit_ids, constraints + + def smt_xor_quasidifferential_propagation_constraints( + self, + model, + ): + """ + Return SMT constraints for ROTATE quasidifferential propagation. + + A bit rotation is a permutation matrix, hence orthogonal and + self-dual (P^{-1} = P^T): per Beyne & Rijmen, Theorem 3.2 (5) + and Section 4.3, mask and difference propagate through the + SAME rotation. This mirrors + Permutation.smt_xor_quasidifferential_propagation_constraints, + and is exactly what rectangle.py's own permute_bits() does + (applying the same bit permutation to both differences and + masks) for RECTANGLE's row rotations. + + INPUT: + + - ``model`` -- **model object**; a model instance + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.rotate_cipher import RotateCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = RotateCipher(bit_size=2, rotation_amount=1) + sage: rotate_component = cipher.component_from_id('rot_0_0') + sage: smt = SmtXorQuasidifferentialModel(cipher) + sage: variables, constraints = rotate_component.smt_xor_quasidifferential_propagation_constraints(smt) + sage: variables + ['rot_0_0_0', 'rot_0_0_1', 'qdt_rot_0_0_0', 'qdt_rot_0_0_1'] + sage: constraints + ['(assert (= rot_0_0_0 plaintext_1))', + '(assert (= rot_0_0_1 plaintext_0))', + '(assert (= qdt_rot_0_0_0 qdt_plaintext_1))', + '(assert (= qdt_rot_0_0_1 qdt_plaintext_0))'] + """ + + # A rotation is a bit permutation, so the mask goes through the + # same rotation as the difference. + rotation = self.description[1] + positions = list(range(self.input_bit_size)) + + return model._bit_moving_propagation_constraints( + self, list(zip(range(self.output_bit_size), positions[-rotation:] + positions[:-rotation])) + ) diff --git a/claasp/components/sbox_component.py b/claasp/components/sbox_component.py index 7420aa664..795be408a 100644 --- a/claasp/components/sbox_component.py +++ b/claasp/components/sbox_component.py @@ -23,7 +23,12 @@ from sage.arith.misc import is_power_of_two from sage.crypto.sbox import SBox - +from claasp.cipher_modules.models.smt.utils import utils +from claasp.cipher_modules.models.smt.utils.utils import ( + deinterleave_qdt_matrix, + generate_weight_tables, + quasidifferential_transition_matrix, +) from claasp.cipher_modules.models.milp.utils import utils as milp_utils from claasp.cipher_modules.models.milp.utils.generate_inequalities_for_large_sboxes import ( get_dictionary_that_contains_inequalities_for_large_sboxes, @@ -41,6 +46,9 @@ from claasp.cipher_modules.models.milp.utils.utils import espresso_pos_to_constraints from claasp.cipher_modules.models.sat.utils import constants from claasp.cipher_modules.models.smt.utils import utils as smt_utils +from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import ( + SmtXorQuasidifferentialModel, +) from claasp.component import Component, free_input from claasp.input import Input @@ -595,6 +603,7 @@ class Sbox(Component): **Benefit**: Reduces constraint bloat in models with repeated S-box instances and improves solver performance. """ + sboxes_ddt_templates = {} sboxes_lat_templates = {} @@ -2250,7 +2259,9 @@ def sat_xor_differential_propagation_constraints(self, model=None): check_table_feasibility(ddt, "DDT", "SAT") get_hamming_weight_function = lambda input_bit_len, entry: input_bit_len - int(math.log2(entry)) - template = sat_build_table_template(ddt, get_hamming_weight_function, self.input_bit_size, self.output_bit_size) + template = sat_build_table_template( + ddt, get_hamming_weight_function, self.input_bit_size, self.output_bit_size + ) self.sboxes_ddt_templates[f"{sbox_values}"] = template bit_ids = input_bit_ids + output_bit_ids + hw_bit_ids @@ -2321,7 +2332,9 @@ def sat_xor_linear_mask_propagation_constraints(self, model=None): check_table_feasibility(lat, "LAT", "SAT") get_hamming_weight_function = lambda input_bit_len, entry: input_bit_len - int(math.log2(abs(entry))) - 1 - template = sat_build_table_template(lat, get_hamming_weight_function, self.input_bit_size, self.output_bit_size) + template = sat_build_table_template( + lat, get_hamming_weight_function, self.input_bit_size, self.output_bit_size + ) self.sboxes_lat_templates[f"{sbox_values}"] = template bit_ids = input_bit_ids + output_bit_ids + hw_bit_ids @@ -2437,7 +2450,9 @@ def smt_xor_differential_propagation_constraints(self, model): check_table_feasibility(ddt, "DDT", "SMT") get_hamming_weight_function = lambda input_bit_len, entry: input_bit_len - int(math.log2(entry)) - template = smt_build_table_template(ddt, get_hamming_weight_function, self.input_bit_size, self.output_bit_size) + template = smt_build_table_template( + ddt, get_hamming_weight_function, self.input_bit_size, self.output_bit_size + ) sboxes_ddt_templates[f"{sbox_values}"] = template bit_ids = input_bit_ids + output_bit_ids + hw_bit_ids @@ -2492,7 +2507,9 @@ def smt_xor_linear_mask_propagation_constraints(self, model): check_table_feasibility(lat, "LAT", "SMT") get_hamming_weight_function = lambda input_bit_len, entry: input_bit_len - int(math.log2(abs(entry))) - 1 - template = smt_build_table_template(lat, get_hamming_weight_function, self.input_bit_size, self.output_bit_size) + template = smt_build_table_template( + lat, get_hamming_weight_function, self.input_bit_size, self.output_bit_size + ) sboxes_lat_templates[f"{sbox_values}"] = template bit_ids = input_bit_ids + output_bit_ids + hw_bit_ids @@ -2500,3 +2517,158 @@ def smt_xor_linear_mask_propagation_constraints(self, model): constraints = smt_get_sbox_probability_constraints(bit_ids, template) return bit_ids, constraints + + def smt_xor_quasidifferential_propagation_constraints(self, model): + """ + Return a variable list and SMT-LIB asserts representing the S-BOX + for the SMT XOR quasidifferential model. + + A QDT transition is represented as: + + (a, u) -> (b, v) + + where: + + a = input XOR difference + u = input quasidifferential mask + b = output XOR difference + v = output quasidifferential mask + + A transition is allowed if the corresponding QDT coefficient is + non-zero. + + INPUT: + + - ``model`` -- **model object**; a ``SmtXorQuasidifferentialModel`` instance + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.sbox_cipher import SboxCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = SboxCipher(bit_size=2, lookup_table=[0, 1, 3, 2]) + sage: sbox = cipher.component_from_id('sbox_0_0') + sage: variables, constraints = sbox.smt_xor_quasidifferential_propagation_constraints(SmtXorQuasidifferentialModel(cipher)) + sage: variables + ['sbox_0_0_0', 'sbox_0_0_1', 'qdt_sbox_0_0_0', 'qdt_sbox_0_0_1'] + sage: len(constraints), constraints[0].startswith('(assert (or') + (1, True) + + ``[0, 1, 3, 2]`` is linear, so every admissible transition has weight 0 + and the S-box needs no weight indicator. + """ + + input_diff_bit_ids = self._generate_input_ids() + output_diff_bit_ids = self._generate_output_ids() + + input_qdt_bit_ids = model._qdt_input_bit_ids(self) + + output_qdt_bit_ids = [f"qdt_{output_bit_id}" for output_bit_id in output_diff_bit_ids] + + sbox_values = self.description + cache_key = str(sbox_values) + + if cache_key not in model.sboxes_qdt_templates: + + def sbox_function(x): + return sbox_values[x] + + qdt = quasidifferential_transition_matrix( + sbox_function, + self.input_bit_size, + self.output_bit_size, + ) + + qdt = deinterleave_qdt_matrix( + qdt, + self.input_bit_size, + self.output_bit_size, + primary="diff", + ) + + weights = generate_weight_tables( + qdt, + self.input_bit_size, + self.output_bit_size, + ) + + transitions = SmtXorQuasidifferentialModel.get_qdt_transitions(weights) + + model.sboxes_qdt_templates[cache_key] = transitions + # Cache the deinterleaved QDT matrix itself too (not just the + # weight-grouped transitions, which discard the coefficient's + # sign): needed for post-processing sign computation on an + # already-solved trail (see + # SmtXorQuasidifferentialModel.compute_trail_sign). + model.sboxes_qdt_matrices[cache_key] = qdt + + transitions = model.sboxes_qdt_templates[cache_key] + + # Keep only the transitions that agree with this S-box's fixed input and + # output difference, when the characteristic decides them. The others + # cannot happen, so writing them out would only make the model bigger. + # An S-box the characteristic leaves undecided keeps its whole table. + if self.id in model.sbox_differences: + a_fixed, b_fixed = model.sbox_differences[self.id] + transitions = [ + transition + for transition in transitions + if transition["a"] == a_fixed and transition["b"] == b_fixed + ] + if not transitions: + raise ValueError( + f"{self.id}: the differential " + f"{a_fixed:#x} -> {b_fixed:#x} has no quasidifferential " + f"transition, so the characteristic is impossible" + ) + + max_weight = max(transition["weight"] for transition in transitions) + weight_bit_ids = model._qdt_local_weight_variables(self, max_weight) + + transition_formulae = [] + + for transition in transitions: + literals = [] + + # Input XOR difference = a + literals.extend( + model._value_literals( + input_diff_bit_ids, + transition["a"], + ) + ) + + literals.extend( + model._value_literals( + input_qdt_bit_ids, + transition["u"], + ) + ) + + literals.extend( + model._value_literals( + output_diff_bit_ids, + transition["b"], + ) + ) + + literals.extend( + model._value_literals( + output_qdt_bit_ids, + transition["v"], + ) + ) + + literals.extend( + model._qdt_weight_constraints( + weight_bit_ids, + transition["weight"], + ) + ) + + transition_formulae.append(utils.smt_and(literals)) + + constraints = [utils.smt_assert(utils.smt_or(transition_formulae))] + + variables = output_diff_bit_ids + output_qdt_bit_ids + weight_bit_ids + + return variables, constraints diff --git a/claasp/components/shift_component.py b/claasp/components/shift_component.py index c3d74f56d..896ffd776 100644 --- a/claasp/components/shift_component.py +++ b/claasp/components/shift_component.py @@ -49,6 +49,7 @@ class Shift(Component): sage: print(component.description) ['SHIFT', -1] """ + def __init__( self, current_round_number, @@ -711,7 +712,7 @@ def sat_constraints(self): shift_amount = -shift_amount for output_bit_id, input_bit_id in zip(output_bit_ids, input_bit_ids[shift_amount:]): constraints.extend(sat_utils.cnf_equivalent([output_bit_id, input_bit_id])) - for output_bit_id in output_bit_ids[self.output_bit_size - shift_amount:]: + for output_bit_id in output_bit_ids[self.output_bit_size - shift_amount :]: constraints.append(f"-{output_bit_id}") else: for output_bit_id in output_bit_ids[:shift_amount]: @@ -857,7 +858,7 @@ def smt_constraints(self): for output_bit_id, input_bit_id in zip(output_bit_ids, input_bit_ids[shift_amount:]): equation = smt_utils.smt_equivalent((output_bit_id, input_bit_id)) constraints.append(smt_utils.smt_assert(equation)) - for output_bit_id in output_bit_ids[self.output_bit_size - shift_amount:]: + for output_bit_id in output_bit_ids[self.output_bit_size - shift_amount :]: constraints.append(smt_utils.smt_assert(smt_utils.smt_not(output_bit_id))) else: for output_bit_id in output_bit_ids[:shift_amount]: @@ -930,3 +931,57 @@ def smt_xor_linear_mask_propagation_constraints(self, model=None): constraints.append(smt_utils.smt_assert(smt_utils.smt_not(input_bit_id))) return input_bit_ids + output_bit_ids, constraints + + def smt_xor_quasidifferential_propagation_constraints( + self, + model, + ): + """ + Return SMT constraints for SHIFT quasidifferential propagation. + + SHIFT is linear but, unlike Rotate, NOT invertible: it discards + the bits shifted out. Per Beyne & Rijmen, Theorem 3.2 (5), a + linear map L propagates differences forwards (b = L(a)) and + masks backwards through its TRANSPOSE (u = L^T(v)). The + transpose of a shift is the shift in the OPPOSITE direction, + and the mask bits corresponding to positions that the shift + discards are forced to zero -- which is precisely the structure + already encoded by this class's own + smt_xor_linear_mask_propagation_constraints, reused here with + the qdt_-prefixed variable names of the quasidifferential + model. + + Weight is 0: linear maps have a delta-function correlation and + contribute no weight loss. + + INPUT: + + - ``model`` -- **model object**; a model instance + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.shift_cipher import ShiftCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = ShiftCipher(bit_size=2, shift_amount=1) + sage: shift_component = cipher.component_from_id('shift_0_0') + sage: smt = SmtXorQuasidifferentialModel(cipher) + sage: variables, constraints = shift_component.smt_xor_quasidifferential_propagation_constraints(smt) + sage: len(variables) + 4 + """ + + # The transpose of a shift is the shift the other way, and the + # bits the shift discards carry a zero mask. + shift_amount = self.description[1] + inputs = list(range(self.input_bit_size)) + outputs = list(range(self.output_bit_size)) + + if shift_amount < 0: + shift_amount = -shift_amount + mask_pairs = [(None, position) for position in inputs[:shift_amount]] + mask_pairs += list(zip(outputs[:-shift_amount], inputs[shift_amount:])) + else: + mask_pairs = list(zip(outputs[shift_amount:], inputs[:-shift_amount])) + mask_pairs += [(None, position) for position in inputs[-shift_amount:]] + + return model._bit_moving_propagation_constraints(self, mask_pairs) diff --git a/claasp/components/shift_rows_component.py b/claasp/components/shift_rows_component.py index bdba5a02c..bc449a0f0 100644 --- a/claasp/components/shift_rows_component.py +++ b/claasp/components/shift_rows_component.py @@ -45,6 +45,7 @@ class ShiftRows(Rotate): sage: print(component.description) ['ROTATE', 2] """ + def __init__( self, current_round_number, diff --git a/claasp/components/sigma_component.py b/claasp/components/sigma_component.py index 38d378f41..584c23760 100644 --- a/claasp/components/sigma_component.py +++ b/claasp/components/sigma_component.py @@ -47,6 +47,7 @@ class Sigma(LinearLayer): sage: print(component.input_bit_size) 4 """ + def __init__( self, current_round_number, diff --git a/claasp/components/theta_gaston_component.py b/claasp/components/theta_gaston_component.py index 2e6cb51c6..2b8f766fa 100644 --- a/claasp/components/theta_gaston_component.py +++ b/claasp/components/theta_gaston_component.py @@ -63,6 +63,7 @@ class ThetaGaston(LinearLayer): sage: print(component.input_bit_size) 320 """ + def __init__( self, current_round_number, diff --git a/claasp/components/theta_keccak_component.py b/claasp/components/theta_keccak_component.py index 783e9869a..614f40de1 100644 --- a/claasp/components/theta_keccak_component.py +++ b/claasp/components/theta_keccak_component.py @@ -46,6 +46,7 @@ class ThetaKeccak(LinearLayer): sage: print(component.input_bit_size) 25 """ + def __init__( self, current_round_number, diff --git a/claasp/components/theta_xoodoo_component.py b/claasp/components/theta_xoodoo_component.py index 217251c0e..c9cdb0843 100644 --- a/claasp/components/theta_xoodoo_component.py +++ b/claasp/components/theta_xoodoo_component.py @@ -46,6 +46,7 @@ class ThetaXoodoo(LinearLayer): sage: print(component.input_bit_size) 384 """ + def __init__( self, current_round_number, diff --git a/claasp/components/variable_rotate_component.py b/claasp/components/variable_rotate_component.py index 27566f5bf..832f3b236 100644 --- a/claasp/components/variable_rotate_component.py +++ b/claasp/components/variable_rotate_component.py @@ -46,6 +46,7 @@ class VariableRotate(Component): sage: print(component.description) ['ROTATE_BY_VARIABLE_AMOUNT', -1] """ + def __init__( self, current_round_number, diff --git a/claasp/components/variable_shift_component.py b/claasp/components/variable_shift_component.py index d3f3f3273..4809a3a63 100644 --- a/claasp/components/variable_shift_component.py +++ b/claasp/components/variable_shift_component.py @@ -50,6 +50,7 @@ class VariableShift(Component): sage: print(component.description) ['SHIFT_BY_VARIABLE_AMOUNT', 1] """ + def __init__( self, current_round_number, @@ -451,11 +452,11 @@ def sat_constraints(self): 'var_shift_0_2_2 -state_0_var_shift_0_2_2 key_2', '-var_shift_0_2_3 state_0_var_shift_0_2_3', '-var_shift_0_2_3 -key_2', - 'var_shift_0_2_3 -state_0_var_shift_0_2_3 key_2'] + 'var_shift_0_2_3 -state_0_var_shift_0_2_3 key_2'] """ input_bit_ids = self._generate_input_ids() - input_ids = input_bit_ids[:self.output_bit_size] - shift_ids = input_bit_ids[self.output_bit_size:] + input_ids = input_bit_ids[: self.output_bit_size] + shift_ids = input_bit_ids[self.output_bit_size :] output_bit_ids = self._generate_output_ids() number_of_states = int(math.log2(self.output_bit_size)) - 1 states = [[f"state_{i}_{output_bit_id}" for output_bit_id in output_bit_ids] for i in range(number_of_states)] @@ -468,22 +469,24 @@ def sat_constraints(self): for i in range(1, number_of_states): # state is a copy if no shift, shifted otherwise for state_id, prev_state_id, shift_state_id in zip( - states[i][:self.output_bit_size - 2**i], states[i - 1], states[i - 1][2**i:] + states[i][: self.output_bit_size - 2**i], states[i - 1], states[i - 1][2**i :] ): constraints.extend(sat_utils.cnf_vshift_id(state_id, prev_state_id, shift_state_id, shift_ids[-1 - i])) # state is a copy if no shift, null otherwise for state_id, prev_state_id in zip( - states[i][self.output_bit_size - 2**i:], states[i - 1][self.output_bit_size - 2**i:] + states[i][self.output_bit_size - 2**i :], states[i - 1][self.output_bit_size - 2**i :] ): constraints.extend(sat_utils.cnf_vshift_false(state_id, prev_state_id, shift_ids[-1 - i])) # MSB straightforward in the output for output_id, prev_state_id, shift_state_id in zip( - output_bit_ids[:-2**number_of_states], states[-1], states[-1][2**number_of_states:] + output_bit_ids[: -(2**number_of_states)], states[-1], states[-1][2**number_of_states :] ): constraints.extend( sat_utils.cnf_vshift_id(output_id, prev_state_id, shift_state_id, shift_ids[-1 - number_of_states]) ) - for output_id, prev_state_id in zip(output_bit_ids[-2**number_of_states:], states[-1][-2**number_of_states:]): + for output_id, prev_state_id in zip( + output_bit_ids[-(2**number_of_states) :], states[-1][-(2**number_of_states) :] + ): constraints.extend(sat_utils.cnf_vshift_false(output_id, prev_state_id, shift_ids[-1 - number_of_states])) return output_bit_ids, constraints @@ -527,8 +530,8 @@ def smt_constraints(self): '(assert (ite key_2 (not var_shift_0_2_3) (= var_shift_0_2_3 state_0_var_shift_0_2_3)))'] """ input_bit_ids = self._generate_input_ids() - input_ids = input_bit_ids[:self.output_bit_size] - shift_ids = input_bit_ids[self.output_bit_size:] + input_ids = input_bit_ids[: self.output_bit_size] + shift_ids = input_bit_ids[self.output_bit_size :] output_bit_ids = self._generate_output_ids() states = [] number_of_states = int(math.log2(self.output_bit_size)) - 1 @@ -549,14 +552,14 @@ def smt_constraints(self): # intermediate shifts for i in range(1, number_of_states): for state_id, prev_state_id, shift_state_id in zip( - states[i][:self.output_bit_size - 2**i], states[i - 1], states[i - 1][2**i:] + states[i][: self.output_bit_size - 2**i], states[i - 1], states[i - 1][2**i :] ): consequent = smt_utils.smt_equivalent((state_id, shift_state_id)) alternative = smt_utils.smt_equivalent((state_id, prev_state_id)) shift = smt_utils.smt_ite(shift_ids[-1 - i], consequent, alternative) constraints.append(smt_utils.smt_assert(shift)) for state_id, prev_state_id in zip( - states[i][self.output_bit_size - 2**i:], states[i - 1][self.output_bit_size - 2**i:] + states[i][self.output_bit_size - 2**i :], states[i - 1][self.output_bit_size - 2**i :] ): consequent = smt_utils.smt_not(state_id) alternative = smt_utils.smt_equivalent((state_id, prev_state_id)) @@ -565,13 +568,15 @@ def smt_constraints(self): # last shift for output_id, prev_state_id, shift_state_id in zip( - output_bit_ids[:-2**number_of_states], states[-1], states[-1][2**number_of_states:] + output_bit_ids[: -(2**number_of_states)], states[-1], states[-1][2**number_of_states :] ): consequent = smt_utils.smt_equivalent((output_id, shift_state_id)) alternative = smt_utils.smt_equivalent((output_id, prev_state_id)) shift = smt_utils.smt_ite(shift_ids[-1 - number_of_states], consequent, alternative) constraints.append(smt_utils.smt_assert(shift)) - for output_id, prev_state_id in zip(output_bit_ids[-2**number_of_states:], states[-1][-2**number_of_states:]): + for output_id, prev_state_id in zip( + output_bit_ids[-(2**number_of_states) :], states[-1][-(2**number_of_states) :] + ): consequent = smt_utils.smt_not(output_id) alternative = smt_utils.smt_equivalent((output_id, prev_state_id)) shift = smt_utils.smt_ite(shift_ids[-1 - number_of_states], consequent, alternative) diff --git a/claasp/components/word_permutation_component.py b/claasp/components/word_permutation_component.py index 413d427b8..187b922c6 100644 --- a/claasp/components/word_permutation_component.py +++ b/claasp/components/word_permutation_component.py @@ -56,6 +56,7 @@ class WordPermutation(Permutation): sage: print(component.description) [[1, 0], 2] """ + def __init__( self, current_round_number, diff --git a/claasp/components/xor_component.py b/claasp/components/xor_component.py index c1c0f0b30..c63de86ed 100644 --- a/claasp/components/xor_component.py +++ b/claasp/components/xor_component.py @@ -1454,6 +1454,117 @@ def smt_xor_linear_mask_propagation_constraints(self, model=None): return bit_ids, constraints + def smt_xor_quasidifferential_propagation_constraints( + self, + model, + ): + """ + Return SMT constraints for XOR quasidifferential propagation. + + Handles an arbitrary number of operands (not just 2), matching + the general ``Xor`` component (``self.description[1]`` addends). + + Per Beyne & Rijmen, XOR is a linear map, so Theorem 3.2 applies: + + - difference propagation is the ordinary XOR rule (weight 0); + - mask propagation requires ALL masks meeting at the XOR node + (every input operand's mask AND the output mask) to be equal + -- the standard "branching" rule of linear cryptanalysis, + which is also what lets masks flow into a round-key XOR + branch (Section 4.4 of the paper). + + INPUT: + + - ``model`` -- **model object**; a model instance + + EXAMPLES:: + + sage: from claasp.ciphers.single_component_ciphers.xor_cipher import XorCipher + sage: from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import SmtXorQuasidifferentialModel + sage: cipher = XorCipher(word_bit_size=2, number_of_inputs=2) + sage: xor_component = cipher.component_from_id('xor_0_0') + sage: smt = SmtXorQuasidifferentialModel(cipher) + sage: variables, constraints = xor_component.smt_xor_quasidifferential_propagation_constraints(smt) + sage: variables + ['xor_0_0_0', 'xor_0_0_1', 'qdt_xor_0_0_0', 'qdt_xor_0_0_1'] + sage: constraints + ['(assert (= xor_0_0_0 (xor plaintext_0 key_0)))', + '(assert (= xor_0_0_1 (xor plaintext_1 key_1)))', + '(assert (= qdt_plaintext_0 qdt_xor_0_0_0))', + '(assert (= qdt_key_0 qdt_xor_0_0_0))', + '(assert (= qdt_plaintext_1 qdt_xor_0_0_1))', + '(assert (= qdt_key_1 qdt_xor_0_0_1))'] + """ + + # Ordinary XOR difference input identifiers. + input_bit_ids = self._generate_input_ids() + + # Ordinary XOR difference output identifiers. + + output_bit_ids_result = self._generate_output_ids() + + if ( + isinstance(output_bit_ids_result, (tuple, list)) + and output_bit_ids_result + and isinstance(output_bit_ids_result[-1], list) + ): + output_bit_ids = output_bit_ids_result[-1] + else: + output_bit_ids = output_bit_ids_result + + # QDT input mask identifiers. + qdt_input_bit_ids = model._qdt_input_bit_ids(self) + # QDT output mask identifiers. + qdt_output_bit_ids = [f"qdt_{bit_id}" for bit_id in output_bit_ids] + + word_size = self.output_bit_size + + if word_size == 0 or len(input_bit_ids) % word_size != 0: + raise ValueError(f"Unexpected XOR input size for {self.id}: {len(input_bit_ids)} bits") + + variables = output_bit_ids + qdt_output_bit_ids + + constraints = [] + + # XOR difference propagation (n-ary): + # + # dz_i = dx_0_i XOR dx_1_i XOR ... XOR dx_{k-1}_i + + for i, output_bit in enumerate(output_bit_ids): + operands = input_bit_ids[i::word_size] + + equation = smt_utils.smt_equivalent( + [ + output_bit, + smt_utils.smt_xor(operands), + ] + ) + + constraints.append(smt_utils.smt_assert(equation)) + + # QDT mask propagation (n-ary, branching rule): + # + # u_0_i = u_1_i = ... = u_{k-1}_i = uz_i + + for i, output_bit in enumerate(qdt_output_bit_ids): + operand_masks = qdt_input_bit_ids[i::word_size] + + for operand_mask in operand_masks: + equation = smt_utils.smt_equivalent( + [ + operand_mask, + output_bit, + ] + ) + + constraints.append(smt_utils.smt_assert(equation)) + + return ( + variables, + constraints, + ) + + def cp_transform_xor_components_for_first_step(self, model): """ Transform a XOR component into components involving only one byte for CP. diff --git a/claasp/name_mappings.py b/claasp/name_mappings.py index 7c77d738f..45c7e1063 100644 --- a/claasp/name_mappings.py +++ b/claasp/name_mappings.py @@ -41,7 +41,7 @@ SEMI_DETERMINISTIC_TRUNCATED_XOR_DIFFERENTIAL_OPTIMAL_SOLUTION = "semi_deterministic_truncated_xor_differential_optimal_solution" IMPOSSIBLE_XOR_DIFFERENTIAL = "impossible_xor_differential" BOOMERANG_XOR_DIFFERENTIAL = "boomerang_xor_differential" - +XOR_QUASIDIFFERENTIAL = "xor_quasidifferential" # cipher inverse CIPHER_INVERSE_SUFFIX = "_inverse" diff --git a/docs/references.rst b/docs/references.rst index a080cf701..9781fa20c 100644 --- a/docs/references.rst +++ b/docs/references.rst @@ -148,6 +148,14 @@ Arai, K. (eds) Intelligent Computing. Lecture Notes in Networks and Systems, vol 285. Springer +.. [BR2022] + Beyne T., Rijmen V. : *Differential Cryptanalysis in the Fixed-Key + Model* : In Advances in Cryptology -- CRYPTO 2022, LNCS 13509, + pp. 687-716, Springer 2022 : + https://doi.org/10.1007/978-3-031-15982-4_23 (extended version: + Cryptology ePrint Archive, Paper 2022/837, + https://eprint.iacr.org/2022/837) + .. [BKLPPRSV2007] Bogdanov A., Knudsen L., Leander G., Paar C., Poschmann A., Robshaw M., Seurin Y., Vikkelsoe C. : *PRESENT: An Ultra-Lightweight Block Cipher* diff --git a/tests/unit/cipher_modules/models/smt/smt_models/smt_xor_quasidifferential_model_test.py b/tests/unit/cipher_modules/models/smt/smt_models/smt_xor_quasidifferential_model_test.py new file mode 100644 index 000000000..53e15707e --- /dev/null +++ b/tests/unit/cipher_modules/models/smt/smt_models/smt_xor_quasidifferential_model_test.py @@ -0,0 +1,556 @@ + +import pytest + +from claasp.cipher_modules.models.smt.smt_models.smt_xor_differential_model import SmtXorDifferentialModel +from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import ( + SmtXorQuasidifferentialModel, +) +from claasp.cipher_modules.models.smt.solvers import Z3_EXT +from claasp.cipher_modules.models.smt.utils import constants +from claasp.cipher_modules.models.utils import integer_to_bit_list, set_fixed_variables +from claasp.ciphers.block_ciphers.des_block_cipher import DESBlockCipher +from claasp.ciphers.block_ciphers.rectangle_block_cipher import RectangleBlockCipher +from claasp.ciphers.block_ciphers.simon_block_cipher import SimonBlockCipher +from claasp.ciphers.block_ciphers.speck_block_cipher import SpeckBlockCipher +from claasp.ciphers.toys.heys_block_cipher import HeysBlockCipher +from claasp.ciphers.toys.toyspn1 import ToySPN1 +from claasp.name_mappings import INPUT_KEY, INPUT_PLAINTEXT, XOR_QUASIDIFFERENTIAL + + +def test_find_lowest_weight_xor_quasidifferential_trail_on_rectangle(): + rectangle = RectangleBlockCipher(number_of_rounds=1) + smt = SmtXorQuasidifferentialModel(rectangle) + plaintext = set_fixed_variables(INPUT_PLAINTEXT, "not_equal", range(64), (0,) * 64) + trail = smt.find_lowest_weight_xor_quasidifferential_trail(fixed_values=[plaintext]) + assert trail["total_weight"] == 0.0 + + +def test_find_one_xor_quasidifferential_trail_on_simon(): + simon = SimonBlockCipher(number_of_rounds=1) + smt = SmtXorQuasidifferentialModel(simon) + solution = smt.find_one_xor_quasidifferential_trail() + assert str(solution["cipher"]) == "simon_p32_k64_o32_r1" + assert solution["solver_name"] == Z3_EXT + assert solution["components_values"]["and_0_4"]["weight"] == solution["total_weight"] + + +def test_compute_trail_sign(): + speck = SpeckBlockCipher(number_of_rounds=6) + smt = SmtXorQuasidifferentialModel(speck) + trail = smt.find_one_xor_quasidifferential_trail_with_fixed_weight( + 13, fixed_values=_speck_six_round_characteristic(), fixed_masks=smt.boundary_masks() + ) + assert trail["total_weight"] == 13.0 + assert smt.compute_trail_sign(trail) == 1 + + +def test_estimate_fixed_key_probability(): + speck = SpeckBlockCipher(number_of_rounds=6) + smt = SmtXorQuasidifferentialModel(speck) + fixed_masks = [ + {"component_id": INPUT_PLAINTEXT, "bit_positions": range(32), "bit_values": [0] * 32}, + {"component_id": INPUT_KEY, "bit_positions": range(64), "bit_values": [0] * 64}, + {"component_id": "cipher_output_5_12", "bit_positions": range(32), "bit_values": [0] * 32}, + ] + result = smt.estimate_fixed_key_probability( + max_weight=13, + min_weight=13, + fixed_values=_speck_six_round_characteristic(), + fixed_masks=fixed_masks, + ) + assert result["num_trails"] == 1 + assert result["trails"][0]["sign"] == 1 + assert result["estimated_probability"] == 2.0**-13 + + +def test_fork_constraints_tie_branch_masks_by_xor(): + # At a fork the source mask is the XOR of the branch masks, not their + # equality. Checked against Equation (4) on the copy map F(x) = (x, x): + # of the 512 three-bit transitions with a non-zero coefficient, all + # satisfy u = v1 xor v2 and only 8 satisfy u = v1 = v2, so sharing one + # variable among consumers is a constraint 64 times too strong. + speck = SpeckBlockCipher(number_of_rounds=2) + smt = SmtXorQuasidifferentialModel(speck) + variables, constraints = smt._fork_constraints() + + forks = [wire for wire, consumers in smt._wire_consumers.items() if len(consumers) > 1] + + assert len(forks) == 96 + assert len(constraints) == 96 + assert len(variables) == 256 + assert constraints[0].startswith("(assert (= qdt_") + assert " (xor " in constraints[0] + + +def test_forked_wires_use_one_mask_variable_per_consumer(): + speck = SpeckBlockCipher(number_of_rounds=2) + smt = SmtXorQuasidifferentialModel(speck) + + modadd = speck.component_from_id("modadd_0_1") + mask_ids = smt._qdt_input_bit_ids(modadd) + + assert any(mask_id.endswith("_to_modadd_0_1") for mask_id in mask_ids) + assert all("_to_" not in mask_id or "_to_modadd_0_1" in mask_id for mask_id in mask_ids) + + +def test_each_read_of_a_wire_gets_its_own_branch(): + # DES's expansion feeds 16 bits of permutation_0_0 into BOTH halves of + # xor_0_7. Keying a branch by consumer id alone would give the two reads + # one name, and the fork assertion would then XOR it with itself, where + # it cancels -- the branch would drop out of the source relation. + des = DESBlockCipher(number_of_rounds=1) + smt = SmtXorQuasidifferentialModel(des) + + xor = des.component_from_id("xor_0_7") + mask_ids = smt._qdt_input_bit_ids(xor) + + assert len(mask_ids) == len(set(mask_ids)) + + doubly_read = [ + wire + for wire, consumers in smt._wire_consumers.items() + if [consumer for consumer, _ in consumers].count("xor_0_7") > 1 + ] + assert doubly_read + + source_id, position = doubly_read[0] + _, constraints = smt._fork_constraints() + assertion = next(c for c in constraints if c.startswith(f"(assert (= qdt_{source_id}_{position} ")) + branches = [token for token in assertion.split() if "_to_" in token] + + assert len(branches) == len(set(branches)) + + +def test_masks_of_unread_cipher_input_bits_are_zero(): + # Half of Speck's key is never read at two rounds. Those mask variables + # are otherwise free, yet _qdt_get_operands puts them in every blocking + # clause, so each assignment would count as a distinct trail. + speck = SpeckBlockCipher(number_of_rounds=2) + smt = SmtXorQuasidifferentialModel(speck) + + constraints = smt._unread_input_mask_constraints() + + assert len(constraints) == 32 + assert all(c.startswith("(assert (not qdt_key_") for c in constraints) + + +def test_masks_of_terminal_output_taps_are_zero(): + # A round-output tap exposes a wire without consuming it, so it is not a + # coordinate of the function the trail describes. Left free, its fork + # branch lets the solver dump mask into the tap and decouple the rounds. + # The cipher output is excluded: its bits ARE output coordinates. + speck = SpeckBlockCipher(number_of_rounds=2) + smt = SmtXorQuasidifferentialModel(speck) + + constraints = smt._terminal_tap_mask_constraints() + tapped = {c.split("qdt_")[1].rsplit("_", 1)[0] for c in constraints} + + assert "intermediate_output_0_6" in tapped + assert not any("cipher_output" in c for c in constraints) + + +def test_sbox_with_a_non_power_of_two_qdt_is_refused(): + # The weight of a transition is -log2|coefficient| and the model encodes + # it as an integer, so a coefficient of 3/8 would be silently recorded as + # weight 1. The differential models already refuse such an S-box through + # check_table_feasibility; this is the QDT-side counterpart. + smt = SmtXorQuasidifferentialModel(HeysBlockCipher(number_of_rounds=1)) + + with pytest.raises(ValueError, match="not a power of two"): + smt.build_xor_quasidifferential_trail_model(weight=2) + + +def test_model_admits_the_masks_of_equation_4(): + admissible = [ + (0x00, 0x00, 1), # coefficient +0.5000 + (0x40, 0x42, 2), # coefficient -0.2500 + (0x40, 0x53, 2), # coefficient +0.2500 + (0x80, 0x0F, 3), # coefficient +0.1250 + (0x80, 0x1E, 3), # coefficient -0.1250 + ] + + for input_mask, output_mask, weight in admissible: + result = _solve_speck8_with_masks(input_mask, output_mask, weight) + assert result["status"] == "SATISFIABLE", ( + f"an admissible mask was rejected: u={input_mask:#04x} " + f"v={output_mask:#04x} weight {weight}" + ) + + +def test_model_rejects_the_masks_outside_equation_4(): + # The direction that matters whenever a constraint is relaxed: the risk + # then is over-permissiveness, which no SATISFIABLE assertion can catch. + inadmissible = [(0x00, 0x01), (0x00, 0x02), (0x00, 0x03)] + + for input_mask, output_mask in inadmissible: + for weight in (1, 2, 3): + result = _solve_speck8_with_masks(input_mask, output_mask, weight) + assert result["status"] == "UNSATISFIABLE", ( + f"an impossible mask was accepted: u={input_mask:#04x} " + f"v={output_mask:#04x} weight {weight}" + ) + + +def _solve_speck8_with_masks(input_mask, output_mask, weight): + speck = SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=1) + smt = SmtXorQuasidifferentialModel(speck) + + fixed_values = [ + set_fixed_variables(INPUT_KEY, "equal", range(16), (0,) * 16), + set_fixed_variables(INPUT_PLAINTEXT, "equal", range(8), integer_to_bit_list(0x01, 8, "big")), + set_fixed_variables("cipher_output_0_6", "equal", range(8), integer_to_bit_list(0x19, 8, "big")), + ] + + smt.build_xor_quasidifferential_trail_model(weight=weight, fixed_variables=fixed_values) + if smt._counter == smt._sequential_counter: + smt._sequential_counter_greater_or_equal(weight, "dummy_hw_1") + + masks = [ + {"component_id": INPUT_PLAINTEXT, "bit_positions": range(8), + "bit_values": integer_to_bit_list(input_mask, 8, "big")}, + {"component_id": "cipher_output_0_6", "bit_positions": range(8), + "bit_values": integer_to_bit_list(output_mask, 8, "big")}, + ] + extra = smt._build_fixed_mask_constraints(masks) + smt._model_constraints = ( + smt._model_constraints[: -len(constants.MODEL_SUFFIX)] + extra + constants.MODEL_SUFFIX + ) + + return smt.solve(XOR_QUASIDIFFERENTIAL, solver_name=Z3_EXT) + + +def _simon_six_round_characteristic(): + cipher = SimonBlockCipher(number_of_rounds=6) + differences = [0x00400110, 0x00100040, 0x00000010, 0x00100000, 0x00400010, 0x01100040, 0x01100040] + taps = [c.id for c in cipher.all_components() + if c.description[0] in ("round_output", "cipher_output")] + + fixed_values = [ + set_fixed_variables(INPUT_KEY, "equal", range(64), (0,) * 64), + set_fixed_variables(INPUT_PLAINTEXT, "equal", range(32), + integer_to_bit_list(0x01100400, 32, "big")), + ] + for component_id, difference in zip(taps, differences): + fixed_values.append( + set_fixed_variables(component_id, "equal", range(32), + integer_to_bit_list(difference, 32, "big")) + ) + + boundary_masks = [ + {"component_id": INPUT_PLAINTEXT, "bit_positions": range(32), "bit_values": [0] * 32}, + {"component_id": "cipher_output_5_13", "bit_positions": range(32), "bit_values": [0] * 32}, + ] + + return cipher, fixed_values, boundary_masks + + +def test_estimate_fixed_key_probability_applies_the_key_factor(): + # This weight-12 Simon characteristic has four trails with zero boundary + # masks: the characteristic itself, two weight-14 corrections of opposite + # sign carrying disjoint key masks A and B, and a weight-16 trail carrying + # A xor B. The probability therefore depends on the key only through + # chi_A(k) and chi_B(k), and the average is NOT the fixed-key value. + cipher, fixed_values, boundary_masks = _simon_six_round_characteristic() + + def probability(key): + return SmtXorQuasidifferentialModel(cipher).estimate_fixed_key_probability( + max_weight=16, min_weight=12, + fixed_values=fixed_values, fixed_masks=boundary_masks, key=key, + ) + + average = probability(None) + assert average["averaged_over_keys"] is True + assert average["num_trails"] == 1 # only the zero-key-mask trail survives averaging + assert average["num_trails_found"] == 4 + assert average["estimated_probability"] == 2.0**-12 + + zero_key = probability(0) + assert zero_key["averaged_over_keys"] is False + assert zero_key["num_trails"] == 4 + assert zero_key["estimated_probability"] == 2.0**-12 - 2 * 2.0**-14 + 2.0**-16 + + # 0x8000 is a single bit of A and lies outside B, so it flips chi_A only. + flipped = probability(0x8000) + assert flipped["estimated_probability"] == 2.0**-12 - 2.0**-16 + assert flipped["estimated_probability"] != zero_key["estimated_probability"] + + +def test_trail_sign_does_not_depend_on_solve_order(): + # compute_trail_sign reconstructs input masks from the solver assignment. + # Held on the model, that assignment is overwritten by every later solve, + # so a stored solution would be scored with the LAST trail's masks. Each + # solution carries its own, so the order of the calls cannot matter. + cipher, fixed_values, boundary_masks = _simon_six_round_characteristic() + smt = SmtXorQuasidifferentialModel(cipher) + + solutions = [ + solution + for weight in (12, 14) + for solution in smt._solutions_at_weight(weight, fixed_values, boundary_masks, Z3_EXT, None, None)[0] + ] + assert len(solutions) == 3 + + forwards = [smt.compute_trail_sign(solution) for solution in solutions] + backwards = [smt.compute_trail_sign(solution) for solution in reversed(solutions)] + + assert forwards == list(reversed(backwards)) + assert len(set(forwards)) > 1 # otherwise the check proves nothing + assert all(solution["qdt_variable_assignment"] for solution in solutions) + + +def test_weights_the_sequential_counter_cannot_express(): + # _sequential_counter_greater_or_equal rewrites "at least w" as "at most + # n - w", so w == n collapses its inner dimension and it raises + # IndexError. On 8-bit Speck at one round n is 4, so the crash sits right + # inside the range a caller would naturally ask for. + speck = SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=1) + smt = SmtXorQuasidifferentialModel(speck) + + smt.build_xor_quasidifferential_trail_model(weight=1) + indicators = len([v for v in smt._variables_list if v.startswith("hw_")]) + assert indicators == 4 + + assert smt.find_one_xor_quasidifferential_trail_with_fixed_weight(indicators - 1)["total_weight"] == 3.0 + + for weight in (indicators, indicators + 1, indicators + 3): + assert smt.find_one_xor_quasidifferential_trail_with_fixed_weight(weight)["total_weight"] is None + + +def test_fixed_key_probability_matches_brute_force_on_an_spn(): + # The end-to-end reference so far was 8-bit Speck, an ARX: the S-box path + # had never been compared with a measured probability. ToySPN1 is a 6-bit + # SPN -- round-key XOR, two 3-bit S-boxes, a rotation -- so a + # differential's exact probability can be counted over all 64 plaintexts, + # for any key, and held against the signed sum of its trails. + # + # The comparison is made key by key, not only on the average: averaging + # keeps only the zero-key-mask trails, so it would leave both the key + # masks and the signs untested. + toyspn = ToySPN1(number_of_rounds=2) + delta_in, delta_out = 0x02, 0x20 + + smt = SmtXorQuasidifferentialModel(toyspn) + smt.build_xor_quasidifferential_trail_model() + indicators = len([v for v in smt._variables_list if v.startswith("hw_")]) + assert indicators == 8 # no trail can weigh more, so the sum below is complete + + fixed_values = [ + set_fixed_variables(INPUT_KEY, "equal", range(6), (0,) * 6), + set_fixed_variables(INPUT_PLAINTEXT, "equal", range(6), integer_to_bit_list(delta_in, 6, "big")), + set_fixed_variables("cipher_output_1_6", "equal", range(6), integer_to_bit_list(delta_out, 6, "big")), + ] + boundary_masks = [ + {"component_id": INPUT_PLAINTEXT, "bit_positions": range(6), "bit_values": [0] * 6}, + {"component_id": "cipher_output_1_6", "bit_positions": range(6), "bit_values": [0] * 6}, + ] + + # key=0 keeps every trail in the list, each with its own key mask, so the + # sum can be re-evaluated for the other keys without solving again. + result = SmtXorQuasidifferentialModel(toyspn).estimate_fixed_key_probability( + max_weight=indicators, min_weight=0, + fixed_values=fixed_values, fixed_masks=boundary_masks, key=0, + ) + trails = result["trails"] + assert len(trails) == 4 + assert len([trail for trail in trails if trail["key_mask"]]) == 2 + + def from_trails(key): + return sum( + (-1) ** bin(trail["key_mask"] & key).count("1") * trail["sign"] * 2.0 ** -trail["weight"] + for trail in trails + ) + + def brute_force(key): + outputs = [toyspn.evaluate([plaintext, key]) for plaintext in range(64)] + hits = sum(1 for plaintext in range(64) if outputs[plaintext] ^ outputs[plaintext ^ delta_in] == delta_out) + return hits / 64 + + measured = {key: brute_force(key) for key in (0x00, 0x01, 0x02, 0x05, 0x0A, 0x3F)} + + assert set(measured.values()) == {0.0, 0.125, 0.25} # otherwise the keys prove nothing + for key, exact in measured.items(): + assert from_trails(key) == exact + + # The average is a different quantity, and the model says so itself. + average = sum(trail["sign"] * 2.0 ** -trail["weight"] for trail in trails if trail["key_mask"] == 0) + assert average == 0.125 + assert average != measured[0x00] + + +def test_enumeration_bounds_report_truncation(): + cipher, fixed_values, boundary_masks = _simon_six_round_characteristic() + + exact = 2.0**-12 - 2 * 2.0**-14 + 2.0**-16 + + bounded = SmtXorQuasidifferentialModel(cipher).estimate_fixed_key_probability( + max_weight=16, min_weight=12, + fixed_values=fixed_values, fixed_masks=boundary_masks, key=0, + max_trails_per_weight=1, + ) + assert bounded["truncated"] is True + assert bounded["truncated_weights"] == [12, 14, 16] + assert bounded["num_trails"] == 3 # one of the two at weight 14 is missing + assert bounded["estimated_probability"] != exact + + # timeout_per_weight=0 stops after the first trail of each weight too, + # which makes the time-based bound checkable without a slow test. + timed = SmtXorQuasidifferentialModel(cipher).estimate_fixed_key_probability( + max_weight=16, min_weight=12, + fixed_values=fixed_values, fixed_masks=boundary_masks, key=0, + timeout_per_weight=0, + ) + assert timed["truncated_weights"] == bounded["truncated_weights"] + assert timed["estimated_probability"] == bounded["estimated_probability"] + + # Unbounded, the same call is exhaustive and says so. + speck = SpeckBlockCipher(number_of_rounds=6) + fixed_masks = [ + {"component_id": INPUT_PLAINTEXT, "bit_positions": range(32), "bit_values": [0] * 32}, + {"component_id": INPUT_KEY, "bit_positions": range(64), "bit_values": [0] * 64}, + {"component_id": "cipher_output_5_12", "bit_positions": range(32), "bit_values": [0] * 32}, + ] + exhaustive = SmtXorQuasidifferentialModel(speck).estimate_fixed_key_probability( + max_weight=13, min_weight=13, + fixed_values=_speck_six_round_characteristic(), fixed_masks=fixed_masks, + ) + assert exhaustive["truncated"] is False + assert exhaustive["truncated_weights"] == [] + assert exhaustive["estimated_probability"] == 2.0**-13 + + +def _speck_six_round_characteristic(): + differences = { + INPUT_PLAINTEXT: 0x02110A04, + "intermediate_output_0_6": 0x28000010, + "intermediate_output_1_12": 0x00400000, + "intermediate_output_2_12": 0x80008000, + "intermediate_output_3_12": 0x81008102, + "intermediate_output_4_12": 0x8000840A, + "cipher_output_5_12": 0x850A9520, + } + fixed_values = [set_fixed_variables(INPUT_KEY, "equal", range(64), (0,) * 64)] + for component_id, difference in differences.items(): + bit_values = [(difference >> (31 - i)) & 1 for i in range(32)] + fixed_values.append(set_fixed_variables(component_id, "equal", range(32), bit_values)) + + return fixed_values + + +def _rectangle_three_round_key_alternating(): + """The first three rounds of the 14-round RECTANGLE characteristic of + Beyne & Rijmen, CRYPTO 2022, Table 11, differential i, on the + key-alternating form. + + The paper prints the 4x16 state column-major (bit 4*col + row) and CLAASP + stores it row-major (bit 16*row + col), so these are the paper's rows 0, 2, + 4 and 6 transposed. + """ + rectangle = RectangleBlockCipher(number_of_rounds=3).remove_key_schedule() + differences = { + INPUT_PLAINTEXT: 0x0000010021000000, + "intermediate_output_0_31": 0x0000020042000000, + "intermediate_output_1_31": 0x0000040084000000, + "intermediate_output_2_32": 0x0000080008010000, + } + fixed_values = [ + set_fixed_variables(input_id, "equal", range(64), (0,) * 64) + for input_id in rectangle.inputs + if input_id.startswith("key") + ] + for component_id, difference in differences.items(): + fixed_values.append( + set_fixed_variables(component_id, "equal", range(64), integer_to_bit_list(difference, 64, "big")) + ) + + return rectangle, fixed_values + + +def test_sbox_differences_are_derived_from_the_characteristic(): + rectangle, fixed_values = _rectangle_three_round_key_alternating() + smt = SmtXorQuasidifferentialModel(rectangle) + assert smt.sbox_differences == {} + + smt.build_xor_quasidifferential_trail_model(fixed_variables=fixed_values) + + sboxes = [component.id for component in rectangle.all_components() if component.type == "sbox"] + assert len(sboxes) == 48 + assert sorted(smt.sbox_differences) == sorted(sboxes) + + +def test_sbox_constraints_are_restricted_to_the_derived_differences(): + rectangle, fixed_values = _rectangle_three_round_key_alternating() + sbox = next(component for component in rectangle.all_components() if component.type == "sbox") + + unrestricted = SmtXorQuasidifferentialModel(rectangle) + _, before = sbox.smt_xor_quasidifferential_propagation_constraints(unrestricted) + + restricted = SmtXorQuasidifferentialModel(rectangle) + restricted.build_xor_quasidifferential_trail_model(fixed_variables=fixed_values) + _, after = sbox.smt_xor_quasidifferential_propagation_constraints(restricted) + + assert before[0].count("(and ") == 10885 + assert after[0].count("(and ") < before[0].count("(and ") + + +def test_averaged_probability_agrees_with_the_differential_model(): + """Theorem 4.3: averaging over keys leaves only the zero-key-mask trail, so + the quasidifferential model must reproduce the characteristic weight that + the differential model reports, by a completely separate route.""" + rectangle, fixed_values = _rectangle_three_round_key_alternating() + weight = SmtXorDifferentialModel(rectangle).find_one_xor_differential_trail( + fixed_values=fixed_values + )["total_weight"] + assert weight == 15.0 + + smt = SmtXorQuasidifferentialModel(rectangle) + average = smt.estimate_fixed_key_probability( + min_weight=15, max_weight=17, fixed_values=fixed_values, fixed_masks=smt.boundary_masks() + ) + + assert not average["truncated"] + assert average["num_trails"] == 1 + assert average["estimated_probability"] == 2.0**-15 + + +def test_fixed_key_probability_on_a_key_alternating_cipher(): + """For one key nothing cancels, so the extra weight-17 trail counts too and + the answer differs from the average.""" + rectangle, fixed_values = _rectangle_three_round_key_alternating() + smt = SmtXorQuasidifferentialModel(rectangle) + + result = smt.estimate_fixed_key_probability( + min_weight=15, max_weight=17, fixed_values=fixed_values, + fixed_masks=smt.boundary_masks(), key=0, + ) + + assert not result["truncated"] + assert result["num_trails"] == 2 + assert result["estimated_probability"] == 2.0**-15 + 2.0**-17 + + +def _speck8_one_round(): + speck = SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=1) + return speck, SmtXorQuasidifferentialModel(speck) + + +def test_find_one_trail_honours_fixed_masks(): + _, smt = _speck8_one_round() + trail = smt.find_one_xor_quasidifferential_trail(fixed_masks=smt.boundary_masks()) + assert int(trail["components_values"][INPUT_PLAINTEXT]["mask"], 16) == 0 + assert int(trail["components_values"]["cipher_output_0_6"]["mask"], 16) == 0 + + +def test_find_all_trails_at_a_weight_honour_fixed_masks(): + _, smt = _speck8_one_round() + assert len(smt.find_all_xor_quasidifferential_trails_with_fixed_weight(0)) == 96 + assert len( + smt.find_all_xor_quasidifferential_trails_with_fixed_weight(0, fixed_masks=smt.boundary_masks()) + ) == 3 + + +def test_find_all_trails_up_to_a_weight_pass_fixed_masks_through(): + _, smt = _speck8_one_round() + assert len(smt.find_all_xor_quasidifferential_trails_with_weight_at_most(0)) == 96 + assert len( + smt.find_all_xor_quasidifferential_trails_with_weight_at_most(0, fixed_masks=smt.boundary_masks()) + ) == 3 diff --git a/tests/unit/cipher_modules/report_test.py b/tests/unit/cipher_modules/report_test.py index 0d4361c75..1288280b8 100644 --- a/tests/unit/cipher_modules/report_test.py +++ b/tests/unit/cipher_modules/report_test.py @@ -99,11 +99,14 @@ def _generate(): def _cached_speck_algebraic_results(): + # A system whose Groebner basis completes well within the timeout: when the + # alarm fires instead, PolyBoRi may only honour it minutes later, which made + # this fixture randomly exceed the per-test timeout on CI. def _generate(): - cipher = SpeckBlockCipher(number_of_rounds=2) - return AlgebraicTests(cipher).algebraic_tests(timeout_in_seconds=1) + cipher = SpeckBlockCipher(block_bit_size=8, key_bit_size=16, number_of_rounds=1) + return AlgebraicTests(cipher).algebraic_tests(timeout_in_seconds=60) - return _get_cached_result('speck_r2_algebraic_tests', _generate) + return _get_cached_result('speck_b8_r1_algebraic_tests', _generate) def _cached_speck_component_analysis(): @@ -223,7 +226,8 @@ def _run_show(): neural_network_tests_report.show(fixed_input_difference=None) neural_network_tests_report.show(fixed_input_difference='0xa') -def test_save_as_latex_table(): +def test_save_as_latex_table(tmp_path): + output_dir = str(tmp_path / 'test_reports') simon = SimonBlockCipher(number_of_rounds=2) smt = SmtXorDifferentialModel(simon) @@ -242,17 +246,18 @@ def test_save_as_latex_table(): avalanche_test_results = AvalancheTests(simon).avalanche_tests() avalanche_report = Report(avalanche_test_results) - avalanche_report.save_as_latex_table(fixed_input='plaintext',fixed_output='round_output',fixed_test='avalanche_weight_vectors') - avalanche_report.clean_reports() + avalanche_report.save_as_latex_table(output_dir=output_dir, fixed_input='plaintext',fixed_output='round_output',fixed_test='avalanche_weight_vectors') + avalanche_report.clean_reports(output_dir=output_dir) trail_report = Report(trail) - trail_report.save_as_latex_table() - trail_report.clean_reports() + trail_report.save_as_latex_table(output_dir=output_dir) + trail_report.clean_reports(output_dir=output_dir) dieharder=DieharderTests(simon) report_sts = Report(dieharder.dieharder_statistical_tests('avalanche', dieharder_test_option=100)) - report_sts.save_as_latex_table() - report_sts.clean_reports() + report_sts.save_as_latex_table(output_dir=output_dir) + report_sts.clean_reports(output_dir=output_dir) -def test_save_as_dataframe(): +def test_save_as_dataframe(tmp_path): + output_dir = str(tmp_path / 'test_reports') speck = SpeckBlockCipher(number_of_rounds=2) cp = MznXorDifferentialModel(speck) plaintext = set_fixed_variables( @@ -269,31 +274,32 @@ def test_save_as_dataframe(): avalanche_results = AvalancheTests(speck).avalanche_tests() avalanche_report = Report(avalanche_results) - avalanche_report.save_as_dataframe(fixed_input='plaintext',fixed_output='round_output',fixed_test='avalanche_weight_vectors') - avalanche_report.clean_reports() + avalanche_report.save_as_dataframe(output_dir=output_dir, fixed_input='plaintext',fixed_output='round_output',fixed_test='avalanche_weight_vectors') + avalanche_report.clean_reports(output_dir=output_dir) trail_report = Report(trail) - trail_report.save_as_dataframe() - trail_report.clean_reports() + trail_report.save_as_dataframe(output_dir=output_dir) + trail_report.clean_reports(output_dir=output_dir) dieharder = DieharderTests(speck) report_sts = Report(dieharder.dieharder_statistical_tests('avalanche', dieharder_test_option=100)) - report_sts.save_as_dataframe() - report_sts.clean_reports() + report_sts.save_as_dataframe(output_dir=output_dir) + report_sts.clean_reports(output_dir=output_dir) -def test_save_as_json(): +def test_save_as_json(tmp_path): + output_dir = str(tmp_path / 'test_reports') speck = SpeckBlockCipher(number_of_rounds=2) neural_network_blackbox_distinguisher_tests_results = NeuralNetworkTests(speck).neural_network_blackbox_distinguisher_tests(nb_samples=10) blackbox_report = Report(neural_network_blackbox_distinguisher_tests_results) - blackbox_report.save_as_json(fixed_input='plaintext',fixed_output='round_output') - blackbox_report.clean_reports() + blackbox_report.save_as_json(output_dir=output_dir, fixed_input='plaintext',fixed_output='round_output') + blackbox_report.clean_reports(output_dir=output_dir) simon = SimonBlockCipher(number_of_rounds=2) dieharder = DieharderTests(simon) report_sts = Report(dieharder.dieharder_statistical_tests('avalanche', dieharder_test_option=100)) - report_sts.save_as_json() - report_sts.clean_reports() + report_sts.save_as_json(output_dir=output_dir) + report_sts.clean_reports(output_dir=output_dir) present = PresentBlockCipher(number_of_rounds=2) sat = SatXorDifferentialModel(present) related_key_setting = [ @@ -309,8 +315,8 @@ def test_save_as_json(): avalanche_results = AvalancheTests(simon).avalanche_tests() avalanche_report = Report(avalanche_results) - avalanche_report.save_as_json(fixed_input='plaintext',fixed_output='round_output',fixed_test='avalanche_weight_vectors') - avalanche_report.clean_reports() + avalanche_report.save_as_json(output_dir=output_dir, fixed_input='plaintext',fixed_output='round_output',fixed_test='avalanche_weight_vectors') + avalanche_report.clean_reports(output_dir=output_dir) def test_show(monkeypatch, tmp_path): captured_fig_shows = [] diff --git a/tests/unit/components/and_component_test.py b/tests/unit/components/and_component_test.py index 863648aaf..1befaeb80 100644 --- a/tests/unit/components/and_component_test.py +++ b/tests/unit/components/and_component_test.py @@ -4,7 +4,9 @@ ) from claasp.ciphers.single_component_ciphers.and_cipher import AndCipher from claasp.components.and_component import And, cp_xor_differential_probability_ddt, cp_xor_linear_probability_lat - +from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import ( + SmtXorQuasidifferentialModel, +) def test_cp_xor_differential_probability_ddt(): assert cp_xor_differential_probability_ddt(2) == [4, 0, 2, 2, 2, 2, 2, 2] @@ -107,3 +109,31 @@ def test_milp_bitwise_deterministic_truncated_xor_differential_constraints(): assert str(constraints[1]) == '1 - 4*x_36 <= x_0 + x_12' assert str(constraints[-2]) == 'x_35 <= 2 + 2*x_47' assert str(constraints[-1]) == '2 <= x_35 + 2*x_47' + +def test_smt_xor_quasidifferential_propagation_constraints(): + cipher = AndCipher(word_bit_size=2, number_of_inputs=2) + model = SmtXorQuasidifferentialModel(cipher) + and_component = cipher.component_from(0, 0) + variables, constraints = and_component.smt_xor_quasidifferential_propagation_constraints(model) + + assert variables == ['and_0_0_0', 'and_0_0_1', 'qdt_and_0_0_0', 'qdt_and_0_0_1', + 'hw_qdt_and_0_0_0', 'hw_qdt_and_0_0_1'] + + assert len(constraints) == 8 + assert constraints[0] == '(assert (=> and_0_0_0 (or plaintext_0 key_0)))' + assert constraints[3] == '(assert (= hw_qdt_and_0_0_0 (or plaintext_0 key_0 qdt_and_0_0_0)))' + assert constraints[-1] == '(assert (= hw_qdt_and_0_0_1 (or plaintext_1 key_1 qdt_and_0_0_1)))' + + +def test_smt_xor_quasidifferential_propagation_constraints_more_than_two_operands(): + cipher = AndCipher(word_bit_size=2, number_of_inputs=3) + model = SmtXorQuasidifferentialModel(cipher) + and_component = cipher.component_from(0, 0) + + try: + and_component.smt_xor_quasidifferential_propagation_constraints(model) + raised = False + except NotImplementedError: + raised = True + + assert raised \ No newline at end of file diff --git a/tests/unit/components/cipher_output_component_test.py b/tests/unit/components/cipher_output_component_test.py index 69c92f3d2..5e798b410 100644 --- a/tests/unit/components/cipher_output_component_test.py +++ b/tests/unit/components/cipher_output_component_test.py @@ -1,5 +1,8 @@ from claasp.components.cipher_output_component import CipherOutput - +from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import ( + SmtXorQuasidifferentialModel, +) +from claasp.ciphers.block_ciphers.rectangle_block_cipher import RectangleBlockCipher def test_cp_constraints(): output_component = CipherOutput( @@ -38,3 +41,19 @@ class DummyModel: assert constraints[0] == 'constraint intermediate_output_0_35_value[0] = xor_0_31_value[0];' assert constraints[-1] == 'constraint intermediate_output_0_35_active[15] = xor_0_34_active[3];' + +def test_smt_xor_quasidifferential_propagation_constraints(): + cipher = RectangleBlockCipher(number_of_rounds=1) + model = SmtXorQuasidifferentialModel(cipher) + cipher_output = cipher.component_from_id('cipher_output_0_33') + variables, constraints = cipher_output.smt_xor_quasidifferential_propagation_constraints(model) + + assert len(variables) == 128 + assert variables[0] == 'cipher_output_0_33_0' + assert variables[-1] == 'qdt_cipher_output_0_33_63' + + assert len(constraints) == 128 + assert constraints[0] == '(assert (= cipher_output_0_33_0 xor_0_30_0))' + assert constraints[-1] == ( + '(assert (= qdt_cipher_output_0_33_63 qdt_xor_0_30_63_to_cipher_output_0_33))' + ) diff --git a/tests/unit/components/constant_component_test.py b/tests/unit/components/constant_component_test.py index 5421d3ab0..ea47a6895 100644 --- a/tests/unit/components/constant_component_test.py +++ b/tests/unit/components/constant_component_test.py @@ -1,5 +1,8 @@ from claasp.components.constant_component import Constant - +from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import ( + SmtXorQuasidifferentialModel, +) +from claasp.ciphers.block_ciphers.rectangle_block_cipher import RectangleBlockCipher def test_cp_wordwise_deterministic_truncated_xor_differential_constraints(): class DummyModel: @@ -63,3 +66,17 @@ def test_smt_xor_linear_mask_propagation_constraints(): assert output_bit_ids[-1] == 'constant_0_2_31_o' assert constraints == [] + +def test_smt_xor_quasidifferential_propagation_constraints(): + cipher = RectangleBlockCipher(number_of_rounds=1) + model = SmtXorQuasidifferentialModel(cipher) + constant_component = cipher.component_from_id('constant_0_26') + variables, constraints = constant_component.smt_xor_quasidifferential_propagation_constraints(model) + + assert len(variables) == 10 + assert variables[0] == 'constant_0_26_0' + assert variables[-1] == 'qdt_constant_0_26_4' + + assert len(constraints) == 5 + assert constraints[0] == '(assert (not constant_0_26_0))' + assert constraints[-1] == '(assert (not constant_0_26_4))' \ No newline at end of file diff --git a/tests/unit/components/linear_layer_component_test.py b/tests/unit/components/linear_layer_component_test.py index 3d910fa39..e4ad05838 100644 --- a/tests/unit/components/linear_layer_component_test.py +++ b/tests/unit/components/linear_layer_component_test.py @@ -7,7 +7,9 @@ ) from claasp.ciphers.single_component_ciphers.linear_layer_cipher import LinearLayerCipher from claasp.components.linear_layer_component import LinearLayer - +from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import ( + SmtXorQuasidifferentialModel, +) MATRIX = [ [1, 0, 1, 0], [1, 1, 0, 1], @@ -275,3 +277,46 @@ def test_milp_wordwise_deterministic_truncated_xor_differential_constraints(): assert str(constraints[1]) == "1 <= 1 + x_1 + x_4 + x_5 - x_9" assert str(constraints[-2]) == "1 <= 1 + x_5 - x_6" assert str(constraints[-1]) == "1 <= 1 + x_1 - x_2" + + +def test_smt_xor_quasidifferential_propagation_constraints(): + linear_layer_component = make_linear_layer_component() + model = SmtXorQuasidifferentialModel(make_linear_layer_cipher()) + variables, constraints = linear_layer_component.smt_xor_quasidifferential_propagation_constraints(model) + + assert len(variables) == 19 + assert variables[:4] == [ + "linear_layer_0_0_0", + "linear_layer_0_0_1", + "linear_layer_0_0_2", + "linear_layer_0_0_3", + ] + assert variables[4:8] == [ + "qdt_linear_layer_0_0_0", + "qdt_linear_layer_0_0_1", + "qdt_linear_layer_0_0_2", + "qdt_linear_layer_0_0_3", + ] + assert variables[8] == "qdt_dummy_0_qdt_linear_layer_0_0_0" + assert variables[-1] == "qdt_dummy_2_qdt_linear_layer_0_0_3" + + assert len(constraints) == 12 + + # Differences: the ordinary linear-layer constraints. + assert constraints[:4] == [ + "(assert (= linear_layer_0_0_0 (xor input_0 input_1 input_3)))", + "(assert (= linear_layer_0_0_1 (xor input_1 input_2 input_3)))", + "(assert (= linear_layer_0_0_2 (xor input_0 input_2 input_3)))", + "(assert (= linear_layer_0_0_3 (xor input_1 input_3)))", + ] + + # Masks: propagated backwards through the transpose, via dummy + # variables carrying the qdt_ naming convention. + assert constraints[4] == ( + "(assert (= qdt_input_0 qdt_dummy_0_qdt_linear_layer_0_0_0 " + "qdt_dummy_0_qdt_linear_layer_0_0_3))" + ) + assert constraints[-1] == ( + "(assert (= qdt_linear_layer_0_0_3 (xor qdt_dummy_0_qdt_linear_layer_0_0_3 " + "qdt_dummy_1_qdt_linear_layer_0_0_3 qdt_dummy_2_qdt_linear_layer_0_0_3)))" + ) \ No newline at end of file diff --git a/tests/unit/components/mix_column_component_test.py b/tests/unit/components/mix_column_component_test.py index 56763f70f..32317adf0 100644 --- a/tests/unit/components/mix_column_component_test.py +++ b/tests/unit/components/mix_column_component_test.py @@ -4,7 +4,9 @@ from claasp.cipher_modules.models.milp.milp_model import MilpModel from claasp.ciphers.single_component_ciphers.mix_column_cipher import MixColumnCipher from claasp.components.mix_column_component import MixColumn - +from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import ( + SmtXorQuasidifferentialModel, +) MATRIX = [[1, 2], [3, 1]] IRREDUCIBLE_POLYNOMIAL = 0b10011 WORD_SIZE = 4 @@ -288,3 +290,82 @@ def test_smt_xor_linear_mask_propagation_constraints(): "(assert (= mix_column_0_0_7_o (xor dummy_0_mix_column_0_0_7_o dummy_1_mix_column_0_0_7_o " "dummy_5_mix_column_0_0_7_o dummy_6_mix_column_0_0_7_o)))" ) + + +def test_smt_xor_quasidifferential_propagation_constraints(): + mix_column_component = make_mix_column_component() + model = SmtXorQuasidifferentialModel(make_mix_column_cipher()) + variables, constraints = mix_column_component.smt_xor_quasidifferential_propagation_constraints(model) + + assert len(variables) == 55 + assert variables[0] == "mix_column_0_0_0" + assert variables[7] == "mix_column_0_0_7" + assert variables[8] == "qdt_mix_column_0_0_0" + assert variables[15] == "qdt_mix_column_0_0_7" + assert variables[16] == "qdt_dummy_1_qdt_mix_column_0_0_0" + assert variables[-1] == "qdt_dummy_6_qdt_mix_column_0_0_7" + + assert len(constraints) == 24 + + # Differences: the same constraints as the ordinary model. + assert constraints[:8] == [ + "(assert (= mix_column_0_0_0 (xor plaintext_0 plaintext_5)))", + "(assert (= mix_column_0_0_1 (xor plaintext_1 plaintext_6)))", + "(assert (= mix_column_0_0_2 (xor plaintext_2 plaintext_4 plaintext_7)))", + "(assert (= mix_column_0_0_3 (xor plaintext_3 plaintext_4)))", + "(assert (= mix_column_0_0_4 (xor plaintext_0 plaintext_1 plaintext_4)))", + "(assert (= mix_column_0_0_5 (xor plaintext_1 plaintext_2 plaintext_5)))", + "(assert (= mix_column_0_0_6 (xor plaintext_0 plaintext_2 plaintext_3 plaintext_6)))", + "(assert (= mix_column_0_0_7 (xor plaintext_0 plaintext_3 plaintext_7)))", + ] + + # Masks: propagated backwards through the transpose, via dummy + # variables carrying the qdt_ naming convention. + assert constraints[8] == ( + "(assert (= qdt_plaintext_0 qdt_dummy_0_qdt_mix_column_0_0_1 " + "qdt_dummy_0_qdt_mix_column_0_0_2 qdt_dummy_0_qdt_mix_column_0_0_4 " + "qdt_dummy_0_qdt_mix_column_0_0_6 qdt_dummy_0_qdt_mix_column_0_0_7))" + ) + assert constraints[15] == ( + "(assert (= qdt_plaintext_7 qdt_dummy_7_qdt_mix_column_0_0_0 " + "qdt_dummy_7_qdt_mix_column_0_0_2 qdt_dummy_7_qdt_mix_column_0_0_4 " + "qdt_dummy_7_qdt_mix_column_0_0_5))" + ) + assert constraints[16] == ( + "(assert (= qdt_mix_column_0_0_0 (xor qdt_dummy_1_qdt_mix_column_0_0_0 " + "qdt_dummy_3_qdt_mix_column_0_0_0 qdt_dummy_4_qdt_mix_column_0_0_0 " + "qdt_dummy_5_qdt_mix_column_0_0_0 qdt_dummy_6_qdt_mix_column_0_0_0 " + "qdt_dummy_7_qdt_mix_column_0_0_0)))" + ) + assert constraints[-1] == ( + "(assert (= qdt_mix_column_0_0_7 (xor qdt_dummy_0_qdt_mix_column_0_0_7 " + "qdt_dummy_1_qdt_mix_column_0_0_7 qdt_dummy_5_qdt_mix_column_0_0_7 " + "qdt_dummy_6_qdt_mix_column_0_0_7)))" + ) + + +def test_smt_xor_quasidifferential_propagation_constraints_restores_description(): + """ + MixColumn delegates to LinearLayer by temporarily swapping its + description for the transposed binary matrix. The swap must be + undone, otherwise a second call on the same component would work on + the wrong matrix. + """ + mix_column_component = make_mix_column_component() + model = SmtXorQuasidifferentialModel(make_mix_column_cipher()) + + description_before = list(mix_column_component.description) + mix_column_component.smt_xor_quasidifferential_propagation_constraints(model) + + assert list(mix_column_component.description) == description_before + + +def test_smt_xor_quasidifferential_propagation_constraints_is_idempotent(): + mix_column_component = make_mix_column_component() + model = SmtXorQuasidifferentialModel(make_mix_column_cipher()) + + first_variables, first_constraints = mix_column_component.smt_xor_quasidifferential_propagation_constraints(model) + second_variables, second_constraints = mix_column_component.smt_xor_quasidifferential_propagation_constraints(model) + + assert first_variables == second_variables + assert first_constraints == second_constraints \ No newline at end of file diff --git a/tests/unit/components/modadd_component_test.py b/tests/unit/components/modadd_component_test.py index 33f094b50..8474460de 100644 --- a/tests/unit/components/modadd_component_test.py +++ b/tests/unit/components/modadd_component_test.py @@ -3,7 +3,9 @@ MilpBitwiseDeterministicTruncatedXorDifferentialModel, ) from claasp.ciphers.single_component_ciphers.modadd_cipher import ModaddCipher - +from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import ( + SmtXorQuasidifferentialModel, +) def test_algebraic_polynomials(): cipher = ModaddCipher(word_bit_size=6, number_of_inputs=3) @@ -48,4 +50,31 @@ def test_milp_bitwise_deterministic_truncated_xor_differential_constraints(): assert str(constraints[0]) == 'x_48 <= 15' assert str(constraints[1]) == '0 <= x_48' assert str(constraints[-2]) == '2 <= 4 + x_47 - 4*x_157 + 4*x_160' - assert str(constraints[-1]) == 'x_157 <= x_15 + x_31' \ No newline at end of file + assert str(constraints[-1]) == 'x_157 <= x_15 + x_31' + +def test_smt_xor_quasidifferential_propagation_constraints(): + cipher = ModaddCipher(word_bit_size=2, number_of_inputs=2, modulus=4) + model = SmtXorQuasidifferentialModel(cipher) + modadd_component = cipher.component_from(0, 0) + variables, constraints = modadd_component.smt_xor_quasidifferential_propagation_constraints(model) + + assert len(variables) == 20 + assert variables[:4] == ['modadd_0_0_0', 'modadd_0_0_1', 'qdt_modadd_0_0_0', 'qdt_modadd_0_0_1'] + assert variables[-2:] == ['hw_qdt_modadd_0_0_0', 'hw_qdt_modadd_0_0_1'] + + assert len(constraints) == 23 + assert constraints[0] == '(assert (= modadd_aprime_modadd_0_0_0 (xor key_0 modadd_0_0_0)))' + + +def test_smt_xor_quasidifferential_propagation_constraints_more_than_two_operands(): + cipher = ModaddCipher(word_bit_size=2, number_of_inputs=3, modulus=4) + model = SmtXorQuasidifferentialModel(cipher) + modadd_component = cipher.component_from(0, 0) + + try: + modadd_component.smt_xor_quasidifferential_propagation_constraints(model) + raised = False + except NotImplementedError: + raised = True + + assert raised \ No newline at end of file diff --git a/tests/unit/components/modsub_component_test.py b/tests/unit/components/modsub_component_test.py index d7383a670..45599c0fb 100644 --- a/tests/unit/components/modsub_component_test.py +++ b/tests/unit/components/modsub_component_test.py @@ -2,7 +2,10 @@ from claasp.cipher_modules.models.algebraic.algebraic_model import AlgebraicModel from claasp.components.modsub_component import ModSub from claasp.name_mappings import PERMUTATION - +from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import ( + SmtXorQuasidifferentialModel, +) +from claasp.ciphers.single_component_ciphers.modsub_cipher import ModsubCipher def test_algebraic_polynomials(): cipher = Cipher("cipher_name", PERMUTATION, ["input"], [8], 8) @@ -101,3 +104,30 @@ def test_smt_constraints(): assert constraints[-2] == '(assert (= modsub_0_7_30 (xor modadd_0_4_30 temp_input_plaintext_62 ' \ 'carry_modsub_0_7_30)))' assert constraints[-1] == '(assert (= modsub_0_7_31 (xor modadd_0_4_31 temp_input_plaintext_63)))' + +def test_smt_xor_quasidifferential_propagation_constraints(): + cipher = ModsubCipher(word_bit_size=2, number_of_inputs=2, modulus=4) + model = SmtXorQuasidifferentialModel(cipher) + modsub_component = cipher.component_from(0, 0) + variables, constraints = modsub_component.smt_xor_quasidifferential_propagation_constraints(model) + + assert len(variables) == 20 + assert variables[:4] == ['modsub_0_0_0', 'modsub_0_0_1', 'qdt_modsub_0_0_0', 'qdt_modsub_0_0_1'] + assert variables[-2:] == ['hw_qdt_modsub_0_0_0', 'hw_qdt_modsub_0_0_1'] + + assert len(constraints) == 23 + assert constraints[0] == '(assert (= modsub_aprime_modsub_0_0_0 (xor key_0 plaintext_0)))' + + +def test_smt_xor_quasidifferential_propagation_constraints_more_than_two_operands(): + cipher = ModsubCipher(word_bit_size=2, number_of_inputs=3, modulus=4) + model = SmtXorQuasidifferentialModel(cipher) + modsub_component = cipher.component_from(0, 0) + + try: + modsub_component.smt_xor_quasidifferential_propagation_constraints(model) + raised = False + except NotImplementedError: + raised = True + + assert raised \ No newline at end of file diff --git a/tests/unit/components/not_component_test.py b/tests/unit/components/not_component_test.py index d71158d26..9e8b2a6b3 100644 --- a/tests/unit/components/not_component_test.py +++ b/tests/unit/components/not_component_test.py @@ -5,7 +5,9 @@ ) from claasp.ciphers.single_component_ciphers.not_cipher import NotCipher from claasp.components.not_component import Not - +from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import ( + SmtXorQuasidifferentialModel, +) def test_algebraic_polynomials(): cipher = NotCipher(bit_size=64) @@ -263,3 +265,17 @@ def test_milp_deterministic_truncated_xor_differential_constraints(): assert str(constraints[1]) == 'x_33 == x_1' assert str(constraints[-2]) == 'x_62 == x_30' assert str(constraints[-1]) == 'x_63 == x_31' + + +def test_smt_xor_quasidifferential_propagation_constraints(): + cipher = NotCipher(bit_size=2) + model = SmtXorQuasidifferentialModel(cipher) + not_component = cipher.component_from(0, 0) + variables, constraints = not_component.smt_xor_quasidifferential_propagation_constraints(model) + + assert variables == ['not_0_0_0', 'not_0_0_1', 'qdt_not_0_0_0', 'qdt_not_0_0_1'] + + assert constraints == ['(assert (= not_0_0_0 plaintext_0))', + '(assert (= not_0_0_1 plaintext_1))', + '(assert (= qdt_not_0_0_0 qdt_plaintext_0))', + '(assert (= qdt_not_0_0_1 qdt_plaintext_1))'] \ No newline at end of file diff --git a/tests/unit/components/or_component_test.py b/tests/unit/components/or_component_test.py index 303d3effd..9d588310a 100644 --- a/tests/unit/components/or_component_test.py +++ b/tests/unit/components/or_component_test.py @@ -2,7 +2,9 @@ from claasp.cipher_modules.models.cp.mzn_model import MznModel from claasp.ciphers.single_component_ciphers.or_cipher import OrCipher from claasp.components.or_component import Or - +from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import ( + SmtXorQuasidifferentialModel, +) def test_algebraic_polynomials(): cipher = OrCipher(word_bit_size=4, number_of_inputs=2) @@ -77,3 +79,30 @@ def test_smt_constraints(): assert constraints[1] == '(assert (= or_0_0_1 (or plaintext_1 key_1)))' assert constraints[-2] == '(assert (= or_0_0_2 (or plaintext_2 key_2)))' assert constraints[-1] == '(assert (= or_0_0_3 (or plaintext_3 key_3)))' + +def test_smt_xor_quasidifferential_propagation_constraints(): + cipher = OrCipher(word_bit_size=2, number_of_inputs=2) + model = SmtXorQuasidifferentialModel(cipher) + or_component = cipher.component_from(0, 0) + variables, constraints = or_component.smt_xor_quasidifferential_propagation_constraints(model) + + assert variables == ['or_0_0_0', 'or_0_0_1', 'qdt_or_0_0_0', 'qdt_or_0_0_1', + 'hw_qdt_or_0_0_0', 'hw_qdt_or_0_0_1'] + + assert len(constraints) == 8 + assert constraints[0] == '(assert (=> or_0_0_0 (or plaintext_0 key_0)))' + assert constraints[-1] == '(assert (= hw_qdt_or_0_0_1 (or plaintext_1 key_1 qdt_or_0_0_1)))' + + +def test_smt_xor_quasidifferential_propagation_constraints_more_than_two_operands(): + cipher = OrCipher(word_bit_size=2, number_of_inputs=3) + model = SmtXorQuasidifferentialModel(cipher) + or_component = cipher.component_from(0, 0) + + try: + or_component.smt_xor_quasidifferential_propagation_constraints(model) + raised = False + except NotImplementedError: + raised = True + + assert raised \ No newline at end of file diff --git a/tests/unit/components/permutation_component_test.py b/tests/unit/components/permutation_component_test.py index 7238f6011..c949ab4ff 100644 --- a/tests/unit/components/permutation_component_test.py +++ b/tests/unit/components/permutation_component_test.py @@ -11,6 +11,10 @@ from claasp.ciphers.single_component_ciphers.permutation_cipher import PermutationCipher from claasp.components.permutation_component import Permutation +from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import ( + SmtXorQuasidifferentialModel, +) + PERMUTATION = [1, 3, 2, 0] @@ -377,3 +381,31 @@ def test_milp_wordwise_deterministic_truncated_constraints(): assert len(variables) == 24 assert len(constraints) == 12 + +def test_smt_xor_quasidifferential_propagation_constraints(): + cipher = PermutationCipher(bit_size=4, permutation_description=PERMUTATION) + model = SmtXorQuasidifferentialModel(cipher) + permutation_component = cipher.component_from_id("permutation_0_0") + variables, constraints = permutation_component.smt_xor_quasidifferential_propagation_constraints(model) + + assert variables == [ + "permutation_0_0_0", + "permutation_0_0_1", + "permutation_0_0_2", + "permutation_0_0_3", + "qdt_permutation_0_0_0", + "qdt_permutation_0_0_1", + "qdt_permutation_0_0_2", + "qdt_permutation_0_0_3", + ] + + assert constraints == [ + "(assert (= permutation_0_0_0 plaintext_3))", + "(assert (= permutation_0_0_1 plaintext_0))", + "(assert (= permutation_0_0_2 plaintext_2))", + "(assert (= permutation_0_0_3 plaintext_1))", + "(assert (= qdt_permutation_0_0_0 qdt_plaintext_3))", + "(assert (= qdt_permutation_0_0_1 qdt_plaintext_0))", + "(assert (= qdt_permutation_0_0_2 qdt_plaintext_2))", + "(assert (= qdt_permutation_0_0_3 qdt_plaintext_1))", + ] diff --git a/tests/unit/components/rotate_component_test.py b/tests/unit/components/rotate_component_test.py index f0b822608..25829cafb 100644 --- a/tests/unit/components/rotate_component_test.py +++ b/tests/unit/components/rotate_component_test.py @@ -4,6 +4,9 @@ from claasp.cipher_modules.models.utils import integer_to_bit_list, set_fixed_variables from claasp.ciphers.single_component_ciphers.rotate_cipher import RotateCipher from claasp.components.rotate_component import Rotate +from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import ( + SmtXorQuasidifferentialModel, +) from claasp.name_mappings import XOR_DIFFERENTIAL @@ -46,6 +49,18 @@ class DummyModel: 'constraint rot_0_18[2] = input3[0];', 'constraint rot_0_18[3] = input0[0];'] +def test_smt_xor_quasidifferential_propagation_constraints(): + cipher = RotateCipher(bit_size=2, rotation_amount=1) + model = SmtXorQuasidifferentialModel(cipher) + rotate_component = cipher.component_from(0, 0) + variables, constraints = rotate_component.smt_xor_quasidifferential_propagation_constraints(model) + + assert variables == ['rot_0_0_0', 'rot_0_0_1', 'qdt_rot_0_0_0', 'qdt_rot_0_0_1'] + + assert constraints == ['(assert (= rot_0_0_0 plaintext_1))', + '(assert (= rot_0_0_1 plaintext_0))', + '(assert (= qdt_rot_0_0_0 qdt_plaintext_1))', + '(assert (= qdt_rot_0_0_1 qdt_plaintext_0))'] def _rotate(amount, bit_size=8): return Rotate(0, 0, ['input'], [list(range(bit_size))], bit_size, amount) diff --git a/tests/unit/components/sbox_component_test.py b/tests/unit/components/sbox_component_test.py index 1df821dfc..591aedcf0 100644 --- a/tests/unit/components/sbox_component_test.py +++ b/tests/unit/components/sbox_component_test.py @@ -10,12 +10,17 @@ from claasp.cipher_modules.models.milp.milp_models.milp_xor_linear_model import MilpXorLinearModel from claasp.cipher_modules.models.sat.sat_model import SatModel from claasp.cipher_modules.models.smt.smt_model import SmtModel +from claasp.ciphers.block_ciphers.rectangle_block_cipher import RectangleBlockCipher from claasp.ciphers.single_component_ciphers.sbox_cipher import SboxCipher from claasp.components.sbox_component import ( Sbox, cp_update_ddt_valid_probabilities, cp_update_lat_valid_probabilities, ) +from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import ( + SmtXorQuasidifferentialModel, +) + PRESENT_SBOX = [12, 5, 6, 11, 9, 0, 10, 13, 3, 14, 15, 8, 4, 7, 1, 2] @@ -440,3 +445,19 @@ def test_milp_wordwise_deterministic_truncated_xor_differential_simple_constrain assert str(variables[0]) == "('x_class[plaintext_word_0_class]', x_0)" assert constraints == [] + +def test_smt_xor_quasidifferential_propagation_constraints(): + cipher = RectangleBlockCipher(number_of_rounds=1) + model = SmtXorQuasidifferentialModel(cipher) + sbox_component = cipher.component_from_id('sbox_0_1') + variables, constraints = sbox_component.smt_xor_quasidifferential_propagation_constraints(model) + + assert variables == ['sbox_0_1_0', 'sbox_0_1_1', 'sbox_0_1_2', 'sbox_0_1_3', + 'qdt_sbox_0_1_0', 'qdt_sbox_0_1_1', 'qdt_sbox_0_1_2', 'qdt_sbox_0_1_3', + 'hw_qdt_sbox_0_1_0', 'hw_qdt_sbox_0_1_1', 'hw_qdt_sbox_0_1_2'] + + # The sbox constraint is a single disjunction over every valid QDT + # transition: it is millions of characters long, so only its shape + # is checked here. + assert len(constraints) == 1 + assert constraints[0].startswith('(assert (or') \ No newline at end of file diff --git a/tests/unit/components/shift_component_test.py b/tests/unit/components/shift_component_test.py index 57a4d8aa9..e2b79a648 100644 --- a/tests/unit/components/shift_component_test.py +++ b/tests/unit/components/shift_component_test.py @@ -9,7 +9,9 @@ ) from claasp.ciphers.single_component_ciphers.shift_cipher import ShiftCipher from claasp.components.shift_component import Shift - +from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import ( + SmtXorQuasidifferentialModel, +) def make_shift_component(bit_size=32, parameter=4): return Shift(0, 0, ['plaintext'], [list(range(bit_size))], bit_size, parameter) @@ -216,3 +218,15 @@ def test_milp_wordwise_deterministic_truncated_xor_differential_constraints(): assert str(variables[0]) == "('x_class[in0_word_0_class]', x_0)" assert "('x[shift_0_18_31]'" in str(variables[-1]) assert str(constraints[-1]).endswith('== 0') + +def test_smt_xor_quasidifferential_propagation_constraints(): + cipher = ShiftCipher(bit_size=2, shift_amount=1) + model = SmtXorQuasidifferentialModel(cipher) + shift_component = cipher.component_from(0, 0) + variables, constraints = shift_component.smt_xor_quasidifferential_propagation_constraints(model) + + assert variables == ['shift_0_0_0', 'shift_0_0_1', 'qdt_shift_0_0_0', 'qdt_shift_0_0_1'] + + assert len(constraints) == 4 + assert constraints[0] == '(assert (not shift_0_0_0))' + assert constraints[-1] == '(assert (not qdt_plaintext_1))' \ No newline at end of file diff --git a/tests/unit/components/xor_component_test.py b/tests/unit/components/xor_component_test.py index 45f17995d..8d6fd8eb8 100644 --- a/tests/unit/components/xor_component_test.py +++ b/tests/unit/components/xor_component_test.py @@ -8,7 +8,9 @@ ) from claasp.ciphers.single_component_ciphers.xor_cipher import XorCipher from claasp.components.xor_component import Xor, cp_build_truncated_table, generic_with_constant_sign_linear_constraints - +from claasp.cipher_modules.models.smt.smt_models.smt_xor_quasidifferential_model import ( + SmtXorQuasidifferentialModel, +) def test_cp_build_truncated_table(): assert cp_build_truncated_table(3) == 'array[0..4, 1..3] of int: xor_truncated_table_3 = ' \ @@ -187,3 +189,18 @@ def test_milp_wordwise_deterministic_truncated_xor_differential_simple_constrain assert str(constraints[1]) == '1 + x_0 + x_1 - 7*x_3 <= 2' assert str(constraints[-2]) == 'x_2 <= 2 + 6*x_6 + 6*x_7' assert str(constraints[-1]) == '2 <= x_2 + 6*x_6 + 6*x_7' + +def test_smt_xor_quasidifferential_propagation_constraints(): + cipher = XorCipher(word_bit_size=2, number_of_inputs=2) + model = SmtXorQuasidifferentialModel(cipher) + xor_component = cipher.component_from(0, 0) + variables, constraints = xor_component.smt_xor_quasidifferential_propagation_constraints(model) + + assert variables == ['xor_0_0_0', 'xor_0_0_1', 'qdt_xor_0_0_0', 'qdt_xor_0_0_1'] + + assert constraints == ['(assert (= xor_0_0_0 (xor plaintext_0 key_0)))', + '(assert (= xor_0_0_1 (xor plaintext_1 key_1)))', + '(assert (= qdt_plaintext_0 qdt_xor_0_0_0))', + '(assert (= qdt_key_0 qdt_xor_0_0_0))', + '(assert (= qdt_plaintext_1 qdt_xor_0_0_1))', + '(assert (= qdt_key_1 qdt_xor_0_0_1))'] \ No newline at end of file