抽象的加密哈希功能在确保数据安全性,从可变长度输入中生成固定长度哈希至关重要。Hash函数SHA-256因其二十多年的严格审查后的弹性而被信任数据安全性。其关键特性之一是碰撞电阻,这意味着找到具有相同哈希的两个不同输入是不可行的。当前,最佳的SHA-256碰撞攻击使用差分密码分析在SHA-256的简化版本中找到碰撞,这些碰撞减少以更少的步骤,从而使发现碰撞是可行的。在本文中,我们使用满意度(SAT)求解器作为搜索步骤减少的SHA-256碰撞的工具,并借助于计算机代数系统(CAS),动态地指导求解器,用于检测不一致之处并推断信息,否则求解器将不会单独检测到求解器。我们的混合动力SAT + CAS求解器明显超过了纯SAT方法,从而使我们能够在步骤减少的SHA-256中发现碰撞,并具有更大的步骤。使用SAT + CAS,我们找到了带有修改初始化向量的SHA-256的38步碰撞,这是由Mendel,Nad和Schläffer的高度复杂搜索工具首先找到的。相反,纯粹的SAT方法可能会发现不超过28个步骤的碰撞。但是,我们的工作仅使用SAT求解器Cadical及其程序化接口Ipasir-Up。
主要关键词