attacks Module

Overview

The attacks module provides a unified framework for modeling and solving MILP/SAT-based cryptanalysis attacks on block ciphers. It supports flexible model configuration, automated constraint/objective function generation, and integration of advanced strategies such as Matsui’s branch-and-bound method.

---

Key components

This module consists of four main functional components:

• Model Behavior Configuration
  • Provides flexible specification and automatic filling of cipher states, rounds, layers, and positions.
  • Enables configuration of model versions to customize and control the modeling process.
• Model Constraint and Objective Function Generation
  • Automates the generation of constraints and objective functions for each states, round, layer, or operation in the cipher.
  • Supports parameterized.
• Modeling and Solving for Attacks
  • Offers unified interfaces for building and solving MILP/SAT models for attacks.
  • Supports parameterized.
• Additional Constraints and Advanced Strategies
  • Supports injection of user-defined constraints and standard predefined constraints (e.g., input non-zero).
  • Implements advanced cryptanalysis techniques such as Matsui’s branch-and-bound strategy to enhance search efficiency. """

---

Main Interfaces

modeling_solving_optimal_solution(cipher, model_type, filename, add_constraints=None, model_args=None, solving_args=None)

modeling_solving_optimal_solution
│
├── gen_attacks_model
│   ├── gen_round_model_constraint
│   ├── [if Matsui MILP] gen_matsui_constraints_milp
│   │       └── gen_predefined_constraints
│   ├── [if Matsui SAT] gen_matsui_constraints_sat
│   │       ├── gen_round_obj_fun
│   │       ├── gen_sequential_encoding_sat
│   │       └── gen_matsui_partial_cardinality_sat
│   ├── [if objective_function] gen_round_obj_fun
│   │       ├── [if SAT and obj_sat] gen_sequential_encoding_sat
│   └── solving.gen_milp_model / solving.gen_sat_model
│
├── solving.solve_milp / solving.solve_sat
├── solving.formulate_solutions
└── vis.print_trails

Modeling and Solving for SAT

There are four main functions for SAT-based modeling and solving:

1. modeling_solving_optimal_sat: Finds the optimal solution by starting from objective value 0 and incrementally increasing until a solution is found.
2. modeling_solving_optimal_start_from_sat: General interface that incrementally solves SAT from a specified starting objective value to find the optimal solution within a defined maximum limit.
3. modeling_solving_at_most_sat: Solves the SAT model with an upper bound on the objective function (i.e., obj ≤ max_val).
4. modeling_solving_exactly_sat: Solves the SAT model with an exact constraint on the objective function (i.e., obj = exact_val).

Configuration Parameters for SAT Modeling

In config_model, the following parameters can be used to control the behavior and encoding of SAT modeling:

Key	Type	Default	Description
optimal_search_strategy_sat	str	"AT_MOST"	Strategy for optimization. Supports "AT_MOST" to find solutions with obj ≤ v, and "EXACTLY" to enforce obj = v.
max_obj_sat	int	100	Maximum objective value to try when incrementally searching for an optimal solution.
decimal_encoding_sat	str	"INTEGER_DECIMAL"	Encoding strategy for decimal-weighted objective functions. Options: "INTEGER_DECIMAL", "BOOLEAN".
atmost_encoding_sat	str/int	"SEQUENTIAL"	Encoding scheme for "at most" constraints. Options: "SEQUENTIAL", 0,1,2,3,4,5,6,7,8,9.
exact_encoding_sat	int	1	Encoding scheme for "exactly" constraints. Options: 0,1,2,3,4,5,6,7,8,9.
atleast_encoding_sat	str/int	"SEQUENTIAL"	Encoding scheme for "at least" constraints. Options: "SEQUENTIAL", 0,1,2,3,4,5,6,7,8,9.
matsui_constraint	dict	None	Optional dictionary specifying extra Matsui's cutoff constraints, such as best objective, round index, and group selection parameters.