（计算机应用技术专业论文）安全协议形式化分析中认证测试方法的研究.pdf

摘要 摘要 安全协议是安全共享网络资源的机制和规范，是构建网络安全环境的基石， 其安全性对整个网络环境的安全起着至关重要的作用。由于协议安全属性的多样 性和微妙性、攻击者模型的不确定性、协议运行环境的复杂性和协议会话的高并 发性，安全协议的设计与分析至今仍是一项具有挑战性的工作。形式化方法的出 现有助于精确定义安全协议的目标，准确描述安全协议的行为，验证安全协议是 否满足预期目标。人们在安全协议的形式化分析上研究探索了近三十年，但这个 领域仍然远未成熟。串空间理论的出现将安全协议形式化分析推向了一个新的高 度，它以简洁、严谨、高效的特点成为近年来安全协议形式化领域的研究热点。 在串空间理论上发展起来的认证测试方法以挑战应答机制为基础，它充分利用串 空间理论中代表事件因果关系的偏序结构，不仅继承了传统串空间模型简单直观、 状态空间少的优点，还简化了证明过程，更符合安全协议形式化分析的发展方向。 本文以认证测试方法在协议形式化分析和协议辅助设计中的应用、认证测试 理论的扩展和改进，基于认证测试的协议自动化分析算法的设计与实现为主要内 容，进行了系统深入的研究，取得了如下创新性成果： 1 从协议分析的角度考虑对协议安全构成威胁的攻击类型和攻击者行为，着重对 最为常见的攻击形式重放攻击进行了分类研究。指出了s y v e r s o n 重放攻击 分类法的不足，按攻击产生的原因将重放攻击分成了五类，针对每个类别列出 具体的攻击实例，并提出抵御该类攻击的原则性方法。这种新的重放攻击分类 法对于更好地认识各种攻击的原理及寻找有效解决措施具有积极的意义。 2 分别使用串空间最小元素方法、理想诚实方法和认证测试方法对o t w a y - r e e s 协议进行分析，总结了这三种方法进行协议分析的过程和特点，指出认证测试 方法是前两者的归纳与概括，是理论上的进一步深入，其证明过程更简洁高效。 使用认证测试方法对x 5 0 9 三消息协议进行保密性和认证性分析，指出该协议 存在的问题及可能受到的攻击；对协议加以改进，并使用认证测试方法证明了 改进协议的正确性。 3 结合协议设计一般原则和j d g u t t m a n 的协议设计思想，阐述了将认证测试方 法用于辅助协议设计的可行性，提出了基于认证测试的通用协议设计思想。将 协议设计过程分解为五个步骤，详细讨论了对称密钥体制和不对称密钥体制下 摘要 构造认证测试的方法。并使用该方法设计了一个新的双向认证密钥协商协议， 扩展了认证测试方法的应用范围。 4 将基于认证测试的安全协议形式化分析过程标准化，解决了“认证测试方法的 证明过程过于依赖分析人员的主观判断 和“认证测试元素出现位置可能不唯 一”的问题，使得认证测试的应用过程更严谨规范，有利于自动化分析工具的 实现。使用标准化方法对b a n y a h a l o m 协议进行分析，找到了针对该协议的 一个已知攻击的更普遍形式。 5 分析了认证测试方法中“测试元素不能是任何常规结点消息组成元素的真子 项这一局限性产生的根本原因，指出了p e r r i g 和s o n g 改进方案的漏洞，提 出的新认证测试理论有效突破了认证测试定理无法分析多重加密协议的局限 性，并通过理论证明和实例分析说明了新认证测试定理的正确性，进一步扩展 了认证测试方法的应用范围。 6 针对“认证测试理论不能识别类型缺陷攻击 的不足，结合强制类型检查思想， 将消息项的类型和检查机制引入认证测试方法，使得认证测试方法可以根据应 用需求检测出不同层次的类型缺陷攻击。并以o t w a y r e e s 、a n d r e wr p c 和 w o o l a m 改进协议的分析为例，确认了这一改进的成功。 7 根据认证测试理论的上述三点改进，模拟手工证明过程，设计了一个基于认证 测试的协议自动化分析算法a t a p a 并进行了初步实现。该算法利用串空间理 论和认证测试方法的思想，有效避免了传统自动化分析工具的状态空间爆炸问 题，同时能获得较高的分析效率。使用a t a p a 算法对n s l 协议、w o o l a m 改 进协议的认证属性进行分析，得到了与目标一致的结论，一方面证明了协议自 动化分析算法的成功，另一方面也验证了改进认证测试理论的正确性。 关键词：串空间，认证测试，安全协议，协议自动化分析 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 s a red e s i g n e df o rc o m m u n i c a t i o no v e ri n s e c u r en e t w o r k s e c u r i t yp r o t o c o l sw o r ka sc o r ec o m p o n e n t so fn e t w o r ks e c u r i t y , s o t h e i rc o r r e c t n e s si s c r u c i a lt on e t w o r ks e c u r i t y t h ed e s i g n i n ga n da n a l y z i n go fs e c u r i t yp r o t o c o l sr e m a i n sa c h a l l e n g ef o rt h es u b t l e t yo fs e c u r i t yg o a l s ，t h eu n c e r t a i n t yo fp e n e t r a t o rm o d e l ，t h e c o m p l e x i t yo f t h er u n n i n ge n v i r o n m e n t ，a n dt h eh i 。g hc o n c u r r e n c yo fp r o t o c o ls e s s i o n s f o r m a lm e t h o d sc o n t r i b u t et od e f i n es e c u r i t yg o a lo fp r o t o c o l sp r e c i s e l y , d e s c r i b e b e h a v i o r o fp r o t o c o la c c u r a t e l y , a n dv e d f yw h e t h e rt h ep r o t o c o lm e e tt h et a r g e t c o r r e c t l y t h r o u g hn e a r l yt h r e ed e c a d e so fd e v e l o p m e n t ，f o r m a la n a l y s i s o fs e c u r i t y p r o t o c o l si si m m a t u r ey e t t h ee m e r g e n c eo fs t r a n ds p a c et h e o r ys e t so f f an e w u p s u r g e o fs e c u r i t yp r o t o c o l sf o r m a la n a l y s i s s t r a n ds p a c et h e o r ya t t r a c t ss i g h t so fr e s e a r c h e r s s o o nf o ri t sc o m p a c tm o d e l ，p r e c i s ed e f i m t i o na n de f f i c i e n tp r o o f a u t h e n t i c a t i o nt e s t b a s e du p o nc h a l l e n g e r e s p o n s em e c h a n i s mi san o v e lm e t h o dd e r i v e df r o ms t r a n ds p a c e t h e o r y i ti n h e r i t sa d v a n t a g e so fs t r a n ds p a c e ，s i m p l i f i e sp r o v i n gp r o c e s sf u r t h e r , a n d p r o v i d e sm o r ep o w e r f u la n a l y s i sc a p a b i l i t i e so na u t h e n t i c a t i o np r o p e r t i e s t h i st h e s i sm a k e sa ni n d e p t hs t u d yo fa u t h e n t i c a t i o n t e s t s a p p l i c a t i o ni n a n a l y z i n ga n dd e s i g n i n go fs e c u r i t yp r o t o c o l s ，e x p a n d sa u t h e n t i c a t i o nt e s tt h e o r yi n t h r e ea s p e c t s ，a n dt h e nd e s i g n sa na u t o m a t i cp r o t o c o lv e r i f i c a t i o na l g o r i t h mb a s e do n e n h a n c e da u t h e n t i c a t i o nt e s t r e l a t e de f f o r t sr e s u l ti nf o l l o w i n gm a j o ri n n o v a t i v e a c h i e v e m e n t s ： 1 t a x o n o m i cs t u d yo fr e p l a ya t t a c k sw h i c hm a yd og r e a th a r mt os e c u r i t yo fp r o t o c o l s p r o p o s e dan e wc l a s s i f i c a t i o nm e t h o db a s e do nt h eu n d e r l y i n gr e a s o n sf o rs u c c e s s o fa t t a c k s f o re a c hc a t e g o r y , e x a m p l e so fs u c c e s s f u la t t a c k sa r el i s t e da n dt h e m e t h o d sa g a i n s tt h o s ea t t a c k si np r i n c i p l ea r ep r e s e n t e d 2 m i n i m a l - e l e m e n tm e t h o d i d e a l - h o n e s tm e t h o da n da u t h e n t i c a t i o nt e s tm e t h o da r e s e p a r a t e l yu s e dt ov e r i f ys e c r e c ya n da g r e e m e n tp r o p e r t i e so fo t w a y - r e e sp r o t o c o l ， f o l l o w e db ys u m m a r i z i n gt h ec h a r a c t e r i s t i c so fe a c hm e t h o dt h r o u g hc o m p a r i s o n i t s h o w st h a ta u t h e n t i c a t i o nt e s ti st h em o s tc o n c i s ea n de f f i c i e n to n ef o rp r o t o c o l a n a l y s i s a sa c a s es t u d y , s e c r e c ya n da g r e e m e n tp r o p e r t i e so fx 5 0 9 ，a na s y m m e t r i c i i i a b s t r a c t k e yp r o t o c o l ，a rev e r i f i e d ，t h e nf o u n da n da m e n d e dt h ef l a w si ni t 3 a p p l i e da u t h e n t i c a t i o nt e s t t oa u x i l i a r yp r o t o c o ld e s i g n i n g d e s c r i b e dt h et h o u g h t a n dp r o c e d u r eo fd e s i g n i n gp r o t o c o l si nt e r m so fa u t h e n t i c a t i o nt e s tf r o ms t a n d p o i n t o f p r o t o c o la n a l y s i s e s p e c i a l l y d i s c u s s e dt h ed i f f e r e n c ei n c o n s t r u c t i n g a u t h e n t i c a t i o nt e s tu n d e r s y m m e t r i c k e y a n d a s y m m e t r i c k e yc r y p t o g r a p h y d e s i g n e dan e wm u t u a la u t h e n t i c a t i o np r o t o c o l 、i t hk e yn e g o t i a t i o nu s i n gt h a t a p p r o a c h 4 s t a n d a r d i z e dt h ep r o v i n gp r o c e s so fp r o t o c o l s s e c u r i t ya t t r i b u t e s 、历t 1 1a u t h e n t i c a t i o n t e s t t om a k ei tm o r er i g o r o u s ，f o r m a la n de a s yt oi m p l e m e n ti na u t o m a t i ct o o l s b a n - y a h a l o mi sa n a l y z e d 州t i lt h es t a n d a r d i z e dp r o v i n gm e t h o d ，a n df o u n da n o r m a lf o r mo fa na t t a c kt oi t 5 i l l u s t r a t e dt h ee s s e n t i a lc a u s eo fl i m i m t i o no fa u t h e n t i c a t i o nt e s t , t h a tt e s tc o m p o n e n t c a n n o to c c u r sa sp r o p e rs u b t e r mo fo t h e rc o m p o n e n t p o i n t e do u tt h ed e f i c i e n c yi n p e r r i ga n ds o n g sa u t h e n t i c a t i o n t e s tv e r s i o n ，t h e np r o p o s e dt h ei m p r o v e d a u t h e n t i c a t i o nt e s ta n d p r o v e di t ss o u n d n e s sb o t hi nf o r m a la n dc a s es t u d y 6 w i t ht h ei d e ao ff o r c e dt y p ec h e c k a g e ，d e f i n e dd i f f e r e n tt y p e sf o rt e r m si nm e s s a g e s ， d e s i g n e dt h ei n s p e c t i o n r u l e so fa u t h e n t i c a t i o nt e s tm e t h o d ，s oa st od e t e c t t y p e f l a w - a t t a c k s o nd i f f e r e n tl e v e l s a c c o r d i n g t o a p p l i c a t i o nr e q u i r e m e n t s c o n f i r m e dt h ee f f e c t i v e n e s so fo u ri m p r o v e m e n t sb ya n a l y z i n go t w a y r e e s ， a n d r e wr p ca n dw o o l a mp r o t o c o l s 7 i m i t a t i n gt h em a n u a lp r o v i n gp r o c e s s ，d e s i g n e da na u t o m a t i cp r o t o c o lv e r i f i c a t i o n a l g o r i t h ma t a p a b a s e do ni m p r o v e da u t h e n t i c a t i o nt e s tt h e o r ym e n t i o n e da b o v e w i t ht h ep r o g r a m m i n gi m p l e m e n t a t i o no ft h ea l g o r i t h m ，v e r i f i e dt h ea t t r i b u t e so f n s la n dw o o - l a i np r o t o c o l s p r o v e dt h es o u n d n e s so fb o t ht h ea l g o r i t h ma n dt h e i m p r o v e da u t h e n t i c a t i o nt e s tt h e o r y k e y w o r d s ：s t r a n ds p a c e ，a u t h e n t i c a t i o nt e s t ，s e c u r i t yp r o t o c o l s ，a u t o m a t i cp r o t o c o l v e r i f i c a t i o n i v 缩略语 缩略语 a i ma u t h e n t i c a t i o nt e s tb a s e da u t o m a t i cp r o t o c o la n a l y s i sa l g o r i t h m 基于认证测试的协议自动化分析算法 c c i t tc o n s u l t a t i v ec o m m i t t e ef o ri n t e r n a t i o n a lt e l e g r a p ha n dt e l e p h o n e 国际电报电话咨询委员会 i t u i n t e r n a t i o n a lt e l e g r a p hu n i o n 国际电信联盟 c s pc o m m u n i c a t i o ns e q u e n t i a lp r o c e s s e s 通信顺序进程 e a te n h a n c e da u t h e n t i c a t i o nt e s t 改进认证测试 i k ei n t e m e tk e y e x c h a n g ep r o t o c o l 互联网密钥交换协议 m a c m e s s a g ea u t h e n t i c a t i o nc o d e 消息认证码 p k ip u b l i ck e yi n f r a s t r u c t u r e 公共密钥基础设施 r p cr e m o t ep r o c e d u r ec a l lp r o t o c o l 远程过程调用协议 s e ts e c u r ee l e c t r o n i ct r a n s a c t i o np r o t o c o l 安全电子商务协议 s s ls e c u r es o c k e tl a y e rp r o t o c o l 安全套接层协议 s s ms t r a n ds p a c em o d e l 串空间模型 t l s t r a n s p o r tl a y e rs e c u r i t yp r o t o c o l 安全传输层协议 r r pt r u s t e dt h i r dp a r t y 可信第三方 i x 主要符号表 串空间主要符号 主要符号表 符号描述 a 消息集合 t 原子消息集合 k 密钥集合 晦攻击者掌握的密钥集合 。 项的符号 串空间 c 丛 s串 n 结点 i 理想 协议描述中的主要符号 符号描述 a b 常规主体串 s 可信第三方串 i 攻击者串 k a ，k b 主体的公钥 k a i , k b 1主体的私钥 k a s ，k b s主体之间的共享密钥 t a ，t b时间戳 n a ，n b随机数 m会话标识符 x 独创性声明 本人声明所呈交的学位论文是本人在导师指导下进行的研究工 作及取得的研究成果。据我所知，除了文中特别加以标注和致谢的地 方外，论文中不包含其他人已经发表或撰写过的研究成果，也不包含 为获得电子科技大学或其它教育机构的学位或证书而使用过的材料。 与我一同工作的同志对本研究所做的任何贡献均已在论文中作了明 确的说明并表示谢意。 签名： 型垒垄 i ! ii i i i ：加一7 年月男日 关于论文使用授权的说明 本学位论文作者完全了解电子科技大学有关保留、使用学位论文 的规定，有权保留并向国家有关部门或机构送交论文的复印件和磁 盘，允许论文被查阅和借阅。本人授权电子科技大学可以将学位论文 的全部或部分内容编入有关数据库进行检索，可以采用影印、缩印或 扫描等复制手段保存、汇编学位论文。 ( 保密的学位论文在解密后应遵守此规定) 签名：萄复查导师签名： 日期：加口7 年月彦日 第一章绪论 第一章绪论 计算机网络的迅猛发展和普及，给人们的工作和生活带来了日新月异的变化。 电子商务、电子政务、网上银行、视频会议等网络应用的蓬勃发展使得网络成为 人们工作生活不可或缺的重要组成部分。随着人们对网络应用需求的增加，网络 中存在的安全问题变得日益突出，在开放的网络环境中能否提供安全可靠的服务 成为网络应用成功的关键因素。安全协议正是为了满足网络上安全共享资源的需 求，为网络通信安全提供保障。安全协议是建立在密码体制基础上的一种通信协 议，它运用密码算法和协议逻辑来实现保密、认证和密钥分配等目标。随着人们 对信息安全问题的日益重视，安全协议的应用也越来越广泛，因此有关安全协议 的分析研究已经成为信息安全领域的重要课题。 1 1 课题背景及研究现状 安全协议是构建网络安全环境的基石，其安全性对整个网络环境的安全起着 至关重要的作用。从1 9 7 8 年n e e d h a m s c h r o e d e r 协议的诞生算起，安全协议的发 展已经历经三十年了。但是安全协议分析这个领域仍然远未成熟，研究人员仍然 面临着诸多困难和挑战。迄今为止，在密码协议设计分析方面还没有出现完善的 商业产品，大型工业级安全协议的设计和分析仍然是一项艰巨的工作。如何有效 证明安全协议的安全性、如何设计出满足安全需求的最优协议、如何提高安全协 议分析验证的效率等都是安全协议研究领域需要不断探索的问题。安全协议的安 全性对于确保网络应用的安全有着重要意义，安全协议的分析设计也就成为一个 亟待研究和解决的课题。 1 9 7 8 年r o g e rn e e d h a m 和m i c h a e ls c h r o e d e r 在文献【l 】中提出了几个应用于开 放网络的安全协议，他们在文章结尾这样写道“协议，例如本文提出的几个协议， 很容易带有难以察觉的细微错误或者漏洞，从而遭受攻击。证明协议正确性的需 求非常之大，我们鼓励对此领域有兴趣的研究人员参与进来。这篇文章拉开了一 个新研究领域的序幕安全协议分析。 在安全协议研究的三十年间，研究人员提出了各种安全协议分析方法和模型， 其中最完善的一类就是形式化方法【2 】。形式化方法使用数学和逻辑方法对系统进行 电子科技大学博士学位论文 描述和验证，核心是为安全协议建立形式化模型，力求从中找到不安全的状态。 最早将形式化方法用于安全协议分析的成果则是d o l e v 和y a o 在1 9 8 3 年发表的论 文p j 。文中作者主要做了两项工作：一是将安全协议本身与安全协议采用的密码系 统分开，在假定密码系统是完善的前提下讨论安全协议的各种属性，称为完美密 码假设；二是建立了攻击者模型，对攻击者的身份、知识和能力进行了描述，称 为d o l e v y a o 模型。完美密码假设和d o l e v y a o 模型的提出具有重大意义和深远影 响，所有的安全协议形式化分析方法都遵循d o l e v 和y a o 的基本框架。完美密码 假设和d o l e v y a o 模型构成了安全协议形式化分析的前提和基础。 通常将安全协议形式化分析方法分成两大类：一是模型检测方法，借助自动 化分析工具，从协议的初始状态开始，对合法主体和攻击者的所有可能执行路径 进行穷尽搜索以期找到可能的错误状态【4 】，但是模型检测方法最大的局限性是状态 空间爆炸问题，只能限制参与协议的主体数目，证明小系统假设下协议的安全性； 另一种是定理证明方法，从用户接收和发送的消息出发，通过一系列的推理证明 协议是否满足目标安全属性，需要协议分析人员参与，进行手动证明。也有学者 认为除了以上两类，还有一类是以b a n 类逻辑和用于电子商务协议分析的k a i l a r 逻辑p j 为代表的信念逻辑方法【6 1 。但信念逻辑方法与定理证明方法中在思想和方法 上有着相似之处 7 1 ，因此合并在一起，统称为基于推导的定理证明方法。 模型检测方法中比较著名的有n r l 协议分析器、c a s p e r + f d r 工具、 i n t e r r o g a t o r 工具和a v i s p a 工具集【8 j 等。 n r l 协议分析器例是由m e a d o w s 开发的基于p r o l o g 的模型检测工具。n r l 使 用规则来描述攻击者生成消息的能力，包括攻击者自己通过加密解密来生成消息， 以及通过冒充某些主体参与协议来得到响应消息。首先给出不安全状态，然后根 据p r o l o g 规则反向推理，如果一直搜索到初始状态，就说明协议是不安全的。 m e a d o w s 使用n r l 分析器发现了许多已知和未知的安全协议漏洞，并成功地用于 分析i e t f 标准因特网密钥交换协议i k e 1 0 】。 c s p ( c o m m u n i c a t i o ns e q u e n t i a lp r o c e s s e s ) t 1 1j 是由牛津大学h o a r e 提出的用于 并行系统设计和分析的代数理论，f o r m a ls y s t e m sl t d 公司基于c s p 实现了通用模 型检测工具f d r ( f a i l u r ed i v e r g e n c er e f i n e m e n t ) 1 1 2 , b l 。g a v i nl o w e 首次将f d r 用 于安全协议的形式化分析【1 4 】，由于直接使用c s p 来描述密码协议非常困难，开发 了c a s p e r 工具【l5 1 。c a s p e r 实际上是面向安全协议设计与分析的简易接口， f d r c a s p e r + f d r 是现有模型检测工具中一个比较成熟的工具。g a v i nl o w e 等人利用 c a s p e r + f d r 分析了大约五十多种协议，对大多数协议找到了已知的攻击，并发现 2 第一章绪论 了少数未知的攻击。 i n t e r r o g a t o r t l 6 】工具将协议参与者视为通信状态机，攻击者可截取、毁坏、修改 参与者之间传输的消息。假设最后状态是秘密消息泄露，然后尝试生成所有可能 到达该状态的路径。如果找到这样的路径，那么协议存在安全漏洞，该路径构成 了攻击消息记录。 常见的定理证明方法除了b a n 类逻辑，还有s p i 演算方法、p a u l s o n 归纳法、 s c h n e i d e r 秩函数和串空间方法。 1 9 8 9 年，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 逻辑成功地对 n e e d h a m s c h r o e d e r 等几个著名的协议进行了分析，并发现了多个安全协议存在的 问题。b a n 逻辑的成功激发了学者们对安全协议形式化分析技术的兴趣，掀起了 该领域的研究热潮，研究人员纷纷进入这个领域进行探索，涌现出了许多新的研 究成果，从此安全协议形式化分析技术成为学术界和工业上的研究热点，许多学 术机构和工业组织纷纷积极开展这个领域的研究工作。b a n 类逻辑中著名而具有 深远影响的还有g n y 逻辑1 1 8 】、v o 逻辑1 1 9 1 、s v o 逻辑【2 0 】和a t 逻辑1 2 1 1 。b a n 类 逻辑在安全协议分析形式化进程中占据了非常重要的位置，有力地推动了安全协 议研究领域的发展进程。b a n 类逻辑普遍存在的一个问题是对协议的抽象过程是 非形式化的，b a n 逻辑的推理分析依赖于所做的初始假设，不合理的初始假设将 导致不正确的结论。n e s s e t t 使用一个简单的例子说明了这一点【2 2 】。 s p i 演算2 3 1 方法是由a b a d i 和g o r d o n 在p i 演算 2 4 1 的基础上建立的。这种方法 根据d o l e v y a o 模型，假定协议执行的每一步都可能与攻击者的执行步骤交叉。p i 演算是并发计算的基础，它引入了通道和作用域的概念。s p i 演算对p i 演算进行了 增强与扩充，增加了支持密码系统的原语，使s p i 演算可以描述基于密码系统的安 全协议。除了a b a d i 和g o r d o n 的研究之外，应用s p i 演算分析安全协议的重要工 作还有文献【2 5 之7 】。 p a u l s o n 归纳法1 2 8 】是基于协议消息和事件的一种定理证明方法，将协议归纳定 义为所有可能事件路径的集合，每条路径是一个包含多轮协议通信的事件序列， 主体接收到一个路径，可转发它或者根据协议规则进行扩展。该方法能模拟所有 攻击和密钥丢失。 s c h n e i d e r 秩函数【2 9 l 对系统中所有可能的消息进行赋值，赋值的结果作为消息 的可循环不变式，进而运用不变式技术对协议的安全属性进行证明。s c h n e i d e r 秩 函数使用c s p 进行描述。 3 电子科技大学博士学位论文 定理证明方法中，串空间理论的出现将安全协议形式化分析推向了一个新的 高度。1 9 9 8 年，t h a y e r 、h e r z o g 和g u t t m a n 提出了串空间【3 0 】的概念。串空间综合 了n r l 协议分析器、s c h n e i d e r 秩函数和p a u l s o n 归纳法的思想，其协议模型简 洁，是一种高效、严谨、直观的形式化分析方法。串空间中引入了反映因果关系 的偏序结构，有效减少了协议分析中的状态空间，避免了模型检测方法普遍存在 的状态空间爆炸问题。另外一个重要特性就是把协议的执行过程用图示法表示， 不仅简单直观，也有利于借助图的理论和算法对安全协议进行分析。串空间的出 现受到了研究人员的广泛关注，近年来对串空间理论的研究日益深入。 同年，t h a y e r 、h e r z o g 和g u t t m a n 又在论文中提出了诚实理捌3 l j ( h o n e s ti d e f l s o ns t r a n ds p a c e s ) 等概念，进一步扩展了串空间模型。在不考虑具体协议的基础上， t h a y e r 、h e r z o g 和g u t t m a n 通过理想的概念，给出入侵者能力限定的证明。并将 所得性质用于协议分析中。在此基础上，a l 丘e dp m a n e k i 对诚实的概念进行了进 一步扩展【3 2 l ，使得串空间模型能够运用到更多的协议上。 1 9 9 9 年，s o n g 等人将串空间模型与模型检测技术结合，设计出协议自动验证 工具a t h e n a 3 3 殚l 。a t h e n a 引入了串空间中的串和丛等要素，并使用模型检测方法 通过对安全协议目标的绑定进行安全性验证。该工具使用逆向搜索技术生成和遍 历所有能够生成该目标的状态，同时提出了状态不可达理论，用来削减搜索的状 态空间。a t h e n a 运行结束时，或者说明协议是安全的，或者构造并输出针对不安 全协议的攻击形式。虽然状态不可达理论能在一定程度上减少a t h e n a 产生和遍历 的状态数量，但仍然不能解决模型检测方法固有的状态空间随协议规模成级数增 长的问题。 2 0 0 0 年，g u t t m a n 和t h a y e r 发表论文【3 5 1 ，作者在文中提出了基于串空间理 论的认证测试方法，这是串空间发展过程中的又一大突破。认证测试方法以挑战 一应答机制为基础，通过寻找具有唯一源发性质的数据的特殊形式变换，构造认 证测试实例，证明协议丛中特定的常规结点的存在，从而证明协议的认证属性。 认证测试方法作为一种串空间理论上发展而来的形式化分析方法，侧重于图论和 偏序关系，并以此作为协议分析推导的出发点。它充分利用了串空间模型状态空 间少的优点，进一步简化了传统串空间的证明过程，证明过程简洁、优美、直观。 2 0 0 2 年，j o s h u ad g u t t m a n 在认证测试理论上做了进一步的工作，首次将认证测 试定理用于电子商务协议的辅助设计1 3 6 1 ，设计了一个新的电子商务协议 a t s p e c t ，为认证测试定理的应用开辟了一个新的空间。 许多学者和研究人员在使用串空间理论进行安全协议形式化分析上做了大量 4 第一章绪论 的工作，在理论扩展和自动化实现方面都取得了丰硕的成果。f j t h a y e r 等人提出 了混合串空间的概念【了7 1 ，并从理论上指出混合串空间中各协议串互不干扰完成认 证的充分条件。j d g u t t m a n 也指出如果两个协议采用不同的加密方式使得加密项 集合独立，则主协议认证属性的满足与另一协议存在与否无关l j 引。p a u ls y v e r s o n 将串空间模型同b a n 逻辑相结合，既保留b a n 逻辑的简单性，又能够弥补其 语义不明的缺陷1 3 9 。f e d e r i c oc r a z z o l a r a 等人指出串空间模型在非确定模式下验证 安全协议的局限性，并提出了复合串空间模型( c o m p o s i n gs t r a n ds p a c e ) 1 4 们。r o b i n 等人在串空间中引入了时序路径的概念【4 ，能对协议消息的新鲜性进行验证。m i k e 等人对认证测试理论的基础一挑战应答机制进行了进一步的研刭4 引。自动化实现 方面以d a w ns o n g 为代表的a t h e n a 项目组开发了一个安全协议工具包a g v i ( a u t o m a t i cg e n e r a t i o n , v e r i f i c a t i o na n di m p l e m e n t a t i o no fs e c u r i t yp r o t o c o l s ) 1 4 3 - 4 6 1 ， 实现了安全协议的自动生成、安全属性的自动验证和实现。 国内方面，中科院软件所信息安全国家重点实验室在安全协议的形式化分析 方面做了大量的工作，也取得了大量的成剁4 9 1 。范红等人对安全协议形式化分 析方法现状及存在的问题【5 0 1 、基于推理结构性方法和基于攻击结构性方澍5 2 1 进 行了总结。卿斯汉研究员探讨了串空间模型在逻辑分析中的应用以及串空间模型 指导安全协议形式化设计的可能性1 5 3 1 ，还通过具体的例子将串空间模型与c s p 方 法的分析特点进行了比较【5 4 1 。冯登国研究员从方法论的角度，采用模型化观点介 绍了可证明安全性理论的发展历程和重要结果【5 5 1 。季庆光等人提出了通用串空间 一g s s m ( g e n e r a l i z e d s t r a n ds p a c em o d e l ) t 5 6 】，通过增加新的串描述对原有串空间 模型进行了扩展。华东明对安全协议面向主体的形式描述语言【5 7 】，基于知识和信 念逻辑的协议设计分析方法进行了研究。李永建使用串空间理论对k e r b e r o sv 协 议进行了形式化分析【5 引。除此之外，上海交通大学信息安全工程学院李建华教授 带领的研究小组【5 9 】、电子科技大学刘璨博士后【删等都在安全协议形式化分析方面 做了许多工作，许多学校、科研机构和企业也都有大量研究人员在从事这一课题 的研究。此外，由信息安全国家重点实验室主办、每年一度的安全协议研讨会【6 l 】 也对我国安全协议的形式化研究起到了有力的推动作用。 1 2 研究内容及论文结构 串空间以其简洁、严谨、高效的特点成为近年来安全协议形式化研究领域的 热点，认证测试方法作为一种串空间理论上发展而来的形式化分析方法，充分利 5 电子科技大学博士学位论文 用了串空间模型状态空间少的优点，进一步简化了传统串空间的证明过程，证明 过程简洁、直观、优美，既可用于协议属性分析，也可用于协议辅助设计。另外， 由于认证测试方法的简洁直观，它还非常适合作为安全协议自动化分析工具的理 论基础。因此论文将认证测试方法的应用、扩展改进和基于认证测试的协议自动 化分析作为研究对象，主要做了以下几个方面的工作： 1 从协议分析的角度考虑对协议安全构成威胁的攻击类型和攻击者行为，着重对 重放攻击进行了分类研究。指出了s y v e r s o n 重放攻击分类法的不足，按攻击产 生的原因将重放攻击分成了五类，针对每个类别列出具体的攻击实例，并提出 抵御该类攻击的原则性方法。这种新的重放攻击分类方法对于更好地认识各种 攻击的原理及寻找有效解决措施具有积极的意义。 2 以对称密钥协议o t w a y r e e s 为例，从保密属性和认证属性两方面说明了串空 间最小元素方法、理想诚实方法和认证测试方法在安全协议形式化分析上的应 用；对比了三种方法进行协议分析的过程和特点，指出认证测试方法是前两种 方法的归纳与概括，是前两种方法在理论上的进一步深化，它的证明过程更为 简洁直观。并通过对不对称密钥协议x 5 0 9 的分析和改进，总结了使用认证测 试方法对协议进行形式化分析的一般过程。 3 结合协议设计一般原则和j d g u t t m a n 的协议设计思想，阐述了将认证测试理 论用于辅助协议设计的可行性，提出了基于认证测试的通用协议设计思想。将 协议设计过程分解为五个步骤，详细讨论了对称密钥体制和不对称密钥体制下 构造认证测试的方法。并使用该方法设计了一个新的双向认证密钥协商协议， 扩展了认证测试方法的应用范围。 4 针对“认证测试方法的证明过程过于依赖分析人员的主观判断 和“认证测试 元素出现位置可能不唯一的问题，将使用认证测试方法进行安全协议属性分 析的过程标准化，使得认证测试方法的应用过程更严谨规范，并且有利于自动 化分析工具的实现。使用标准化的认证测试分析方法对b a n y a h a l o m 协议进 行分析，找到了针对该协议的一个已知攻击的更普遍形式。 5 分析了认证测试方法中“测试元素不能是任何常规结点消息组成元素的真子 项 这一局限性产生的根本原因，指出了p e r r i g 和s o n g 改进方案的漏洞，提 出的新认证测试定理有效突破了认证测试定理无法分析多重加密协议的局限 性，并通过理论证明和实例分析说明了新认证测试定理的正确性。 6 针对“认证测试理论