分组密码路线的自动化搜索及SM4、SPECK线性分析

分组密码路线的自动化搜索及 SM4、SPECK 线性分析随着科技的进展,特别是智能手机的普及,网络已经触及到生活的每个角落,使得大众对于网络的依赖性逐渐增强,并且在一定程度上改变了原有的生活方式。在这样的背景下,人们对于安全的网络环境的需求日益巨大,全世界的网络安全学者都致力于满足人们不同应用场景和不同安全需求的密码协议的讨论,包括:软件和硬件安全,信息传播安全,网络系统信息安全,交互数据安全等。其中加密是实现数据机密性的一种重要的手段,可以将传播的信息变成对非认证用户隐藏的乱码。分组密码算法是实现数据加密的方式之一,并且容易实现同步,故而适用于很多应用场景,诞生了很多著名的密码算法,其中 SPECK 算法族是在 2025 年 6 月由美国国家安全局公开的为了优化软件实现的轻量级分组密码算法族。基于 SPECK 算法广泛的应用前景,很有必要全面的评估该算法抗各种攻击的安全性分析。目前已有很多 SPECK 的安全性分析结果。SMS4 算法在 2025 年由中国政府发行公布,作为底层分组密码算法服务于WAPI(WLAN 认证和隐私的基础设施)的无线局域网的安全性。于 2025 年,SMS4 算法被宣布为中国商业分组密码的标准,更名为 SM4。SM4 从出现之初就受到了密码社会很多的关注,已有很多分析结果。分组密码算法的分析方法也是多种多样,最早的安全性评估方法是著名的差分分析方法,这种分析方法很快就被整个密码分析学界所熟知并被广泛使用,成为了密码算法最主要的分析方法之一,也是设计新算法时必须考虑可以免疫的分析方法。另一个著名的分析方法是线性分析,线性分析和差分分析是分析分组密码算法的最主要的两种方法。从这两种分析方法逐步衍生出很多其它的分析方法比如:截断差分分析,反弹攻击,多线性分析,飞去来器攻击,多维线性分析,线性壳分析等。除此之外还有代数攻击,积分分析,零相关线性分析方法,不可能差分分析等。对于一个分组密码算法而言,需要考量算法的安全性,这就需要对算法用各种分析方法进行分析。本文的第一部分,介绍了如何构建搜索基于 S 盒的密码算法的(不可能)差分和线性路线的 STP Constant solver 模型。构建基于 S 盒的密码算法的(不可能)差分和线性路线的 STP 模型:近年来,自动化搜索工具在设计新的密码算法或者评估密码算法的安全性上发挥了重要的作用。常见的用于密码学的自动化搜索工具有三大类:基于 MILP 的自动化搜索模型,基于 SAT/SMT 的自动化搜索模型以及基于 CP 的自动化搜索模型。...