安全协议形式化分析理论与方法研究综述

《安全协议形式化分析理论与方法研究综述》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、第20卷第4期中国科学院研究生院学报Vol120No142003年12月JournaloftheGraduateSchooloftheChineseAcademyofSciencesDec12003综述3安全协议形式化分析理论与方法研究综述冯登国　范　红(中国科学院软件研究所,北京100080)(2003年5月29日收稿;2003年8月20日收修改稿)摘　要　综述目前安全协议形式化分析的理论与方法,包括安全协议的分类与模型,安全协议形式化分析的3种典型方法(基于推理的结构性方法,基于攻击的结构性方法,基于证明的结构性

2、方法),安全协议分析的形式化语言,安全协议设计的形式化方法,以及安全协议形式化分析面临的挑战。关键词　安全协议,安全模型,形式化分析,形式化语言中图分类号　TP3931　引言　　计算机网络正以惊人的速度向各个领域渗透,成为各领域发展的新源泉,各种现实世界里的组织与系统正在走进网络这个虚拟的世界里,使网络世界变得越来越精彩;与此同时,安全问题也变得越来越突出,也越来越复杂,解决安全问题对许多网络应用来说已是头等大事。从目前解决安全问题的方式来看,安全协议是解决网络安全问题最有效的手段之一。它可以有效地解决以下一些重要的

3、安全问题:源认证和目标认证,消息的完整性,匿名通信,抗拒绝服务,抗抵赖,授权等。另一方面,随着网络技术的飞速发展,多播技术已不断走向成熟,由多播应用带动的安全问题也变得更加复杂,为解决这些问题也是通过一种称为群协议的安全协议来完成的。目前研究的热点之一的多主体系统中的安全主体问题,在很大程度上也是依靠有效的安全协议的设计来完成的。可见,安全协议的研究具有强大的现实应用背景。尽管安全协议是保护信息系统安全的重要手段之一,但是分析安全协议中可能存在的缺陷,却是一个非常困难的问题。目前已经有多种研究安全协议的理论与方法,如

4、形式化分析方法、可证明安全理论、零知识证明理论等。本文主要综述安全协议形式化分析的理论与方法。为了便于更好地理解这些理论和方法的应用背景,首先对安全协议的一些基本问题作一简要概述。1.1安全协议的概念和分类所谓协议,就是两个或两个以上的参与者采取一系列步骤以完成某项特定的任务。这个定义包含3层意思:(1)协议至少需要2个参与者。一个人可以通过执行一系列的步骤来完成一项任务,但它不构成协议;(2)在参与者之间呈现为消息处理和消息交换交替进行的一系列步骤;(3)通过执行协议必须能够完成某项任务或达成某种共识。协议与算法的

5、概念是不尽相同的。算法应用于协议中消息处理的环节,对不同的消息处理方式则要求用不同的算法,而对算法的具体化则可定义出不同的协议类型。因此,简单地说,安全协议就是在消息处理环节采用了若干密码算法的协议。由此可见,密码算法和安全协议处于网络安全体系的不同层次,是网络数据安全的两个主要内容。具体而言,密码算法为网络上传递的消息提供高强度的加解密操作和其他辅助算法(如Hash函数),而安全协议是在这些密码算法的基础上,为各种网络安全性方面的需求提3国家重点基础研究发展规划项目(G1999035802)和国家杰出青年科学基金项

6、目(60025205,60273027)资助390中国科学院研究生院学报第20卷供实现方案。在网络通信中最常用的、最基本的安全协议按照其目的可以分成以下4类:(1)密钥交换协议。这类协议用于完成会话密钥的建立。一般情况下是在参与协议的2个或者多个实体之间建立共享的秘密,如用于1次通信中的会话密钥。协议中的密码算法可采用对称密码体制,也可以采用非对称密码体制。(2)认证协议。认证协议包括实体认证(身份认证)协议、消息认证协议、数据源认证协议和数据目的认证协议等,用来防止假冒、篡改、否认等攻击。(3)认证密钥交换协议。这

7、类协议将认证协议和密钥交换协议结合在一起,先对通信实体的身份进行认证,在认证成功的基础上,为下一步安全通信分配所使用的会话密钥,它是网络通信中应用最普遍的一种安全协议。常见的认证密钥交换协议有互联网密钥交换(IKE)协议、分布式认证安全服务(DASS)协议、Kerberos认证协议、X.509协议等。(4)电子商务协议。与上述协议最为不同的是,电子商务协议中主体往往代表交易的双方,其利益目标是不一致的,或者根本就是矛盾的。因此,电子商务协议最为关注的就是公平性,即协议应保证交易双方都不能通过损害对方利益而得到它不应得

8、的利益。常见的电子商务协议有SET协议,iKP协议等。1.2安全协议系统模型在一个大的分布式环境中,运行安全协议所面临的最大问题是其所处的网络通信环境是不安全的。如果将协议及其所处的环境视为一个系统,那么在这个系统中,一般而言包括发送和接收消息的诚实的主体和一个攻击者,以及用于管理消息发送和接收的规则。协议的合法消息可被攻击者截取、重放和篡改。