安全协议形式化分析研究  

A Survey on Formal Analysis of Security Protocols

作　　者：高尚[1] 胡爱群[1] 石乐[1] 陈先棒 

机构地区：[1]东南大学信息科学与工程学院信息安全研究中心,南京210096

出　　处：《密码学报》2014年第5期504-512,共9页Journal of Cryptologic Research

基　　金：国家重点基础研究发展项目(973计划)(2013CB338003)

摘　　要：计算机网络中,安全协议为通信双方的信息交互提供安全保证,是计算机网络安全的基础.而当安全协议中存在安全漏洞时,会对信息安全产生重大威胁,造成数据泄露、身份被冒用等危害.因此,对于安全协议安全性的研究,历来都属于安全领域的重要研究方向.目前的安全性分析方法主要是通过协议形式化分析与验证来实现.形式化分析方法的理论体系大致可分为三类:模态逻辑技术、模型检测技术和定理证明技术.在不同类别的理论体系中,所使用的技术方法各有不同,对安全协议分析的侧重点也略有不同.对于每一种理论体系,研究者们也提出了不同的方法,以及针对经典方案的改进来提高形式化分析的准确性.对于复合协议,其主要问题是通过对多种现有可靠安全协议加以组合,构成新的协议并保持其安全性可靠.对于复合协议的安全性分析,也有异于普通的安全协议形式化分析.本文总结了各种类别中的主要分析方法,并比较了每种方法的优缺点,同时特别针对复合协议的安全性分析技术进行了概述.最后指出了形式化分析方法中需要解决的问题,以及下一步的研究方向.Security protocols are basis for computer network security, and provide important secure insurance for information exchanging. It may cause great threat to the information security such as data leakage and fraudulent identity when there are flaws in security protocols. Therefore, it has always been a hot research area for the security of these protocols. The nowadays study for them is mainly through formal analysis. It can be classified into three types for theses protocols analysis; they are the model logic axiomatic technology, the modelchecking technology and the theorem proving technology. Each technology uses different ideas and lays different emphasis for each type. For each technology, researches also propose different methods and improvements for classic methods to improve the accuracy of formal analysis. For composed protocols, the main problem is to merge several secure protocols into one new protocol and ensure its security at the same time. In this paper, we first make a survey on various kinds of method in different analysis technologies, and conclude advantages and disadvantages of each method. Furthermore, we make an overview of the security analysis for composed protocols. Finally, we point out several problems and some research directions for further study in formal analysis of security protocols.

关 键 词：安全协议 协议形式化分析 复合协议 

分 类 号：TP393.08[自动化与计算机技术—计算机应用技术]