C2P:基于Pi演算的协议C代码形式化抽象方法和工具

形式化方法为安全协议分析提供了理论工具,但经过形式化验证过的协议标准在转换为具体程序实现时可能无法满足相应的安全属性.为此,提出了一种检测安全协议代码语义逻辑错误的形式化验证方法.通过将协议C源码自动化抽象为Pi演算模型,基于Pi演算模型对协议安全属性形式化验证.最后,给出了方案转换的正确性证明,并通过对Kerberos协议实例代码验证表明方法的有效性.根据该方案实现了自动化模型抽象工具C2P与成熟的协议验证工具ProVerif结合,能够为协议开发者或测试人员检测代码中的语义逻辑错误提供帮助.     

基于块存储结构的彩虹表时空折中方法

Thing提出的基于彩虹表的时空折中方法(Digital Investigation, 2009, No.6)不能对存储数据进行排序及去重,导致假警出现概率和表搜索代价过高。为此,设计一种基于块存储结构的彩虹表,给出相应的表搜索方法,在此基础上提出一种新的时空折中方法,通过在预计算阶段合并终结点相同的链,降低假警率、提高表搜索效率。分析结果表明,与同类方法相比,该方法在成功率、存储空间利用率及搜索代价方面更具优势。     

基于进程演算的公钥密码体制安全性自动化证明系统

可证安全是一种通过严格证明确保密码体制安全性的形式化方法,但由于其证明结论严重依赖于证明者个人的经验和技巧,这一方法本身的可靠性受到了质疑。文章设计并实现了一套公钥密码体制安全性自动化证明系统,使用一种概率多项式时间进程演算描述可证安全模型,借助进程间的互模拟等价关系和进程约减实现基于游戏的可证安全自动化证明。系统在C语言环境下实现,已完成ElGamal加密体制和FDH签名体制在内的一系列密码体制的安全性证明测试。     

基于状态转移系统的安全协议形式模型

提出一种基于状态转移系统的安全协议模型,以Dolev-Yao攻击者模型为前提假设,以状态转移系统为框架,用语义编码的方式定义消息和事件,用重写关系定义协议规则,用事件的集合来描述协议的安全属性,并给出安全属性的检验策略。该模型能够对安全协议进行精确的形式化描述,且便于实现自动化分析。     

开放授权协议OAuth2.0的安全性形式化分析

开放授权协议OAuth是云上一个新的开放标准,解决了用户多账号通用和资源共享的问题.文章针对OAuth2.0的协议规范,利用Alice-Bob标记语言和HLPSL协议高级语言对其进行了形式化描述,并借助基于状态空间搜索的安全协议分析工具,分别讨论了通信三方在使用和未使用HTTPS加密的情况下协议的安全性,对于不安全的情况得到了相应的攻击路径.另外,在实际的网络环境中观察分析了OAuth2.0的相应实现,对国内访问量前100名的网站做了统计,发现其中可以作为OAuth2.0协议服务端的网站有63.6％存在安全漏洞,可以作为客户端的网站有90.2％存在安全漏洞,实验结果对规范网络安全环境有重要的作用和意义.     

公钥加密体制自动化安全性证明方法研究

可证明安全是目前分析密码协议安全性的一种重要方法,但是手工证明的难度较大,正确性也难以保证。利用计算机技术实现可证明安全性的自动化分析是目前的一个研究热点。文章在前人工作的基础上,设计了一个适用于更多密码协议的安全性证明的自动化证明工具。着重介绍了利用高级描述语言来描述的输入文件即＂初始攻击游戏＂的结构,并以带Hash的E lGamal加密体制为例,利用证明工具,实现了其安全性的自动化证明。     

可证明安全性自动化证明方法研究

可证明安全性是密码协议安全性评估的重要依据,但手写安全性证明容易出错且正确性难以判定。该文论述了基于游戏(Game based)转换的安全性证明及其自动化实现方法,重点论述了基于进程演算的自动化证明方法,并以该方法研究OAEP＋的自动化安全性证明,首次给出了其初始游戏和相关的观察等价式。     

一种NTRU格上基于身份全同态加密体制设计

全同态加密可以用来解决云计算环境中的隐私保护问题,然而现有体制具有系统参数大、效率低的缺点.针对现有攻击技术,首先设计了一种高效的NTRU格上的基于身份公钥加密体制,无需借助额外的安全性假设,具有更高的安全性和更小的系统参数.之后,基于近似特征向量技术,构造了一种高效的全同态加密转化方式.通过将以上两种方法结合,给出了一种高效的基于身份全同态加密体制.和现有体制相比,除了不需要计算密钥、实现了真正意义上的基于身份特性以外,还减小了密钥、密文尺寸,提高了计算和传输效率.     

基于高效彩虹表存储的快速时空折中攻击

自从Oechslin提出彩虹表,时空折中方法已成为实现密码攻击的最常用方法之一.在彩虹表技术基础上,提出一种新的预计算表计算方法和存储结构.将该方法用于攻击95个全可打印字符集上、最大口令长度为8的口令,和彩虹表方法相比,存储空间中的记录数增加了约70%,从而使得在存储和计算复杂度相同的条件下,成功概率提高了7.8%~15.6%(针对不同的链长).该方法还可进一步与Checkpoints方法相结合,在链的中间位置设置一个Checkpoint点,可使在线分析阶段的计算代价降低10%~20%.