如何在Choco-solver中实现约束条件？AES差分特性求解复用需求

核心思路 #

AES差分特性的本质是寻找满足每一轮差分传播规则的输入/输出差分序列。在Choco-solver中，我们需要：

1. 为每一轮的字节差分创建整数变量（取值0-255，对应8位XOR差分）；
2. 为AES的每一个操作（S盒、行移位、列混合、轮密钥加）添加对应的约束；
3. 设置目标（比如最大化差分概率，或寻找特定轮数的有效差分路径）；
4. 调用求解器搜索可行解。

可复用组件设计 #

把AES各操作的约束封装成可复用函数，能大幅简化不同任务（比如不同轮数、不同差分概率阈值）的开发流程。以下是关键组件：

1. S盒差分约束函数 #

AES的S盒差分传播有固定的概率表，我们可以预定义所有可能的输入差分→输出差分的合法映射，然后用约束限制变量关系：

public static void addSboxDiffConstraint(Model model, IntVar inputDiff, IntVar outputDiff) {
    // 预定义S盒差分合法映射（key:输入差分, value:所有可能的输出差分列表）
    Map<Integer, List<Integer>> sboxDiffMap = precomputeSboxDiffMap();
    // 将合法映射转为Choco的int数组集合
    int[][] allowedPairs = sboxDiffMap.entrySet().stream()
        .flatMap(entry -> entry.getValue().stream().map(v -> new int[]{entry.getKey(), v}))
        .toArray(int[][]::new);
    // 添加约束：(inputDiff, outputDiff)必须属于合法对集合
    model.table(new IntVar[]{inputDiff, outputDiff}, allowedPairs).post();
}

注：precomputeSboxDiffMap()需要提前根据AES S盒计算所有输入差分对应的可能输出差分（可以离线生成后硬编码，避免重复计算）。

2. 列混合差分约束函数 #

列混合的差分传播是线性变换，可通过GF(2^8)上的矩阵乘法推导约束，封装成函数后直接传入列的四个差分变量即可：

public static void addMixColumnsDiffConstraint(Model model, IntVar[] colDiffs) {
    // GF(2^8)上的列混合变换矩阵
    int[][] mixMatrix = {{2, 3, 1, 1}, {1, 2, 3, 1}, {1, 1, 2, 3}, {3, 1, 1, 2}};
    // 为每个输出字节添加线性约束（GF(2^8)乘法等价于特定位运算）
    for (int i = 0; i < 4; i++) {
        IntVar[] terms = new IntVar[4];
        for (int j = 0; j < 4; j++) {
            // 封装GF(2^8)乘法为Choco的自定义操作
            terms[j] = model.intVar(model.arithm(colDiffs[j], "*", mixMatrix[i][j]).reify().getId());
        }
        // 列混合后的差分是四个项的XOR（GF(2^8)加法即XOR）
        model.xor(terms, colDiffs[i]).post();
    }
}

注：需要实现GF(2^8)乘法的Choco自定义操作，可通过IntVar的位运算组合实现。

3. 轮级差分约束封装 #

把一轮的所有操作（S盒→行移位→列混合→轮密钥加）封装成函数，输入当前轮的差分变量，输出下一轮的差分变量：

public static IntVar[] addRoundDiffConstraint(Model model, IntVar[] currentRoundDiffs) {
    IntVar[] afterSbox = model.intVarArray(16, 0, 255);
    // 1. S盒差分约束
    for (int i = 0; i < 16; i++) {
        addSboxDiffConstraint(model, currentRoundDiffs[i], afterSbox[i]);
    }
    // 2. 行移位差分约束（行移位不改变差分，只是位置置换）
    IntVar[] afterShiftRows = permuteShiftRows(afterSbox);
    // 3. 列混合差分约束
    IntVar[] afterMixColumns = model.intVarArray(16, 0, 255);
    for (int col = 0; col < 4; col++) {
        IntVar[] colDiffs = new IntVar[4];
        for (int row = 0; row < 4; row++) {
            colDiffs[row] = afterShiftRows[row * 4 + col];
        }
        addMixColumnsDiffConstraint(model, colDiffs);
        // 将列混合后的差分放回对应位置
        for (int row = 0; row < 4; row++) {
            afterMixColumns[row * 4 + col] = colDiffs[row];
        }
    }
    // 4. 轮密钥加差分约束（轮密钥加的差分等于输入差分，因为密钥XOR不改变差分）
    return afterMixColumns;
}

完整流程示例 #

以寻找4轮AES的差分特性为例，调用上述可复用函数：

public static void findAesDifferential() {
    Model model = new Model("AES Differential Search");
    // 初始输入差分变量（可固定部分字节为目标差分，或全范围搜索）
    IntVar[] inputDiff = model.intVarArray(16, 0, 255);
    // 固定第一个字节差分为0x01，其他为0（示例）
    model.arithm(inputDiff[0], "=", 0x01).post();
    for (int i = 1; i < 16; i++) {
        model.arithm(inputDiff[i], "=", 0).post();
    }
    // 迭代添加轮约束
    IntVar[] currentDiffs = inputDiff;
    for (int round = 0; round < 4; round++) {
        currentDiffs = addRoundDiffConstraint(model, currentDiffs);
    }
    // 设置目标：寻找输出差分非零的解（或最大化概率，需结合概率约束）
    Solver solver = model.getSolver();
    while (solver.solve()) {
        // 输出解
        System.out.println("输入差分：" + Arrays.toString(inputDiff));
        System.out.println("4轮后输出差分：" + Arrays.toString(currentDiffs));
    }
}

关键优化点 #

• 预计算差分表：把S盒、列混合的差分规则提前计算好，避免求解时重复运算；
• 变量域裁剪：根据已知的差分传播规则（比如某些差分不可能出现），缩小变量的取值范围；
• 并行求解：利用Choco-solver的并行搜索能力，加速大规模差分空间的搜索。

内容的提问来源于stack exchange，提问作者Huy By