（信息与通信工程专业论文）基于串空间理论的无线网络安全协议分析与设计.pdf

摘要 摘要 随着无线网络在各领域的广泛应用和不断发展，人们越来越关注无线网络的安全问题。无线信 道的开放性和不稳定性使得无线网络面临着较人的安全风险；移动终端在硬件资源上不同程度的限 制也决定了某些密码技术无法适用于无线环境；不同类型和用途的无线网络也对安全性和相关实现 技术有着不同的要求。由于和有线网络的巨大差异，现有众多的安全方案和技术并不能直接用于无 线网络，而且无线网络环境的复杂性和不稳定性也使得安全目标的实现困难重重。 安全协议作为网络安全通信系统的核心技术，其重要性不言而喻。然而，如何分析安全协议的 安全性，从而证明安全协议的有效性? 如何设计安全协议，从而确保所设计协议的安全性? 这些则 都是需由安全协议形式化方法来解决的问题。安全协议的形式化方法作为安全协议分析和设计的理 论基础，自d o l e v 和y a o 的开创性工作以来，目前已有了较大的发展，形成了两大流派，其中典型 的有串空间模型理论等。然而，在如何应用抽象的形式化理论或方法来研究现行通信系统中大型、 复杂并行系统的安全协议，发现其安全缺陷或证明其安全性? 在如何扩展现有形式化理论，使之能 够解决网络中出现的新的威胁? 以及在如何应用形式化理论指导安全协议的设计等几个方面还有待 进一步的研究。 鉴于此，本文基于串空间模型理论，针对无线网络中上述的问题进行了深入的研究，并提出了 一些有效的解决方案，得到了一些研究成果。主要t 作有： 1 基于扩展的串空间模型，对i e e e8 0 2 1 1 i 协议进行分析，发现了四步握手协议在协议可用 性上存在的漏洞，并提出了修改方案，最后对修改后的协议进行形式化证明； 2 基于扩展的串空问模型，对i e e e8 0 2 1 6 e 相关安全协议进行了分析，发现了i e e e8 0 2 1 6 e p k m v 2e a pt l s 认证的一个安全漏洞，并提出相应修改，同时也对修改后的协议进行形 式化验证； 3 提出了基于串空问模型指导的安全协议设计方法，并设计一个目标用于g s m 网络语音通道 端剑端安全通信的认证与密钥交换协议，并对其做出形式化安全性分析，证明了其安全性。 关键字：形式化方法；串空间模型；安全协议；i e e e8 0 2 1 l i ；i e e e8 0 2 1 6 ；g s m ；端到端安 全通信 a b s t r a c t a b s t i 认c t a l o n gw i 也t h ed e v e l o p m e n ta n da p p l i c a t i o no fw i r e l e s sn e t w o r k s ，m o r ea i l dm o r ec o n c e m sa r ep u t o n s e c 谢t ) ，i s s u c s c o m p a r e d 嘶mt h e i rw i r e dc o u n t e 印龇惚，w i i e l e s sn e t w o r i ( sr i s km u c hm o r ed u et ot h e i r 叩锄a n di i l s t a b l ew n l e s sc h a n n e l s ，s e v e r ec o n s 廿a i l l so n 诵r e l e s st e n i l i i l a l s ，a i l d 如q u e n t l yc h a n g e d t o p o l o 黟i i lc o n s e q u e n c e ，w 沁l e s sn e 咐o r ki ss u s c 印t i b l et 0m a n ys e c u r i t ya t t a c k s ，w h i c hc a nb ed e f h d e d e 行c c t i v e l yb yu s i n gs e c u r i t yp r o t o c 0 1 a m o n ga ns e c u r i t yo b j e c t i v e s ，a u t h e n t i c a t i o na n dk e ya g r e e m e l l ta r e e s s e i l t i a lo nw h i c hm o s to t h e rg o a l sa r er e l i e d s e c u r i t yp r o t o c o lw o r i 【sa sak i n do fk e n l e lt e c h n o l o g yf o rs e c u r en e t w o r kc o m m u n i c a t i o ns y s t 锄s ， a i l dt h e 洒忡r t a u l c eo fi ts p e a l 【sf o ri t s e l h o w e v t h ep r o b l e i n s ，w h i c ha r eh o wt o 强a l y z et h es e 砌t yo f t h es e c u r i 够p r o t o c o l 证o r d e rt oe n s u r et l i ev a l i d i t ) ro fi ta n dh o wt 0d e s i g nt h es e c u r i t yp r o t o c o li no r d e rt 0 e i l s u r ed l es e c u 矗锣o fi t ，a r es h 鲫【1 db es o l v e dt h e o i c a l l yb ym ef o 船a lm e t h o d s 氮醪s e c u 矗t yp r o t o c 0 1 t h e f o 硼a lm e t h o d sf o rs e c l l r i t yp r o t o c o l ，w h i c hw o r k 够at h e o r c t i c a lb a s eo f 锄a l y s i sa j l dd e s i 鲈o fs e c u r i t ) ， p r o t o c o l ，h a v eb e e | ld e v e l o p e dd e f i n i t e i y 舶m 也ef i r s tw o r kd o n eb yd o i e va n dy a o ，锄dh a v eb e e n 附o d i s t i n c tv i e w so ff o m a lr c a s o n i n ga b o u ts e c u r i 够7 r h et y p i c a lt 1 1 e o r i e sa r cn l es n a n ds p a c em o d e l ，t h e o r a c l em o d e la n de t c h o w e v c i r ，t h ef o r m a lm e t h o d sh a v es o m ed e f i c i e l l c i e si ns e v e 忧la s p e c t s ，w 【l i c ha r e h o wt oa p p l yt h ea b s 缸a c tf o m a lt h e o r i e st oa n a l ) ，z et h es e c u r i t ) ，p r o t o c o li i lt h ec x i s t i n gc o m p l e xp a r a l l e l s y s t 锄i no r d e rt of m dm es h o r t a g e0 rp r o v et h es c c u r i t yo fm ep r o t o c o l ，h o wt oe x t 肌dm ec x i s t i n gf i o m l a l m e t h o d si no r d e rt 0s o l v et h en e wt i l r e a t si nt l en e t 、) i ，o r ka l l dh o wt oa p p l ym ef o n i l a lm e t h o d sf 0 rd e s i g no f s e c u r i t yp r o t o c 0 1 w h e r e a s ，i nm et h e s i s ，i tm a k e 凡n h e rr e s e a r c ho nt h ea b o v ea r e a sb a s e do nt h es 犍a n ds p a c em o d e l ， p r o p o s es o m ev a l i ds o l u t i o n sa n do b t a i ns e v e i r a lr e s e a r c ha c h i e v 锄e n t 8 1 b a s e d 锄e x t e n ds 舰n ds p a c em o d e l ，i ta n a l y z e si e e e8 0 2 1l i ，a n dp o i n to u tt l l es h o r t a g e sa b o u t a v a i l a b i l i t yi i l4 - w a yh a i l d s h a l ( ep r o t o c o l ，a i l dp r o p o s e sm ei m p r o v e m e n tb a s e do nm ef o 册a l 柚a l y s i s 2 b a s e do ne x t e n ds 仃肌ds p a c em o d e l ，i ta n a l y z e si e e e8 0 2 16 es e c 谢够8 u b l a y 鸭a i l dp o i n to u t t h es h o r t a g e si i la u t l l e n t i c a t i o np r o t o c o lb a s e do np k m v 2 - e 邺l s ，a n dp r o p o s e st h e i i i l p r o v e m e n tb a s e d0 nt h ef b 肋a la n a l y s i s 3 p r o p o s e san e wk i n do fr u ba b o u ts e c 嘶t ) ，p t o c o ld e s i 盟b a s e do ns 昀n ds p a c em o d e l a n d d e s i g na na u m e n t i c a t i o na i l dk e ye x c h a n g ep m t o c o lf o re n d - t o - e n ds e c u r ec o m m u n i c a t i o n si i l g s m f i n a lp r 0 v c si t ss e c u r eb yt h ef o 珊a la i l a l y s i 8 k e yw o r d s ：f b 珊a lm e t h o d ；s 嗽m ds p a c em o d e l ；s e c u r i t yp m t o c 0 1 ；i e e e8 0 2 1li ；i e e e8 0 2 16 e ； g s m ：e n d - t o - e n ds e c u r ec o m m u n i c a t i o n s t i i 表格目录 表格目录 表4 1p k m v 2 _ s a j 。e k j o h a e n g e 消息属性列表7 4 表4 2p k m v 2 s a j 。e k r e q u e s t 消息属性列表7 4 表4 3p k m v 2 _ s a j r e k - r e s p o n s e 消息属性列表7 5 表4 4p k m v 2 一k e y r e q u e s t 消息屙| 生列表7 5 表4 5p k m 以一k e y _ r e p i y 消息属性列表7 6 i i 插图目录 插图目录 图2 1 出认证测试2 2 图2 2 入认证测试2 3 图2 3d o st e s t1 2 7 图2 4d o st e s t2 2 8 图2 5 密钥成分测试3 0 图3 1i e e e8 0 2 11i 协议框架3 3 图3 。2i e e e8 0 2 - 1 1p m p 模式网络拓扑结构3 4 图3 3i e e e8 0 2 1 的协议栈3 4 图3 4i e e e8 0 2 1xe a p 认证过程3 6 图3 5i e e e8 0 2 11l 密钥管理流程3 9 图3 6 对等密钥分层结构4 0 ” 图3 7 组密钥分层结构4 0 图3 8 四步握手协议流程。4 1 图3 9 组密钥更新握手4 2 图3 1ok e r b e r o s 协议流程4 3 图3 1 1w l a n 下的k e r b e r o s 认证结构4 4 图3 12k e r b e r o s 协议的丛4 5 图3 1 3 四步握手协议的形式化5 0 图3 。1 4 四步握手协议中的正常赋权束5 3 图3 15 四步握手协议d o st e s t 分析5 3 图3 16 对四步握手协议d o s 攻击示意图5 4 图3 17 改进后的四步握手协议5 4 图3 1 8 四步握手协议的抗d o s 攻击改进5 5 图3 19 改进后四步握手协议中的正常赋权束5 5 t x 东南大学硕士学位论文 图4 1i e e e8 0 2 16 协议栈5 7 图4 2i e e e8 0 2 16 网络架构5 8 图4 3a s n 参考模型5 9 图4 4l e e e8 0 2 1 6 的简化网络架构5 9 图4 5i e e e 8 0 2 16 e 安全子层协议栈6 0 图4 6p k m v l 密钥体系结构6 l 图4 7p k m v l 安全关联建立过程6 3 图4 8i e e e8 0 2 16 ep k m v 2 密钥体系结构6 6 图4 9p k m v 2 基于r s a 认证流程6 6 图4 10r s a 认证方式下a k 导出示意图。6 8 图4 11p k m v 2 基于一轮e a p 认证流程6 8 图4 1 2 一轮e a p 认证方式下a k 导出示意图6 9 图4 1 3p k m v 2 基于两轮e a p 认证流程6 9 图4 1 4 两轮e a p 认证方式下a k 导出示意图。7 0 图4 1 5p k m v 2 基于r s a + e a p 认证流程7 l 图4 16r s a + e a p 认证方式下a k 导出示意图7 2 图4 1 7 导出消息认证密钥示意图7 3 图4 18 导出消息认证密钥示意图7 3 图4 。19s a t e k 三次握手流程7 4 i 羽4 2 0p k m v 2t e k 消息交换7 5 图4 2 1i e e e8 0 2 16 ep k m v 2e a p j l s 认证的丛7 6 图4 2 2p k m v 2e a pt l s 认证伪冒攻击7 9 图4 2 3 改进后的p k m v 2e a p j - l s 认证协议7 9 图4 。2 4 改进后的p k m v 2e a p j r l s 认证协议束8 0 图5 1n s l 协议的丛8 2 图5 2 认证密钥交换协议消息流程8 6 x 插图目录 图5 3 认证密钥交换协议的束一8 7 x i 东南大学学位论文独创性声明 本人声明所呈交的学位论文是我个人在导师指导下进行的研究工作及取得的研究成果。 尽我所知，除了文中特别加以标注和致谢的地方外，论文中不包含其他人已经发表或撰写过 的研究成果，也不包含为获得东南大学或其它教育机构的学位或证书而使用过的材料。与我 一同工作的同志对本研究所做的任何贡献均已在论文中作了明确的说明并表示了谢意。 觏：0 1 壁：坠强 东南大学学位论文使用授权声明 东南大学、中国科学技术信息研究所、国家图书馆有权保留本人所送交学位论文的复印 件和电子文档，可以采用影印、缩印或其他复制手段保存论文。本人电子文档的内容和纸质 论文的内容相一致。除在保密期内的保密论文外，允许论文被查阅和借阅，可以公布( 包括 刊登) 论文的全部或部分内容。论文的公布( 包括刊登) 授权东南大学研究生院办理。 构目蝴骼。 日期小昭心 第l 章绪论 第l 章绪论 无线通信技术的出现使人类摆脱了长久以来对有线通信线路的依赖和束缚，实现了真正意义上 的移动通信，彻底变革了人类有史以来进行信息交流的方式。在各类无线网络获得蓬勃发展的同时， 网络所面临的安全问题也日益严峻，并受到了越来越多的关注。无线网络本身的脆弱性导致了网络 容易遭受各种攻击，便携式移动终端由于功能限制也不可能提供强有力的安全保障，而且各种新兴 的网络增值业务还提出了更高的安全需求。 安全协议是指运用密码算法实现的特定形式的消息交换，目的在于提供各种安全服务。由于诸 多原因，安全协议的设计极易出错，即使对于最基本的交互认证协议。长期以来由于缺乏严格的设 计和验证方法，安全协议的正确性和安全性始终无法得到有效保障。近几十年米，各种形式化方法、 理论和支持工具的出现和应用，使得这一情况大为改观。借助丁形式化方法，不仅可以有效地验证 协议安全性，发现许多已知和未知安全缺陷，还可以在协议设计阶段起到重要的指导作用，对于保 障协议安全性和正确性有着重人意义。 本章简要介绍了安全协议相关概念，形式化方法在安全协议分析中的应用以及研究近况和无线 网络安全协议概述，最后介绍课题的来源、主要内容、篇章结构和创新点。 1 1 安全协议 1 1 1 安全协议概述 安全协议是利用密码技术在不安全网络上获得安全性的通信协议，也称密码协议。所谓通信协 议，就是两个或两个以上的参与者采取一系列步骤以完成某项特定的任务。这个定义包含三层意思： 协议至少需要两个参与者；在参与者之间呈现为消息处理和消息交换交替进行的一系列步骤； 通过执行协议必须能够完成某项任务，或达成某种共识。 协议与算法的概念是不尽相同的，算法应用于协议中消息处理的环节。可以简单的说，安全协 议就是在消息处理环节采用了若干的密码算法的协议。密码算法和安全协议处丁网络安全体系的不 同层次，是网络数据安全的两个主要内容。具体而言，密码算法为网络上传递的消息提供高强度的 加密操作和其他辅助算法( h a s h 函数等) ，而安全协议是在这些密码算法的基础上为各种网络安全 性方面的需求提供其实现方案。 安全协议是一fj 跨领域、跨学科的科目，涉及到许多领域的知识。密码学是安全协议的学科基 础，如果密码体制被破解则安全协议将会随之被破解而变得毫无意义。一般情况下我们认为在安全 协议中使用的加密算法是安全的、不会被破解的，加密算法对于安全协议而言被看作是一个黑盒子， 它提供对通信协议信息处理环节的加密解密操作。现实的网络提供安全协议运行所需要的环境，然 而，网络的不稳定和不可靠，或者低质量又会影响安全协议的实际使用效果。安全协议是一门艺术 1 东南大学硕十学位论文 的科学，设计安全协议绝非简单的t 作，它需要精确的和复杂的科学思维。安全协议涉及大量数学 领域的知识，安全协议目标的精确和标准的定义必须要借助于数学语言的描述和刻画，对安全协议 的形式化分析同样必须借助数学的模型和手段。安全协议也可以看作是一门工程的科学，不同的是 它必须应对一些活动频繁的、高度智慧的、怀有恶意的敌人的攻击，我们所指的攻击不是针对密码 学体制的攻击，而是针对安全协议设计本身漏洞的发现和查找。 1 1 2 安全协议的安全性质 安全协议的主要目的在于通过协议消息的传递来达成通信主体身份的识别与认证，并在此基础 上为下一步的秘密通信分配所使用的会话密钥，因此对通信双方身份的认证是基础和是前提，而且 在认证的过程中，对关键信息的秘密性及完整性的要求也是十分必要的。评估一个安全协议是否是 安全的就是检查其所欲达剑的安全性质是否遭到攻击者的破坏。 1 认证性 认证性是最重要的安全性质之一，所有其他安全性质的实现都依赖于此性质的实现。认让是分 布式系统中的主体进行身份识别的过程。主体与认证服务器共享一个秘密，通过对拥有此秘密的证 明，主体可建立对其的信任，如在多用户环境中使用口令服务就是这样的一个例子。在认让系统中 往往使用一个加密密钥作为秘密，而加密体制具有这样的特性；如果当主体不拥有密钥时，它将不 能生成一个加密消息或解密用此密钥加密的消息，主体通过用密钥进行加密来证明它拥有此密钥。 认证可以对抗假冒攻击的危险，认证可以用来确保身份，并可用于获取对某人或某事的信任。在协 议的实体认证中可以是单向的也可以是双向的。 2 秘密性 秘密性的目的是保护协议消息不被泄漏给非授权拥有此消息的人，即使是攻击者观测到了消息 的格式，它也无法从中得剑消息的内容或提炼出有用的消息。保证协议消息秘密性的最直接的办法 是对消息进行加密。加密使得消息由明文变为密文，并且任何人在不拥有密钥的情况下是不能解密 消息的。 3 完整性 完整性的目的是保护协议消息不被非法篡改、删除和替代。最常用的方法是封装和签名，即刚 加密的办法或者h a s h 函数产生一个明文的摘要附在传送的消息上，作为验证消息完整性的依据，称 为完整性校验值( i c v ) 。通信双方必须事先达成有关算法的选择等诸项的共识。因为如果个攻击 者不知道加密密钥而修改了密文的一部分，则会导致在解密的过程中产生不正确的结果。 4 。不可否认性 不可否认性是电子商务协议的一个重要的性质。其目的在于通过通信主体提供对方参与协议交 换的证据来保证其合法利益不受侵害，即协议主体必须对自己的合法行为负责，丽不能也无法事后 2 第l 章绪论 否认。证据一般是以签名消息的形式出现的，从而将消息与消息的意定发送者进行了绑定。要达成 不可否认这一目标，协议必须具有以下两个特点：证据的正确性，交易的公平性。在不可否认性之 中还可以引申出电子商务的一些其他的相关性质，如适时中止性、公平性、可追究性等。 1 1 3 安全协议的分类 c l a r k 和j a c o b 在文献中对安全协议进行了概括和总结，列举了一系列有研究意义和实用价值 的安全协议。他们将现有的安全协议进行了如下的分类： 无可信第三方的对称密钥协议。属于这一类的典型协议包括以下的i s o 系列协议【2 】：i s o 对 称密钥o n e - p a s s 和铆o _ p a s s 单方认证协议，i s o 对称密钥押o _ p a s s 双方认证协议，i s o 对 称密钥缸- e e - p 舔s 双方认证协议。还有a n d r e w 安全r p c 协议【3 1 等。 应用密码校验函数( c c d 的认证协议。属于这一类的典型协议包括以下i s o 系列协议【4 】： i s o 应用c c f 的o n e - p 舔s 和栅o - p a s s 单方认证协议、i s o 应用c c f 的t w o - p a s s 双方认 证协议、i s o 应用c c f 的t l 鹏e - p a s s 双方认证协议。 具有可信第三方的对称密钥协议。属于这一类的典型协议包括n s 私钥协议【5 l ，o m a y r e e s 协议【6 】，y a h l o m 协议阴、大嘴青蛙协议【刀，d e 衄i n g s a c c o 协议【8 】，w b o l 锄协议【9 】o 对称密钥重复认证协议。属丁这一类的典型协议有渐b e r o sv 5 ，n e u m a l l s t i l b b l e b i n e 协议 【1 0 1 ，k a o c h o w 重复认证协议【1 1 】等。 无可信第三方的公开密钥协议。属于这一类的典型协议包括以下l s o 系列协议【1 2 】：i s o 公 开密钥o n e p a s s 和t 、) i r o - p a s s 单方认证协议、i s o 公开密钥t w o - p a s s 双方认证协议、i s o 公 开密钥t h r e e - p a s s 双方认证协议、i s o 公开密钥铆o - p a s s 并行双方认证协议，还有 d i 币e h e l l m a n 协议等。 具有可信第三方的公开密钥协议。属于这一类的典型协议有n s 公钥协谢5 1 ，n 供密钥分 发协议【1 4 j 等。 1 1 4 安全协议的缺陷分类 尽管协议设计者尽可能在协议设计时回避可能出现的人为错误，但是安全协议在实际应用时仍 会出现各种类型的缺陷，并且产生缺陷的原因是多种多样的，很难有一种通用的分类方法将安全协 议的安全缺陷进行分类。g d t z a l i s 和s p i i l e l l i s 【1 5 】根据安全缺陷产生的原冈和相应的攻击方法把安全 协议的缺陷分为如下六类： 基本协议缺陷：是指在安全协议的设计中没有采取或者只采取很少防范攻击者攻击的措施， 例如对加密消息签名，由于签名者并不一定知道被加密的消息内容，而且签名者的公钥是 公开的，攻击者可通过用他自己的签名替换原有的前面那个来伪装成发送者。 3 东南大学硕。 ：学位论文 口令密钥猜测缺陷：这类缺陷产生往往是因为用户从一些常川的单词、词组中选择他的密 钥口令，从而导致攻击者能够采取字典攻击的手段进行口令猜测攻击；另外的可能是冈为 用户选取了不安全的伪随机数生成算法构造密钥，使得攻击者能够恢复该密钥。 陈旧消息缺陷：主要由于在安全协议设计时对消息的新鲜性没有充分考虑，从而使攻击者 能够进行消息重放攻击，包括消息源的攻击、消息目的的攻击等等，在文献 7 ，1 1 中的协议 己经被发现存在这种安全缺陷。 并行会话缺陷：也l f 应答机会话缺陷、多角色漏洞，主要是由于攻击者可以通过交换适当 的协议消息从而获得所需要的重要消息。 内在性缺陷：由于协议的消息可达性存在问题安全协议的参与者中至少有一方不能够完 成所有必须的动作而导致的一种协议缺陷。 密码体制缺陷：这是一种根本性的安全协议缺陷，如果安全协议中所使用的密码算法存在 根本性缺陷，则必将导致协议参与各方之间所有交互的加密消息都可能会被解密，由此造 成攻击者可以非常容易或者有很大可能的充当合法的角色参与协议，欺骗诚实的角色。 1 2 安全协议的形式化分析方法 1 2 1 安全协议形式化分析的前提 完善的加密前提 协议采j 甘的密码系统是完美的，不考虑密码系统被攻破的情况； 必须知道解密密钥才能解密加密数据； 无加密项冲突，即若有 所。) 向= 垅z ) 如，则一定有m 一= ，墨= 岛成立。 协议的参与者 参与协议运行的主体分为诚实的合法用户和入侵者。诚实的合法用户将严格按照协议规定参与 协议运行。入侵者也可以是系统的合法用户，拥有自己的加密密钥和解密密钥。但入侵者不会按照 协议规定参与协议运行，而是企图知道他不该知道的秘密，或假冒其他诚实的合法用户。 入侵者的知识与能力 入侵者的知识； 熟悉现代密码学，知道加解密等运算操作； 知道参与协议运行的各主体名及其公钥，并拥有自己的加密密钥和解密密钥； 4 第l 章绪论 每窃听或收到一个消息，即增加自己的知识。 入侵者的能力： 可窃听及中途拦截系统中传送的任何消息； 可解密用他自己的加密密钥加密的消息； 在系统中可插入新的消息； 即使不知道加密部分的内容，也可以重放他所看到的任何消息( 其中可改变明文部分) ； 可运用他知道的所有知识( 如临时值等) ，并可产生新的临时值。 1 2 2 安全协议形式化分析的历史和现状 协议形式化分析k 期以来被视为分析协议安全性的有效工具，最早提出对安全协议进行形式化 分析思想的是n e e d h 锄和s c h r o e d 一5 1 ，1 9 7 8 年他们提出了为进行共享和公钥认证的认证服务器系 统的实现建立安全协议，这些协议引发了安全协议领域的许多重要问题研究。1 9 8 1 年d e i l l l i i l g 和 s a c c 0 在文献【8 】中指出n s 私钥协议的一个错误，人们开始关注安全协议分析。在这一领域具有里 程碑意义的事情发生于2 0 世纪8 0 年代，d 锄y d o l e v 和a n d r e wc y a o 发表了文献 1 6 】，它真正 开始了使用形式化方法分析安全协议的历史，自此之后使用形式化的方法研究安全协议逐渐兴起。 d o l e v 和y a o 在他们的文章中开创性地给出了安全协议可以多步并发执行的形式化系统模型，在这 个系统模型中，包含了那些可以对信息流进行恶意窃取、修改和删除的入侵者和不诚实的参与者， 同时密码学算法被认为是完备的，在分析时仅仅把它看作是一个满足一些代数性质的黑盒子，即使 是土动攻击者也无法通过密码学算法对安全协议进行攻击。紧接着，d o l e v ，e v 铋和l ( a 单开发研 究出了一系列的多项式时间算法，使用这些算法来分析一个限制严格的安全协议簇。但遗憾的是， 在随后的研究中发现它们可以分析的协议太有限，一旦稍许放宽对这个协议簇的限定都将使得协议 的安全性变成不确定的问题，因此这方面的工作并末得到进一步的展开。随后，在d o l e v - y a o 模型 及其变形的基础上发展了很多形式化分析安全协议的t 具。它们大部分采用状态搜索的技术，即首 先定义一个状态空间和安全协议的系统模型，然后进行在此模型内搜索检测以确定是否存在一条路 径对应于攻击者的一次成功的攻击。还有一些t 具采用了归纳定理推证技术开发安全协议分析的通 用工具，并取得了一定的研究成果，其中包括：h l t e l l o g a t 一17 1 ，n r l 协议分析器【1 8 】，l o n g l e y - m g b y 工具，以及其他一些用来解决这个问题的形式化方法。这些早期的验证分析工具都曾成功地发现一 些已有安全协议中存在的漏洞，而在这之前的人工的分析并没有能够发现这些漏洞的存在，如n r l 协议分析器搜索的空间规模可以确保安全性，并成功地发现了s i m m o n s 的选择性广播协议1 1 8 】的缺 陷，l 0 n g l e y 鼬g b y 工具发现了b a n k i n g 协议的缺吲拶】等。 直到1 9 8 9 年，b 1 l r r o w s 。a b a d i 和n e e d l l 锄提出了b a n 逻辑 7 】之后，形式化分析技术逐渐引起 了人们广泛的关注。b a n 逻辑采用了与状态搜索技术完全不同的方法，它是关于主体拥有的知识与 信仰，以及用于从已知信仰推知新的信仰的推理规则的逻辑。这种逻辑通过对认证协议的运行进行 5 东南大学顾十学位论文 形式化分析，来研究认证双方如何通过相互发送和接收消息的方式，从最初的信仰逐渐发展到协议 运行最终要达到的目的一认证舣方的最终信仰。b a n 逻辑的规则十分简沾和直观，因此易于使用。 b a n 逻辑成功地对n s 协议、k c 柏e r o s 协议等几个著名的协议进行了分析，找到了其中已知和朱 知的漏洞。b a n 逻辑的成功极火地激发了密码学家对安全协议形式化分析的兴趣，并导致许多安全 协议形式化分析方法的产生。但是，由于b a n 逻辑的方法还有许多不足，于是产生了这样的尴尬 局面：当逻辑发现协议中的错误时，人们可以确信那是有问题的，但是当逻辑证明一个协议是安全 的时，人们无法确信它的正确性。 1 9 9 6 年g l o w e 使用通用的模型检测工具f d r 发现了n s 公钥密码协议中存在着中间人攻击 【2 0 1 。在这之后，在d 0 1 e v y 幻模型及其变形的基础上结合使用状态搜索技术和定理证明方法的分析 研究工作又取得了很人的进展，并不断涌现出一些新的形式化方法和工具，m u r 巾模型，进程代数 c s p 以m i l l 开发的c a p s l 为协议形式化分析工具提供通用说明语言，标忐着不同形式化分析技 术日趋成熟与集成。1 9 9 7 年p 肌l s o n 提出的基于协议消息和事件的攻击结构方法注记的证明方法， 被称为p a u l s o n 归纳法【2 1 1 ，1 9 9 8 年由f a b r e g a ，h e r z o g 和g 硼【i i l 锄三人提出的基于协议消息节点间 一种偏序关系的可证安全的串空间模型【2 2 1 ，以及2 0 0 2 年李先贤和怀进鹏提出的密码协议代数模型 c p a 【2 3 1 。 随着网络的发展，越来越多的人们依赖网络做各种事情，从网上消费到远程医疗等，这导致了 群通信、匿名通信、电子商务等的出现，并对相应的安全协议设计与分析提出了新的要求。同时， 安全协议也面临着新型威胁，这使协议形式化分析面临新的问题。 1 2 3 安全协议形式化分析的分类 安全协议的形式化分析技术已有十多年历史，目前分为以下三类：第一类是以b a n 逻辑为代 表的基于推理结构性方法，第二类是基于攻击结构性方法，第三类是基于证明结构性方法。 1 基于推理结构性方法 基于推理结构性方法主要是运用逻辑系统从用户接收和发送的消息出发，通过一系列的推理公 理推证协议是否满足其全部说明。这些逻辑系统通常由一些命题和推理公理组成。命题表示主体对 消息的知识( al ( 1 1 0 w sp ) 和信仰( ab e l i e v e sp ) ，而运用推理公理可以从己知的知识和信仰推导出 新的知识和信仰。文献 2 4 】中给出了一个有关此领域的讨论。在这类方法中，最著名的是b a n 及 b a n 类逻辑5 2 4 2 5 1 ，以及用于分析电子商务协议的l o i l a r 逻辑。一般来说，b a n 逻辑只能推出 认证的结果，而不能对一般的安全性进行证明。使用b a n 逻辑分析安全协议的步骤如下：( a ) 协议 的理想化转化；( b ) 假设所有的协议初始状态；( c ) 使用逻辑规则对系统的状态做出断言；( d ) 运用逻辑 原理得到关于信任的断言。最新的研究是d r e d 提出的安全协议的生成理论r v 逻辑。 2 基于攻击结构性方法 基于攻击结构性方法对协议进行分析时，一般要借助于自动工具。从协议的初始状态开始，对 6 第l 章绪论 合法主体和一个攻击者的所有可能的执行路径进行穷尽搜索以期找剑协议可能存在的错误。根据设 计的目的不同，可分为两类： 使用通用的、并非为分析安全协议单独专门设计的形式化描述语言和协议验证工具。这是 一种传统的模型检测方法，其主要思想是把安全协议看作一个模型，方法的目的就是验证 这个模型是否满足安全协议目标，比如一般目的模型检测= 具f d r 【2 伽和m l l r 等。这方 面最为突出的贡献是1 9 9 6 年g a v i l ll 0 w e 使用印r ( f a i l u 坨sd i v e r g e l l c e sr e f i n 锄e n t c h e c k 神发现了n s 协议的一个以前从未被发现的漏洞。由于此类方法将安全协议视为 一般的目标，在不考虑其独有特性的前提下验证其正确性，因此它的最人直接的不足是仅 考虑了正确性，却忽略了安全性。在这一类形式化分析工具中往往j h j 到了状态机的概念。 状态机应片j 可达性分析技术米对认证协议进行分析，对于每一次迁移，使用主体状态和主 体之间信道状态来描述系统的全局状态，分析每一个全局状态并判断其性质，如死锁、正 确性等，如果分析表明一个主体在某一已知状态下应接收到某一消息却并朱收到时，则说 明协议是有问题的。可达性技术通过对协议的说明来判断协议的正确与否，但它并不能保 证协议的秘密性不受到主动攻击。 安全协议的设计者设计专门的用于分析和研究出现的各种情况的特别目的的专家系统，如 h l t e 啪g a t o r l l 刀和n r l 协议分析剁1 引，其主要思想是使用专家系统发现协议是否能够达到 不合理的状态( 比如密钥的泄露等等) 。它从一个不安全的状态出发，并试图发现从出事状态 到这一不安全状态是否是可达的，如果可达则说明协议存在漏洞。这类系统可以找山己知 的攻击，但是不能证明协议的安全性，也无法找出未知的攻击，其分析协议的能力是有限 的，但提供了一个新的研究思路。在文献【1 9 】中，l o n 9 1 e y 和砌g b y 指出了专家系统在协 议形式化分析中所做出的贡献如下：( a ) 为认证协议的理解提供新的视觉；( b ) 是一种不断精 炼协议模型的技术；( c ) 可与模型交互作用，从而使得分析者更能洞察协议内部的操作；( d ) 能同答w h a ti f 问题；( e ) 可对协议模型所提出修改的性能进行测试。专家系统可以与其他形 式化分析工具配合使用，但不能取而代之。试验表明这些工具是有效的，但同时它们也存 在一些问题，突出表现在以下两个方面：( a ) 主体数目的有限性。这些j = 具首先要做的是规 定参与协议的主体的最人数目，这意味着它们只能分析包括有限个主体的协议。即使是这 些工具没有发现一个协议错误，但当协议的主体数目增加时仍可能存在错误。( b ) 无法解决 状态空间爆炸问题。 3 基于证明结构性方法 基于推理结构性的形式化分析方法不能解决秘密性，而且缺乏清晰的语义，甚至有时很难明确 指出信仰逻辑在证明什么。另一方面，由于基于攻击结构性的形式化分析方法不得不对随着协议的 增大而呈指数增长的协议状态空间进行搜索，其所需的时间与空间往往超过可用资源。为解决上述 问题，出现了基于证明结构性方法，基于密码学系统的代数特性开发协议的形式化模型。这种方法 是将安全协议系统当作一个代数系统模型，表示出协议的参与者的各种状态，然后分析某种状态的 7 东南大学硕i ：学位论文 可达性。在此模型中包含了那些可以对信息流进行恶意窃取、修改和删除的入侵者和不诚实的参与 者，同时密码学算法被看作是一个满足一些代数性质的黑盒子，但此模型的缺点在于对可验证的协 议簇限制过于严格。这一领域最著名的是d o l e v - y a o 模型，此后p a u i s o n f 2 1 】，s c l l i l e i d 一2 8 1 以及 m e a d o w s 【2 9 】，w b o 和l a 一3 0 1 等都在此领域做出了很大的贡献。最近一些新的研究为安全协议的分析 提供了自动化的支持，这就是结合模型检测技术和定理证明方法开发安全协议的臼动验证工具。目 前在这方面最有前景和最新的研究成果是f a b r e g a ，h e r z o g 和g u t 廿i l a 【2 2 1 【3 l 】提出的串空间模型，并 已经取得了很大的进展。 1 3 无线网络安全概述 无线通信技术的出现使人类摆脱了长久以米对有线通信线路的依赖和束缚，实现了真正意义上 的移动通信，彻底变革了人类有史以来进行信息交流的方式。在各类无线网络获得蓬勃发展的同时， 网络所面临的安全问题也日益严峻，并受到了越来越多的关注。无线网络本身的脆弱性导致了网络 容易遭受各种攻击，便携式移动终端由于功能限制也不可能提供强有力的安全保障，而且各种新兴 的网络增值业务还提出了更高的安全需求。本节将通过介绍常用无线网络技术，总结出无线网络特 点，并简要分析无线网络的安全威胁与风险并总结出其安