Fix/two step trail search ublock - #480
Conversation
…olumns and permutation-based diffusion Add has_uniform_sboxes() and is_two_step_trail_search_friendly() to Cipher, replacing the overly restrictive is_spn() gate in mzn_model.py so that single-round ciphers (e.g. ToyAES 1-round) and ciphers with heterogeneous or permutation MixColumns (e.g. uBlock) are supported. Add _is_permutation_matrix() to MixColumn and short-circuit cp_xor_differential_propagation_first_step_constraints to emit O(n) equality constraints instead of the O(2^n) truncated table when the diffusion layer is a word permutation, avoiding a hang on 64-bit permutation matrices.
…e S-box first-step model - Add permutation component type to allowed set in has_uniform_sboxes(); remove rotation alignment check (key-schedule non-aligned rotations are irrelevant when key diff is fixed to 0) - Add cp_xor_differential_propagation_first_step_constraints to Permutation component: emits word-level max/OR constraints (output nibble active iff any contributing input nibble is active) - Guard cp_transform_xor_components_for_first_step against non-word-aligned XOR components (e.g. PRESENT 5-bit key-schedule counter XOR) by declaring the output and adding no constraints
solve_full_two_steps_xor_differential_model's attempt loop always returned after attempt 0 (no continue on UNSAT), so when the first step's relaxed active-S-box count wasn't realisable by any concrete trail (the common case for ciphers like uBlock where the word-level relaxation isn't tight), the second-step UNSAT solver output fell through to result parsing and crashed with KeyError instead of retrying with active_sboxes + 1. Also stop the per-attempt "-a"/"-p" command_options mutation from compounding across retries by taking a fresh copy of the base options each attempt.
juaninf
left a comment
juaninf
left a comment
There was a problem hiding this comment.
Since the description this PR will allows the two-technique on uBlock maybe adding a test will be good.
|
|
||
| if any(UNSATISFIABLE in line for line in solver_output) and weight not in (-1, 0): | ||
| if any(UNSATISFIABLE in line for line in solver_output): | ||
| if weight == -1: |
There was a problem hiding this comment.
do we need this if statement?
There was a problem hiding this comment.
Yes, we need it. weight == -1 is the first-step, active-S-box-count-only search: an UNSAT there just means this particular active-S-box count isn't realisable, so we retry with the next higher count (continue) instead of failing the whole search. For any other weight (including 0), UNSAT means no trail exists for that weight, so we return UNSATISFIABLE.
Note the old condition (weight not in (-1, 0)) was actually swallowing UNSAT for weight == 0 too, which looks like a latent bug — a fixed-weight-0 search that is genuinely unsatisfiable would previously fall through and try to parse an UNSAT solver output as if it were a solution. I narrowed the special case to just weight == -1 and added a clarifying comment.
There was a problem hiding this comment.
ok thanks maybe only we need to reword the last sentence "UNSAT means no trail exists for that weight, so we return UNSATISFIABLE." because UNSAT for weight > -1 means that no trail with that weight exists for a particular fixed S-box configuration. You can check in the code that when weight > -1 the actual CLAASP implementation is not enumerating every first step solution (different from the case when weight == -1)
…-search-ublock # Conflicts: # claasp/components/mix_column_component.py # claasp/components/permutation_component.py # tests/unit/cipher_test.py
|
Thanks for the review, @juaninf — replied inline to each comment. Summary of changes pushed in response:
|
Address review feedback: reword the ambiguous 'pattern' comment and explain why the weight == -1 branch is needed to retry the next active-S-box count instead of failing the whole search.
Extract a shared _uniform_sbox_size() helper used by both is_spn and has_uniform_sboxes, removing the duplicated sbox-uniformity check from has_uniform_sboxes so it only deals with the component-type-set check its name implies. Add SHIFT to has_uniform_sboxes' allowed component set so Mantis is recognized as two-step-trail-search friendly. Add pytests for the new behavior and to lock in the current conservative exclusion of LINEAR_LAYER-based ciphers (Skinny with larger tweakeys, Kalyna).
test_cp_xor_differential_first_step_uses_table_for_non_permutation_matrix asserted a 12-row truncated table (branch number 2) for a 2x2 MDS matrix, but branch_number correctly computes 3 for this matrix, producing a 6-row table. test_cp_xor_differential_propagation_first_step_constraints_returns_no_constraints_for_partial_word asserted an empty declarations/constraints result for a word-misaligned XOR component, but the method has no such short-circuit and always builds a truncated-table constraint; renamed and updated to match actual behavior. Cipher-level word alignment is already enforced upstream by is_two_step_trail_search_friendly().
|
There was a problem hiding this comment.
Pull request overview
This PR updates the CP/MiniZinc two-step XOR-differential trail search flow to use a new cipher capability check (is_two_step_trail_search_friendly) instead of a stricter SPN-only check, addressing failures for ciphers like uBlock. It also adds/updates unit tests around first-step constraint generation and the two-step solver retry behavior.
Changes:
- Add
Cipher.has_uniform_sboxes()andCipher.is_two_step_trail_search_friendly()and refactor SPN S-box-size handling via_uniform_sbox_size(). - Update
MznModelinitialization and first-step fixed-variable handling to gate onis_two_step_trail_search_friendly()(instead ofis_spn()). - Improve two-step trail solver loop to retry on UNSAT when searching by active S-box count, and add targeted unit tests for new/changed behaviors.
Reviewed changes
Copilot reviewed 10 out of 10 changed files in this pull request and generated 1 comment.
Show a summary per file
| File | Description |
|---|---|
| tests/unit/components/xor_component_test.py | Adds a regression test ensuring first-step XOR constraints handle partial-word truncation. |
| tests/unit/components/permutation_component_test.py | Adds tests for first-step constraints produced by permutation components under word-wise modeling. |
| tests/unit/components/mix_column_component_test.py | Adds tests for permutation-matrix detection and first-step constraint strategy selection (equalities vs table). |
| tests/unit/cipher_test.py | Updates algebraic test parameters and adds tests for has_uniform_sboxes() / is_two_step_trail_search_friendly(). |
| tests/unit/cipher_modules/models/cp/mzn_models/mzn_xor_differential_trail_search_fixing_number_of_active_sboxes_model_test.py | Adds tests validating UNSAT retry behavior and UNSAT return for fixed weight. |
| tests/unit/cipher_modules/models/cp/mzn_model_test.py | Adds tests ensuring two-step-friendly ciphers set word size appropriately and first-step fixing uses the new friendliness check. |
| claasp/components/permutation_component.py | Minor docstring formatting change. |
| claasp/cipher.py | Introduces _uniform_sbox_size, has_uniform_sboxes, and is_two_step_trail_search_friendly to better characterize cipher compatibility. |
| claasp/cipher_modules/models/cp/mzn_models/mzn_xor_differential_trail_search_fixing_number_of_active_sboxes_model.py | Adjusts two-step solving loop to retry on UNSAT when searching by active S-box count; refactors solver command options handling. |
| claasp/cipher_modules/models/cp/mzn_model.py | Switches from is_spn() to is_two_step_trail_search_friendly() for first-step-related behavior and word-size initialization. |
Comments suppressed due to low confidence (2)
claasp/cipher_modules/models/cp/mzn_model.py:104
- In
initialise_model,word_sizeis derived fromcomponent.output_bit_size, but the two-step trail search friendliness check (andCipher.get_sizes_of_components_by_type) define the word size based on the S-box input size. For non-square S-boxes this can make first-step constraints compute incorrect word indices/lengths.
This issue also appears on line 431 of the same file.
if self._cipher.is_two_step_trail_search_friendly():
for component in self._cipher.get_all_components():
if SBOX in component.type:
self.word_size = int(component.output_bit_size)
break
claasp/cipher_modules/models/cp/mzn_model.py:432
- The first-step branch now checks
is_two_step_trail_search_friendly(), but the exception message still says "Cipher is not SPN", which is misleading and makes debugging harder (e.g., Present would fail SPN but be two-step friendly).
if not self._cipher.is_two_step_trail_search_friendly():
raise ValueError("Cipher is not SPN")
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| for i in range(len(CP_SOLVERS_EXTERNAL)): | ||
| if second_step_solver_name == CP_SOLVERS_EXTERNAL[i]["solver_name"]: | ||
| command_options = deepcopy(CP_SOLVERS_EXTERNAL[i]["keywords"]["command"]) | ||
| base_command_options = CP_SOLVERS_EXTERNAL[i]["keywords"]["command"] | ||
|
|
||
| for attempt in range(10000): | ||
| command_options = deepcopy(base_command_options) |
| """ | ||
| if not self.has_uniform_sboxes(): | ||
| return False | ||
| word_size = next(c.input_bit_size for c in self.get_all_components() if c.type == SBOX) |
There was a problem hiding this comment.
In the model itself, the word_size is instead derived from the output the Sbox:
https://github.com/Crypto-TII/claasp/pull/480/changes#diff-5e2f4dd67c51422f6b06ec17cb3b9598fe45a526fab5d5f42e2e79ffe9ec177cL103
Using the input here is fine for square Sboxes but for non-square ones like in DES, the constraints may not line up properly. For safety, maybe we can add an extra check in has_uniform_sboxes that the SBox should be square
| Key schedule components with non-aligned rotations do not affect correctness when key | ||
| differences are fixed to zero (the standard setting for differential trail searches). |
There was a problem hiding this comment.
I think we should at least raise a warning for runs where the cipher has non-word-aligned rotations in the key schedule (e.g LBlock)
Co-authored-by: Paul Huynh <126582157+p-huynh@users.noreply.github.com>
Fixes error when trying to apply the two steps approach to the uBlock block cipher.
Replaced is_spn check with is_two_steps_approach_friendly.