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

A Survey on Computationally Sound Formal Analysis of Cryptographic Protocols

作　　者：雷新锋[1,2] 宋书民[2] 刘伟兵[2] 薛锐[1] 

机构地区：[1]中国科学院信息工程研究所信息安全国家重点实验室,北京100093 [2]北京信息技术研究所,北京100097

出　　处：《计算机学报》2014年第5期993-1016,共24页Chinese Journal of Computers

基　　金：国家自然科学基金(61170280);中国科学院先导项目(XDA06010701);中国科学院信息工程研究所密码基金资助~~

摘　　要：密码协议的描述和分析有两类截然不同的方法:一类以形式化方法为主要手段,另一类以计算复杂性理论为基础.Abadi和Rogaway首次试图将这两类不同的方法关联起来,证明一个协议在形式化模型下具有某种安全属性,那么在计算模型下也保持相应的安全属性.在这一工作的带动下,形式化方法的计算可靠性研究越来越受到关注,成为密码协议分析研究的一个重要内容.围绕这一热点问题,人们做了大量的工作.该文首先对两类分析方法做概要介绍;其次对形式化分析的计算可靠性研究成果进行分类和总结,并对各种方法的主要思想进行了介绍;最后对该领域未来的研究方向进行了展望.There are two different approaches in analysis of cryptographic protocols.One isbased on formal methods,and the other is based on computational complexity as modern cryptog-raphy does.Abadi and Rogaway tried to reconcile these two approaches in their seminal work.They set up a relation for some formal results that if a security property is proved in formal model,then the corresponding property is also valid in computational model.Motivated by this work,many works appeared in this area.In this survey,we will summarize various approaches oncomputational soundness of formal methods in analysis cryptographic protocols,present theirmain ideas,and point out the future research directions in this area.

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

分 类 号：TP309[自动化与计算机技术—计算机系统结构]