（控制理论与控制工程专业论文）电力系统安全协议形式化分析技术研究.pdf

摘要 摘要 电力通信是电力系统的重要组成部分。电力通信的安全需求包括身份认证， 存取控制，防火墙等，这些安全需求的实现都依靠安全协议。安全协议是构建在 密码体制上的一种交互协议，是电力通信系统可靠性的重要保障。但是，设计一 个符合安全目标的安全协议是十分困难的。从安全协议的发展过程分析，往往是 先设计协议，若在使用过程中发现了某个安全漏洞，弥补该漏洞，再继续使用。 有些漏洞甚至在协议设计后的十几年才得以发现。因此，我们必须借助一些方法 和技术指导协议的设计，并在协议设计后对其进行分析。本文研究协议的分析技 术。 自动化分析一直以来都是国内外研究人员的追求目标，形式化分析是自动化 分析的基础和前期研究，在形式化分析的基础上，通过形式描述语言可以具体实 现自动化分析。本文是针对自动化分析的基础研究：采用b a n 类逻辑( b u r r o w s a b a d in e e d h a ml o g i c ) 和串空间方法，先对安全协议进行不同类型的数学抽象， 再基于这些抽象分析协议的安全性。主要的研究工作和成果有：一是把a o d v 安全协议抽象为数学逻辑模型，利用b a n 类逻辑描述协议的交互过程，并以此 为基础分析协议是否满足其安全目标。二是把h e l s i n k i 协议抽象为串空间模型， 利用串空间模型描述协议的信息交互过程，并通过对攻击行为和协议最小理想的 分析，验证协议的安全性。 关键词：电力通信系统；访问控制；形式化分析；串空间；b a n 类逻辑 a b s t r a c t a b s t r a c t p o w e rt e l e c o m m u n i c a t i o ni st h ei m p o r t a n tc o m p o s i n go fp o w e rs y s t e m , a n dt h es e c u r i t y c o m m a n do ft h ec o m m u n i c a t i o ni n c l u d e sa u t h e n t i c a t i o n , a c c e s sc o n t r o l ，f i r e w a l l , a n ds oo n , w h i c ht h er e a l i z a t i o nd e p e n d e do nt h es e c u r i t yp r o t o c 0 1 t h es e c u r k yp r o t o c o li sa na l t e m a t i n g p r o t o c o lt h a ti sb a s e do nt h ee n c r y p t i o n , a n di ti st h ec r u c i a lg u a r a n t e eo f p o w e rc o m m u n i c a t i o n s y s t e m h o w e r e r , i ti sd i f f i c u l tt od e s i g nas e c u r i t yt h a tm a t c h t h es e c u r i t yo b j e c t r e v i e w i n gt h e d e v e l o p m e n to fs e c u r i t yp r o t o c o l ，i ti sa l w a y sd e s i g n i n gap r o t o c o lf h s t l y , a n dt h e nm o d i f y i n gi t i fs o m ew e a k n e s sw a sd i s c o v e r e d ，s o m ew e a k n e s s e sw e r ef o u n dt e ny e a r sl a t e rw h e nt h e p r o t o c o lw a sd e s i g n e d s o ，i tn e e d ss o m em e t h o d sh e l pt od e s i g nas e c u r i t yp r o t o c o l ，a n d a n a l y s et h ep r o t o c 0 1 t h ea n a l y s i s ea p p r o a c h e sw e r ef o c u s e do n i nt h i st h e s i s t h ea u t o m a t i o na n a l y s i si sa l w a y st h ea i mo fr e s e a r c h e r s ，a n dt h ef o r m a la n a l y s i si st h eb a s e o fi t 。t h ea u t o m a t i o na n a l y s i sc a nb er e a l i z e db a s e do nt h ef o r m a la n a l y s i s ，t h r o u g ht h ef o r m a l d e s c r i p t i o nl a n g u a g e t h i st h e s i si st h eb a s i cr e s e a r c ho fa u t o m a t i o na n a l y s i sf o rw h i c h t h eb a n ( b u r r o w sa b a d in e e d h a ml o g i c ) l o g i ca n ds t r a n ds p a c ew e r ea d o p t e d t h ep r o t o c o l sw e r e a b s t r a c t e di nd i f f e r e n tm a t h e m a t i c sf o r m a t ，a n dt h es e c u r i t yo f t h ep r o t o c o lw a sa n a l y s i s e db a s e d o nt h e s em o d e l s t h em a i nc o n t r i b u t i o no ft h i sw o r ki sa sf o l l o w s ：t h ef i r s ti st h a tt h ea o d v p r o t o c o lw a sa b s t r a c t e dt h r o u g hb a nl o g i c ，a n dt h es e c u r i t yw a sc o n f i r m e db a s e do ni t t h e s e c o n di st h a tt h eh e s i n k ip r o t o c o lw a sm o d e l e dt h r o u g ht h es t r a n ds p a c e ，a n dt h ea t t a c km a n n e r a n dt h em i n i d e aw e r ea n a l y s i s e dt oc o n f n mt h es e c u r i t yo ft h ep r o t o c 0 1 k e y w o r d ：p o w e rt e l e c o m m u n i c a t i o ns y s t e m ；a c c e s sc o n t r o l ；a n t h e n t i c a t i o np r o t o c o l ；f o r m a la n a l y s i s ； s t r a n ds p a c e ；b a nl i k el o g i c i i 原创性声明 独创性声明 秉承学校严谨的学风与优良的科学道德，本人声明所呈交的论文是我个人在 导师的指导下进行的研究工作及取得的研究成果。尽我所知，除了文中特别加以 标注和致谢的地方外，论文中不包含其他人已经发表或撰写过的研究成果，不包 含本人或其他用途使用过的成果。与我一同工作的同志对本研究所做的任何贡献 均已在论文中作了明确的说明，并表示了谢意。 本学位论文成果是本人在广东工业大学读书期间在导师的指导下取得的，论 文成果归广东工业大学所有。 申请学位论文与资料若有不实之处，本人承担一切相关责任，特此声明。 论文作者签字：房【勾殴夤l 指导教师签花瞬铂隈霄 御年g 月6 日 6 2 第一章绪论 第一章绪论 1 。1 研究背景与意义 随着电网的迅速发展，盆动亿以及管理水平不断提高，电网对电力通信系统 也提出了更高的要求。电力通信广泛服务于电网基建、生产、管理以及职工的日 常生活。耀时随着电力然刳改革的不断深入，服务对象隶属关系的不断变化，以 及电信部门为用户提供的网益完善的服务体系，这都要求进一步提高电力通信电 信业务综合管理水平，改蔫服务质量，向用户提供更为优质的和多元化的服务， 从而使得企业通信网的管理更加科学化、规范化，降低运营成本，提升企业的经 济效益，增强电力系统逶信的管理水平和竞争力 i - 3 。 电力通信系统不仅有一般的语音传输，图像传输的要求，同时具有不同的安全 需求。我翻可以将这些薪兴的安全需求分成两类：“计算机安全”( c o m p u t e r s e c u r i t y ) 和“网络安全”( n e t w o r ks e c u r i t y ) 。所谓“计算机安全”，是指我们 将资辩、数据等存放在计算机或相关设备当中，如 霹通过各种规制来防止资料、 数据泄漏或遭到破坏的相关安全需求，其中以各种共享式的系统需求最为迫切， 计算机安全需要多种技术相互配合方可实现，例如：软件安全、操作系统安全、 硬件安全架构；而“网络安全”则着重于使用者与计算机、计算机与计算机之间， 经过有线或者无线的网络，在传输重要信息时，能够确保萁不遭破坏、修改以及 泄密等的需求。除电力通信系统，互联网以外，电力公司内部的计算机所组成的 有线局域网( l o c a la r e an e t w o r k ，简称l a n ) 、无线局域两( w i r e l e s s - l a n ) 、 无线传感器网络( w i r e l e s ss e n s o rn e t w o r k ) 、嵌入式系统网络( e m b e d d e d s y s t e mn e t w o r k ) 、信息家电( i n f o r m a t i o na p p l i a n c e ) 之间的互联网络等，都 是网络安全所涉及的范畴。 各种各样的阙络已经成为人们生活当中必不可少酶元素，因此，网络中的 安全问题更得到人们的普遍重视。信息确认和网络安全控制技术主要包括身份认 证、存敬控制、数据完整性、防止否认、防火墙技术，这些技术都是基于计算 机网络开展的。就具体技术讲，安全包括认证性，数据完整性，保密性和不可否 认性的要求 4 】。这些要求的实现都依赖于安全协议的设计和分析，但是茸前安 全协议无论在设计之初还是设计之后，其安全性都无法保证。形式化分析方法是 广寒t 业大学1 = 学硕士学位论文 国外近年来发展起来一种安全协议分析技术，实践证明该方法是有效的 5 ，并 且已经成为国内外研究的一个热点。囡内以国家级和省级课题为依托 6 ，促进 此技术的发展。本文在此背景下对电力通信系统中的安全协议做了一些有益的探 索。 1 2 国内外网络安全现状 本节对国内外网络安全的现状做分析，以此说明安全协议以及安全协议分 柝技术的重要性和紧迫性。电力通信系统给电力系统带来前所未有的便捷，但同 时也蕴含着诸多的安全风险，我们可以先参考互联网的安全现状。电力通信系统 仍然为通信系统，因此电力通信系统同样也面临着这些安全问题。 由于阚络技术的迅速普及，世界范圈内的网络犯罪行为愈演愈烈，犯罪内 容涉及到金融、欺诈、诽谤、非法入侵、知识产权、泄密、窃密以及扰乱国家治 安等，直接给世界各国的金融、军队、政治、人民生活等造成巨大损失。据统计， 西方，国集团各成员唇每年因为网络安全问题造成损失嘉达4 2 0 亿美元。摆美国 a b 联合会调查专家估计，美国每年因为计算机犯罪所造成的经济损失高达1 5 0 亿 美元 7 。在9 1 1 ”事件后，美国在加强现实空间反恐行动的同时，也大力加强 了嬲络空闻的安全保卫。这些铡子无不壹接反映了网络犯器行为已经在世界范围 内产生相当恶劣的影响。 我国在网络安全方面的现状又是如何呢? 我们首先来看几个数据，中国互 联黼信息中心( c h i n ai n t e r n e tn e t w o r ki n f o r m a t i o nc e n t e r ，c n n i c ) 2 0 0 7 年 7 月公布 8 的调查报告显示我图上网用户总人数已经达到1 6 2 亿，总规模仅次子 美国的2 1 1 亿。上网计算机数达至1 j 6 7 1 0 万，同时以手机为终端的无线接入网民也 数达到了4 4 3 0 万。单纯从数量上而言，我国己经成为世界上数一数二的信息大囡， 但与此同时，c n n i c 较早时公布的一些调查报告也显示出我国在网络安全方面极 大的不足( 部分参考数据如表1 1 所示) 。 第一章绪论 表1 1 被入侵计算机比率和长期不更改帐号密码用户比率 t a b l e1 1t h er a t eb e t w e e ni n t r u s i o na n dl o n g - t i m ew i t h o u tc h a n g i n gp a s s w o r d 调查报告公布时间在过去一年内计算机对于同一帐号，备注 被入侵的用户所占比 一直不更换密码 率的用户所占比率 2 0 0 4 年1 月 7 2 7 3 6 8 包括电子邮件帐 号矛i f t p 帐号 2 0 0 3 年7 月 6 3 0 4 1 4 同上 2 0 0 3 年1 月 5 9 4 4 8 4 仅指电子邮件帐 号 2 0 0 2 年7 月 6 0 1 5 2 6 同上 表1 2 网民对互联网安全性满意程度 t a b l e1 2t h es e c u r i t ys a t i s f a c t i o nr a t eo fi n t e r n e t 调查报告公布时间对互联网安全性满意程度 2 0 0 7 年7 月 2 9 2 2 0 0 7 年1 月 2 8 8 2 0 0 6 年7 月 1 7 3 2 0 0 6 年1 月 2 4 5 2 0 0 5 年7 月 1 9 1 2 0 0 5 年1 月 2 0 4 2 0 0 4 年7 月 2 1 4 在c n n i c 后续公布的报告中显示网民对互联网的安全性满意程度如表1 2 所 示。如表1 1 和表1 2 所示，虽然网民对网络安全的认识正在不断加强，但网民对 当前网络的安全满意程度仍然不高。例如，2 0 0 6 年7 月的调查报告显示对互联网 安全性“非常满意”的用户仅占总数量的2 3 。这样的数据充分反映了我国在网络 安全方面还处于相当不完善的状态。如何有效地控制、保护网络中的各种系统资 源是我们所面对的一个极其复杂同时富有挑战性的课题。 这些事实表明，网络安全问题必须予以高度的重视，而安全协议的分析是解 广东工业大学工学硕士学位论文 决这些问题的方法之一( 但是不全面的，因为通信系统的安全解决是个复杂大系 统，俗称为安全水桶，协议分析为其中的一块木板) 。安全协议的运行是在一些 现实物理环境中，在不考虑具体物理设备的情况下，对各种通信系统我们可以抽 象出具体的通信模型。如图1 1 所示，该模型是一个基本的且被广泛使用的安全 通信模型 9 。通信一方要通过互联网将消息传送给另一方，那么通信双方( 称为 交易的主体) 必须协调努力共同完成消息交换。我们可以通过定义互联网上从源 到宿的路由以及通信主体共同使用的通信协议( 女h t c p i p 协议) 来建立逻辑信息 通道。 图1 1 通信的安全模型 f i n g e r1 1t h es e c u r i t ym o d e lo fc o m m u n i c a t i o ns y s t e m 为了实现安全传输，需要有可信的第三方。例如，第三方负责将秘密信息 分配给通信双方，而对攻击者保密，或者当通信双方关于信息传输的真实性发生 争执时，由可信第三方来仲裁。上述模型说明，设计安全服务应包含下列四个方 面的内容： 1 ) 设计执行安全相关传输的算法，该算法应是攻击者无法攻破的 2 ) 产生算法所使用的秘密信息，即加密密钥和解密密钥 3 ) 设计分配和共享秘密信息的方法 4 ) 指明通信双方使用的协议，该协议利用安全算法和秘密信息实现安全服务 一般来说，目前常见的安全机制和服务都遵循图1 1 所示的通信模型。 4 第一章绪论 1 3 网络安全服务 在上述模型的基础上，我们可以分聿斤出具体的安全需求，根据不问的使用 环境，这些需求会有所差界，但一般来说，以下几项需求是网络安全中最常见的 基本服务 1 0 ： 1 ) 认证( a u t h e n t i c a t i o n ) - - 认证服务与保证通信的真实性有关。在单条 消息的情况下，如条警告或报警信号，认证服务功能是向接收方保证消息来自 所声称的发送方。对于正在进行的交互，如终端和主机连接，就涉及到两个方面。 首先，在连接初始化阶段，认证服务保证两个实体是可信的，也就是说，每个实 体都是他们所声称的实体。其次，认证服务必须保证该连接不受第三方如下方式 的干扰：第三方能够伪装成两个合法实体中的一个进行非授权传输或者接收。 2 ) 存取控制( a c c e s sc o n t r 0 1 ) 一在网络安全中，存耿控制是一种限制、 控制实体通过通信连接对主机和应用进行存瞅的能力。为此，每个试图获得存取 控制的实体必须被识别或认证后，才能获取其相应的存取权限。 3 ) 数据保密性( d a t ac o n f i d e n t i a l i t y ) 一保密性是防止传输的数据遭到 窃听以致泄漏。关于数据传输，可以有几层保护，最广泛的服务在一段时间内为 两个用户所传输的所有用户数据提供保护。也可以定义一种较窄的保密性服务， 可以是对单条消息或对单条消息内某个特定的范围提供保护。保密性的另一个方 面是防止流量分析。这要求攻击者不能观察到消息的源和宿、频率、长度或通信 设施上的其他流量特征。 4 ) 数据完整性( d a t ai n t e g r it y )与保密性相比，完整性可应用于消息 流、单条消息或消息的选定部分。同样，最直接的方法是对整个数据流提供保护。 处理消患流的面向连接的完整性服务保证收到的消息和发出的消息一致，没有复 制、插入、修改、更改顺序或重放。该服务也涉及对数据的破坏。因此，面向连 接的完整性服务处理消息的修改和拒绝服务两个问题。另一个方面，仅仅处理单 条消息面不管大量信息的无连接的完整性服务，通常仅防止对单条消息的修改。 5 ) 不可否认性( n o n r e p u d i a t i o n ) 一不可否认性防止发送方或接收方否认 传输或接收过某条消息。因此，当消息发出后，接收方能证明消息是出声称的发 送方发出的。同样，当消息接收后，发送方能证明消息事实上确实由声称的接收 方收到。 广东工业大学工学硕士学位论文 6 ) 可用性服务( a v a i l a b i l i t y ) 一根据系统的性能说明，能够按照授权的 系统实体的要求存取或使用系统或系统资源的性质( 即当用户请求服务时，根据 系统设计，若系统提供这些服务，则系统是可用的) 。许多攻击可导致可用性的 损失或减少。一些自动防御措施，如认证、加密，可对付某些攻击。 表1 3 是典型的特殊环境中安全要求与安全威胁，以及可能采取的构成防护 措施的安全业务之间的对应关系，这些安全业务的实现都是通过安全协议。也就 是说，系统的安全性是建立在安全协议的基础上的。但这些协议的安全性是否 能够保证? 安全协议的发展历史表明，这些协议的安全性是无法得到保证的，无 论是在协议的设计之初，还是在协议设计之后。因此，国内外研究人员纷纷提出 指导协议设计或分析安全的方法。安全协议的运行不是独立的，而是处于某种不 安全的环境之中，因而它是易错的，并且错误很难完全由人工来识别，必须要借 助形式化的分析方法或工具来完成。安全协议的形式化分析技术，可使协议设计 者通过系统分析，将注意力集中于接口、系统环境的假设、系统在不同条件下的 状态、条件不满足时系统出现的情况，以及系统不变的属性，并通过系统验证， 提供协议必要的安全保证。通俗地讲，安全协议的形式化分析是采用一种正规的、 标准的方法对协议进行分析，以检查协议是否满足其安全目标。因此，安全协议 的形式化分析有助于：( 1 ) 界定安全协议的边界，即协议系统与其运行环境的 界面；( 2 ) 更准确地描述安全协议的行为；( 3 ) 更准确地定义安全协议的特性； ( 4 ) 证明安全协议满足其说明，以及证明安全协议在什么条件下不能满足其说 明。 6 第一章绪论 袭l3 特殊环境中的典型安全威胁与采取的安全业务 t a b l e1 3t h es e c u r i t ys e r v i c ea n dt h et h r e a t e ni nt h ea p p l i c a t i o ne n v i r o n m e n t 网络业务类型安全要求 安全威胁安全业务 所有网络防止外部侵入假冒攻击认证业务 银行防止对传输的数据进完整性侵犯、假认证业务、完整 行欺诈性或偶然性修冒攻击、业务否性业务、不可否 改；区分零售交易用认、窃听攻击 认业务、保密业 户；保护个人身份号以务 防泄露；确保用户的隐 私 电子化贸易保证信源的真实性和假冒攻击、完整认证业务、保密 数据的完整性；保护合性侵犯、窃听攻业务、不可否认 作秘密：对传输的数据 击、业务否认业务 进行数字签名 政癃部门保护非机密但敏感的假冒攻击、授权认证业务、访问 信息以防非授权的泄 侵犯、窃听、完控制业务、保密 露和操作；对政府文件整性侵犯、业务业务、完整性业 进行数字签名否认 务、不可否认业 务 公共电信载体禁止对管理功能或授假冒攻击：授权认证业务、访问 权的个体进行访闯；防侵犯、业务拒绝、控制业务、完整 止业务干扰；保护用户窃听性业务、保密业 的秘密务 互联专用网络保护合作者个体的秘窃听攻击、假冒认证业务、保密 密：确保消息的认证性攻击、完整性侵业务、完整性业 犯 务 7 广东工业大学t 学硕十学位论文 1 4 本文的主要内容及章节安排 第二章介绍安全协议形式化分析的各种方法，为后续章节的分析奠定理论 和方法的基础。形式化分析方法分为基于逻辑推理结构，基于攻击结构方法，基 于定理证明方法。其中重点介绍本文所用的串空间方法和经典的b a n 逻辑方法。 第三章先简要介绍本文的研究对象一安全协议。安全服务的基础是安全协 议，安全协议是以密码体制为基础，密码体制是以某个数学难题( 大数分解，离 散对数等数学难题) 为基础。数学难题( 大数分解，离散对数等数学难题) 是整 个现代密码学的基石，密码体制的安全性是以数学难题的技术上不可破解性为前 提。 第四章，针对a o d v 路由协议本身不具有安全性的问题，基于非对称密钥对 协议进行改进，并基于b a n 逻辑对改进后得协议进行分析，证明改进的协议是安 全的。 第五章，针对相关文献对h e l s i n k i 协议安全性的质疑，基于串空间对 h e l s i n k i 协议进行分析，证明该协议是安全的。 8 第二章安全协议形式化分析方法 第二章安全协议形式化分析方法 以上分析了由于各种安全问题所需的安全服务，这些服务的具体实现都是 依靠安全协议。但安全协议本身是否安全? 是否存在安全漏洞? 形式化分析方法 采用一种规范的方法，对协议进行分析，以回答这两个问题。形式化方法分为基 于推理结构方法，基于攻击结构方法和基于定理证明方法。这些方法都是近十几 年甚至近些年在国外发展起来的( 比如串空间是1 9 9 8 年提出的) ，在国内的研究 是刚刚处于起步阶段。 2 1 发展简介 本节分析安全协议分析技术得现状。目前多数安全协议的设计现状是 1 1 - 1 2 ：提出一种安全协议后，基于某种假想给出其安全性论断；如果该协议 在很长时间，如1 0 年仍不能被破译，大家就广泛接受其安全性论断；一段时间后 可能发现某些安全漏洞，于是对协议再作必要的改动，然后继续使用。这一过程 可能周而复始。这样的设计方法存在以下问题：第一，分析技术的提出时间是 不确定的，在任何时候都有可能提出新的分析技术；第二，这种做法使我们很难 确信协议的安全性，反反复复的修补更增加了人们对安全性的担心，也增加了实 现代价或成本。有一个例子能充分说明安全协议设计的现状，著名的n s 认证协 议公开1 7 年后，它存在的入侵者攻击漏洞才被g l o w e 发现。 d d o l e v 和a c y a o 提出了一个威胁模型 1 3 ，这一模型被广泛地采纳为安 全协议的标准威胁模型。由计算机、设备和资源构成的大型网络( 例如互联网) 是典型开放性的，这就意味着一个任意主体能够加入这样的网络，并通过该网络 来发送和接收消息，而并不需要“超级”主体授权。在开放的环境中，我们必须考 虑到主动攻击者存在的可能性。主动攻击者不仅只是被动的窃听，而且会主动地 改变( 采取一些未知的运算和方法) 、伪造、复制、改变路由、删除或注入消息。 注入的消息可能是恶意的并对接收端主体以破坏性的影响。在本文中，我们称这 类攻击者为m a l i c e 。m a l i c e 可以是单个的，也可以是相互勾结的攻击团伙，甚至 他可能是协议中的一个合法主体( 内部人员) 。在这个模型中，m a li c e 有如下特征： 1 ) 他能获得经过网络的任何消息 2 ) 他是网络的一个合法使用者，因而能够发起与任何其他用户的对话 9 广东工业大学工学硕士学位论文 3 ) 他有机会成为任何主体发出消息的接收者 4 ) 他能够冒充任何别的主体给任意主体发消息。 因此，在d o l e v - y a o 威胁模型中，发送到网络中的任何消息都可看成是发 送给m a l i c e 处理的( 根据他的计算能力) 。因而从网络接收到的任何消息都可以看 作是经过m a l i c e 处理过的。换句话说，可以认为m a l i c e 已经完全控制了整个网络。 事实上，我们应将开放性网络看作是m a l i c e 是无害的”，即m a l i c e 只是忠实地转 发消息，不构成任何威胁。但除非明确声明，我们并不认为m a l i c e 是无所不能的。 这意味着即使把他看成是一个相互勾结的犯罪团伙，能够并行使用跨越丌放网络 中的大量计算机，也仍然有一些是m a l i c e 所不能做的事情。这里对“不能做”的意 思具体描述如下：m a l i c e 不能猜测到从足够大的空间中选出的随机数；没有正确 的密钥( 或私钥) ，m a l i c e 不能由给定的密文恢复出明文；对于完善加密算法， m a l i c e 也不能从给定的明文构造出正确的密文；m a l i c e 不能求出私有部分，比如， 与给定的公钥项匹配的私钥；m a l i c e 虽然能控制我们的计算机甚至通信环境的大 量公共部分，但他不能控制计算环境中的许多私有区域，如访问离线主体的存储 器。 我们将采用d o l e v y a o 威胁模型作为安全机制分析的标准。在该模型下，我 们必须充分考虑攻击者m a lic e 对安全机制攻击和破坏的主动性。 最早提出对安全协议进行形式化分析思想的是n e e d h a m 和s c h r o e d e r ，他们 为进行共享和公钥认证的认证服务器系统的实现建立了安全协议。1 9 81 年 d e n n i n g s a c c o 在文献中指出了n s 私钥协议的一个错误，使得人们开始关注 安全协议分析。在这一领域做出突出贡献的是d o l e v 和y a o ，紧随其后，d o l e v 、 e v e n 和k a r p 在8 0 年代开发了一系列的多项式时间算法，用于对一些协议的安 全性进行分析。 在形式化分析思想基础上发展起来的大多数形式化分析工具都采用了状态 探测技术，即定义一个状态空间，对其探测以确定是否存在一条路径，对应于攻 击者的一次成功的攻击。有些工具中用到了归纳定理推证技术，如在n r l 协议分 析器中，运用此技术证明搜索的空间规模已经可以确保安全性。在形式化分析技 术出现的早期阶段，它已成功地发现了协议中的人工分析难以发现的缺陷。如n r l 协议分析器发现t s i m m o n s 的选择性广播协议的缺陷，l o ng l e yr i g b y 工具发 1 0 第二章安全协议形式化分析方法 现了b a n k i n g 协议的缺陷，等等。 m b u r r o w s ，m a b a d i 和r n e e d h a m 1 4 首次提出的b a n 逻辑，是业界公认的 在解决安全协议形式化分析方面的犟程碑，被广泛应用在认证协议分析领域，至 今在使用逻辑手段分析安全协议方面取得的进展大都以b a n 逻辑为基础。b a n 逻 辑是关予主体信仰以及用于从“已知信仰”推出“新的信仰”的推理逻辑，它通过对 认证协议的运行进行形式化分析，研究认证双方通过相互发送和接收消息能否从 最初的信仰逐渐发展到协议运行的最终西的一认证双方的最终信仰，其嚣的是在 一个抽象层次上分析分布网络系统中认证协议的安全问题。如果在协议执行结束 时未能建立起关于诸如共辜通信密钥、对方身份等信任时，则表明这一协议有安 全缺陷。 自b a n 逻辑提出以来，针对其缺陷和不足，研究者对其进行了改进和补充， 形成了内容丰富的b a n 类逻辑。b a n 逻辑存在不可逾越的障碍使其应用受到限 制，l g o n g ，r n e e d h a m 和r y a h a l o m 提出了g n y 逻辑，g n y 逻辑试图消除b a n 逻 辑中对主体诚实性的假设、消息源假设、可识别假设。m a b a d i 和m r t u r t l e 提 出的a t 逻辑从语义的角度分析了b a n 逻辑，并作出改进，同时a t 逻辑给出了形 式化语义，并证明了其逻辑推理系统的合理性。p f s y v e r s o n 和p c v a n o o r s c h o t 提出的s v o 逻辑标志着b a n 及b a n 类逻辑的成熟。s v o 逻辑吸收了b a n 逻辑、g n y 逻辑、a t 逻辑等逻辑推理系统的优点，同时具有十分简洁的推理规则 和公理。作为目前最完善的b a n 类逻辑语义分析系统，s v o 逻辑在安全协议的分 析中逐步得到了广泛的应用。 1 9 9 8 年，t h a y e r 、h e r z o g 和g u t t m a n 提出了一种新的概念s t r a n ds p a c e 1 5 - 1 6 。这个新的概念吸纳了n r l 协议器、s c h n e i d e r 秩函数和p a u l s o n 归纳 法等思想，是一种新型有效的协议形式化分析方法。s t r a n d 是协议中某个合法 主体或攻击者行为事件的一个序列，由发送和接收的消息组成。对于一个诚实的 主体，s t r a n d 表示它在某轮协议中的行为。如果这个主体在段时间内参与了 多轮协议，则用不同的s t r a n d 表示，露且不同的主体行为用不同的s t r a n d 表示。 攻击者的s t r a n d 中的行为由攻击者己获知的消息的发送与接收行为组成。 s t r a n ds p a c e 是一个s t r a n d 集合，包括不同的协议合法主体的s t r a n d s ，以 及一个攻击者的s t r a n d 。可将之视为包括在协议有效时间内的所有合法的执行， 广东丁业大学丁学硕七学位论文 以及攻击者对这些执行中所包含的消息的所有可能的行为。 s t r a n ds p a c e 的特点是协议模型简洁，并且对协议正确性证明是比较容易 的。这一方法的一个有趣的概念是使用插图法来启发式地描述和推证协议的正确 性，因此可使分析者描绘出安全协议的画面，包括所受到的攻击、正确性定理以 及证明中的关键性步骤等。归纳起来，s t r a n ds p a c e 协议形式化分析方法的优 点可体现在以下几方面： 1 ) 给出一些数据项，如随机数或会话密钥的新鲜性只能出现在一轮协议中 的假设的清晰的语义 2 ) 给出攻击者可能的行为的一个详细模型，从而可开发出用于界定攻击者 能力的一般性定理，并与所分析的协议是不相关的 3 ) 给出了正确性的多种定义，包括秘密性和认证性的说明与推证 4 ) 使分析者能够深入细致地了解协议为什么是正确的，以及所需的假设。证 明是简洁的，可人工完成。 以上是形式化分析的典型方法和简要发展历史，目前常用的分类是把这些技 术分为基于推理结构性方法，基于攻击结构性方法和基于定理证明的方法。 2 2 基于推理的结构性方法 基于推理的结构性方法主要是运用逻辑系统从用户接收和发送的消息出发， 通过一系列的推理公理推证协议是否满足其安全说明。 这些逻辑系统通常由一些命题和推理公理组成。命题表示主体对消息的知识 或信仰，而运用推理公理可以从已知的知识和信仰推导出新的知识和信仰。 s y v e r s o n 在文献中给出了一个有关此领域的讨论。在这类方法中，最著名的就 是b a n 及b a n 类逻辑，以及用于分析电子商务协议的k a i l a r 逻辑。目前在这 方面最新的研究是k i n d r e d 提出的安全协议的生成理论r v 逻辑。 早先的安全协议形式化分析，主要集中于基于b a n 逻辑来说明和验证安全协 议。随后学者们经过研究发现，b a n 逻辑在理想化步骤等方面存在着不可逾越的 障碍，从而引发了为提高b a n 逻辑有效性的各种不同的努力，主要表现在以下几 个方面： ( 1 ) 对b a n 逻辑自身进行扩充导致了b a n 类逻辑的产生，如g ny 逻辑，a t 逻 1 2 第二章安全协议形式化分析方法 辑，s o v 逻辑等 ( 2 ) 为具体的协议设计特定的形式化分析工具，如分析电子商务协议的 k a i l a r 逻辑以及分析与时间相关的协议的c s 逻辑等 ( 3 ) 突破b a n 及b a n 类逻辑对协议主体的假设的局限性而提出的k g 逻辑， 以及突破主体信仰与知识的单调性而提出的n o n m o n o t o m i c 逻辑。 b a n 逻辑是由b u r r o w s 、a b a d i 和n e e d h a m 提出，为解决安全协议的分析问 题迈出了巨大的一步，是安全协议分析的一个里程碑，使用逻辑手段分析安全协 议取得的进展大都以它为基础。b a n 逻辑是一种关于主体信仰，以及用于从已有 信仰推知新的信仰的推理规则的逻辑。这种逻辑通过对认证协议的运行进行形式 化分析，来研究认证双方通过相互发送和接收消息，能否从最初的信仰逐渐发展 到协议运行最终要达到的信仰。其目的是在一个抽象层次上分析分布式网络系统 中认证协议的安全问题。如果在协议执行结束时，未能建立起关于诸如共享通信 密钥、对方身份等信任时，则表明这一协议有安全缺陷。b a n 逻辑的规则十分简 洁和直观，易于使用，因此得到广泛的认可，并成为逻辑形式化分析系统的标准。 b a n 逻辑试图回答以下问题：( 1 ) 协议要达成什么样的目标；( 2 ) 协议基 于的假设是什么；( 3 ) 协议是否存在冗余；( 4 ) 协议中的加密消息是否可以以 明文形式传递而不影响协议的安全性。 g n y 逻辑g n y 逻辑是由g o ng 、n e e d h a m 和y a h a l o m 于1 9 9 0 年提出的。由于 b a n 逻辑存在的不可逾越的障碍，使得其应用受到了限制。g ny 逻辑则试图消 除b a n 逻辑中对主体诚实性的假设、消息源假设、b a n 逻辑进行了改进：( 1 ) 取 消了一些全局假设，从而增加了b a n 逻，用于描述主体对其所期望的消息格式的 识别能力；( 3 ) 区分断言集合和符号集合；( 4 ) g n y 逻辑中引入了若干f r e s h 判断法则；( 5 ) 将主体信念集和拥有集加以区别，使逻辑系统显得更为自然。 b a n 逻辑和g n y 逻辑成功地分析了一些协议的缺陷，但它们都没有对逻辑 系统自身进行形式化的语义分析。s y v e r s o n 指出：语义的重要性在于它提供了 一个评估逻辑的方法。而评估一个逻辑最为关注的两个问题是：( 1 ) 完备性， 是否能够得到所有想得到的； ( 2 ) 合理性，是否能够回避所有不想得到的。 一般情况下，我们更侧重于合理性，这是因为很多逻辑基于生成所有可能 的协议漏洞。但如果逻辑自身是不完备的，也会在客观上错漏一些攻击。逻辑 广东工业大学工学硕士学位论文 语义可用于证明逻辑的完备性和合理性，语义的产生应当是与逻辑无关的。于 是，h b a d i 和t u t t l e 提出了a t 逻辑，这种逻辑给出了形式化语义，并证明了 其推理系统的合理性。 a t 逻辑从以下几个方面对b a n 逻辑进行了改进：( 1 ) 从语义的角度分析 b a n 逻辑，并对某些基本概念进行了修改；( 2 ) a t 逻辑引入了x 的概念，用 于表示并非为主体所生成的消息发送；( 3 ) 引进全部命题联结词，并将推理规 则改写成公理的形式，使逻辑语法更为清晰、简洁；( 4 ) a t 逻辑对b a n 逻辑 的语法进行了较大的改动，区分了公式与一般表达式。 针对b a n 逻辑的缺陷和不足，s y v e r s o n 和o o r s c h o t 从另一角度提出了s v o 逻辑。它的出现标志着b a n 及b a n 类逻辑的成熟。s v o 逻辑吸收了b a n 、g ny 和 a t 等逻辑系统的优点，具有十分简洁的推理规则和公理。它为逻辑系统建立了 用于推证合理性的理论模型。在形式化语义方面，s v o 逻辑对一些概念作了重新 定义，从而取消了a t 逻辑系统中的一些限制。其优点体现在以下几个方面： 1 ) 以往对b a n 逻辑的质疑集中在b a n 及b a n 类逻辑没有提供独立的明确的 语义基础，而这恰恰是逻辑系统的合理性的依据所在( 例如错误的结论不能从正 确的前提衍生) 。a b a 2d i 和t u t t l e 给出t b a n 逻辑的这样一个语义基础。s v o 逻辑的语义基础受到了a t 逻辑的启发，但在本质上又有所不同。 2 ) 具有一个相当详细的模型，从而极大地消除了由于形式化公式含义和推 理规则的推理能力引起的理解模糊问题。因此通过语义解释可使我们更准确理解 协议消息的真实含义，这有助于b a n 及b a n 类逻辑对协议的理想化。 3 ) 作为一个通用语义，s v o 逻辑具有极好的扩展能力，因此其本身并不是 一个复杂的逻辑系统。 k a i l a r 逻辑要从理论上证明一个协议的正确性和安全性是十分困难的问 题，即使对规模有限的协议也难以做到这一点。近几年出现的电子商务协议远比 认证协议复杂，往往要求具有不可否认性和可追究性等安全性服务，这类协议的 形式化分析具有更高的要求。原有的b a n 及b a n 类逻辑基本上是一种信念逻辑， 它的主要目的是证明主体相信某个公式，而电子商务协议中的可追究性的目的在 于某个主体要向第三方证明另一方对某个公式负有责任。所以b a n 及b a n 类逻辑 不能用于电子商务协议可追究性的分析。在这种情况下，一种新型的形式化分析 1 4 第二章安全协议形式化分析方法 工具k a i l a r 逻辑应运而生，它是一种针对电子商务协议的可追究性而开发的形 式化分析工具。 协议的类型是多种多样的。因此，对有些协议进行形式化时，需要根据自 身的特点来构造相应的分析方法。女h r i v e s t 、s h a m i r 矛d w a g n e r 提出了t i m e 的概 于解决与时间相关的安全性问题。根据他们的提法，t i m e d 2 r e l e a s e 秘密是在向 未来，即通过一个可信的第三方提供标准的时间参照，使得秘密只能在某个未来 时间公开。这类协议称为t i m e d 2 r e l e a s e 公钥协议。在上述的b a n 及b a n 类逻辑 的推证结构中没有考虑协议的时间因素，因此不能用于此类协议的分析。c o f f e y 和s a i d h a 提出一种将时间与逻辑结构相结合的逻辑c s 逻辑，其所包含的一些定 理对协议的秘密性进行了推证，如明确指出主体对某些解密消息的不可知性等。 可对c s 逻辑进行适当扩展，使之能更有效地对t i m e dr e l e a s e 类公钥协议进行 形式化分析。 对一个认证协议的分析可视为对主体信仰的评估。基于此，k a i l a r 和 g 1 i g o r 提出了一种与b a n 逻辑极为相似的逻辑，用于推证协议运行中信仰的变 化。在此协议中，信仰的变化由一个状态机表示，未来信仰是由当前信仰和执行 行为决定的： b e l i f e + a c t i o nn e wb e l i f e ，并为每一个消息内容引入了知识 集合的概念。术语“知识集合”是指在某次特定的会话中共享某一消息的主体，k g 逻辑更多侧重于知识集合中的消息交换的交互行为。 n o n m o n o t o m i c 逻辑是由r u b i n 提出的一种新的形式化分析方法。它与以往 的逻辑相比具有以下优点：( 1 ) 是第一个能非单调推理安全协议知识的方法： ( 2 ) 在协议形式化时无需理想化过程； ( 3 )