（计算机系统结构专业论文）基于串空间模型的安全协议分析与验证方法的研究.pdf

原创性声明 本人郑重声明：所呈交的学位论文，是本人在导师的指导下，独立进行研 究所取得的成果。除文中已经注明引用的内容外，本论文不包含任何其他个人 或集体已经发表或撰写过的科研成果。对本文的研究作出重要贡献的个人和集 体，均已在文中以明确方式标明。本声明的法律责任由本人承担。 学位论文作者：霉印蟆 日期：知o 年。月1 日 学位论文使用授权声明 本人在导师指导下完成的论文及相关的职务作品，知识产权归属郑州大学。 根据郑州大学有关保留、使用学位论文的规定，同意学校保留或向国家有关部 门或机构送交论文的复印件和电子版，允许论文被查阅和借阅：本人授权郑州 大学可以将本学位论文的全部或部分编入有关数据库进行检索，可以采用影印、 缩印或者其他复制手段保存论文和汇编本学位论文。本人离校后发表、使用学 位论文或与该学位论文直接相关的学术论文或成果时，第一署名单位仍然为郑 州大学。保密论文在解密后应遵守此规定。 学位论文作者： 隗荚 日期：，。年衫月 日 摘要 摘要 安全协议是网络安全的保障，网络中实体间通信的实现都是经过安全协议 来协助完成的，然而由于网络处在复杂的环境之中以及安全协议本身所具有的 缺陷，使得攻击者能够借助这些缺陷来对协议进行各种各样的攻击，从而达到 对网络安全进行破坏的目的，所以，在网络安全中对安全协议进行正确的分析 发挥着极其重要的作用。 形式化分析方法是分析安全协议一种最重要的方法，认证测试方法的提出 和a t h e n a 自动化方法的提出是串空间模型发展过程中两个最大的成就，本文在 对安全协议分析和验证方法进行深入研究的基础上，所做的主要工作和创新点 主要体现在以下几个方面： 第一，在对协议分析方法进行充分理解的基础上，深入研究和探讨了串空 间模型分析协议的特点，并能够用此种形式化的分析方法对安全协议进行分析 和验证； 第二，掌握了认证测试方法分析协议的特点，并针对该方法在分析协议时 存在的缺陷，对原有的认证测试方法进行了改进，扩大了其分析范围。并用改 进后的方法对t l s 协议进行了分析，分析结果表明改进后的认证测试方法的可 行性； 第三，提出了一种新的安全协议自动化分析方法，给出了相应的模型设计， 并提出了实现该模型所需的一系列算法，介绍了其分析协议的基本过程和特点； 第四，通过实验实现了本文所提出的模型的基本功能，并用所提出的模型 对改进前后的h e l s i n k i 协议进行了分析验证，实验结果表明所提出的协议分析 方法的正确性和高效性； 安全协议的自动化分析方法是形式化分析领域里一个前沿的方向，本文所 提出的安全协议自动化分析方法能有效克服手工分析存在的冗长理论推导和证 明的缺陷，使协议的分析更加简洁和直观，从而提高了安全协议分析的效率。 关键字：安全协议；串空间模型；认证测试方法；a t h e n a ；t l s 协议； 自动化分析；算法；h e l s i n k i 协议 a b s t r a c t a b s t r a c t s e c u r i t yp r o t o c o l sw h i c hp l a ya ni m p o r t a n tp a r ti nn e t w o r kc o m m u n i c a t i o n b e t w e e ne n t i t i e si st h e b a s i so fn e t w o r ks e c u r i t y h o w e v e r , a st h en e t w o r k e n v i r o n m e n ti sc o m p l e xa n dt h ed e f e c t so fs e c u r i t yp r o t o c o l s ，a t t a c k e rc o u l dh a n d t h e s ev u l n e r a b i l i t i e st oc a r r yo u ta v a r i e t yo f a t t a c k so ns e c u r i t yp r o t o c o l st om e e tt h e p u r p o s eo fd a m a g i n gn e t w o r ks e c u r i t y t h e r e f o r e , a n a l y z i n gs e c u r i t yp r o t o c o l s r e a s o n a b l ea n dc o r r e c t l yp l a y sa ni n c r e a s i n g l yi m p o r t a n tr o l ei nt h en e t w o r ks e c u r i t y f o r m a la n a l y s i sm e t h o di so n eo ft h em o s ti m p o r t a n tm e t h o do fs e c u r i t y p r o t o c o la n a l y s i s p r o p o s i n gt h ea u t h e n t i c a t i o nt e s tm e t h o da n da u t o m a t e da n a l y s i s m e t h o do fs e c u r i t yp r o t o c o la t h e n ai st h et w om o s ti m p o r t a n te v e n t si nt h e d e v e l o p m e n to fs t r a n ds p a c em o d e l ，t h i sp a p e rb a s e do nh a v i n gm a d ea ni n t e n s i v e s t u d yo fa n a l y s i sa n dv e r i f i c a t i o nm e t h o d so fs e c u r i t yp r o t o c o lh a sm a i n l yd o n et h e f o l l o w i n gw o r ka n di n n o v a t i o n ： f i r s to fa l l ，ih a v em a d ei n t e n s i v es t u d ya n de x p l o r a t i o no fs t r a n ds p a c em e t h o d o fs e c u r i t yp r o t o c o la n a l y s i sb a s i n go ni n d e p t hu n d e r s t a n d i n go fp r o t o c o la n a l y s i s m e t h o d ，s oic o u l da n a l y z ea n dv 嘶匆s e c u r i t yp r o t o c o lw i t l ls t r a n ds p a c em o d e lo f f o r m a la n a l y s i sm e t h o d s e c o n d l y , ih a v em a s t e r e do ft h ea u t h e n t i c a t i o nt e s tm e t h o do fs e c u r i t yp r o t o c o l a n a l y s i s ，a n dih a v ei m p r o v e dt h eo r i g i n a la u t h e n t i c a t i o nt e s tm e t h o db yo v e r c o m i n g i t ss h o r t c o m i n g ss oa st oe x p a n dt h es c o p eo fi t sa n a l y s i s w h a t sm o r e ，t l sp r o t o c o l h a sb e e na n a l y z e dw i t ht h ei m p r o v e da u t h e n t i c a t i o nt e s tm e t h o da n dt h ea n a l y s i s r e s u l tp r o v e st h ee f f e c t i v e n e s so f t h ei m p r o v e dm e t h o d t h i r d l y , t h i sp a p e rh a sp r o p o s e d a na u t o m a t e da n a l y s i sm e t h o do fs e c u r i t y p r o t o c o la n d i t sc o r r e s p o n d i n gm o d e lh a sa l s ob e e nd e s i g n e d ，a b o v ea l l ，as e r i e so f a l g o r i t h m st h a tt h ec o r eo f t h em e t h o dw e r ep u tf o r w a r dr oa c h i e v et h em o d e l a n d p r e s e n t e dt h ep r o c e s sa n dc h a r a c t e r i s t i co fi t sp r o t o c o la n a l y s i s t h el a s tb u tt h em o s ti m p o r t a n to fa l l ，t h eb a s i cf u n c t i o no ft h em o d e lw a s a c h i e v e db ye x p e r i m e n t s ，a n du s i n gt h em o d e la n a l y z e dt h eo r i g i n a la n di m p r o v e d h e l s i n k ip r o t o c o lt op r o v ea c c u r a c ya n de f f i c i e n to ft h ep r o p o s e dm e t h o d i i a b s t r a c t a u t o m a t e da n a l y s i sm e t h o do fs e c u r i t yp r o t o c o li saf o r w a r dd i r e c t i o ni nt h 彦 f i e l do ff o r m a la n a l y s i s ，t h ea u t o m a t e da n a l y s i sm e t h o dt h a tw a sp r o p o s e di nt h i s p a p e ro v e r c o m e st h ed i s a d v a n t a g eo fm a n u a la n a l y s i so fs e c u r i t yp r o t o c o l ，s oi t m a k e st h ep r o c e s so fs e c u r i t yp r o t o c o la n a l y s i sm o r es i m p l ea n di n t u i t i v e ，a n d i m p r o v e st h ee f f i c i e n c yo fs e c u r i t yp r o t o c o la n a l y s i s k e yw o r d s ：s e c u r i t yp r o t o c o l s ；s t r a n ds p a c em o d e l ；a u t h e n t i c a t i o nt e s tm e t h o d ； a t h e n a ；t l sp r o t o c o l ；a u t o m a t e da n a l y s i s ；a l g o r i t h m s ；h e l s i n k ip r o t o c o l i i i 目录 目录 摘要_ i a b s t r a c t i i 目录：l v 图和附表清单v i i 1 前言1 1 1 安全协议概述1 1 1 1 安全协议简介1 1 1 2 安全协议性质2 1 1 3 协议缺陷类型。3 1 2 研究历史及现状一4 1 3 研究意义及论文结构安排一7 1 4 本章小结7 2 安全协议分析基础8 2 1 密码学知识一8 2 1 1 秘密通信系统8 2 1 2 密码体制lo 2 。1 3 密码学的应用一11 2 2 串空f , j ( s t r a n ds p a c e ) 1 3 2 2 1 串空间模型简介1 3 2 2 2 基本概念一1 4 2 3 串空间模型分析协议1 7 i v 目录 2 3 1 串空间中协议的正确性1 7 2 3 2 串空间的协议分析1 8 2 4 本章小结2 0 3 认证测试方法2 1 3 1 认证测试方法及其扩展2 1 3 1 1 认证测试方法简介2 l 3 1 2 认证测试方法的扩展2 2 3 2t l s 协议分析2 3 3 2 1t l s 协议的串空间模型2 3 3 2 2t l s 协议认证性分析2 4 3 3 本章小结2 6 4 安全协议自动化分析方法2 7 4 1 协议自动化分析简介2 7 4 2 模型设计一2 7 4 2 1 模型架构2 7 4 2 2 模型简介2 8 4 3 算法描述2 8 4 3 1 初始化协议算法2 8 4 3 2 协议串生成算法3 0 4 3 3 协议路径生成算法3l 4 3 3 1 路径图31 4 3 3 2 路径图的邻接矩阵表示3 2 4 3 3 3 协议路径的生成3 3 4 3 4 协议路径分析算法一3 6 4 4 本章小结3 8 5 模型实现及应用3 9 5 1 模型实现3 9 v 目录 5 1 1 数据库设计4 0 5 1 2 功能设计4 l 5 2 模型应用4 3 5 2 1 实验分析4 3 5 2 2 模型评价4 5 5 3 本章小结4 7 6 结尾篇4 8 参考文献4 9 致谢5 2 个人简历在学期间发表的学术论文与研究成果5 3 图和附表清单 图和附表清单 图1 1 安全协议示意图第l 页 图2 1 加解密过程示意图第8 页 图2 2 秘密通信系统模型一第9 页 图2 3 数字签名过程第1 1 页 图2 4r p c 协议串空间模型第1 9 页 图3 1t l s 协议串空间模型第2 4 页 图4 1 安全协议自动化分析模型第2 7 页 图4 2 初始化协议流程图第2 8 页 图4 3 串序列生成算法流程图第3 0 页 图4 4 路径图第3 2 页 图4 5 邻接矩阵第3 2 页 图4 6 状态路径图生成算法流程图第3 3 页 图4 7 状态路径生成流程图第3 5 页 图4 8 状态路径分析流程图第3 7 页 图5 1 模型实现总体结构图第3 9 页 图5 2i p o - 初始化协议模块第4 1 页 图5 3i p o - 串序列生成模块第4 2 页 图5 4i p 0 _ 状态路径生成模块第4 2 页 图5 5i p o - 状态路径分析模块第4 2 页 图5 6h e l s i n k i 协议串第4 3 页 图5 7h e l s i n k i 协议路径及其分析结果第4 3 页 图5 8 改进后h e l s i n k i 协议串第4 5 页 图5 9 改进后h e l s i n k i 协议路径及其分析结果第4 5 页 图5 1 0n s 协议分析状态数对比图第4 6 页 表i 1 协议缺陷分类第3 页 表1 1 协议缺陷分类( 续) 第4 页 表5 1 协议信息表第4 0 页 表5 2 串序列信息表第4 l 页 表5 3 状态路径信息表第4 l 页 表5 4 改进后h e l s i n k i 协议分析过程对比表第4 7 页 v i i 1 前言 1 前言 1 1 安全协议概述 1 1 1 安全协议简介 由于网络所处环境的复杂性和多变性，它的安全性也越来越受到威胁，因 此，对网络安全性的维护也更加重要，安全协议作为网络安全的基础，对其 安全性的分析在整个网络中发挥着非常重要的作用。安全协议工作在互联网中， 是以密码知识为基础的一种通信协议，它主要通过密码算法来达到保密消息和 分配密钥等目的，从而为参与协议的合法主体来提供保障。 按照功能需求可以把网络环境中最普遍的安全协议分为用于认证的协议、 用来交换密钥的协议、前两者结合的协议以及电子商务协议四类。第一种协议 的主要目的是保护合法主体以免受到来自非法用户的截获、伪造和重放等攻击， 它主要有主体身份认证，消息源和消息目的认证等协议；第二种协议主要用于 在协议通信的双方之间分配所需的密钥从而来保证协议的顺利完成，它通常是 和第一种协议共同工作的。网络中使用最多的是第三种协议，它把前两种协议 融合在一起，在对协议主体的身份顺利认证之后，再为其提供完成协议需要的 密钥；最后一种协议它与前几种协议有很大的差别，在这种协议当中，协议主 体关注的是参与交易的主体的公平性，其根本利益是相互冲突的。 图1 1 安全协议示意图 安全协议工作在分布式环境中，这种环境的不安全因素构成了对安全协议 1 前言 最严重的威胁。可以把协议与它工作的环境模拟为一个整体，这个整体构成一 个系统如图1 1 所示的安全协议示意图髓1 ，它主要是由合法主体、攻击者及一 系列规则组成的。攻击者作为一个非法主体可以对所交换的消息进行修改、转 发和重放等恶意操作，攻击者的k s ( k n o w l e d g es e t ) 包括所有已知的消息以及合 法主体所交换的消息，这是通过非法操作实现的，它还可以对k s 中的消息进 行处理，处理后消息也会放到k s 中。 攻击者的行为总体上可分为主动攻击和被动攻击两种，被动攻击者可以窃 听并获得重要信息，而主动攻击者则可对信息截获和做一定的修改，并能够冒 充合法主体来进行协议。对于主动攻击而言，可以通过加密操作来预防，加密 消息的改变会引起解密的错误，这是由于没有得到所需的密钥，这种情况下攻 击者仅仅可以阻止消息的顺利发送，其操作概括起来有如下几种： ( 1 ) 修改后转发消息； ( 2 ) 合并消息； ( 3 ) 把消息转发到它所需要的接收者； ( 4 ) 延长发送时间； ( 5 ) 对消息进行重新发送。 1 1 2 安全协议性质 由所交换的消息来对合法主体进行确认，再提供顺利完成协议必须的密钥 这是安全协议的主要目的，并且在对协议实体身份进行确认的基础上，也必须 确保所交换的主要协议内容的保密和不受攻击者破坏。总之，在协议结束时这 些安全性质都能得到保证是安全协议的最终目标，即测评安全协议安全性的标 准就是考查其需要满足的安全性质是否受到非法用户的攻击。 安全协议的安全性质口1 按照其自身的特点概括起来有保密性、认证性、完 整性和不可否认性。这四个性质是互相交融和渗透的，从而来共同保障安全协 议安全性的实现。其中，保密性顾名思义，是用来确保所交换的消息只被合法 的协议主体所拥有，而不能被非法主体所得到，此目的可以通过加密来实现， 把所交换的消息明文加密为密文，非法用户就算得到了其基本格式，但由于没 有密钥也不可以知道其内容，同时，因为缺乏对所选择的密码算法具体过程的 考虑，有时候会引起保密的顺利完成；认证性是网络中的实体来对相互的身份 确认的衡量标准，它也是协议的其它性质得以实现的基础。协议主体之间信任 2 。 1 前言 的确立是由证明它和可信第三方所拥有的秘密来实现的，认证不仅能够用来核 实参与协议的主体的身份，对协议主体和所交换的消息进行确认，还可以防止 非法用户冒充合法协议主体参与通信。在进行通信的过程中，参与协议的主体 的认证分为单向认证和双向认证，单向认证只需要对协议中一方的身份进行确 认，而双向认证则需要对协议双方的身份都进行确认。进行认证的过程也就是， 如果有那个主体宣告自己是协议参与的一方时，就需要对其身份进行确认，同 时，此主体也可以通过提供能够标识自己身份的证据来完成认证。 协议另外一个重要的性质是完整性，这主要是通过签名和封装来确保协议 所交换的消息不被攻击者所破坏，也就是设置完整性的校验值，在所交换的信 息上加上一个由h a s h 函数生成的附加信息，来对信息的完整性进行确认。其中 重要的一点是，协议主体必须对所选择的算法和其它标识信息有一个统一的标 准，这是由于非法用户在得不到密钥的情况下对所加密的信息进行了修改，就 会出现错误的分析结果，这是通过对所加密协议信息的冗余来保证的。最后一 个性质是不可否认性，它主要是用来对参与协议实体的行为进行监督，经过协 议的一方所掌握的信息提交给可信第三方来对另一方的行为进行确认，使对方 不可以抵赖其发送或接收的信息，从而来保障自己的合法利益，这主要应用于 电子商务协议中。 1 1 3 协议缺陷类型 由于安全协议的设计是多样的以及其工作环境是十分复杂的，因此它在实 际应用是仍然会出现多种类型的缺陷，该缺陷可能是由各种因素引起的，用一 种普遍的分类方法对安全协议缺陷进行分类是不可能的，d s p i n e l l i s 和s g r i t m i s 按照协议缺陷h 1 的起因和对策将安全协议缺陷主要分为如下几种类型： 表1 1 协议缺陷分类 3 1 前言 口令密钥 猜测缺陷 基本协议缺 陷 协议主体所使用的 密钥比较简单，安 全级别相对比较 低，非法实体经过 简单的运算和推导 就能够得到合法主 体的口令或者密 钥，来非法操作 协议设计时缺乏对 攻击者的预防 陈旧消息缺设计协议时没有考 陷虑协议主体交换信 息的新鲜性 并行会话缺协议主体疏忽对非 陷法实体的防备，误 认为攻击者是合法 主体而与其通信 内部协议缺协议不可达 陷 可以充分借助 于口令监视程 序和口令生成 器来加强口令 的安全性和复 杂度，以减少口 令被推导出的 概率。 具有普遍性，协 议设计时要考 虑周密 既可以对信息 的源主体攻击 也可以对目的 主体攻击 非法实体用一 定的信息来换 取合法主体非 常重要的协议 内容 协议在执行过 程中总会有一 方中间停止 通过各种方法推 断用户的口令或 者密钥来对其进 行攻击，可以记 录合法主体登录 次数和相关信息 进行推测口令 非法用户伪造 协议主体消息 非法实体对协议 进行消息重放攻 击 攻击者伪装成合 法主体参与协 议，获取关键的 协议内容，对协 议进行攻击 此种缺陷是由协 议内部因素引起 的 非法实体从第三方 服务器的应答中猜 测口令，进行非法 操作，比如在n s s k 协议中所存在的攻 击，就是由于其存 在此种类型的缺陷 引起的 签名已经加密的协 议内容而引起的攻 击 h e l s i n k i 协议的消 息重放攻击 y a l a l o m 协议在执 行过程中，攻击者 可以冒充合法主体 a 参与协议，得到 主体b 发送的消息 设计的协议对运行 路径的考虑不周到 不能保证正常终1 卜 1 2 研究历史及现状 随着信息化时代的来临，信息在社会经济和生活中发挥着越来越重要的作 用，信息安全的地位也显得尤为重要，它是一个综合的多学科的领域，其中关 4 1 前言 系到安全协议、密码学、信息分析、访问控制、紧急处理和安全的体系结构等， 这里安全协议是信息安全的基础保障。然而，因为安全协议本身设计上的独特 性和所处环境的复杂性，它在执行过程中会遇到很多困难，从而对安全协议的 顺利完成构成威胁并产生错误，这个错误是十分复杂和多样的，用人为的方法 来查找是相当有难度的，因此，对安全协议进行分析时总是通过特定的方法或 者模型来操作的，这样可以较快地发现协议中所存在的缺陷，并对其加以改正， 安全协议的形式化分析方法是一种重要的分析工具，它关键是对协议主体所使 用的密钥进行确认。 对安全协议的安全性进行分析最重要的一种方法就是形式化的分析啼1 方 法，这种方法用于分析协议已经有数十年了，在此期间，形式化的分析方法不 断涌现，每种方法都有各自的优点，并不断改进和完善使之日趋成熟。n e e d h a m 和s c h r o e a e l 开创了安全协议形式化分析方法的先河，随后，s a c c o 和d e n n i n g 在1 9 8 1 年指出了n s 协议嘲所存在的缺陷，由此使更多的人开始从事这方面的 探讨和研究。安全协议的形式化分析方法虽已有一定成效但其发展过程是漫长 的，y a o 和d o l e v 首先实际意义上地在这一领域有所成就，第一次提出了一种 形式化的模型，在该模型当中存在一个以上的协议交叉通信的情况，其中既有 合法的协议主体也有非法的用户，非法的用户可以进行篡改、伪造和窃听等非 法操作，此模型为以后协议形式化分析模型的提出奠定了基础，n r l 协议分析 器口1 ，i n t e r r o g a t o r 和l o n g l e y - r i g b y d o l e v 工具都是基于此模型提出的。形式化分 析过程中也有不成功的探索，比如二十世纪五六十年代e v e n 等提出了许多主要 可以进行安全协议分析的多项式时间算法，但是由于其分析范围有一定的局限 性，此类方法并没有得到推广使用。 状态探测方法是安全协议形式化分析方法中重要的一种，它是在上述模型 基础上发展起来的一种形式化分析工具，其工作原理为，首先定位一个状态集， 然后对这个集合进行扫描以检查非法实体的攻击路径是否能够成立。形式化的 分析工具总是和某种技术相结合使用，在n r l 分析器里就用到了归纳定理推证 技术，来协助核实已经搜索的集合足以证明协议的正确性。此技术在安全协议 形式化分析领域中已经取得了一定的成效，例如运用l o n g l e y - r i g b y 工具成功地 发现了b a n k i n g 所存在的缺陷，首次使用n r l 分析器成功地发现了s i m m o n s s e l e c t i v eb r o a d c a s t 协议所存在的缺陷等。 b a n 逻辑协1 的提出是安全协议形式化分析领域的一个转折点，使形式化分 5 1 前言 析技术上升到一个新的高度，使人们对安全协议形式化分析方法的研究更加深 入，并由此出现了更多的协议分析工具。b a n 逻辑与上述的状态探测方法有很 大的差异，它是通过推理来进行判断的，主要是由己知的知识和信仰来推断新 的知识和信仰的方法。这种方法分析协议具有使分析过程更加清晰和明了的特 点，实现也比较简单，主要是在协议的执行过程中来分析的，从而对协议主体 的原始信仰和主体的目标信仰来进行确认，对协议要满足的性质进行判断。用 这种方法已经对著名的k e r b e r o s 协议、n s 协议等安全协议成功地进行了验证， 发现了其中所存在的缺陷，取得了一定的进展和突破。 b a n 逻辑属于基于推理的结构性验证方法，在这一研究领域里b r a c k i n 在 深入研究g n y 逻辑的基础上提出了h o l 理论，s v o 逻辑总结了前两种系统逻 辑的优点，能够用来验证不可否认协议的安全性，规则的简洁化优化了推理的 过程；基于攻击的结构性验证方法是另外一种形式化分析方法，在此作出突出 贡献的有l o w 提出了使用f d r 队嘲能够检测到n s 协议所存在的攻击，随后， 各种形式化分析方法日趋集中和完善，具有代表性的有s t e m 等通过m u r 模型 分别对t m n 协议、k e r b e r o s 协议和n s 协议进行了分验证析。c a p s l 是m i l l e n 为了统一协议形式化分析语言而提出的，为以后其它方法的提出提供了规范化 的标准，具有较强的应用价值。l o w e 和r o s c o e 在充分探讨研究进程代数c s p 的基础上，各自通过不同的途径使在复杂系统中协议的分析细化到较小系统中 的协议的分析，能达到同样的分析结果，这一理念的提出是一个巨大的创新， 也使得人们更加关注于这一领域的研究；另外种方法是基于证明的结构性验 证方法，这种方法的主要原理是，通过对协议所具有模型的研究并结合协议的 特点从而总结出一套协议分析的方法，串空间模型( s t r a n ds p a c e ) n 1 h 2 1 就是基 于这种方法提出的，它的出现在协议的形式化分析方法发展过程中有重大意义， 使之有了一个质的飞跃。 目前，对串空间理论的研究日益深入，它是协议形式化分析的一种重要方 法，基于此的研究也不断出现，首先是g u t t m a n 在此基础上提出的认证测试方 法n 3 14 l ，其次是s o n g 等人也在此基础上开发了协议自动证明工具a t h e n a n 副， 这种方法集模型检测和定理证明于一体，吸取了各自的优点，是一种全新的协 议分析方法，安全协议的自动化分析方法是当前协议形式化分析领域的前沿方 向。 6 1 前言 1 3 研究意义及论文结构安排 本文主要对基于串空间模型的安全协议形式化分析方法进行了重点研究， 在深入探讨串空间模型分析安全协议的基础上，针对认证测试方法存在的问题， 对其进行了改进和扩展，扩大了其分析范围，首次提出了主动测试中对测试分 量新鲜性的检验，从而进一步完善了认证测试方法；提出了一种协议自动化分 析方法，并给出了实现该模型的一些算法，通过实验实现了该模型的基本功能， 进一步提高了协议分析的效率。本文的结构安排如下： 首先，在前言部分，主要介绍了当前的研究现状以及研究意义，在安全协 议分析基础部分，重点介绍了密码学基础知识和串空间有关内容；其次，在对 基本理论有所了解的基础上，介绍了本文的主要工作和创新点，一方面是对认 证测试方法的改进和扩展，另一方面是提出了一种协议自动化分析方法，并且 实现了该模型的基本功能；最后是本文的总结部分。 1 4 本章小结 安全协议的形式化分析方法是本文研究的重点内容，这一章首先重点介绍 了安全协议的有关基础知识，包括安全协议的概念和主要性质，以及安全协议 形式化分析方法的分类、安全协议缺陷的类型以及安全协议研究历史和现状， 在对安全协议分析方法探讨的基础上，引出了当前安全协议形式化分析方法的 前沿方向一串空间模型以及在此基础上的认证测试方法和协议自动化分析方法， 这在以后章节中会有详细的介绍，最后给出了本文的结构安排。 7 2 安全协议分析基础 2 安全协议分析基础 2 1 密码学知识 密码学是安全协议的基础，协议双方通过密码学原语来完成相互之间的协 议内容，认证协议也是根据其中的密码体制n 胡来完成协议执行过程的，密码学 作为信息安全领域的重要组成部分，主要是对破译密码方法和秘密编码原理进 行探讨的一种体制。关键是对密码分析学和密码编制学有关内容进行研究的， 它们相互渗透，共同组成了密码学的整体机制。 2 1 1 秘密通信系统 为了对协议主体所发送的信息进行保密，使之不受攻击者的破坏，可以通 过秘密通信系统n 刀来实现。明文是协议发起者所发送的消息，密文是对明文进 行一系列操作所得到的变换后的信息，例如数据项p 称为明文，可以经过加密 将其转化为不能够被攻击者所识别的数据项c ，c 就是所对应的密文，同理，也 可以由c 通过解密运算来得到原始的明文p ，通常情况下，加解密操作只受所 使用的密钥的限制，但它所使用的算法是可以公开的，上述变换过程可以如下 图2 1 所示： 加密 图2 1 加解密过程示意图 解密 通常情况下密码员通过使用加密算法对原有的信息来进行加密从而得到密 文信息，接收方得到密文信息后要用解密算法对其进行操作从而得到原有明文 信息，密钥分为加密密钥和解密密钥两种，是用来对加解密过程所使用的算法 进行操作的，并协助其完成工作。 在一个系统当中进行消息传输时，除了上述的密码员以外还有密码分析员， 8 k 一 = 一 一 脚 一 ， 一 寄蝉， e 一 一 k 一 一 2 安全协议分析基础 密码分析员的主要职责就是对非法主体通过非法手段所得到的密文进行分析， 经过一系列的运算和推测，来得到原始的密钥或者明文信息。一个秘密信息系 统既可以有主动攻击也可以有被动攻击，上述过程经过非法操作获得密文并破 解出明文的行为是被动攻击，相对而言主动攻击是指，攻击者通过假冒、重放、 添加和破坏等手段直接对系统发起攻击，破坏原有的数据和安全性来满足自 身的利益以达到其攻击目的。 信源 p 搭线信道 非法接入i ( 主动攻击) 者ic 加密器 萨( p ) 琵圜 五 |k 密钥源 k l 密钥通道 搭线信道 ( 被动攻击) 解密器 p = d k j c c ) 蓊幽 b 密钥源 l j 图2 2 秘密通信系统模型 密码分析员lp l ( 窃听者) i 母 秘密通信系统模型示意图如上图2 2 所示，该系统主要包括如下主要内容： p 代表明文信息集合，y 代表密文信息集合，k ；和k ，组成了密钥集合，如果 是单钥体制下，那么k i = k f k ，进行的加密操作为：e 毛：p y 这里的k i ek i ， 该过程是由加密器来实现的；所进行的解密运算为：d 。：y p ，这里的k i k i ， 上述过程是由解密器来完成的。在这个整体的秘密信息系统当中，把特定的明 文信息p p 使用密钥岛k ；经过加密运算从而得到密文y 的过程为： ) ，= f ( p ，k i ) = ek i ( p ) p p k i k i 密文信息的接收者从安全信道那里来得到对所加密的信息进行解密的密钥 k ，k ，然后对它所收到的密文信息进行操作运算，进而得到原有的明文p ， 解密过程为： p = dl j ( y )p p ，k j e 蝎 此时，密码分析者就会对得到的密文进行分析和推算，一般使用的是函数 9 2 安全协议分析基础 h 来完成操作的，对密文y 进行操作后会得到一个明文集合p 中的数据，变换 如下： p l = h ( 奶 然后对得到的明文和原始明文进行比较，若p 。= p ，那么所进行的操作就 是成功的。 2 1 2 密码体制 密码体制在安全协议中发挥着相当重要的作用，它是安全协议的基础，从 基本原理上可以将其主要分为对称密码体制和公钥密码体制两种。 就对称密码体制而言，它所使用的解密密钥和加密密钥可以相互推导出， 对于采用对称密码体制的系统来说，其保密性主要是由密钥来决定的而和所使 用的加解密算法无关。在此系统当中起主要作用的是密钥的保密性，在获得密 文后如果不知道密钥，而仅仅知道所使用的加密算法，要推导出明文也是不可 以实现的。在对称密码体制中密钥既可以是由发送者确定的再通过保密的方法 传给接收者，也可以由可信第三方确定然后秘密地发送到通信合法主体，该体 制的关键是怎样确定通信过程所需要的密钥和怎样把所确定的密钥秘密地传送 到通信合法主体。 h e l l m a n 和d i f f i e 于1 9 7 6 年第一次引入了公钥密码体制，在密码学的研究 领域具有重要意义，a d l e m a n ，r i v e s t 和s h a m i r 于1 9 7 7 发明了著名的r s a 算 法。在这种密码体制当中，任何一个合法主体都会使用一个私有密钥s k 和一个 公开密钥p k ，和对称密钥加密体制相同的是，它所使用的加解密算法也是可以 公开的，然而由公开密钥推导私有密钥是不可行的。该密码体制可以通过使用 单向陷门数学函数来确保其可靠性，它具有如下的特点： 解密不能够由加密密钥来实现，也就是dp k ( e p k ( p ) ) p ； 解密和加密所对应的操作可以交换次序，明文p 使用加密密钥p k 加密 后，可以通过d ( e ( p ) ) = p 或者e ( d ( p ) ) = p 用解密密钥s k 来解密从而得到 明文； 公开密钥和私有密钥可以一起生成，但是由公开密钥来推导出私有密 钥是不可能的。 解决一些问题在计算上所存在的难度是公钥算法最根本的出发点，而分解 大整数是其中的一个难题。然而r s a 算法也存在一定的不可靠因素，因为密码 1 0 2 安全协议分析基础 分析者可以根据所得到的公钥k 推算出p 和毋由此也促使了更多的人关注于数 论领域中有关分解因子的研究，而且有了一定的进展。 2 1 3 密码学的应用 数字签名n 町是保证信息完整性和保密性的重要技术，它随着互联网技术的 不断发展也在日益改进，在一个完整的数字签名当中，对于接收方而言，只有 它具有对签名进行核实的权限，使得除此之外的主体不可以冒充签名；对发送 方而言，它不可以抵赖其签名行为；对可信第三方而言，它可以解决双方对已 经签名的确认而发生的冲突。 在具体的应用中，若所传输的内容是能够公开的，但是一定要保证信息不 被篡改，这可以用数字签名技术来实现上述目标；若所传输的内容是需要保密 的，此时就需要在确保其完整性的同时还要确保其保密性，这就必须把数字签 名和加密相结合来完成。 发送方a 用a 的私 钥签名 图2 3 数字签名过程 接收方b 用a 的公 钥验证 比较 数字签名的工作过程如上图所示，具体步骤为： ( 1 ) 产生信息摘要，发