（计算机软件与理论专业论文）rfid安全协议形式化分析研究及drap协议的建立与实现.pdf

摘要 随着计算机网络通信的迅猛发展，网络安全开始被人们所重视，其中 安全协议分析验证已成为一个研究热点。对安全协议的分析验证的方法和 手段有很多，其中形式化分析方法已被证明是分析和验证安全协议的最为 有效手段。 r f i d ( r a d i of r e q u e n c yi d e n t i f i c a t i o n ) 技术近年来得到了长足的发展， 成功的应用于各个领域，但由于r f i d 系统组成的特殊性，分析与设计安 全、高效、低成本的r f i d 安全协议仍然是一个具有挑战性的课题，它的 研究对安全协议、电子商务、r f i d 系统领域具有重要的意义。 首先，本文以串空间理论作为基础建立动作集合、事件集合、串以及 串空间，将协议实体模型化，并通过通信端的理想与诚实界定攻击者的能 力，用以发现协议实体中可能出现的漏洞。 然后，分析了现有的r f i d 安全协议的优缺点，使用串空间理论方法 着重分析了其中的数字图书馆r f i d 协议，根据分析结果提出了一个r f i d 系统的安全协议，并根据b a n 逻辑分析方法的分析结果对其进行了相应 修改，得到了一个适用于r f i d 系统的d r a p 协议模型，随后通过串空间理 论对其优缺点以及攻击者能力作出了精确的描述。 最后，本文根据先前的分析结果，采用三方通信密码命中的模拟方式 进行试验。使用基于a c e ( a d a p t i v ec o m m u n i c a t i o ne n v i r o n m e n t ) 框架的 c + + 语言对上述协议模型进行实现，得到相关试验数据，经对比分析试验 数据验证了分析结果的正确性。 关键词安全协议；r f i d 系统；串空间；b a n 逻辑；形式化分析；d r a p 协议 燕山大学工学硕士学位论文 a b s t r a c t w i t ht h er a p i dd e v e l o p m e n to fn e t w o r kc o m m u n i c a t i o n , n e t w o r ks e c u r i t y i sg a i n i n gm u c hm o r ea t t e n t i o na n ds e c u r i t yp r o t o c o la n a l y s i si sc o n s i d e r e da c h i e f c o n c e r na sw e l l t h e r ea l ev a r i o u sa p p r o a c h e st os e c u r i t yp r o t o c o la n a l y s i s ， a m o n gw h i c hf o r m a la n a l y s i sm e t h o dh a sb e e np r o v e dt ob et h em o s te f f e c t i v e w a y a tp r e s e n t i nr e c e n ty e a r s ，r f i d ( r a d i o f r e q u e n c yi d e n t i f i c a t i o n ) t e c h n i q u eh a sb e e n 觚l yd e v e l o p e da n ds u c c e s s f u l l ya p p l i e di nd i f f e r e n tf i e l d s c o n s i d e r i n gi t s s p e c i a lc h a r a c t e r i s t i c s ，i ti ss t i l lac h a l l e n g i n gt a s kt oa n a l y z ea n dd e s i g nas e c u r e r f i ds e c u r i t yp r o t o c o lo fh i g he f f i c i e n c ya n dl o wc o s t , w h i c hh a sg r e a t s i g n i f i c a n c et ot h ef i e l d s ，s u c ha s ：s e c u r i t yp r o t o c o l ，e l e c t r o n i cc o m l r l e r c e ，r f i d s y s t e m b a s e d0 1 1s t r a n ds p a c et h e o r y , t h ea r t i c l eb u i l ta c t i o n s ，e v e n t s ，s t r a n da n d s t r i n gs p a c e ，r e a l i z e dm o d e l i z ep r o t o c o ls u b s t a n c e ，a n dd e t e r m i n et h ec a p a b i l i t y o f a t t a c k e rb yc o m r n u n i c a t e r si d e a la n dh o n e s t ，a n dt h e nl o c a t et h ed e f e c tw h i c h i sl i k e l yt oo c c u ri np r o t o c o ls u b s t a n c e s e c o n d l y ，i tw e i g h e dt h em e r i ta n dd e m e d to ft h ec u r r e n tr f i ds e c u r i t y p r o t o c o l ，m a d ea d j u s t m e n tt oi ta c c o r d i n gt ot h er e s u l to fb a nl o g i ca n a l y s i s m e t h o d ，a n dt h e nc a m eu pw i t hd r a pp r o t o c o la d a p t a b l et or f i ds y s t e m m e a n w h i l e ，t h et h e s i sa l s og a v ea na c c u r a t ed e s c r i p t i o no fb o t hi t sa d v a n t a g e a n dd i s a d v a n t a g ea n dt h ec a p a b i l i t yo fa t t a c k e rw i t ht h el a wo fs m m ds p a c e t h e o r y a c c o r d i n gt ot h ep r e v i o u sr e s n i to fr e s e a r c h , t h ea r t i c l ef i n a l l yc o n d u c t e d e x p e r i n a e n t 谢出a t t a c k c o m m u n i c a t i o n b y h i tt h ec o d es i m u l a t em e t h o d r e a l i z e d t h ea b o v e - m e n t i o n e dm o d e lw i t hc + + b a s e do na c e ( a d a p t i v ec o m m u n i c a t i o n e n v i r o n m e n t ) f r a m e ，o b t a i n e dt h er e l e v a n td a t aw i t hw h i c ht h er e s n i to fa n a l y s i s h a sb e e np r o v ec o r r e c t a b s t r a c t k e y w o r d ss e c u r i t yp r o t o c o l ；r f i ds y s t e m ；s t r a n ds p a c e ；b a nl o g i c a l ； f o r m a la n a l y s i s ；d r a pp r o t o c o l i l l 燕山大学硕士学位论文原创性声明 本人郑重声明：此处所提交的硕士学位论文r f i d 安全协议形式化分 析研究及d r a p 协议的建立与实现，是本人在导师指导下，在燕山大学攻 读硕士学位期间独立进行研究工作所取得的成果。据本人所知，论文中除已 注明部分外不包含他人已发表或撰写过的研究成果。对本文的研究工作做出 重要贡献的个人和集体，均已在文中以明确方式注明。本声明的法律结果将 完全由本人承担。 作者签字：谁易 磊日期：二。7 年妒，j 日 燕山大学硕士学位论文使用授权书 r f i d 安全协议形式化分析研究及d p - , a p 协议的建立与实现系本人在 燕山大学攻读硕士学位期间在导师指导下完成的硕士学位论文。本论文的研 究成果归燕山大学所有，本论文的研究内容不得以其它单位的名义发表。本 人完全了解燕山大学关于保存、使用学位论文的规定，同意学校保留并向有 关部门送交论文的复印件和电子版本，允许论文被查阅和借阅。本人授权燕 山大学，可以采用影印、缩印或其它复制手段保存论文，可以公布论文的全 部或部分内容。 保密口，在年解密后适用本授权书。 本学位论文属于， 不保密母 ， 表示，这里的一是序列 长度。 ( 3 ) 挈( s t r a n d ) 指的是一轮协议运行到某个时刻时某个协议的参与者 所执行的事件的序列，一个串就代表一个参与者。为了使得串的描述更加 形象化，使用映射f r 将一个串映射到有限序列消息集( 彳) ，映射f r 称为 迹映射，映射的像( 某个有限消息序列) 称为原像( 所给的串) 的迹，通常把 串的迹就为串。 ( 4 ) 串空间( s t r i n gs p a c e ) 二元组( ，t r ) 定义了一个串空间，其中是串 的集合，f r 是串中所定义的迹映射。下面是集合中的一些基本概念： 假设串j ，根据前面的定义j 是一系列事件的序列，定义其中的 每一个事件口q 做串j 的一个节点。使用元素对 表示一个节点刀，f 燕山大学工学硕士学位论文 是节点n 在串s 中的序号，称做节点n 属于串j ，表示为n j 。使用字母 标记节点集合。 节点萨 n ，定义i n d e x ( n ) = i ，s t r a n d ( n ) = s ，称i n d e x 为节点序 号函数，s t r a n d 为节点串函数。假设节点n 所代表的参与者的动作为 ( t r 0 ) ) ，= 盯口，定义t e r m ( n ) = 仃口，u n s _ t e r m ( n ) = a ，s i g n ( n ) = 仃，称t e r m 为 节点事件函数，“鄹t e r m 为节点消息函数，s i g n 为节点符号函数。通常也 会使用一个节点代表一个事件。 节点啊，n 2 n ，定义关系“- - ”：啊_ 也表示啊= 切，且n 2 = - a ，称 作发送消息a 给，或者，z 从喝接收消息a 。 节点，n 2 n ，定义关系“j ”：啊j n z 表示啊f ，n 2es ，并且 等式i n d e x ( n 1 ) = i n d e x ( r h ) - 1 成立，称作事件玛和吃相继顺次发生。定义 关系。j + ”：啊等+ r h 表示喁s ，且r h s ，称作事件和顺序发生。 假定，是无符号消息集合，定义节点n n 是集合，的入口点：当且 仅当3 t 1 ，其中t e r m ( n ) = + t ，且对v n j + n ，必须满足u n $ ! e r m ( n ) 仨。 定义消息项r 发源于节点n s ：当且仅当s i g n ( n ) = + ，其中 t “昭一t e r m ( n ) ，并且对v n j + n ，满足t c 堋一纪r m ( n ) 。 定义消息项t 唯一地发源于节点竹：当且仅当r 发源节点集合包含唯 一的一个节点元素n ；随机数等要求保持新鲜性的内容通常都要求具有唯 一发源的性质。 定义串s 叫做串j 。的子串：如果串s 包含串s 中的所有节点，记作 j s 。这样，由节点集和边关系n t 专n 2 和啊j 也一起构成一个有向图 。 3 2 3 丛和节点关系 丛( b u n d l e s ) ：丛c 是节点有向图 的一个子图，使用二 元组 表示，它对应于某个串空间；其中集合c 是附属于边集 的节点集，边集露= ( 一u ) 代表了节点之间的两种关系n t 斗n 2 和 塌j n 2 。定义节点n c ，当且仅当n r c 。定义串j c ，当且仅当v n e j ， 满足啊c 。任意丛c - - - - 还必须要满足如下三个条件： 1 6 第3 章串空间理论与模型及其扩展 第一，c 是非空有限和非循环的； 第二，若节点n e c ，且s f g n ( n e ) = - ，则c 中存在唯一的节点啊使 得，l i 寸坞，且有向边m 哼坞最； 第三，若节点n 2 r f ，且c 中存在节点啊使得强；啦，则有向边 喝jr h 历。因为c 是一个图，所以条件2 和3 蕴涵着啊c ，我们可 以把丛的边看作节点间的因果关系。 无论通信是同步的还是异步的，上述关于丛的定义都形式化了一个通 信过程模型的三个特征： ( 1 ) 一个串可以发送或接收一个消息，但是不能同时进行这两种操作； ( 2 ) 当一个串收到一个消息，有唯一的一个节点发送了该消息； ( 3 ) 当一个串发送了一个消息，可能有很多串接收到该消息。 图3 1 就是一个合法的丛。 - f 图3 1 丛不意图 f i g 3 - 1b u n d l e s sc h a r t 丛高度( c - h e i g h t ) ：若c 是一个丛，则使得节点 c 最大的i 的 值称为串s 的从高度；串j 的迹为打) = ，则册就是 j 的丛高度。 节点关系：假设s 是一个边的集合，且s c ( 一u 等) ，m 是附属于各 1 7 岫0叶0h 10托0可0飞0坩0坞 f 5 0 二 燕山大学工学硕士学位论文 边的节点集。对于v n l ，啦j ，定义节点之间的关系“ ，”和关系“毛”： 玛 ，n 2 表示在s 中存在一条从节点n l 到节点他的由呻和j 类型边组成的 路径，边的数目必须大于零。啊5 ，吃表示在s 中存在一条从节点惕到节 点的由_ 和j 类型边组成的路径，边的数目必须大于或者等于零。显 然 ，关系具有传递和闭合的性质，而毛关系满足自反、传递和闭合的性 质。如果s 是一个丛，则关系 。是偏序的。 引理3 1 ；假设c 是丛，因为二元关系刍是偏序的，所以c 的任意 非空节点子集都有! ，最小元，一般使用5 代替曼，。 引理3 1 是串空间理论的重点，大部分的证明都将被转换成求解某个 节点集的三，最小元。证明的思路就是求解“一个主体知道什么消息，他 又是什么时候知道这些消息的? ”这样一个问题的答案，这是一种归纳法 的原理，它吸纳了s c h n e i d e r 秩函数和p a u l s o n 归纳法的思想。 引理3 2 ：假定c 是丛，s 是c 的一个节点子集，并限定该子集中的 所有满足等式珊t e r m ( m ) = u n s) 两个节点和必须具有隶属 关系一致性，即要么都属于& _ 要_ t e r 么m 都( m 不属于在m 上述m 前提下，如下结 论成立：