计算可靠的密码协议形式化分析综述

作者：雷新锋; 宋书民; 刘伟兵; 薛锐

来源：计算机学报, 2014, 37(05): 993-1016.

• 密码协议
• 形式化方法
• 计算可靠性
• 信息安全
• 网络安全

密码协议的描述和分析有两类截然不同的方法:一类以形式化方法为主要手段,另一类以计算复杂性理论为基础.Abadi和Rogaway首次试图将这两类不同的方法关联起来,证明一个协议在形式化模型下具有某种安全属性,那么在计算模型下也保持相应的安全属性.在这一工作的带动下,形式化方法的计算可靠性研究越来越受到关注,成为密码协议分析研究的一个重要内容.围绕这一热点问题,人们做了大量的工作.该文首先对两类分析方法做概要介绍;其次对形式化分析的计算可靠性研究成果进行分类和总结,并对各种方法的主要思想进行了介绍;最后对该领域未来的研究方向进行了展望.

• 单位
  中国科学院信息工程研究所; 信息安全国家重点实验室