当下社会的繁荣发展,离不开密码学的保驾护航。基于S盒的密码算法是最经典的分组密码算法之一,ARX型结构因其软件友好实现性被业界广泛应用,同时差分分析是对现代密码算法最经典的分析方法,因此研究基于S盒的密码算法和ARX型密码算法抵抗差分分析的安全性具有重要意义。本文重点研究了基于S盒的密码算法和ARX型密码算法的建模问题,利用MILP技术对Craft算法、SM4算法和Ballet算法进行差分分析。针对基于S盒的密码算法,一方面引入分支定界的思想,另一方面提出分析Large S-boxes型密码算法的MILP新模型。针对ARX型密码算法,重点研究了模加操作的建模,并引入编程技巧来加快模型求解。本文主要的研究成果如下所示:对于Craft算法,我们求解模型给出了其1-17轮的活跃S盒个数的下界,我们的结果与已知结果一致,证明了 Craft算法在单密钥模式下的安全性。值得注意的是,对于Craft算法的第9轮,不采用优化方法需要1881s得出结果,采用优化方法仅需要732s;另外我们还验证了一条13轮概率为2-124的差分特征。这说明我们的模型构建以及代码实现是正确的,为后边分析Large S-boxes型密码算法和ARX型密码算法奠定了良好的基础。对于SM4算法,我们分别用Abdelkhalek模型和Wu模型对其S盒建模,对这两种模型下的实验结果分析研究后,我们提出针对Large S-boxes型密码算法的MILP新模型。我们利用新模型对SM4算法建模,给出了 1-24轮的最小活跃S盒个数,与其他论文相比,我们有的轮数得到的下界更紧。对于SM4算法的19轮,我们不仅找到了概率为2-124的差分特征,而且找到了概率为2-123的差分特征,这是目前基于MILP技术找到的概率最高的差分特征。对于SM4算法的20轮,当最小活跃S盒个数为18时找不到相应的差分特征,所以我们认为20轮SM4算法差分特征的最小活跃S盒个数大于18。另外,我们得出24轮的活跃S盒个数至少为22个,而SM4的S盒最大的差分概率是2-6,可以证明SM4算法是抵抗差分分析的。对于ARX型密码算法Ballet,我们采用MILP方法,用1+13 ×（n-1）个线性不等式刻画模加操作,并提出一个编程技巧来减少模型变量,进而提高模型求解速度,与设计者论文基于SAT技术给出的9轮差分特征概率为2-43的结果相比,我们给出了 1-7轮的准确概率,对于8-9轮仅是给出了一个模糊的界,仍可以证明Ballet算法可以抵抗差分分析,但也说明基于MILP的模型还有较大的优化空间,值得进一步研究。