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

摘要

密码协议安全验证分析是信息安全重点研究之一.常用的密码协议安全分析(例如,形式化分析、计算模型分析、计算可靠的形式化分析)只能从理论上验证或证明密码协议的安全,无法确保密码协议代码实际执行的安全.只有当密码协议在代码执行时被验证或证明安全,才能保障密码协议在实现中是安全的.因此,代码级的密码协议安全验证分析是值得关注的方向.文中分别从自动模型提取、代码自动生成、操作语义及程序精化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.In this 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 of cryptographic protocols implementation on real code which is based on operational semantics analyzes the security of the properties of a cryptographic protocol,such as the sequence of the traces,the match of messages during the process of the implementation of a cryptographic protocol and so on.The program refinement security analysis analyzes the security of a cryptographic protocol by applying the relation of the program refinement.At the end of this paper,we prospect the research direction of security verification analysis of cryptographic protocols implemented on real code in six parts:Model checking techniques (such as program refinement,program verification and so on) are applied to analyze and verify cryptographic protocol implementation on real code;Based on Dolev-Yao model,the security of cryptographic protocols is automatically analyzed and verified on real code;Programming languages(C/C++,Java,F# and so on) are applied to build models or frames (F7,CoSP,Spi2Java,etc.) in the process of security verification analysis of cryptographic protocols;Security verification analysis of cryptographic protocol implementation on real code is based on semantic security;Computational sound formal analysis is applied to analyze and verify the security of cryptographic protocols implementation on real code;Concurrency security verification analysis of cryptographic protocols implemented on real code is developed.