摘要
密码协议的描述和分析有两类截然不同的方法:一类以形式化方法为主要手段,另一类以计算复杂性理论为基础.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.
出处
《计算机学报》
EI
CSCD
北大核心
2014年第5期993-1016,共24页
Chinese Journal of Computers
基金
国家自然科学基金(61170280)
中国科学院先导项目(XDA06010701)
中国科学院信息工程研究所密码基金资助~~
关键词
密码协议
形式化方法
计算可靠性
信息安全
网络安全
cryptographic protocol
formal method
computational soundness
information security
network security
