对DES的Rectangle攻击和Boomerang攻击

作为加密标准，DES（data encryption standard）算法虽然已被AES（advanced encryption standard）算法所取代，但其仍有着不可忽视的重要作用．在一些领域，尤其是金融领域，DES和Triple DES仍被广泛使用着．而近年来又提出了一些新的密码分析方法，其中，Rectangle攻击和Boomerang攻击已被证明是非常强大而有效的．因此，有必要重新评估DES算法抵抗这些新分析方法的能力．研究了DES算法针对Rectangle攻击和Boomerang攻击的安全性．利用DES各轮最优差分路径及其概率，分别得到了对12轮DES的Rectangle攻击和对11轮DES的Boomerang攻击．攻击结果分别为：利用Rectangle攻击可以攻击到12轮DES，数据复杂度为2~(62)。个选择明文，时间复杂度为2~(42)次12轮加密；利用Boomerang攻击可以攻击到11轮DES，数据复杂度为2~(58)个适应性选择明密文，时间复杂度为2~(38)次11轮加密．由于使用的都是DES各轮的最优差分路径，所以可以相信，该结果是Rectangle攻击和Boomerang攻击对DES所能达到的最好结果．

Isabelle在分析安全操作系统状态机模型中的应用

为了解决已有的状态机模型的形式化框架在分析安全操作系统状态机模型时不够直观．简洁的问题，提出了一套使用Isabelle工具对安全操作系统模型状态中的类型、变量、常量、关系、映射、函数，以及模型中的安全不变量和状态迁移规 则进行形式化描述的新方法．通过实际验证一种典型的安全操作系统状态机模型——可信进程模型，总结出了有效地使用Isabelle辅助形式化设计、分析、验证模型的策略．

基于Isabelle定理证明器算法程序的形式化验证

形式化验证对保证软件的正确性和可靠性具有十分重要的意义.定理机械证明是形式化验证的一个重要研究领域,Isabelle系统是一个被广泛运用的定理证明辅助工具.本文在分析Dijkstra最弱前置谓词理论的基础上,根据PAR方法开发的算法程序循环不变式,提出了一种使用Isabelle定理证明器对算法程序进行机械验证的方法.该方法既克服了传统手工验证过程的繁琐性和易错性等缺点,又达到"提高验证效率和保证算法程序高可信"的目标,具有很好的实用价值.