1. 项目概述当自动化工具遇上密码分析在密码学领域评估一个哈希函数或分组密码的安全性最直接的方法就是尝试“破解”它——当然这里的破解是指在学术研究框架内寻找比暴力穷举更高效的分析方法。中间相遇攻击Meet-in-the-Middle, MITM就是这类方法中的一把经典利器。它的思想非常直观与其从一头算到尾不如把计算路径从中间“劈开”两头分别计算然后在中间某个点“碰头”比对。如果两边的计算结果能对上那我们就找到了一个候选解。这种方法能显著降低搜索的时空复杂度尤其是在面对AES这类结构规整的算法时效果尤为明显。然而手工为复杂的密码算法设计一条高效的MITM攻击路径就像在迷宫里寻找最短路线既考验直觉又充满运气成分。随着算法轮数增加、结构变复杂人工分析几乎变得不可能。这时自动化搜索工具的价值就凸显出来了。近年来混合整数线性规划Mixed Integer Linear Programming, MILP因其强大的建模和优化求解能力被密码学家们引入用于自动化地搜索最优的MITM攻击路径。简单来说就是把“如何划分计算块”、“在哪里匹配”这些密码分析问题转化成一堆数学上的变量和不等式约束条件然后丢给专业的求解器比如Gurobi, CPLEX去算最终得到一个在给定模型下“最优”的攻击方案。我们这次聚焦的目标是Areion256-DM一个在CHES 2023上提出的、专为短输入设计的高效哈希函数。它完全基于AES指令集构建在特定场景下性能出众。设计者声称其能提供256比特的原像攻击安全性。但密码学的乐趣就在于总有人想看看“声称”的安全边界到底在哪里。之前的研究已经能攻击到5轮和7轮忽略末轮交换。我们的工作就是利用一种新的MILP建模思路不仅重新审视了这些攻击还找到了更优的路径将攻击推向了6轮并且显著降低了所需的内存开销。2. 核心思路拆解从“叠加态”到“线性组合”要理解我们工作的创新点得先看看前人是怎么做的。在MITM的MILP模型中我们需要用数学变量来刻画每个字节或者说每个状态单元在攻击过程中的“角色”。传统的模型比如Bao等人在EUROCRYPT 2021提出的框架以及后来引入的“叠加技术”Superposition Technique是这么处理的2.1 传统模型的瓶颈变量膨胀在叠加技术框架下为了精确描述一个字节可能同时受到“前向块”和“后向块”中立字节的影响每个物理字节都被视为两个虚拟字节的叠加。你可以想象成这个字节有“两个分身”一个只记录蓝色块前向的影响另一个只记录红色块后向的影响。这样一来整个系统的状态变量数量直接翻倍。对于一个有n个字节的状态原本需要n组变量来描述现在需要2n组。这带来了一个很现实的问题模型规模急剧膨胀。MILP求解器的时间复杂度通常与变量和约束的数量高度相关。当攻击轮数增加需要建模的中间状态越来越多时一个变量数翻倍的模型可能会变得非常庞大甚至超出求解器的处理能力或者需要极其漫长的计算时间。这就限制了自动化工具分析更高轮数或更复杂结构的能力。2.2 我们的新视角引入“黄色”属性我们问了自己一个问题是否必须用两个独立的虚拟字节来刻画这种“混合影响”仔细观察密码算法的线性操作比如AES的列混合MixColumns和异或XOR当一个蓝色字节和一个红色字节相加时产生的字节值其实是这两个字节的一个线性组合。基于这个观察我们提出了一个新的建模属性黄色。在我们的新模型中一个字节的状态由三个二元变量(x, y, z)决定蓝色 (1,0,0)该字节的值仅由蓝色块的中立字节决定。红色 (0,1,0)该字节的值仅由红色块的中立字节决定。灰色 (1,1,0)该字节是预先固定的常数对蓝、红块都已知。黄色 (0,0,1)该字节的值是某个蓝色字节和某个红色字节的线性组合。白色 (0,0,0)该字节的值是蓝、红字节的非线性组合或依赖双方在单边计算中无法确定。这个“黄色”属性的引入是模型简化的关键。它直接刻画了线性组合的结果而无需再为这个结果维护两个独立的虚拟源头。这样一来描述一个字节的属性从原来叠加技术需要的4个二元变量两个虚拟字节各自的蓝/红/灰/白状态减少到了现在的3个二元变量。2.3 新模型的优势不仅仅是变量减少变量减少直接带来了约束不等式数量的降低。以描述列混合操作的MC-RULE为例先前基于叠加技术的模型需要26个不等式而我们的新模型只需要15个。这对于MILP求解器来说是实实在在的负担减轻。更重要的是新模型更贴近密码操作的语义。“黄色”属性清晰地表达了“线性组合”这一密码学事实使得模型本身更易于理解和验证。它避免了叠加技术中可能出现的、为了建模而引入的间接性和复杂性。当然新模型也需要一套与之配套的、全新的传播规则Propagation Rules。我们需要精确定义当两个不同颜色的字节经过XOR或MixColumns操作后输出字节的颜色应该如何变化以及在什么情况下需要消耗“自由度”。这部分工作是我们模型的核心也是将密码分析直觉转化为数学约束的过程。实操心得模型设计的权衡在设计自动化密码分析模型时始终要在“表达精度”和“模型规模”之间做权衡。叠加技术非常精确但代价是规模大。我们的线性组合模型在保持对线性操作精确建模的前提下通过更紧凑的属性表示压缩了规模。这提醒我们在将密码学问题形式化为数学问题时深入理解算法本身的结构特性往往能找到简化模型的突破口。不要盲目套用现有框架多思考“这个操作的本质是什么”。3. 新MILP模型详解规则、约束与实现有了“蓝、红、灰、黄、白”这五色属性体系我们需要为密码算法中的基本操作主要是XOR和MixColumns制定详细的“染色”规则。这些规则决定了颜色如何在计算路径中传播并最终影响攻击的复杂度。3.1 XOR操作的颜色传播规则异或操作是密码算法中最常见的线性操作之一。我们的XOR-RULE需要处理所有可能的输入颜色组合。规则的核心思想是灰色常数是“强”颜色白色未知是“弱”颜色蓝/红相遇会产生黄色线性组合同色合并可能消耗自由度。涉及白色任何颜色与白色字节异或结果都是白色。因为白色代表完全未知的依赖会污染所有结果。涉及灰色灰色字节与任何颜色字节异或结果保持另一操作数的颜色。因为常数与任何值异或只是改变了该值的“偏移”不改变其依赖关系。蓝红相遇一个蓝色字节与一个红色字节异或结果变为黄色。这正是我们新模型要捕捉的核心情况——线性组合。蓝蓝/红红合并两个蓝色字节异或结果可以仍然是蓝色不消耗资源也可以通过消耗1个蓝色块的自由度将结果变为灰色。红色字节同理。这个规则很重要它允许攻击者在必要时“合并”同色路径以换取在后续匹配点获得更多已知信息灰色但代价是减少了该颜色块可自由赋值的字节数自由度。涉及黄色黄色字节与蓝、红或黄字节异或结果通常退化为黄色。但是如果在这个过程中消耗了红色或蓝色的自由度结果可以进化为蓝色或红色。这为颜色转换提供了灵活性。将这些文字规则转化为MILP约束需要引入辅助变量如cx,cy表示此XOR操作消耗的蓝、红自由度并建立一系列线性不等式。这些不等式确保了变量赋值颜色和消耗的所有可能组合都符合我们定义的语义规则。论文中给出的不等式组公式2就是这一转化的具体实现它确保了模型在数学上的严密性。3.2 MixColumns操作的颜色传播规则列混合是AES-like结构中的另一个关键线性操作。我们的MC-RULE相对复杂因为它处理的是整个一列例如4个字节的并行变换。白色污染如果输入列中有任何一个白色字节那么整个输出列的所有字节都退化为白色。这是因为MDS矩阵的扩散性质使得任何一个未知输入都会影响所有输出。全灰继承如果输入列所有字节都是灰色常数那么输出列所有字节也是灰色且不消耗自由度。一般情况这是最复杂也最常见的情况。输入列由i个蓝、j个红、k个灰、l个黄字节组成。经过MixColumns后输出列变为i’个蓝、j’个红、k’个灰、l’个黄字节。这个过程可能会消耗蓝色和红色的自由度。消耗自由度的目的是将一些蓝/红字节在计算后变为灰色已知从而在匹配点提供更多信息。约束条件确保了颜色数量的变化是合理的并且消耗的自由度与颜色转换相匹配。例如输出列中蓝色和黄色字节的总数(j’k’)必须小于输入列中蓝色和黄色字节的总数(il)除非后者为零即没有蓝/黄输入则输出全灰。论文中的公式(3)-(5)详细描述了这些不等式约束其中引入了x,y,ω等辅助变量来标记输入列中是否包含蓝、红、白字节。3.3 匹配规则与内存约束找到攻击路径后我们需要评估其效率核心是计算匹配度。匹配度计算匹配通常发生在MixColumns操作的输入/输出处。利用MDS矩阵的性质如果已知的输入输出字节数之和超过矩阵的行数(Nrow)那么就可以建立一个线性方程组来过滤掉不匹配的候选值。匹配度mi就是已知字节数之和 - Nrow如果为负则取0。总匹配度DoM是所有列匹配度之和。匹配度越高过滤效果越好攻击的时间复杂度越低。内存复杂度约束MITM攻击需要存储两个列表蓝表和红表。列表的大小由各自剩余的自由度决定即2^DoFB和2^DoFR。我们需要存储的是较小的那个列表大小为min(2^DoFB, 2^DoFR)。在我们的MILP模型中可以很容易地加入一个约束如公式6要求这个最小值不超过某个阈值2^t。这允许我们主动搜索那些低内存复杂度的攻击路径这对于实际攻击的实施至关重要因为内存访问往往比计算更昂贵。注意事项自由度的消耗与平衡在设计攻击时自由度的分配是一门艺术。蓝色块和红色块的初始自由度由中立字节数量决定是固定的。在传播过程中XOR和MixColumns操作会消耗这些自由度以产生更多的灰色已知字节来提升匹配度。但消耗过多会导致某个列表变得太小反而可能增加另一个列表的大小或降低匹配效率。我们的MILP模型通过优化目标函数如最大化min(dB, dR, dM)即最小化时间复杂度自动寻找自由度消耗的最佳平衡点。在实际使用求解器时可以将时间复杂度的公式作为目标函数让求解器去寻找全局最优解。4. 攻击Areion256-DM从模型到具体攻击实例理论模型建立后我们将其应用于Areion256-DM哈希函数。我们的目标是寻找对更多轮数的原像攻击或者对已知轮数攻击进行优化降低时间或内存复杂度。4.1 针对6轮Areion256-DM的攻击这是我们得到的一个重要新结果。攻击的配置如图4所示参见原论文。初始状态被划分为蓝色和红色中立字节。通过MILP模型搜索我们找到了一条攻击路径其中蓝色自由度初始有15个蓝色中立字节但为了确保蓝、红块计算独立需要施加13个约束条件因此剩余自由度DoFB 15 - 13 2即2个字节16比特。红色自由度初始有16个红色中立字节施加10个约束剩余DoFR 16 - 10 66个字节48比特。匹配度DoM 11个字节8比特。攻击步骤详解初始化与列表构建随机固定所有灰色字节常量的值。然后求解那13个蓝色约束方程和10个红色约束方程。这会分别得到蓝色中立字节和红色中立字节的所有可能解集合。我们将蓝色解存入表TB大小约为2^(2*8) 2^16红色解存入表TR大小约为2^(6*8) 2^48。前向/后向计算与部分匹配对TB中的每一个蓝色候选值我们从初始状态出发分别向前和向后计算直到匹配点图4中P3和Q3之间。在匹配点我们利用MixColumns的线性关系如公式7,8构造出一个等式其中一端Cred仅依赖于红色字节另一端Cblue仅依赖于蓝色字节。我们计算所有蓝色候选值对应的Cblue值并将其与对应的蓝色中立字节值一起存储在一个列表L[Cblue]中按Cblue值索引。反向查找与验证对TR中的每一个红色候选值同样计算到匹配点并得到对应的Cred值。对于每个Cred我们去列表L中查找是否有相同的Cblue值。由于匹配度为8比特我们平均期望有2^(1648-8) 2^56个部分匹配。对于每一个部分匹配对蓝红我们利用已知的灰色字节和这对蓝红中立字节可以重构出完整的初始状态候选。然后将其代入完整的6轮Areion256-DM计算中验证其哈希值是否与目标值匹配。复杂度分析时间复杂度主要开销在于步骤2和3。我们需要遍历TB2^16和TR2^48但通过部分匹配过滤后平均只需验证2^56个全状态候选。然而要找到一个256比特的原像平均需要尝试2^256个输入。我们每次迭代固定一组灰字节能覆盖2^(1648)2^64个初始状态。因此预计需要2^(256-64) 2^192次迭代。总时间约为2^192 * (2^16 2^48) ≈ 2^240次6轮计算。由于2^48远大于2^16主导项是2^192 * 2^48 2^240。内存复杂度只需要存储较小的蓝色列表TB即2^16个条目。这比之前的一些攻击方案要低得多。4.2 针对5轮和7轮无末轮交换的攻击应用相同的模型和方法我们也找到了对5轮Areion256-DM的新攻击以及针对忽略末轮交换的7轮变体的、内存复杂度更低的攻击。5轮攻击时间复杂度和内存复杂度分别为2^232和2^24。与设计者给出的初始攻击相比我们的时间复杂度和内存复杂度都有所优化。7轮攻击无末轮交换Hou等人之前的工作攻击7轮需要2^64内存。我们的新攻击在相同时间复杂度的水平下2^240将内存复杂度降低到了2^16。这再次证明了我们模型在搜索低内存攻击方面的有效性。实操心得MILP求解的调参与技巧直接运行一个包含数千变量和约束的MILP模型去搜索最优攻击可能非常耗时。在实践中我们采用了一些技巧来加速搜索分层搜索先固定一个较小的匹配度目标或内存上限让求解器快速找到一个可行解。然后以此解为起点逐步收紧约束要求更低的复杂度引导求解器向更优解搜索。利用对称性Areion256结构具有对称性。我们在建模时可以加入对称性约束减少搜索空间避免求解器浪费时间在等价的解上。分解问题有时将一个大问题分解成几个阶段性的MILP问题来求解会更高效。例如先优化自由度的划分再在固定划分下优化匹配点的位置。并行尝试由于MILP求解具有一定随机性特别是在使用启发式算法时用不同的初始参数或求解器配置并行运行多个求解进程可以提高找到好解的概率。5. 模型对比、局限与未来方向5.1 与叠加技术的直观对比为了更清晰地展示我们模型的优势我们将其与经典的叠加技术模型在几个关键维度上进行对比特性维度叠加技术模型我们的线性组合模型优势分析核心思想每个物理字节视为两个独立虚拟字节的叠加引入“黄色”属性直接表示线性组合字节概念更直接更贴合线性操作语义变量需求每个字节需要4个二元变量 (2虚拟字节 × 2属性)每个字节需要3个二元变量 (x,y,z)变量数减少25%直接降低模型规模MC-RULE约束数26个不等式15个不等式约束数减少约42%显著简化模型模型求解效率变量和约束多求解可能较慢尤其对于大规模问题模型更紧凑求解速度通常更快能处理更大轮数提升搜索效率拓展了自动化分析的范围内存复杂度优化支持但模型更重支持且轻量级模型更容易整合内存约束能更高效地搜索低内存攻击路径这张表清晰地表明我们的模型通过更精简的属性系统在保持描述能力的同时实现了模型复杂度的显著降低。5.2 当前模型的局限性与挑战尽管新模型取得了不错的效果但它并非万能也存在一些局限对高度非线性操作建模的复杂性我们的模型核心优势在于处理线性操作XOR, MixColumns。对于AES的S盒SubBytes这类非线性操作通常的处理方式是将其视为“黑盒”规定其输入输出颜色必须相同例如输入是蓝色输出也是蓝色因为S盒会破坏线性关系。如果算法中包含更复杂或可利用的非线性组件模型需要进一步扩展。搜索空间与最优性MILP求解器给出的解通常是在给定模型下的“最优解”但这是数学意义上的最优不一定是密码学意义上“最好”的攻击。模型是对现实的抽象一些微妙的密码学性质可能无法完全用线性不等式刻画。此外对于非常大的模型例如攻击全轮算法即使我们的模型更小求解全局最优解仍然可能非常困难此时我们得到的往往是“当前找到的最好”解。通用性我们的模型针对的是具有串行XOR和线性层如MDS矩阵的密码算法如AES-like结构和Feistel结构。对于其他类型的密码原语如基于ARX的算法需要设计新的属性传播规则。5.3 未来可能的拓展方向这项工作的结束恰恰是更多可能性的开始应用于其他密码算法最直接的拓展就是将这套自动化工具应用到更多的Feistel结构密码或AES-like哈希函数上。许多旧的攻击结果有可能通过我们的模型进行复现和优化甚至发现新的攻击路径。结合其他自动化技术MILP可以与其他自动化分析技术结合例如SAT可满足性理论求解器或符号执行。MILP擅长优化全局指标如复杂度而SAT可能更擅长处理复杂的布尔逻辑关系。混合使用或许能攻克更难的密码分析问题。探索量子密码分析中间相遇攻击的思想可以自然地延伸到量子计算场景如Grover算法。如何修改我们的MILP模型使其能够搜索最优的量子中间相遇攻击路径是一个非常有前景的方向。这需要将量子查询复杂度等新指标纳入目标函数。模型本身的优化能否进一步减少变量能否为特定的密码操作如比特置换、模加设计更高效的传播规则我们的“黄色”属性是一个开始或许还有更巧妙的属性定义方法等待发现。回过头看密码分析就像一场在精心设计的迷宫里的寻宝游戏。自动化工具尤其是像MILP这样的形式化方法为我们提供了绘制迷宫地图和计算最短路径的罗盘与量尺。我们的工作就是改进了这件工具让它更轻便、更高效。虽然我们针对Areion256找到的新攻击路径距离威胁其全轮安全性还有很远10轮中攻击了5-7轮但这个过程本身的价值在于它不断测试和确认着密码算法安全边际的牢固程度并推动着自动化密码分析这门技术向着更深、更广的方向发展。每一次模型的改进每一点复杂度的降低都是对“安全性”更深刻理解的一块基石。