Skip to content

Commit

Permalink
FEATURE/Add: Adding semi-deterministic truncated model
Browse files Browse the repository at this point in the history 
This feature implements a heuristic to compute truncated xor differential trails using on ARX ciphers using SAT techniques.
  • Loading branch information
@juaninf
juaninf committed Jan 16, 2025
1 parent cb2c6ab commit cbc559d
Show file tree
Hide file tree
Showing 8 changed files with 673 additions and 0 deletions.
292 changes: 292 additions & 0 deletions ..._modules/models/sat/sat_models/sat_semi_deterministic_truncated_xor_differential_model.py
View file

Large diffs are not rendered by default.

254 changes: 254 additions & 0 deletions claasp/cipher_modules/models/sat/utils/utils.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -851,3 +851,257 @@ def _update_component_model_types_for_linear_components(component_model_types, l
for component_model_type in component_model_types:
if component_model_type["component_id"] in linear_components:
component_model_type["model_type"] = "sat_xor_linear_mask_propagation_constraints"


def get_semi_deterministic_cnf_window_0(
A_t0, A_t1, A_v0, A_v1,
B_t0, B_t1, B_v0, B_v1,
C_t0, C_t1, C_v0, C_v1,
p0, q0, r0
):
return [
f'{C_v1} {B_t1} {C_t0} {B_v0} {A_v0} {A_t0} {A_t1} {B_v1} -{C_v0} {A_v1} {B_t0}',
f'{C_v1} {B_t1} {C_t0} {B_v0} -{A_v0} {A_t0} {A_t1} {B_v1} {C_v0} {A_v1} {B_t0}',
f'{C_v1} {B_t1} {C_t0} -{B_v0} {A_v0} {A_t0} {A_t1} {B_v1} {C_v0} {A_v1} {B_t0}',
f'{C_v1} {B_t1} {C_t0} -{B_v0} -{A_v0} {A_t0} {A_t1} {B_v1} -{C_v0} {A_v1} {B_t0}',
f'{C_v1} {B_t1} -{C_t0} {A_t1} {B_v1} {A_v1} {C_t1}',
f'{C_v1} {B_t1} -{p0} {A_t1} {B_v1} {A_v1}',
f'{C_v1} {B_t1} {B_v0} {A_v0} {A_t1} {B_v1} -{C_v0} {A_v1} {C_t1}',
f'{C_v1} {B_t1} {B_v0} -{A_v0} {A_t1} {B_v1} {C_v0} {A_v1} {C_t1}',
f'{C_v1} {B_t1} -{B_v0} {A_v0} {A_t1} {B_v1} {C_v0} {A_v1} {C_t1}',
f'{C_v1} {B_t1} -{B_v0} -{A_v0} {A_t1} {B_v1} -{C_v0} {A_v1} {C_t1}',
f'{C_v1} {B_t1} -{r0} {A_t1} {B_v1} {A_v1}',
f'{C_v1} {B_t1} -{A_t0} {A_t1} {B_v1} {A_v1} {C_t1}',
f'{C_v1} {B_t1} {A_t1} {B_v1} {A_v1} -{B_t0} {C_t1}',
f'{C_v1} {C_t0} {p0} {B_v0} {A_v0} {A_t0} -{C_v0} {B_t0}',
f'{C_v1} {C_t0} {p0} {B_v0} -{A_v0} {A_t0} {C_v0} {B_t0}',
f'{C_v1} {C_t0} {p0} -{B_v0} {A_v0} {A_t0} {C_v0} {B_t0}',
f'{C_v1} {C_t0} {p0} -{B_v0} -{A_v0} {A_t0} -{C_v0} {B_t0}',
f'{C_v1} {C_t0} {p0} {A_t0} -{B_v1} {B_t0}',
f'{C_v1} {C_t0} {p0} {A_t0} -{A_v1} {B_t0}',
f'{C_v1} {C_t0} {B_v0} {r0} {A_v0} {A_t0} -{C_v0} {B_t0}',
f'{C_v1} {C_t0} {B_v0} {r0} -{A_v0} {A_t0} {C_v0} {B_t0}',
f'{C_v1} {C_t0} -{B_v0} {r0} {A_v0} {A_t0} {C_v0} {B_t0}',
f'{C_v1} {C_t0} -{B_v0} {r0} -{A_v0} {A_t0} -{C_v0} {B_t0}',
f'{C_v1} {C_t0} {r0} {A_t0} -{B_v1} {B_t0}',
f'{C_v1} {C_t0} {r0} {A_t0} -{A_v1} {B_t0}',
f'-{C_v1} {B_t1} -{C_t0} {A_t1} -{B_v1} -{A_v1} {C_t1}',
f'-{C_v1} {B_t1} -{p0} {A_t1} -{B_v1} -{A_v1} {C_t1}',
f'-{C_v1} {B_t1} {B_v0} {A_v0} {A_t1} -{B_v1} {C_v0} -{A_v1} {C_t1}',
f'-{C_v1} {B_t1} {B_v0} -{A_v0} {A_t1} -{B_v1} -{C_v0} -{A_v1} {C_t1}',
f'-{C_v1} {B_t1} -{B_v0} {A_v0} {A_t1} -{B_v1} -{C_v0} -{A_v1} {C_t1}',
f'-{C_v1} {B_t1} -{B_v0} -{A_v0} {A_t1} -{B_v1} {C_v0} -{A_v1} {C_t1}',
f'-{C_v1} {B_t1} -{r0} {A_t1} -{B_v1} -{A_v1} {C_t1}',
f'-{C_v1} {B_t1} -{A_t0} {A_t1} -{B_v1} -{A_v1} {C_t1}',
f'-{C_v1} {B_t1} {A_t1} -{B_v1} -{A_v1} -{B_t0} {C_t1}',
f'-{C_v1} {C_t0} {p0} {B_v0} {A_v0} {A_t0} {C_v0} {B_t0}',
f'-{C_v1} {C_t0} {p0} {B_v0} -{A_v0} {A_t0} -{C_v0} {B_t0}',
f'-{C_v1} {C_t0} {p0} -{B_v0} {A_v0} {A_t0} -{C_v0} {B_t0}',
f'-{C_v1} {C_t0} {p0} -{B_v0} -{A_v0} {A_t0} {C_v0} {B_t0}',
f'-{C_v1} {C_t0} {p0} {A_t0} {B_v1} {B_t0}',
f'-{C_v1} {C_t0} {p0} {A_t0} {A_v1} {B_t0}',
f'-{C_v1} {C_t0} {B_v0} {r0} {A_v0} {A_t0} {C_v0} {B_t0}',
f'-{C_v1} {C_t0} {B_v0} {r0} -{A_v0} {A_t0} -{C_v0} {B_t0}',
f'-{C_v1} {C_t0} -{B_v0} {r0} {A_v0} {A_t0} -{C_v0} {B_t0}',
f'-{C_v1} {C_t0} -{B_v0} {r0} -{A_v0} {A_t0} {C_v0} {B_t0}',
f'-{C_v1} {C_t0} {r0} {A_t0} {B_v1} {B_t0}',
f'-{C_v1} {C_t0} {r0} {A_t0} {A_v1} {B_t0}',
f'{B_t1} {C_t0} {A_t0} {A_t1} {B_v1} {A_v1} {B_t0} -{C_t1}',
f'{B_t1} -{p0} {A_t1} {B_v1} {A_v1} -{C_t1}',
f'{B_t1} -{r0} {A_t1} {B_v1} {A_v1} -{C_t1}',
f'-{B_t1} {C_t0} {p0} {A_t0} {B_t0}',
f'-{B_t1} {C_t0} {r0} {A_t0} {B_t0}',
f'{C_t0} {p0} {B_v0} {A_v0} {A_t0} {B_v1} -{C_v0} {B_t0}',
f'{C_t0} {p0} {B_v0} {A_v0} {A_t0} -{B_v1} {C_v0} {B_t0}',
f'{C_t0} {p0} {B_v0} {A_v0} {A_t0} {C_v0} -{A_v1} {B_t0}',
f'{C_t0} {p0} {B_v0} {A_v0} {A_t0} -{C_v0} {A_v1} {B_t0}',
f'{C_t0} {p0} {B_v0} -{A_v0} {A_t0} {B_v1} {C_v0} {B_t0}',
f'{C_t0} {p0} {B_v0} -{A_v0} {A_t0} -{B_v1} -{C_v0} {B_t0}',
f'{C_t0} {p0} {B_v0} -{A_v0} {A_t0} {C_v0} {A_v1} {B_t0}',
f'{C_t0} {p0} {B_v0} -{A_v0} {A_t0} -{C_v0} -{A_v1} {B_t0}',
f'{C_t0} {p0} -{B_v0} {A_v0} {A_t0} {B_v1} {C_v0} {B_t0}',
f'{C_t0} {p0} -{B_v0} {A_v0} {A_t0} -{B_v1} -{C_v0} {B_t0}',
f'{C_t0} {p0} -{B_v0} {A_v0} {A_t0} {C_v0} {A_v1} {B_t0}',
f'{C_t0} {p0} -{B_v0} {A_v0} {A_t0} -{C_v0} -{A_v1} {B_t0}',
f'{C_t0} {p0} -{B_v0} -{A_v0} {A_t0} {B_v1} -{C_v0} {B_t0}',
f'{C_t0} {p0} -{B_v0} -{A_v0} {A_t0} -{B_v1} {C_v0} {B_t0}',
f'{C_t0} {p0} -{B_v0} -{A_v0} {A_t0} {C_v0} -{A_v1} {B_t0}',
f'{C_t0} {p0} -{B_v0} -{A_v0} {A_t0} -{C_v0} {A_v1} {B_t0}',
f'{C_t0} {p0} {A_t0} -{A_t1} {B_t0}',
f'{C_t0} {p0} {A_t0} {B_v1} -{A_v1} {B_t0}',
f'{C_t0} {p0} {A_t0} -{B_v1} {A_v1} {B_t0}',
f'{C_t0} {p0} {A_t0} {B_t0} -{C_t1}',
f'{C_t0} {B_v0} {r0} {A_v0} {A_t0} {B_v1} -{C_v0} {B_t0}',
f'{C_t0} {B_v0} {r0} {A_v0} {A_t0} -{B_v1} {C_v0} {B_t0}',
f'{C_t0} {B_v0} {r0} {A_v0} {A_t0} {C_v0} -{A_v1} {B_t0}',
f'{C_t0} {B_v0} {r0} {A_v0} {A_t0} -{C_v0} {A_v1} {B_t0}',
f'{C_t0} {B_v0} {r0} -{A_v0} {A_t0} {B_v1} {C_v0} {B_t0}',
f'{C_t0} {B_v0} {r0} -{A_v0} {A_t0} -{B_v1} -{C_v0} {B_t0}',
f'{C_t0} {B_v0} {r0} -{A_v0} {A_t0} {C_v0} {A_v1} {B_t0}',
f'{C_t0} {B_v0} {r0} -{A_v0} {A_t0} -{C_v0} -{A_v1} {B_t0}',
f'{C_t0} -{B_v0} {r0} {A_v0} {A_t0} {B_v1} {C_v0} {B_t0}',
f'{C_t0} -{B_v0} {r0} {A_v0} {A_t0} -{B_v1} -{C_v0} {B_t0}',
f'{C_t0} -{B_v0} {r0} {A_v0} {A_t0} {C_v0} {A_v1} {B_t0}',
f'{C_t0} -{B_v0} {r0} {A_v0} {A_t0} -{C_v0} -{A_v1} {B_t0}',
f'{C_t0} -{B_v0} {r0} -{A_v0} {A_t0} {B_v1} -{C_v0} {B_t0}',
f'{C_t0} -{B_v0} {r0} -{A_v0} {A_t0} -{B_v1} {C_v0} {B_t0}',
f'{C_t0} -{B_v0} {r0} -{A_v0} {A_t0} {C_v0} -{A_v1} {B_t0}',
f'{C_t0} -{B_v0} {r0} -{A_v0} {A_t0} -{C_v0} {A_v1} {B_t0}',
f'{C_t0} {r0} {A_t0} -{A_t1} {B_t0}',
f'{C_t0} {r0} {A_t0} {B_v1} -{A_v1} {B_t0}',
f'{C_t0} {r0} {A_t0} -{B_v1} {A_v1} {B_t0}',
f'{C_t0} {r0} {A_t0} {B_t0} -{C_t1}',
f'-{C_t0} -{p0}',
f'-{C_t0} -{r0}',
f'-{q0}',
f'{p0} -{r0}',
f'-{p0} {r0}',
f'-{p0} -{A_t0}',
f'-{p0} -{B_t0}',
f'-{r0} -{A_t0}',
f'-{r0} -{B_t0}'
]


def get_cnf_semi_deterministic_window_1(
A_t0, A_t1, A_t2, A_v0, A_v1, A_v2,
B_t0, B_t1, B_t2, B_v0, B_v1, B_v2,
C_t0, C_t1, C_t2, C_v0, C_v1,
p0, q0, r0
):
return [
f'{C_v1} {A_t1} {A_v1} {A_t0} {B_t1} {C_t0} {B_t0} {A_v0} {B_v1} {B_v0} -{C_v0}',
f'{C_v1} {A_t1} {A_v1} {A_t0} {B_t1} {C_t0} {B_t0} {A_v0} {B_v1} -{B_v0} {C_v0}',
f'{C_v1} {A_t1} {A_v1} {A_t0} {B_t1} {C_t0} {B_t0} -{A_v0} {B_v1} {B_v0} {C_v0}',
f'{C_v1} {A_t1} {A_v1} {A_t0} {B_t1} {C_t0} {B_t0} -{A_v0} {B_v1} -{B_v0} -{C_v0}',
f'{C_v1} {A_t1} {A_v1} -{A_t0} {C_t1} {B_t1} {B_v1}',
f'{C_v1} {A_t1} {A_v1} {C_t1} {B_t1} -{C_t0} {B_v1}',
f'{C_v1} {A_t1} {A_v1} {C_t1} {B_t1} -{B_t0} {B_v1}',
f'{C_v1} {A_t1} {A_v1} {C_t1} {B_t1} {A_v0} {B_v1} {B_v0} -{C_v0}',
f'{C_v1} {A_t1} {A_v1} {C_t1} {B_t1} {A_v0} {B_v1} -{B_v0} {C_v0}',
f'{C_v1} {A_t1} {A_v1} {C_t1} {B_t1} -{A_v0} {B_v1} {B_v0} {C_v0}',
f'{C_v1} {A_t1} {A_v1} {C_t1} {B_t1} -{A_v0} {B_v1} -{B_v0} -{C_v0}',
f'{C_v1} {A_t1} {A_v1} {C_t1} {B_t1} -{p0} {B_v1}',
f'{C_v1} {A_t1} {A_v1} -{r0} {B_t1} {B_v1}',
f'{C_v1} {A_t1} {A_v1} {A_v2} {B_t1} -{C_t2} {A_t2} {B_t2} {B_v2} -{p0} {B_v1}',
f'{C_v1} {A_t1} {A_v1} {B_t1} {A_v0} -{p0} {B_v1} {B_v0} -{C_v0}',
f'{C_v1} {A_t1} {A_v1} {B_t1} {A_v0} -{p0} {B_v1} -{B_v0} {C_v0}',
f'{C_v1} {A_t1} {A_v1} {B_t1} -{A_v0} -{p0} {B_v1} {B_v0} {C_v0}',
f'{C_v1} {A_t1} {A_v1} {B_t1} -{A_v0} -{p0} {B_v1} -{B_v0} -{C_v0}',
f'{C_v1} -{A_v1} {A_t0} {r0} {C_t0} {B_t0}',
f'{C_v1} -{A_v1} {A_t0} {C_t0} {B_t0} {p0}',
f'{C_v1} {A_t0} {r0} {C_t0} {B_t0} {A_v0} {B_v0} -{C_v0}',
f'{C_v1} {A_t0} {r0} {C_t0} {B_t0} {A_v0} -{B_v0} {C_v0}',
f'{C_v1} {A_t0} {r0} {C_t0} {B_t0} -{A_v0} {B_v0} {C_v0}',
f'{C_v1} {A_t0} {r0} {C_t0} {B_t0} -{A_v0} -{B_v0} -{C_v0}',
f'{C_v1} {A_t0} {r0} {C_t0} {B_t0} -{B_v1}',
f'{C_v1} {A_t0} {C_t0} {B_t0} {A_v0} {p0} {B_v0} -{C_v0}',
f'{C_v1} {A_t0} {C_t0} {B_t0} {A_v0} {p0} -{B_v0} {C_v0}',
f'{C_v1} {A_t0} {C_t0} {B_t0} -{A_v0} {p0} {B_v0} {C_v0}',
f'{C_v1} {A_t0} {C_t0} {B_t0} -{A_v0} {p0} -{B_v0} -{C_v0}',
f'{C_v1} {A_t0} {C_t0} {B_t0} {p0} -{B_v1}',
f'-{C_v1} {A_t1} -{A_v1} -{A_t0} {C_t1} {B_t1} -{B_v1}',
f'-{C_v1} {A_t1} -{A_v1} {C_t1} -{r0} {B_t1} -{B_v1}',
f'-{C_v1} {A_t1} -{A_v1} {C_t1} {B_t1} -{C_t0} -{B_v1}',
f'-{C_v1} {A_t1} -{A_v1} {C_t1} {B_t1} -{B_t0} -{B_v1}',
f'-{C_v1} {A_t1} -{A_v1} {C_t1} {B_t1} {A_v0} -{B_v1} {B_v0} {C_v0}',
f'-{C_v1} {A_t1} -{A_v1} {C_t1} {B_t1} {A_v0} -{B_v1} -{B_v0} -{C_v0}',
f'-{C_v1} {A_t1} -{A_v1} {C_t1} {B_t1} -{A_v0} -{B_v1} {B_v0} -{C_v0}',
f'-{C_v1} {A_t1} -{A_v1} {C_t1} {B_t1} -{A_v0} -{B_v1} -{B_v0} {C_v0}',
f'-{C_v1} {A_t1} -{A_v1} {C_t1} {B_t1} -{p0} -{B_v1}',
f'-{C_v1} {A_v1} {A_t0} {C_t1} {r0} {C_t0} {B_t0}',
f'-{C_v1} {A_v1} {A_t0} {r0} {A_v2} {C_t0} {B_t0} -{C_t2} {A_t2} {B_t2} {B_v2}',
f'-{C_v1} {A_v1} {A_t0} {C_t0} {B_t0} {p0}',
f'-{C_v1} {A_t0} {C_t1} {r0} {C_t0} {B_t0} {A_v0} {B_v0} {C_v0}',
f'-{C_v1} {A_t0} {C_t1} {r0} {C_t0} {B_t0} {A_v0} -{B_v0} -{C_v0}',
f'-{C_v1} {A_t0} {C_t1} {r0} {C_t0} {B_t0} -{A_v0} {B_v0} -{C_v0}',
f'-{C_v1} {A_t0} {C_t1} {r0} {C_t0} {B_t0} -{A_v0} -{B_v0} {C_v0}',
f'-{C_v1} {A_t0} {C_t1} {r0} {C_t0} {B_t0} {B_v1}',
f'-{C_v1} {A_t0} {r0} {A_v2} {C_t0} {B_t0} {A_v0} -{C_t2} {A_t2} {B_t2} {B_v2} {B_v0} {C_v0}',
f'-{C_v1} {A_t0} {r0} {A_v2} {C_t0} {B_t0} {A_v0} -{C_t2} {A_t2} {B_t2} {B_v2} -{B_v0} -{C_v0}',
f'-{C_v1} {A_t0} {r0} {A_v2} {C_t0} {B_t0} -{A_v0} -{C_t2} {A_t2} {B_t2} {B_v2} {B_v0} -{C_v0}',
f'-{C_v1} {A_t0} {r0} {A_v2} {C_t0} {B_t0} -{A_v0} -{C_t2} {A_t2} {B_t2} {B_v2} -{B_v0} {C_v0}',
f'-{C_v1} {A_t0} {r0} {A_v2} {C_t0} {B_t0} -{C_t2} {A_t2} {B_t2} {B_v2} {B_v1}',
f'-{C_v1} {A_t0} {C_t0} {B_t0} {A_v0} {p0} {B_v0} {C_v0}',
f'-{C_v1} {A_t0} {C_t0} {B_t0} {A_v0} {p0} -{B_v0} -{C_v0}',
f'-{C_v1} {A_t0} {C_t0} {B_t0} -{A_v0} {p0} {B_v0} -{C_v0}',
f'-{C_v1} {A_t0} {C_t0} {B_t0} -{A_v0} {p0} -{B_v0} {C_v0}',
f'-{C_v1} {A_t0} {C_t0} {B_t0} {p0} {B_v1}',
f'{A_t1} {A_v1} {A_t0} -{C_t1} {A_v2} {B_t1} {C_t0} {B_t0} -{C_t2} {A_t2} {B_t2} {B_v2} {B_v1}',
f'{A_t1} {A_v1} {A_t0} -{C_t1} {B_t1} {C_t0} {B_t0} {A_v0} {B_v1} {B_v0} -{C_v0}',
f'{A_t1} {A_v1} {A_t0} -{C_t1} {B_t1} {C_t0} {B_t0} {A_v0} {B_v1} -{B_v0} {C_v0}',
f'{A_t1} {A_v1} {A_t0} -{C_t1} {B_t1} {C_t0} {B_t0} -{A_v0} {B_v1} {B_v0} {C_v0}',
f'{A_t1} {A_v1} {A_t0} -{C_t1} {B_t1} {C_t0} {B_t0} -{A_v0} {B_v1} -{B_v0} -{C_v0}',
f'{A_t1} {A_v1} -{C_t1} -{r0} {B_t1} {B_v1}',
f'{A_t1} {A_v1} -{C_t1} {A_v2} {B_t1} -{C_t2} {A_t2} {B_t2} {B_v2} -{p0} {B_v1}',
f'{A_t1} {A_v1} -{C_t1} {B_t1} {A_v0} -{p0} {B_v1} {B_v0} -{C_v0}',
f'{A_t1} {A_v1} -{C_t1} {B_t1} {A_v0} -{p0} {B_v1} -{B_v0} {C_v0}',
f'{A_t1} {A_v1} -{C_t1} {B_t1} -{A_v0} -{p0} {B_v1} {B_v0} {C_v0}',
f'{A_t1} {A_v1} -{C_t1} {B_t1} -{A_v0} -{p0} {B_v1} -{B_v0} -{C_v0}',
f'-{A_t1} {A_t0} {r0} {C_t0} {B_t0}',
f'-{A_t1} {A_t0} {C_t0} {B_t0} {p0}',
f'-{A_t1} {r0} -{p0}',
f'{A_v1} {A_t0} {r0} {C_t0} {B_t0} {A_v0} {B_v0} -{C_v0}',
f'{A_v1} {A_t0} {r0} {C_t0} {B_t0} {A_v0} -{B_v0} {C_v0}',
f'{A_v1} {A_t0} {r0} {C_t0} {B_t0} -{A_v0} {B_v0} {C_v0}',
f'{A_v1} {A_t0} {r0} {C_t0} {B_t0} -{A_v0} -{B_v0} -{C_v0}',
f'{A_v1} {A_t0} {r0} {C_t0} {B_t0} -{B_v1}',
f'{A_v1} {A_t0} {C_t0} {B_t0} {A_v0} {p0} {B_v0} -{C_v0}',
f'{A_v1} {A_t0} {C_t0} {B_t0} {A_v0} {p0} -{B_v0} {C_v0}',
f'{A_v1} {A_t0} {C_t0} {B_t0} -{A_v0} {p0} {B_v0} {C_v0}',
f'{A_v1} {A_t0} {C_t0} {B_t0} -{A_v0} {p0} -{B_v0} -{C_v0}',
f'{A_v1} {A_t0} {C_t0} {B_t0} {p0} -{B_v1}',
f'-{A_v1} {A_t0} -{C_t1} {r0} {C_t0} {B_t0}',
f'-{A_v1} {A_t0} {r0} {C_t0} {B_t0} {A_v0} {B_v0} {C_v0}',
f'-{A_v1} {A_t0} {r0} {C_t0} {B_t0} {A_v0} -{B_v0} -{C_v0}',
f'-{A_v1} {A_t0} {r0} {C_t0} {B_t0} -{A_v0} {B_v0} -{C_v0}',
f'-{A_v1} {A_t0} {r0} {C_t0} {B_t0} -{A_v0} -{B_v0} {C_v0}',
f'-{A_v1} {A_t0} {r0} {C_t0} {B_t0} {B_v1}',
f'-{A_v1} {A_t0} {C_t0} {B_t0} {A_v0} {p0} {B_v0} {C_v0}',
f'-{A_v1} {A_t0} {C_t0} {B_t0} {A_v0} {p0} -{B_v0} -{C_v0}',
f'-{A_v1} {A_t0} {C_t0} {B_t0} -{A_v0} {p0} {B_v0} -{C_v0}',
f'-{A_v1} {A_t0} {C_t0} {B_t0} -{A_v0} {p0} -{B_v0} {C_v0}',
f'-{A_v1} {A_t0} {C_t0} {B_t0} {p0} {B_v1}',
f'-{A_v1} {r0} -{p0}',
f'{A_t0} -{C_t1} {r0} {A_v2} {C_t0} {B_t0} -{C_t2} {A_t2} {B_t2} {B_v2}',
f'{A_t0} -{C_t1} {r0} {C_t0} {B_t0} {A_v0} {B_v0} -{C_v0}',
f'{A_t0} -{C_t1} {r0} {C_t0} {B_t0} {A_v0} -{B_v0} {C_v0}',
f'{A_t0} -{C_t1} {r0} {C_t0} {B_t0} -{A_v0} {B_v0} {C_v0}',
f'{A_t0} -{C_t1} {r0} {C_t0} {B_t0} -{A_v0} -{B_v0} -{C_v0}',
f'{A_t0} -{C_t1} {r0} {C_t0} {B_t0} -{B_v1}',
f'{A_t0} -{C_t1} {C_t0} {B_t0} {p0}',
f'{A_t0} {r0} -{B_t1} {C_t0} {B_t0}',
f'{A_t0} {r0} {C_t0} {B_t0} {A_v0} {B_v1} {B_v0} -{C_v0}',
f'{A_t0} {r0} {C_t0} {B_t0} {A_v0} {B_v1} -{B_v0} {C_v0}',
f'{A_t0} {r0} {C_t0} {B_t0} {A_v0} -{B_v1} {B_v0} {C_v0}',
f'{A_t0} {r0} {C_t0} {B_t0} {A_v0} -{B_v1} -{B_v0} -{C_v0}',
f'{A_t0} {r0} {C_t0} {B_t0} -{A_v0} {B_v1} {B_v0} {C_v0}',
f'{A_t0} {r0} {C_t0} {B_t0} -{A_v0} {B_v1} -{B_v0} -{C_v0}',
f'{A_t0} {r0} {C_t0} {B_t0} -{A_v0} -{B_v1} {B_v0} -{C_v0}',
f'{A_t0} {r0} {C_t0} {B_t0} -{A_v0} -{B_v1} -{B_v0} {C_v0}',
f'{A_t0} -{B_t1} {C_t0} {B_t0} {p0}',
f'{A_t0} {C_t0} {B_t0} {A_v0} {p0} {B_v1} {B_v0} -{C_v0}',
f'{A_t0} {C_t0} {B_t0} {A_v0} {p0} {B_v1} -{B_v0} {C_v0}',
f'{A_t0} {C_t0} {B_t0} {A_v0} {p0} -{B_v1} {B_v0} {C_v0}',
f'{A_t0} {C_t0} {B_t0} {A_v0} {p0} -{B_v1} -{B_v0} -{C_v0}',
f'{A_t0} {C_t0} {B_t0} -{A_v0} {p0} {B_v1} {B_v0} {C_v0}',
f'{A_t0} {C_t0} {B_t0} -{A_v0} {p0} {B_v1} -{B_v0} -{C_v0}',
f'{A_t0} {C_t0} {B_t0} -{A_v0} {p0} -{B_v1} {B_v0} -{C_v0}',
f'{A_t0} {C_t0} {B_t0} -{A_v0} {p0} -{B_v1} -{B_v0} {C_v0}',
f'-{A_t0} -{r0}',
f'-{A_t0} -{p0}',
f'{C_t1} {r0} -{p0}',
f'{r0} {A_v2} -{C_t2} {A_t2} {B_t2} {B_v2} -{p0}',
f'{r0} -{B_t1} -{p0}',
f'{r0} {A_v0} -{p0} {B_v0} -{C_v0}',
f'{r0} {A_v0} -{p0} -{B_v0} {C_v0}',
f'{r0} -{A_v0} -{p0} {B_v0} {C_v0}',
f'{r0} -{A_v0} -{p0} -{B_v0} -{C_v0}',
f'{r0} -{p0} -{B_v1}',
f'-{r0} -{C_t0}',
f'-{r0} -{B_t0}',
f'-{r0} {p0}',
f'-{C_t0} -{p0}',
f'-{B_t0} -{p0}',
f'-{q0}'
]
3 changes: 3 additions & 0 deletions claasp/components/cipher_output_component.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -526,6 +526,9 @@ def sat_bitwise_deterministic_truncated_xor_differential_constraints(self):

return out_ids_0 + out_ids_1, constraints

def sat_semi_deterministic_truncated_xor_differential_constraints(self):
return self.sat_bitwise_deterministic_truncated_xor_differential_constraints()

def sat_xor_differential_propagation_constraints(self, model=None):
"""
Return a list of variables and a list of clauses representing CIPHER OUTPUT for SAT XOR DIFFERENTIAL model
Expand Down
3 changes: 3 additions & 0 deletions claasp/components/constant_component.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -593,6 +593,9 @@ def sat_bitwise_deterministic_truncated_xor_differential_constraints(self):
constraints = [f'-{out_id}' for out_id in out_ids_0] + [f'-{out_id}' for out_id in out_ids_1]
return out_ids_0 + out_ids_1, constraints

def sat_semi_deterministic_truncated_xor_differential_constraints(self):
return self.sat_bitwise_deterministic_truncated_xor_differential_constraints()

def sat_xor_differential_propagation_constraints(self, model=None):
"""
Return a list of variables and a list of clauses representing CONSTANT for SAT XOR DIFFERENTIAL model
Expand Down
Loading

0 comments on commit cbc559d

Please sign in to comment.