密码协议代码执行的安全验证分析综述  

A Survey:Security Verification Analysis of Cryptographic Protocols Implementations on Real Code

作　　者：张焕国[1,2] 吴福生[1,2] 王后珍 王张宜[1,2] 

机构地区：[1]武汉大学计算机学院,武汉430072 [2]武汉大学空天信息安全与可信计算教育部重点实验室,武汉430072

出　　处：《计算机学报》2018年第2期288-308,共21页Chinese Journal of Computers

基　　金：国家自然科学基金(613030212;61202385);国家自然科学基金重点项目(61332019);国家"九七三"重点基础研究发展规划项目基金(2014CB340600)资助~~

摘　　要：密码协议安全验证分析是信息安全重点研究之一.常用的密码协议安全分析(例如,形式化分析、计算模型分析、计算可靠的形式化分析)只能从理论上验证或证明密码协议的安全,无法确保密码协议代码实际执行的安全.只有当密码协议在代码执行时被验证或证明安全,才能保障密码协议在实现中是安全的.因此,代码级的密码协议安全验证分析是值得关注的方向.文中分别从自动模型提取、代码自动生成、操作语义及程序精化4个方面,综述代码级的密码协议安全验证分析,并对当前代码级的密码协议安全验证分析领域中的最新成果进行详细比较、分析、总结和评论.文中以常用程序语言(C、Java、F#等)编写的密码协议为例,重点阐述密码协议代码执行的安全验证分析,并展望代码级的密码协议安全验证分析的研究方向.Security verification analysis of cryptographic protocols is one of the most important fields of researching the information security in network.Although common ways to analyze the security of cryptographic protocols(such as formal analysis,computational model analysis,and computational sound formal analysis)can theoretically verify or prove whether cryptographic protocols are secure,they can't guarantee that cryptographic protocols are secure in the process of implementation on real code.However,if cryptographic protocols are verified or proved to be secure during the process of implementation on real code,it can be insured that cryptographic protocols are implemented safely.Therefore,it is worthwhile to focus on the field of researching security verification analysis of cryptographic protocols implemented on real code.In this paper,first of all,we summarize the research status of security verification analysis of cryptographic protocols at home and abroad.Furthermore,we summarize the research status of security verification analysis of cryptographic protocols implemented on real code,and there are four branches:automated model extraction,automated code generation,operational semantics and program refinement.Meanwhile,we compare,analyze,summarize and comment the latest achievements in the research of security verification analysis of cryptographic protocols implemented on real code.Inthis paper,taking common programming languages as examples(such as C,Java,F#,and so on),we carry out the discussion and focus on four kinds of security analysis.Based on classical abstract theories,automated model extraction analyzes the security of a cryptographic protocol by applying an abstract mapping,which maps the properties of a cryptographic protocol from concrete program state space onto a corresponding abstract model.Automated code generation,based on the specifications of a cryptographic protocol,generates the codes automatically and analyzes the security of a cryptographic protocol with these codes.The security analysis

关 键 词：密码协议 模型 代码 执行 安全验证 

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