（信号与信息处理专业论文）形式化方法在安全协议验证领域内的应用研究.pdf

论文摘要 y5 6 9 1 6 0 本文中，我们探讨了形式化方法在安全协议验证领域内的相关应用问题。其 中，我们工作的重点将集中在s t r a n d 空间方法上。 首先，我们介绍了安全协议描述方法发展的三个阶段，由此引出形式化方法 应用于安全协议验证领域内的初衷。随后，我们分三条线索：d o l e v y a o 模型及 其影响、b a n 逻辑与其后续工作，以及形式化方法的自动化技术，对形式化方 法在安全协议验证领域内的发展动态进行了全面而客观的评述。 第二，我们概述了本领域内三个最具影响力的形式化方法的应用过程，它们 分别是：d o l e v y a o 模型、b a n 逻辑，与s t r a n d 空间。为了进一步说明这些方法 的实用性，我们还给出了相应的实例分析。 第三，我们对近来颇受关注的s t r a n d 空间展开了一系列研究。这部分工作基 于五个目标：其一、细化理想结构的描述方式；其二、形式化表述安全密钥的概 念：其三、揭示安全密钥与协议秘密属性之间的关系；其四、给出安全密钥的相 关性质；其五、提出一个证明安全协议的新思路。为实现这些目标，我们引入新 的记号以表示理想的内部结构；利用理想的概念给出了安全密钥的形式化描述； 在特定条件下，通过对比安全密钥与秘密属性各自的理想表达，证明了他们之间 的等价关系：借助入侵者密钥的定义与入侵者行为对应的消息序列，证明了安全 密钥特有的性质；最后，基于以上工作，我们提出一个基于安全密钥概念的协议 证明思路。 第四，我们基于s t r a n d 空间提出了一个新的针对安全协议缺陷的分类法。这 个分类法将协议缺陷分为以下八类：当前性缺失缺陷、方向性缺失缺陷、类型缺 失缺陷、独立性缺失缺陷、轮数标识缺失缺陷、认证过程缺失缺陷、认证测试形 式相同缺陷，与认证测试部分形式相同缺陷。并且，对于前四类协议缺陷，我们 利用认证测试方法完成了相应的协议分析工作。 最后，我们介绍了形式化方法在安全协议设计领域内的应用现状，并且讨论 了这个领域内今后的研究方向。 关键词：安全协议，形式化方法，缺陷分类法，协议验证。 a b s t r a e t i nt h i sp a p e r , w ed i s c u s st h ep r o b l e m sr e l a t e dt ot h ea p p l i c a t i o n so ft h ef o r m a l m e t h o d si nt h ef i e l do f s e c u r i t yp r o t o c o l sv e r i f i c a t i o n a n do u rw o r k i sm a i n l yo nt h e r e s e a r c ho fs t r a n ds p a c e s f i r s t l y , w ei n t r o d u c et h r e es t a g e so f t h ed e s c r i p t i o nm e t h o d so f s e c u r i t yp r o t o c o l s ， w h i c hg i v e st h ei n i t i a li d e a st h a ta p p l y i n gf o r m a lm e t h o d st ov e r i f ys e c u r i t yp r o t o c o l s t h e nf r o mt h ef o l l o w i n gt h r e et h r e a d s ：d o l e v y a om o d e la n di t si n f l u e n c e s ，b a n l o g i c a n dt h ew o r k sa f t e ri t ，a n dt h ea u t o m a t i ct e c h n i q u e so ff o r m a lm e t h o d s ，w e d i s c u s st h es t a t eo ft h ea r to ff o r m a lm e t h o d sa p p l i e dt ot h ef i e l do ft h e s e c u r i t y p r o t o c o l s v e r i f i c a t i o nt h o r o u g h l ya n d o b j e c t i v e l y s e c o n d l y , w eg e n e r a l i z et h ea p p l i c a t i o np r o c e d u r e so ft h r e e i n f l u e n t i a lf o r m a l m e t h o d si nt h i sf i e l d t h e ya r ed o l e v y a om o d e l ，b a nl o g i c ，a n ds t r a n ds p a c e s i n o r d e rt od e m o n s t r a t et h ep r a c t i c a b i l i t yo ft h e s em e t h o d s ，w eg i v et h ec o r r e s p o n d i n g e x a m p l e so f t h ep r o t o c o l v e r i f i c a t i o n t h i r d l y , w ec o n c e n t r a t eo u r r e s e a r c ho ns t r a n ds p a c e sw h i c hh a sm u c h a p p e a lf o r p e o p l er e c e n t l y a n do u rw o r ki s t of u l f i l lt h ef o l l o w i n gf i v eg o a l s ：f i r s t l y , t og i v ea d e t a i ld e s c r i p t i o no ft h ei d e a ls t r u c t u r e ；s e c o n d l y , t of o r m a l i z et h ec o n c e p to fs a f ek e y s t h i r d l y , t od i s c l o s et h er e l a t i o nb e t w e e ns a f ek e y sa n dt h ep r o t o c o ls e c r e c yp r o p e r t y ； f o u r t h l y ，t of i n dt h ep r o p e r t i e sr e l a t e dt os a f ek e y s ；f i f t h l y , t os u g g e s ta n e w p r o t o c o l s p r o o fm e t h o d i no r d e rt o f u l f i l lt h ea b o v ei d e a s ，w ei n t r o d u c eas e r i e so fn e w n o t a t i o n st od e s c r i b et h ei n n e rs t r u c t u r e so ft h ei d e a l s ；g i v eaf o r m a ld e f i n i t i o no fs a f e k e y sb y t h ec o n c e p to f i d e a l s ；p r o v et h ee q u i v a l e n c er e l a t i o nb e t w e e ns a f ek e y sa n d s e c r e c yp r o p e r t yu n d e rc e r t a i nc i r c u m s t a n c e sb yc o m p a r i n gt h ei d e a l sd e s c r i p t i o n so f t h e m ；p r o v et h ep r o p e r t i e sp e r t a i n i n gt os a f ek e y sb y t h ec o n c e p t so f p e n e t r a t o rk e y s a n dt r a c e s b a s e do nt h ea b o v ew o r k s ，w e p u tf o r w a r d t h ei d e ao f t h es e c u r i t yp r o t o c o l p r o o f m e t h o d b a s e do nt h ec o n c e p to fs a f ek e y sa tl a s t f o u r t h l y , w es u g g e s tan e wt a x o n o m yo ft h es e c u r i t yp r o t o c o lf l a w sb a s e do n i i s t r a n ds p a c e s t h i st a x o n o m yp a r t i t i o n st h ef l a w si n t oe i g h tc l a s s e s t h a ti s ，n o n c e l o s sf l a w , d i r e c t i o nl o s sf l a w , t y p el o s sf l a w , i n d e p e n d e n c el o s sf l a w , r u ni d e n t i f i e rl o s s f l a w , a u t h e n t i c a t i o np r o c e d u r el o s sf l a w , t h es a m ef o r ma u t h e n t i c a t i o nt e s tf l a w , a n d t h es a m ef o r ma u t h e n t i c a t i o nt e s tc o m p o n e n tf l a w w ea l s oa n a l y z et h ep r o t o c o l sw i t h o n eo ft h ef r o n tf o u rc l a s sf l a w sb yt h ea u t h e n t i c a t i o nt e s tm e t h o d f i n a l l y , w ei n t r o d u c et h e c u r r e n ts t a t eo ff o r m a lm e t h o d sa p p l i e dt o s e c u r i t y p r o t o c o l sd e s i g n i na d d i t i o n ，w ed i s c u s st h ed e v e l o p m e n td i r e c t i o n s & t h i s f i e l d k e yw o r d s ：s e c u r i t yp r o t o c o l ，f o r m a lm e t h o d ，f l a w st a x o n o m y , p r o t o c o l v e r i f i c a t i o n i i i 第一章绪论 1 1 、来自安全领域的需求 形式化方法的发展在很大程度上要归功于来自安全领域的实际需求。早在七 十年代到八十年代早期，形式化方法发展的雏形阶段，该领域内的研究与开发资 金就主要来源于美国国家安全局 1 0 5 1 。其后，随着i n t e m e t 应用在全球的迅速普 及：政府机构的网上办公、商业团体的网上交易、以及个人用户的网上购买，不 仅提高了人们的办公效率与生活质量，还将人们对安全问题的关注程度提升到了 一个前所未有的高度。无疑，这就为各种成熟的安全技术创造了最佳的应用时机。 那么，形式化方法是否是一个成熟的安全技术呢? 通过下面对形式化方法在安全 协议验证领域内的发展过程的阐述，我们来回答这个问题，并进一步引出本文工 作的背景与意义。 1 2 、安全协议的描述方法 简单来说，安全协议就是指那些利用密码学算法以实现某些安全目标( 性质) 的协议，其中安全目标包括：秘密性、认证性、不可否认性，与公平性等等。我 们通常所说的认证协议就是指那些将秘密性与认证性作为安全目标的协议。回顾 安全协议的描述方法，我们可以发现它大致经历了如下三个发展阶段：自然语言 描述阶段、符号化( s y m b o l i z a t i o n ) 描述阶段、与形式化( f o r m a l i z a t i o n ) 描述阶段。 1 2 1 、自然语言方法 借助自然语言描述协议的过程很类似于描述一个剧本：首先，介绍每个参与 者在剧本中承担的角色，如图1 所示。 人名角色 a 1 i c e b o b t r e n t 协议的发起者 协议的响应者 协议的仲裁者 图1 其次，描述每个角色在剧本中的表演顺序与内容。这里，我们将以 皇里型茎奎兰矍主鲎笪婆苎一一 n e 。d h a m s c h r o e d e r 共享密钥协j , s l 7 6 1 的前三三个步骤为例： f 1 1a l i e e 将囊；l 魏豹名字缩写a ，b o b 兹名字缩写b 与涎季建数蜀组或麓游惠发送 给t r e n t 。 ( 2 ) t r e n t 产生个随机会话嶷钥五。然后，他用与b o b 共享的密钥。对随机会 话密锾髭与a l i c e 匏名字缎写蠢缝或醵湾怠进行麓寮。睫蜃，德瓣与a l i c e 共享的密钥彤。对a l i c e 的随机值r 。、b o b 的名字缩写b 、会话密钥世，以 及刚刚产生的密文组成的消息进行加密，最后将产生的密文传送绘a l i c e 。 ( 3 ) a l i c e 簿密浚謦戆溃塞骧爨致置，势确谈与爱一莛发送给筵懿氏与楚在( 1 ) 中发送给t r e n t 的一样。然后，她将使用t r e n t 与b o b 共享密钥加密的消息 传送给b o b 。 1 2 。2 、符号纯方法 在使用符号化方法描述协议之前，我们首先给出如下约定：使用大写字母表 示参与协议的主体，倒妇使用a 代表a l i c e ，使用，代表t r e n t ；使周袁。表示随枫 数；使用趸。表示a l i c e 与t r e n t 之间共享的长期密钥；使用譬表示t r e n t 分发静 会话密钥；使用 lmi 。表示利用长期密钥k 。加密的密文，其中m 表示某个明文； 使耀符号_ 表示消息黄送的方向；使用逗号分隔消惠中的不嗣部分；馒蠲冒号分 隔消怠内容与消怠传送方向。如果遂驮如上约定，那么我们就可以给出 n e e d h a m s c h r o e d e r 共享密钥协议前三个步骤的符号化描述，如下所示。 1 a _ t ：a ，b ，r z 2 + a ： | 曩 ，鸯，爱， | k ，a l 岛l 戤 3 a - - ) b ： | k ，a ) 与自然语言描述方法相比较，符号化攒述方法的优点是简洁明了。 1 2 。3 、形式讫方法 形式化方法是一种用于描述系统性质的数学方法，它主要用于发现个系统 中翳跛义性、不一致性，与不宠餐性 1 0 4 】。鄹么这个系统霹班丈到菜个企业级戆 软件、硬件系统，也可以小到我们讨论范围内的菜个协议。 与符号化方法相比较，我们使用形式化方法对协议进行描述不仅媳为了简化 描述避程，丽是为了进一步剥耀澎式纯方法对强议进行验_ i 囊：迁馥癸议楚正确豹， 酃实虢了为其粼悫的各稚安全性目标；或者分析出协议存在的缺陷。函此，形式 第一章绪论 化方法在给出描述协议的符号集合基础上，还会在该集合上定义各种关系与运 算，以进一步揭示隐藏在协议内部的各种性质。 那么如何运用形式化方法证明协议的正确性呢? 证明过程通常可以分为三 个部分：第一、确定证明的目标，即协议需要实现何种安全目标；第二、建立协 议的形式化模型，即给出协议的形式化描述；第三、证明。 虽然形式化方法为协议的验证工作提供了强大的证明手段，但是形式化方法 并不能为协议的正确性提供百分之百的保证。这是因为：首先，协议e 确性的证 明总是在证明它的形式化方法所采用的特定假设下进行的，如果违背了这些假 设，那么原先的证明结果也就失去了意义。例如，已知对于n e e d h a m s c h r o e d e r 共享密钥协议存在一个经典的重放攻击 2 2 】。在该协议基础上设计的k e r b e r o s 协 议 5 1 5 2 1 中使用的票据( t i c k e t ) 的概念本来是为了实现系统的单一登陆功能，来提 高协议的应用效率。但是通过观察，票据的使用过程在理论上就类似于上述的经 典重放攻击。那么为什么还认为k e r b e r o s 协议是正确的呢? 这其中的原因不乏理 论在技术上的折衷，更重要的是我们假设：入侵者不具有在票据的生存期内破解 票据中的会话密钥的能力。在这个假设下，我们就可以放心的享受单一登陆给我 们带来的工作上的便捷。其次，要给出针对协议证明过程中的所有隐含假设通常 来说是不现实的并且也是无法实施的。这是因为我们在给出一个形式化方法时不 可避免地会遗漏某些条件；并且形式化方法受自身因素限制也会采用不同的假 设。这自然会导致如下情况：协议被某个形式化方法证明是正确的而又被另一个 形式化方法证明存在缺陷。例如，b a n 逻辑【5 】没有发现l o w e 提出的存在于 n e e d h a m s c h r o e d e r 公钥协议中的缺陷 5 7 】，就是因为在b a n 逻辑中假设协议的 合法主体是诚实的。而s t r a n d 空n 1 0 1 没有采用这个假设，因此可以证明该协议 存在缺陷。但是s l x a n d 空间也不可避免此类问题。例如，由于它采用了强类型抽 象假设 4 3 ，因此对于具有类型缺陷的协议最初也束手无策。 最后，需要指出的是：目前形式化方法主要用于研究协议的性质，这在很大 程度上独立于协议所包含的密码算法的性质，因此下文中我们总是假设协议所使 用的密码算法是不可破解的。 1 3 、形式化方法在安全协议验证领域的应用 上世纪七十年代末，n e e d h a m 与s c h r o e d e r 第一次明确指出：使用非形式化 3 中国科授大学博士学位论文 方法很难检查协议设计中存在的缺陷，研究人员应该开始寻找能够验证协议正确 幢翡耨方法f 7 魏。在这个倡议一f ，籍形式纯方法应爱予安全耱谈验证弱番秀究工馋 逐步开展起来。 1 3 1 、d o l e v - y a o 模型 上世纪八十年代裙，d o l e v 与y a o 首先为安全协议建立了一个代数模型 2 5 1 。 其中，协议消息的接收与发送分别对应一缀代数表达式与相应的变换规则。并且， 网络被认为是处予入侵者的羧涮之下：入侵卷可以读取所有的瀵患，弗具有创建、 修敬与破坏消怠瀚能力。因戴，d o l e v - y a o 模型又被称为入侵者模登。 在d o l e v - y a o 模型中假设：在协议执行之前，入侵糟不知道合法主体的任何 秘蜜。但在协议执行过程中，入侵者可以执 亍舍法主体隧够执行的糅 乍。j 遨外， 漓怠满足重写规刚，即，消意 2 l ，= 协( 爿，b ) i 对于所有彳曰与f 1 对于某个m ( ，y ) ，如果存在某个y ，使得下式成立， yn ，( x ，】，) = 其中，旯表示一个空序列。那么我们称协议t 是不安全的；否则称t 是安全的。 2 1 3 、实例 我们考虑如下简单级连协议s t ，其协议执行过程如下所示： ( a ) a 向b 发送消息：( a ，e 。( m ) ，b ) ； ( b ) b 向a 发送消息：( 日，e a ( m ) ，m 。 首先，我们利用d o l e v y a o 模型给出上述协议的形式化描述如下： ( d ) n l ( 爿，b ) m = a l ( 4 ，b ) m = e 8 ( m )其中口，( a ，b ) = e 。 ( b ) n 2 ( a ，b ) m = 届( a ，b ) n l ( a ，b ) m = 届( a ，b ) a l ( a ，b ) m = e a d b e a ( m )其中属( 4 ，b ) = e a d 。 = e ( m ) 那么入侵者z 将对协议s t 展开如下攻击： ( 1 ) z 截获在步骤( a ) 中a 向b 发送的消息：( a ，e b ( m ) ，b ) ： ( 2 ) z 将消息( a ) 中的发送者名称a 改为z ，然后将改动后的消息发送给曰 ( z ，e 。( 肘) ，b ) 。 ( 3 )曰按照协议要求回复z 消息：( 口，e ，( m ) ，z ) ( 4 ) z 收到消息来自b 的消息：e ，( m ) ( 5 ) z 使用自己的私钥解密消息e z ( m ) 以获得明文消息：m 。 巾国科技大学博士学位论文 于是，在d o l e v y a o 模型中就会检查到存在y = d 。屈( z ，彩，使得 rn ；( ，嚣) = 磁磊( z ，b ) n l ( a ，b ) = d z e z d b n l ( a ，雪) = d z e z d 8 e 8 = 童 这也就验证了协议s t 是不安象的。 2 。2 、b a n 逻辑 在b a n 逻辑【5 】中给出了l o 个命题符号；并且给出9 类推理规则。这早我们 只奔绍与实例相关的6 个基本命题符号与3 个主要推理规则。并且，我们选用的 实鲷莱瘸弱热密箨法基予对禳凝密方案。 2 2 1 、命题符号与公理 首先，给出6 个基本命题雅号如下： ( 1 ) p x ：p 鬻觅了x ； ( 2 ) p l x ：p 瞥经说过x ； ( 3 ) p 每x ：p 糕信x ： ( 4 ) p 睁x ：p 褥权给蠢x ； ( 5 ) # ( x ) ：x 是新鲜的； ( 6 ) p ”9 ：p 与q 共享对豫密绸k 。 其次，洽出3 个主要摧琏瓶剜如下： a 1 消息含义公理： 石 墨| 篓望竺翌! 曼墨 | 茎| ! 墨 p 净q l a 2 n o n c e 验证公理： p 睁# ( x ) ，p | s q 卜羔 p | - 窖高x a 3 裁决权公理： 曼睦垒! 三兰! 曼基望睦墨 p 睦x 整兰皇室皇垫堂堂薹垡垦至查婆蹩盟兰型一 2 2 2 、分柝过程与目标 b a n 溅辑的形式纯分析过程为： ( 1 ) 理想化协议，即，逻辑公式化； kj s ( 2 ) 绘出初始假设，铡，a 净a 种s f 3 ) 戬公理为基础进行稚遴。 b a n 逻辑的形式化分析目标为： 2 , 2 3 、实例 蜀 a 每尘壬熬 芷 b k a 君 我们考虑如下经简化的协议部分s p ， m e s g l 。a 寸s ：b , n m e s 9 2 。s 斗a ： l n a ，b ，爱“8l 。 首先，理想化上述简化协议， k _ o m 1 囊 s ：嚣，n m 2 。s 专a ： l n ，童h 嚣 。 其次，建立如下初始假设， p 1 a l s # ( n ) * p 2 。a 巨( s = ，a 露) k s p 3 a 睁( 爿针s ) 最后，进行逻辑攘理，过程如下： ( i ) 裰据协议理怒纯漓爨m 2 ，可褥缀论r l ： k 日 a 司( ，ahb ) ； 2 ) 提据初始啜设p 3 、绻论l ，与公理崖i ，可愿缡论f 2 ： 嚣 0 a i ；s 卜( n 4 ，a 廖) ： ( 3 ) 根据协议理想化消息m 2 与初始假设j p l ，可得结论r 3 ： 芹f a 净器( _ ，a b ) ； ( 4 ) 根据结论r 3 、丁2 ，与公理爿2 ，可得结论r 4 ； k a s a ；s | a b ； ( 5 ) 根据初始假设p 2 、绪论，4 ，与公理彳3 ，可褥结论r 5 ： 妻璧整垄查兰簦主兰壁笙苎 k 口 a | ；ahb 通过利用b a n 逻辑对协议部分s p 进行分析，我们得到主体爿相信他与b 共 享会话密钥k 。8 的结论。 2 3 、s t r a n d 空闻 在利用s t r a n d 空间证明认诞协议的j 下确性时，相关文献中曾经出现三种不同 的证明方法 3 4 】 1 0 2 】：基本的诞明方法、借助理想概念的证明方法，与认证测试 的证明方法。这里我们将采用藜本黥涯明方法来验证我镪对n e e d h a m s c h r o e d e r 公钥秘议豹浚逮蔽本懿谈证髓痰。 2 3 1 、协议描述 一个协议通常包括几个角色，例如：协议发起者、协议响应者，与认证服务 器。谤议稳瘸一个参数剜表，例如：主体名称、会逶寝镜、n o n c e 等，预先定义 了每个受魏疆需撬行静瀵患枣舞。这个漕恩序甍可以表示为：角色 参数弼表】。 当给定角色与参数列表也就意味潜确定了该角色的消息序列实例。这个消息序列 实例也就对j 藏着一个s t r a n d 集台，例如：下文2 3 4 节中讨论的n s l 协议的发起 者s t r a n d 表示为i n i t a ，b ，n 。，巩】。因此，一个协议的正常执行过程也就形成了一 个b u n d l e 。 2 3 2 、入侵模型 入侵者消息序列具有八种不同的类型，参见附录a 中定义a 4 1这些类型 同样可以被褥作是入侵者扮演的不同角色，并且可以记作：拍嘲、k 彤】、f 【翻、 t 【g ，h 】、c g ，h 】、s g ，h 】、e g ，h 】、【窖，h 】。此憝熬漶法与瓣录一中的臻有不弱， 是为了与：角色f 参数列表】，静格式相一致。 2 3 3 、安企目标 对于认诚协议，通常的安全目标是指：认证目标与秘密目标。 ( 1 ) 谈证嚣搽 s t r a n d 空障采庵了l o w e 掇蹬的一致往( a g f c e m e 哟鼙标 6 1 】。铡如：协议响应 者对发起者的非单射一致性认证目标的逻辑表达如下； v c r e s p ( _ j ) c 等i n i t ( i ) e c 1 6 篓三童窒全望釜垄茎堡鍪鎏壅婆錾望茎篓一一一 其中c 是b u n d l e 变量，r e s p ( i ) 与i n i t ( 膏) 分别表示数据i 给定盾的响应者与 发起糟s t r a n d 。 ( 2 ) 秘襄墅耩 锖辩蘩令涟患顼v 翁秘密往，s t r a n d 空闯采臻了弱下翁遥疆表达式； _ 1 j c ( r e s p ( 王) c n o d e ( + v ) c ) 2 3 4 、实例 在下文豹讨论中，我们憋蓉是绘出n e e d h a m 。s c h r o e d e r 公钥秘议豹认证辊割， 从两遴一步分析它的设计缺陷，然后援出针对该协议的勇一静改避方法。最后， 我们将利用s t r a n d 空间来诋明这个改进方法的正确性。 2 3 4 1 、针对n e e d h a m s c h r o e d e r 公钥协议的改进 ( 1 ) n e e d h a m s c h r o e d e r 公锈协议翡谈话祝制 我们采雳l o w e 绘窭匏n e e d h a m s c h r o e d e r 公镇协谈酶餐讫敝零 5 7 1 ，鄄，霰 设协议的合法主体已经得到其所需要的公钥，如下所示： 1 爿斗b ： | n 。，爿阢。 2 嚣哼a ： l 虬，n b 艮。 3 + a 寸b ： | 辑| 。 上述协议可以分为两个单向过程：首先是a 对口的认证过程；其次是b 对爿 的认证过程。为了研究认i 藏过程所采用的认证机制，将上述协议解析为如下两个 部分，分别称为c r l 与c r 2 ： c r lc r 2 a lr a 寸b ： l 以，a | b 2 + b 峥a ： 菇，n 6l n b l b 哼a ： | n 。，x 1 ) “ a 2 a - - b ： l n bi ) 如 在c r l 部分暂不考虑随机数氓的作用，所以使用符号j 代替了它的出现。 对予在c r l 中豹醚掇数。骰疑撵豹娃理。可以瑟嚣c r l 与c r 2 繇袋敬兹谈证飘 到是纂本婚鹰询应答( c h a l l e n g e - r e s p o n s e ) 、跌证梳南l 。 下面进一步分析c r l 中的消息a 1 。消息口1 怒4 向口发出的质询，它由随机数 n 。和身份标识爿组成，并且使用b 的公钥k b 进行加密。可以看到，随机数虬标 识了消慧的掰鲜性。身份标识0 说明消惠来自传方，它掏成了消患黝源标识；公 1 7 串溪辩按夫学藉学经论义 钥k 。说明消息欲发往何处，它构成了消息的目的标识。 再来观察c r 2 中的质询消息6 2 。可以发现：6 2 中没有包含消息的源标识b 。 对于协议设计的初襄可作如下解释：6 2 与6 1 一同发送，其中6 l 包含的虬为5 2 构 建了主下文蓼壤，疆示了2 懿采源。举弼寒蘧，穰竣蠢嚣时淘b 帮c 发爨矮稳， 那么就会为嚣和c 分别生成。与。，如图2 步骤l ，并保存它们与对应的响 应者身份标识之间的映射关系r = ( n o ，b ) ，( 。，c ) ) 。当曰与c 同时应铃a 时， 如图2 步骤2 ，a 根据应答消息中的随机数与保存的关系r 就能判断出应答来自 蔼处。魏暴随麓这两个应答一起发送8 与e 对4 酌溪淘，如图2 步骤3 ，那么在 这嚣个震诲漓怠中就可敬省去滔慧豹源标识，强下溺掰示。 1 b ! ! 笠：生! ! a ! ! ! ；：曼i ! 墅- c 2 b! 墨：篓| ! a ! 竖：兰i ! 些e 3 bg 墨塾l ! 妊，a i 圣整l ! 生c 图2 ( 2 ) n e e d h a m s c h r o e d e r 公钥协议的认证缺陷 鼠主一小节懿分褥中可美簿蘸这样的结论：燕溪2 步骤3 瑟示，在艿与c 惫 a 发送的质询消息中不用加入消息的源标识，这是因为在步骤2 中它们对a 的应 答消息已经潦先说明步骤3 中的质询消息来自何处。但是得出该结论的前提是入 侵者不会是参与协议的合法主体。现在将去掉这个前提，继续来研究图3 ，它是 l o w e 攻壶【5 明的示意图。 | n o ，a n o ，a l 1 a i b i n o ，x i ) 粕 2 a - 。二 i ! 竺：兰堕b a ! 苎塾| kl ! 墨苎| ! 塾b 3 a 坚监- i ! 塾监- b 图3 1 8 燕三兰室全塑婆丝塞垡墼堡查鎏鏖曼兰型 图3 中，主体j 是主体爿发起的协议的合法响应者，因此a 保存关系记录 蠢= ( 咒，劲。但是在步骤l 中f 将源蠡叠的痿询游惑的霞的标谚 盘，改荛嚣， 将此质询黧定向至占。因此在步骤2 中当爿收到由露产生的应豁时，他会根据记 录矗将此应答的发送者别定为，。于是，可以进一步利用一来应搭嚣发出的质询， 并在步骤3 中将兹痤答潞惑的匿懿标谈出j 改为嚣。这样j 裁藏功遥隘酶身份 与占完成了身份认证。问题的关键在于：在步骤2 中，对a 的应答消息中，随机 数。已经不能起到暗承消息来源的作耀。这是因为在此之前融将包含。的消 怠重定两绘嚣，这释a 瓣关系记录实际上交作霞= ( 蜕，) ，( 蜕，露) ，a 逮裁不能 依据n 。给出的上下文关系正确地判定步骤2 中的消息来源。 f 3 ) n e e d h a m 。s c h r o e d e r 公锷协议靛致避方法 在上- d , 节中分析了造成n e e d h a m s c h r o e d e r 公镅协议设计缺陷的原因，即， 如果质询消息可以被重定向，而接下来的应答消息又不具备明确的方向标识，就 会引发类似豹攻击。霆她狂稳定掺改方察薅裁可以遵矮两条墨潞：其一，疆i 匕簸 询消息被鬃定向；其二，给应答消患加入缺失的方向标识。 改进方法一 款第一条瑟露警发；之驻敬j 霹骇重定彝寒鑫a 弱蒺谗演惫，跫透为恐爨毫 私钥世i 1 ，在具有阅读质询消息的能力的同时还具有改动消息的能力，那么为了 使，改动消息的能力受到限制而又使其不丧失阅读消息的基本能力，也就是要求 a 发送豹游惑只有尘有投浚动，显然瓣办法是要求幺黠萁发送戆瀵惠送行签名。 按照这个设想，得到如下形式的协议，我们称之为n s r 协议： 1 - a 斗b ：爿，删乜，a i k 。 f = i 2 t 雪叠： | n 。，甄| 岛 3 一斗b ： | 帆f ) 如 改进方法二 校据露二条思路甭寒豹改遗方法楚给应答港患热入映失静方淹标谖，印在 n e e d h a m - s c h r o e d e r 公钥协议消息2 中加入协议响成者的身份标识，以说明消息 的真实出处。这也是l o w e 对n e e d h a m - s c h r o e d e r 公钥协议提出的修改方式【5 7 】， 鲡下所示，遴常被称之莠n s l 旃议。 主旦型型塑鲨塑塑l 一 1 a 寸b ： j n 。，a i ) 2 b a ： i n 。n ，b 1 ) k 。 3 a 呻b ： i 6i ) 。 2 3 4 2 、利用s t r a n d 空间证明n s r 协议的认证目标 在上文中讨论的n e e d h a m s c h r o e d e r 公钥协议的两个改进版本中，n s l 协议 的正确性证明可以参考文献 1 0 2 ，下面为了验证我们提出的n s r 协议的正确性， 我们将同样利用s t r a n d 空间给出关于它的认证目标的证明。 ( 1 ) n s r 协议的s t r a n d 空l 司 一个n s r 的s t r a n d 空间是如下三类s t r a n d 的并集： 、入侵者的s t r a n d 为s 毋。： 、发起者的s t r a n d 为s i n i t a ，b ，n 。，n b ，其对应的消息序列如下： ( + l l 。4 i ) 1 ) 。? ，一 ；。n1 ) b ，+ l a1 ) ) 其中，爿，b t 。，n 。，n g ，但是j v 。茌。i n i t a ，b ，n 。，n 】表示具 有如上消息序列的所有s t r a n d 的集合。与这类s t r a n d 相关联的主体为4 。 、响应者的s t r a n d 为s r e s p a ，b ，n 。，n b 】，其对应的消息序列如下： ( 一洲n 。a ，+ l n 。n b ，一 i 虬i k 。) 其中，a ，b t 。，n 。，n 6 f ，但是n 6g 。r e s p a ，b ，n 。，n 6 】表示具 有7 女r l 上消息序列的所有s t r a n d 的集合。与这类s t r a n d 相关联的主体为b 。 ( 2 ) n s r 协议的认证目标 这里我们只讨论协议响应者口对协议发起者a 的认证目标。假设： 、匹是一个n s r 空间，c 是匹中的一个b u n d l e ，并且s 是r e s p a ，b ，n 。，n b 中 一个高度为3 的s t r a n d ： 、巧1 诺；并且； 、n 。n 6 并且。、n b 分别唯一地产成于匹。 那么c 中包含一个高度为3 的发起者s t r a n d t i n i t a ，b ，n 。，n b 】。 2 0 第二章安全协议形式化验证方汝庶用举倒 ( 3 ) 认证目标的证明 首先为了下文表示方袋，我翻设磺： v = 洲n 。a 然后采诞明如下结论：嶷台s = 妇e c ：v 匕t e r m 扔) 具有一个! 一疆小节点弘，该 节点为合法节点且符号为正。 因为”2 = c 并且vr - t e r m ( n 2 ) ，所以集合s 非空。根据附录爿中的命 题a 2 1 ，则s 具有一个蔓一最小节点拨。根据引理a ，2 2 ，可躲弹，的符号为正。 下面我们采糟反证法来证明琢为合法节点。缓设哺所在的入侵蠢s t r a n d 为p ，我 们来考察p 可能对应的消息序列t r ( p ) 的所有形式。 藜，：+ ) ，其孛f 彰。因为v 旗t ，瑟竣臻不凌对应魏静淤惑痔剜酶p 主。 ：( 一g ) a 对应此种消息序列的p 不包含正结点，因此一不在p 上。 l ：( 一g ，+ g ，+ g ) 。对应此种消息序列的p 上的正节点在c 中不是最小出 魂，戮毙托不在p 上。 4 c 甜：( 一g ，一h ，+ g h ) 。如果v c t e r r n ( g h ) ，那么有vr - - t e r m ( g ) 或者 v r - t e r m ( h ) 这与强飓s 中的! 一娥小节点相矛盾，因此啊不在p 上。 s 酗：一妙，+ 塾+ 矗) 。热象v 拦t e r m ( g ) 或畿vr - t e r m ( h ) ，郡么有 v 匕t e r m ( g h ) ，这与m 是s 中的一最小节点相矛盾，因此煽不在p 上。 已，r ：( k ，一h ，+ ih 1 ) 。) 。如果vr - l 矗| ) 。且v 啦h ，那么有 = 。以i ) 。 虽爱= 鬏，这与鬏设置7 星品耱矛詹，因_ 毙栉，不在p 土。 d ：( x ，一 i h f ) r ，+ h ) 。如果vr - - h ，那么v e 引h 阪，这与聍。是s 中 的! 一最小节点相矛盾，因此巩不在p 上。 逶遘上溪豹讨论可簸毪不在尹上，因筵裾，舞会法节点。鬣察落空闻著考纛至l v 的形式，”l 所在的合法s t r a n d 只能是发起者s t r a n d 。设强所在的发起者s t r a n d 为t7 ，则t 7 i n i t a ，b ，n 。，n 】对于某个，并且高度至少为1 。 密文献【1 0 2 】中瓣g l 骥5 , 9 ，我餐霹缮如下结论：在霪孛存在一个发超者s t r a n d t i n i t a ，d ，n 。，n b 】，对于某个d ；并且f 的高度为3 。 在上面两个结论的基础上，接下来我们证明如下结论：在搭中，有f ，；t 且 t , t i n i t a ，b ，a 乞，甄】，并且 ，t 豹褰泼为3 。 我们采用反证法：假设f t 。那么，区1 ) b t i n i t a ，d ，n 。，虬】对于某个d ， 2 1 中国科技大学博上学位论文 可以得出n 。产生于 ；因为f i n i t a ，b ，n 。，n 对于某个n ，可以得出n 。产 生于 。这与。唯一地产生于匹相矛盾，所以f 7 = t 。因此有d = b ，以及 7 = 。，于是有t = t i n i t a ，b ，n 。，n 6 ，并且f ，7 高度为3 。口 关于主体一对主体b 的认证性的证明以及。与。的秘密性的证明与文献 1 0 2 】中给出的证明方法相同，这罩不再赘述。 2 4 、本章小结 通过上文对d o l e v y a o 模型、b a n 逻辑，与s t r a n d 空间的应用过程的讨论， 尤其是利用s t r a n d 空间证明针对n e e d h a m s c h r o e d e r 公钥协议的新的改进版本 n s r 协议的认证性质的过程，我们可以看到形式化方法在安全协议的验证工作中 发挥的切实作用，从而说明在利用形式化方法验证安全协议这个领域内的研究绝 非仅是一种理论上的游戏。 第三章针对s t r a n d 空间中理想结构的研究 在s t r a n d 空间的相关文献【9 9 【1 0 2 中只勾勒出理想结构的大致轮廓，本文我 们引入新的符号，在如下命题的证明过程中进一步表达理想结构的内部细节。 3 1 、理想概念的回顾 对于理想的定义可以参考附录a 中的定义a 5 1 。在展开下文的讨论之前， 我们还需要回顾一下附录a 中的命题彳5 1 ：“ 如果s 三月，那么i k s _ u ，。s l k x 。” 与引理a 5 1 ：“ 设& = s ，s + 。= 1 9 1 。：g 厶 s 】，k k 。那么，k 【s = u ，厶【s 。” 对于上述引理中的下标索引i