Adding SAT xor differential-linear model

claasp/cipher_modules/models/sat/sat_models/sat_differential_linear_model.py

@@ -243,6 +243,14 @@ def build_xor_differential_linear_model(
             )
             self._variables_list.extend(variables)
             self._model_constraints.extend(constraints)
+        for vari in self._variables_list:
+            if vari.startswith('cipher_output'):
+                print(vari)
+
+        minimize_vars = [f'cipher_output_7_24_{i}_o' for i in range(512)]
+        n_vars, v_const = self._sequential_counter(minimize_vars, 3, "dummy_id_unknown")
+        self._variables_list.extend(n_vars)
+        self._model_constraints.extend(v_const)
 
         self._get_connecting_constraints()
 

claasp/cipher_modules/models/sat/utils/utils.py

@@ -1109,8 +1109,13 @@ def get_cnf_semi_deterministic_window_1(
 
 
 def get_cnf_semi_deterministic_window_2(
-        p0, B_t0, A_t2, C_t3, C_t2, B_t1, B_v3, A_v2, C_t1, B_v1, A_v3, B_v0, C_v1,
-        B_v2, r0, A_t3, B_t3, A_t0, C_t0, A_v1, B_t2, q0, C_v0, A_t1, A_v0
+        A_t0, A_t1, A_t2, A_t3,
+        A_v0, A_v1, A_v2, A_v3,
+        B_t0, B_t1, B_t2, B_t3,
+        B_v0, B_v1, B_v2, B_v3,
+        C_t0, C_t1, C_t2, C_t3,
+        C_v0, C_v1,
+        p0, q0, r0
 ):
     return [
         f'{p0} {B_t0} -{A_t2} -{C_t1} {A_t0} {C_t0}',
@@ -1367,3 +1372,68 @@ def get_cnf_semi_deterministic_window_2(
         f'-{B_t2} -{q0}',
         f'-{q0} -{A_t1}'
     ]
+
+
+def get_cnf_semi_deterministic_window_3(
+        A_t0, A_t1, A_t2, A_t3, A_t4,
+        A_v0, A_v1, A_v2, A_v3, A_v4,
+        B_t0, B_t1, B_t2, B_t3, B_t4,
+        B_v0, B_v1, B_v2, B_v3, B_v4,
+        C_t0, C_t1, C_t2, C_t3, C_t4,
+        C_v0, C_v1, p0, q0, r0):
+    return [
+        f'{A_t4} {A_v4} {B_t4} {B_v4} -{C_t4} -{q0} {r0}',
+        f'{A_t3} {A_v3} {B_t3} {B_v3} -{C_t3} -{q0} -{r0}',
+        f'-{A_t3} -{q0} {r0}',
+        f'-{A_v3} -{q0} {r0}',
+        f'-{B_t3} -{q0} {r0}',
+        f'-{B_v3} -{q0} {r0}',
+        f'{C_t3} -{q0} {r0}',
+        f'{A_t1} {A_v0} -{A_v1} {B_t1} {B_v0} -{B_v1} {C_t1} {C_v0} -{C_v1}',
+        f'{A_t1} -{A_v0} -{A_v1} {B_t1} -{B_v0} -{B_v1} {C_t1} {C_v0} -{C_v1}',
+        f'{A_t1} -{A_v0} -{A_v1} {B_t1} {B_v0} -{B_v1} {C_t1} -{C_v0} -{C_v1}',
+        f'{A_t1} {A_v0} -{A_v1} {B_t1} -{B_v0} -{B_v1} {C_t1} -{C_v0} -{C_v1}',
+        f'-{A_v1} -{q0}',
+        f'-{B_v1} -{q0}',
+        f'{A_t0} {A_t2} {A_v2} {B_t0} {B_t2} {B_v2} {C_t0} -{C_t1} -{C_t2} {q0} {r0}',
+        f'{A_t1} -{A_v1} {B_t1} -{B_v1} {C_t1} -{C_v1} -{r0}',
+        f'{A_t0} {A_t1} -{A_v0} {A_v1} {B_t0} {B_t1} {B_v0} {B_v1} {C_t0} -{C_t1} {C_v0}',
+        f'{A_t0} {A_t1} {A_v0} {A_v1} {B_t0} {B_t1} -{B_v0} {B_v1} {C_t0} -{C_t1} {C_v0}',
+        f'{A_t0} {A_t1} {A_v0} {A_v1} {B_t0} {B_t1} {B_v0} {B_v1} {C_t0} -{C_t1} -{C_v0}',
+        f'{A_t0} {A_t1} -{A_v0} {A_v1} {B_t0} {B_t1} -{B_v0} {B_v1} {C_t0} -{C_t1} -{C_v0}',
+        f'{A_t0} -{A_t2} {B_t0} {C_t0} -{C_t1} {p0}',
+        f'{A_t1} {A_v1} {B_t1} {B_v1} -{C_t1} {q0} -{r0}',
+        f'{A_t0} {A_t1} -{A_v0} {A_v1} {B_t0} {B_t1} {B_v0} {B_v1} {C_t0} {C_v0} {C_v1}',
+        f'{A_t0} {A_t1} {A_v0} {A_v1} {B_t0} {B_t1} -{B_v0} {B_v1} {C_t0} {C_v0} {C_v1}',
+        f'{A_t0} {A_t1} {A_v0} {A_v1} {B_t0} {B_t1} {B_v0} {B_v1} {C_t0} -{C_v0} {C_v1}',
+        f'{A_t0} {A_t1} -{A_v0} {A_v1} {B_t0} {B_t1} -{B_v0} {B_v1} {C_t0} -{C_v0} {C_v1}',
+        f'{A_t1} {A_v1} {B_t1} {B_v1} {C_v1} {q0} -{r0}',
+        f'{A_t0} -{A_v2} {B_t0} {C_t0} -{C_t1} {p0}',
+        f'{A_t0} {B_t0} {B_v1} {C_t0} -{C_v1} {p0} {q0}',
+        f'{A_t0} {B_t0} -{B_t2} {C_t0} -{C_t1} {p0}',
+        f'{C_t1} -{p0} {r0}',
+        f'{A_t0} {B_t0} -{B_v2} {C_t0} -{C_t1} {p0}',
+        f'{A_t0} -{A_v1} {B_t0} {C_t0} -{C_t1} {r0}',
+        f'{A_t0} -{A_v1} {B_t0} {C_t0} {C_v1} {r0}',
+        f'{A_t0} {A_v1} {B_t0} -{B_v1} {C_t0} {r0}',
+        f'-{p0} -{q0}',
+        f'{A_t0} {B_t0} {C_t0} -{C_t1} {C_t2} {p0}',
+        f'-{A_t1} {p0} -{r0}',
+        f'-{B_t1} {p0} -{r0}',
+        f'{p0} {q0} -{r0}',
+        f'{A_t0} -{A_t1} {B_t0} {C_t0} {r0}',
+        f'{A_t0} {B_t0} -{B_t1} {C_t0} {r0}',
+        f'{A_t1} -{A_v1} {B_t1} -{B_v1} -{C_t0} {C_t1} -{C_v1}',
+        f'{A_t1} -{A_v1} -{B_t0} {B_t1} -{B_v1} {C_t1} -{C_v1}',
+        f'-{A_t0} {A_t1} -{A_v1} {B_t1} -{B_v1} {C_t1} -{C_v1}',
+        f'{A_t1} {A_v1} {B_t1} {B_v1} -{C_t0} {C_t1} {C_v1}',
+        f'{A_t1} {A_v1} -{B_t0} {B_t1} {B_v1} {C_t1} {C_v1}',
+        f'-{A_t0} {A_t1} {A_v1} {B_t1} {B_v1} {C_t1} {C_v1}',
+        f'-{C_t0} -{p0}',
+        f'-{B_t0} -{p0}',
+        f'-{A_t0} -{p0}',
+        f'-{C_t0} -{q0}',
+        f'-{B_t0} -{q0}',
+        f'-{A_t0} -{q0}',
+        f'{C_t1} -{q0}',
+    ]

claasp/components/modular_component.py

@@ -1120,7 +1120,7 @@ def position_0_constraints(a_t15, b_t15, c_t15, a_v15, b_v15, c_v15):
         q = [f'hw_q_{self.id}_{i}' for i in range(word_size)]
         r = [f'hw_r_{self.id}_{i}' for i in range(word_size)]
 
-        window_size_ = 1
+        window_size_ = 3
         for bit_position in range(word_size - 1):
             A_t_bit_positions = []
             for i in range(window_size_ + 2):
@@ -1144,7 +1144,29 @@ def position_0_constraints(a_t15, b_t15, c_t15, a_v15, b_v15, c_v15):
                     C_t[bit_position], C_t[bit_position + 1],
                     C_v[bit_position], C_v[bit_position + 1],
                     p[bit_position], q[bit_position], r[bit_position])
-
+            elif len(A_t_bit_positions) == 4:
+                cnf_clauses = sat_utils.get_cnf_semi_deterministic_window_2(
+                    A_t[bit_position], A_t[bit_position + 1], A_t[bit_position + 2], A_t[bit_position + 3],
+                    A_v[bit_position], A_v[bit_position + 1], A_v[bit_position + 2], A_v[bit_position + 3],
+                    B_t[bit_position], B_t[bit_position + 1], B_t[bit_position + 2], B_t[bit_position + 3],
+                    B_v[bit_position], B_v[bit_position + 1], B_v[bit_position + 2], B_v[bit_position + 3],
+                    C_t[bit_position], C_t[bit_position + 1], C_t[bit_position + 2], C_t[bit_position + 3],
+                    C_v[bit_position], C_v[bit_position + 1],
+                    p[bit_position], q[bit_position], r[bit_position])
+            elif len(A_t_bit_positions) == 5:
+                cnf_clauses = sat_utils.get_cnf_semi_deterministic_window_3(
+                    A_t[bit_position], A_t[bit_position + 1], A_t[bit_position + 2], A_t[bit_position + 3],
+                    A_t[bit_position + 4],
+                    A_v[bit_position], A_v[bit_position + 1], A_v[bit_position + 2], A_v[bit_position + 3],
+                    A_v[bit_position + 4],
+                    B_t[bit_position], B_t[bit_position + 1], B_t[bit_position + 2], B_t[bit_position + 3],
+                    B_t[bit_position + 4],
+                    B_v[bit_position], B_v[bit_position + 1], B_v[bit_position + 2], B_v[bit_position + 3],
+                    B_v[bit_position + 4],
+                    C_t[bit_position], C_t[bit_position + 1], C_t[bit_position + 2], C_t[bit_position + 3],
+                    C_t[bit_position + 4],
+                    C_v[bit_position], C_v[bit_position + 1],
+                    p[bit_position], q[bit_position], r[bit_position])
             else:
                 raise "Window size no supported"
 

tests/unit/cipher_modules/models/sat/sat_models/sat_differential_linear_test.py

@@ -290,18 +290,18 @@ def test_differential_linear_trail_with_fixed_weight_8_rounds_chacha():
     """Test for finding a differential-linear trail with fixed weight for 4 rounds of ChaCha permutation.
     This test is using in the middle part the semi-deterministic model.
     """
-    chacha = ChachaPermutation(number_of_rounds=16)
+    chacha = ChachaPermutation(number_of_rounds=15)
 
     import itertools
 
     top_part_components = []
     middle_part_components = []
     bottom_part_components = []
-    for round_number in range(4):
+    for round_number in range(3):
         top_part_components.append(chacha.get_components_in_round(round_number))
-    for round_number in range(4, 5):
+    for round_number in range(3, 4):
         middle_part_components.append(chacha.get_components_in_round(round_number))
-    for round_number in range(5, 8):
+    for round_number in range(4, 7):
         bottom_part_components.append(chacha.get_components_in_round(round_number))
 
     middle_part_components = list(itertools.chain(*middle_part_components))
@@ -346,7 +346,7 @@ def test_differential_linear_trail_with_fixed_weight_8_rounds_chacha():
     sat_heterogeneous_model = SatDifferentialLinearModel(chacha, component_model_types)
 
     trail = sat_heterogeneous_model.find_one_differential_linear_trail_with_fixed_weight(
-        weight=69,
+        weight=80,
         fixed_values=[plaintext1, plaintext2, modadd_6_15],
         solver_name="PARKISSAT_EXT",
         num_unknown_vars=12,
@@ -452,6 +452,71 @@ def test_differential_linear_trail_with_fixed_weight_4_rounds_chacha():
     assert trail["total_weight"] == 11
 
 
+def test_differential_linear_trail_with_fixed_weight_4_rounds_chacha_golden():
+    """Test for finding a differential-linear trail with fixed weight for 4 rounds of ChaCha permutation.
+    This test is using in the middle part the semi-deterministic model.
+    """
+    chacha = ChachaPermutation(number_of_rounds=8)
+    # import ipdb; ipdb.set_trace()
+    import itertools
+
+    top_part_components = []
+    middle_part_components = []
+    bottom_part_components = []
+    for round_number in range(2):
+        top_part_components.append(chacha.get_components_in_round(round_number))
+    for round_number in range(2, 4):
+        middle_part_components.append(chacha.get_components_in_round(round_number))
+    for round_number in range(4, 8):
+        bottom_part_components.append(chacha.get_components_in_round(round_number))
+
+    middle_part_components = list(itertools.chain(*middle_part_components))
+    bottom_part_components = list(itertools.chain(*bottom_part_components))
+
+    middle_part_components = [component.id for component in middle_part_components]
+    bottom_part_components = [component.id for component in bottom_part_components]
+
+    state_size = 512
+
+    plaintext = set_fixed_variables(
+        component_id='plaintext',
+        constraint_type='not_equal',
+        bit_positions=list(range(state_size)),
+        bit_values=[0] * state_size
+    )
+
+    modadd_3_0 = set_fixed_variables(
+        component_id='modadd_4_0',
+        constraint_type='not_equal',
+        bit_positions=list(range(32)),
+        bit_values=[0] * 32
+    )
+
+    component_model_types = _generate_component_model_types(chacha)
+    _update_component_model_types_for_truncated_components(
+        component_model_types,
+        middle_part_components,
+        truncated_model_type='sat_semi_deterministic_truncated_xor_differential_constraints'
+    )
+    _update_component_model_types_for_linear_components(component_model_types, bottom_part_components)
+
+    sat_heterogeneous_model = SatDifferentialLinearModel(chacha, component_model_types)
+
+    trail = sat_heterogeneous_model.find_one_differential_linear_trail_with_fixed_weight(
+        weight=20 - 5,
+        fixed_values=[plaintext, modadd_3_0],
+        solver_name="CADICAL_EXT",
+        num_unknown_vars=8,
+        # unknown_window_size_configuration={
+        #    "max_number_of_sequences_window_size_0": 9,
+        #    "max_number_of_sequences_window_size_1": 5,
+        #    "max_number_of_sequences_window_size_2": 5
+        # },
+    )
+    print(trail)
+    assert trail["status"] == 'SATISFIABLE'
+    assert trail["total_weight"] == 11
+
 def test_diff_lin_chacha():
     """
     This test is verifying experimentally the test test_differential_linear_trail_with_fixed_weight_3_rounds_chacha