MD5作为在计算机安全领域常用的哈希函数,其安全性接受着极大的考验。在我国的密码学专家王小云教授提出模减差分攻击有效攻破MD4,MD5,SHA-0等一系列哈希函数之后,MD5攻击取得了极大的进展。如今针对MD5的碰撞攻击已经能够在1秒的时间里找到多组碰撞。利用SAT公式强大的表达力,将MD5攻击编码成SAT问题后求解,为MD5及其他哈希函数的攻击提供了一种新的研究方法。本文欲借助SAT求解器强大的求解能力来对MD5进行攻击。首先详细介绍了将MD5函数编码成SAT的几种方法,并相应得到三种类型的算例,然后对得到的算例使用SAT2014获奖求解器进行求解。对比不同类型算例的求解结果,得出了最优的编码方法。实验结果表明,CDCL求解器可以成功对27步简化版MD5进行原象攻击和第二原象攻击。另外,在上面MD5函数编码的基础之上,借助于差分攻击的强大助力对MD5进行碰撞攻击。针对王小云教授的差分攻击提出了两种编码方法,实验结果表明,对于差分路径编码方法,使用SAT求解器Lingeling能在103秒的时间里面找到一组碰撞,快于充分条件编码方法,也快于王小云教授差分攻击方法。本文利用MD5布尔函数和加法的特性,设计实现了一个基于随机局部搜索的求解器。在5000秒的时间限制下,该求解器能成功进行25步简化版MD5的第二原象攻击,优于SAT局部搜索求解器。在比较了各个求解器的优缺点之后,文章结尾提出了将子句学习加入MD5攻击的完备型算法的思想。