（计算机软件与理论专业论文）基于进程演算的安全协议形式化研究.pdf

基于进程演算的安全协议形式化研究 摘要 随着网络技术的应用逐步渗透到许多关键部门，以及电子商务的兴起与广泛应 用，信息安全已变得e t 益重要安全协议是信息安全的基础，但其正确性和安全性却 不容乐观，已有的安全协议往往被证实并不如设计所期望的那样安全即使不考虑与 实现相关的协议缺陷和密码系统被成功破译的可能性复杂的网络环境还是使得攻击 者可利用安全协议自身的缺陷来实施各种各样的攻击因此，安全协议是否能达到它 所要求的安全目标是非常关键的问题 对安全协议的分析和验证是保证所设计的协议满足其安全性的重要技术手段，而 借助形式化的方法或工具分析安全协议是非常必要而且行之有效的安全协议的形式 化分析已有二十多年的历史，已逐渐成为安全协议研究的热点近十几年来。世界各 国学者对其进行了广泛和深入的研究，尤其是美国和欧洲的一些国家在这一关键领域 投入了大量的研究经费和力量同时，安全协议设计和分析也引起了国内研究人员的 高度重视虽然安全协议形式化研究领域取得了可喜的成果但尚有诸多问题亟待解 决，譬如，如何群j 确刻画安全协议，如何扩充现在已经成热的理论或方法去研究更多 的安全性质，如何使安全性质在统一的框架下进行分析和验证等等 安全协议是一个典型的并发分布式系统，而进程演算是一个强有力的并发分布式 系统建模工具，具有强大的描述能力和严格的语义，能够精确刻画安全协议中各个参 与者之问的交互行为利用进程演算对安全协议进行分析和验证时，既可以借鉴其作 为代数模型的基本验证理论与方法，又可以使用其作为抽象程序设计语言的程序分析 方法然而，由于进程演算固有的缺乏数据结构支持的特点，难以建模主体拥有的知 识以及知识推理，以至于只能分析很少的安全性质另一方面，基于知识和信念的逻 辑推理方法可以为协议消息和主体建模，但是缺乏推导主体行为的机制而且，协议 的理想化过程过于依赖分析者的直觉，其困难常常导致分析结论的错误所以，我们 将进程演算和知识推理二者实现优势互补，以进程演算为基础，嵌入消息知识推理系 统，为安全协议建模和分析本文的主要成果和创新如下： 1 本文详细探讨了安全协议形式化分析的各种方法，尤其是基于进程演算的各种分 析手段，并做了两个实例研究。一是在对s p i 演算进行适当扩展的基础上分析了 k e r b e r o s 协议的认证性，二是以a p p l i e d ”一演算为基础分析了i k p 协议的认证性 和匿名性 2 以进程演算为基础，结合协议主体知识的逻辑推理以弥补进程演算固有的缺乏数 据结构支持的特点，建立一个适合于安全协议形式化分析的一般模型g s p m 它 可以精确刻画安全协议，在统一的框架下形式化描述和验证各种安全性质g s p m 中的进程演算部分描述了协议参与主体的演化行为，逻辑部分使用了一系列推理 规则推理主体的知识嵌入的知识推理系统具有可扩展性，可以加入新的推理规 则更深入地分析安全协议此外。g s p m 不为攻击者行为单独建模，既最大化了 攻击者能力。又简化了协议的分析过程 3 以g s p m 为基础分析验证安全性质 ( a ) 基于g s p m ，定义了一步可达关系和多步可达关系两个概念，利用可达关系 概念形式化地描述了安全协议的保密性，并以t m n 协议为例作了实例研究 ( b ) 在给出了g s p m 的l t s 操作语义的基础上，形式化地定义了安全协议的认证 性。并以n s p k 协议为倒作了实例研究 ( c ) 基于g s p m 的变体g s p m ，采用博弈思想形式化地定义了公平交换协议的非 否认性和公平性，并以一种认证邮件机制一m d 机制为例作了实例研究 ( d ) 对其它安全性质的形式化描述进行了讨论 4 在g s p m 的变体g s p m + 的基础上提出了一个环境敏感的抽象互模拟等价关系， 形式化地定义了保密性和认证性，并做了简单的实例分析 5 引入了符号化技术解决g s p m 中等待输入消息时导致的无限分叉问题在等待输 入一个匹配项时，将环境能产生的消息项分成有限类，产生有限个替换，选择某 个替换进行迁移，并把替换记录在迁移过程中，非常技巧性地将迁移过程中可能 产生的无穷分叉变成了有限分叉我们分别在以g s p m 为基础的可达关系，l t s 和博弈语义中引入符号化技术。并以实例分析作了说明符号化技术的采用为我 们正在开发的自动验证工具奠定了基础 关键词：安全协议，形式化方法，安全性质，进程演算符号化技术 f o r m a lr e s e a r c ho f s e c u r i t yp r o t o c o l s b a s e do i lp r o c e s sc a l c u l u s 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 k t e c h n o l o g y , i t sa p p l i c a t i o n sa y es e e p i n gi n t om a n y c r i t i c a lo r g a n i z a t i o n s f u r t h e r m o r e ，e - b u s i n e s si sb e c o m i n gu b i q u i t o u sa f t e ri t se m e r g e n c e t h e s em a k ei n f o r m a t i o ns e c u r i t yi n c r e a s i n g l yi m p o r t a n t b u ta sc o n t r a s t ，s e c u r i t yp r o t o c o l s ， t h eb a s eo fi n f o r m a t i o ns e c u r i t y , a r er e c e i v i n gg r e a tc h a l l e n g e so nt h e i rc o r r e c t n e s sa n dr e l i a b i l i t y i ti sc o m m o nt h a tas e c u r i t yp r o t o c o li sp r o v e dn o tt ob et h a ts e c u r ea si t sd e s i g n e r h a se x p e c t e d e v e nw h e nt h eb u g so ft h ei m p l e m e n t a t i o na n dt h ef a i l u r eo ft h eu n d e r l y i n g c r y p t o g r a p h i cs y s t e ma r en o tc o n s i d e r e d ，t h ec o m p l e x i t yo ft h en e t w o r ke n v i r o n m e n tw i l l a l s om a k ei ta v a i l a b l ef o rt h ei n t r u d e rt or a i s ea t t a c k sb yt a k i n ga d v a n t a g eo fv a r i o u sf l a w s o ft h ep r o t o c o l s s o ，i ti sak e yp r o b l e mw h e t h e ras e c u r i t yp r o t o c o lr e a c h e st h ed e s i g n e d s e c u r i t yc r i t e r i a t h ea n a l y s i sa n dv e r i f i c a t i o no fs e c u r i t yp r o t o c o l sa r ev e r yi m p o r t a n tt e c h n i q u e st o g u a r a n t e et h es e c u r i t yp r o p e r t i e sa n dt h ea p p l i c a t i o nr e q u i r e m e n t sm e t f o r m a lm e t h o d s a n da u t o m a t e dt o o l sa r eb o t hn e c e s s a r ya n de f f i c i e n tf o rt h e s ep u r p o s e s f o r m a l i z a t i o no f s e c u r i t yp r o t o c o l sh a sat w e n t y y e a rh i s t o r y , a n di sg e t t i n gh o t i nt h er e s e a r c ha r e ao f s e c u r i t y p r o t o c o l s i nt h er e c e n td e c a d e ，r e s e a r c h e r st h r o u g h o u tt h ew o r l dh a v em a d eb r o a d a n dd e e p s t u d i e so nt h et o p i c ，e s p e c i a l l yt h o s ef r o mu n i t e ds t a t e sa n de u r o p ew h e r et h eg o v e r n m e n t s h a v ei n v e s t e dal o t o u rc o u n t r ya l s ob e g i n st ot a k es e r i o u s l yt h ed e s i g na n dt h ea n a l y s i s o fs e c u r i t yp r o t o c o l s t h o u g hm a n ys a t i s f a c t o r yr e s u l c sh a v eb e e na c h i e v e di nt h ea r e ao f f o r m a l i z a t i o no fs e c u r i t yp r o t o c o l s ，t h e r er e m a i nm a n yp r o b l e m su r g e n tt ob es o l v e d h o w t od e p i c tt h ep r o t o c o l sp r e c i s e l y ? h o wt oe x p a n dt h ee x i s t i n gm a t u r et h e o r i e sa n dm e t h o d s t os t u d ym o r es e c u r i t yp r o p e r t i e s ? h o wt oa n a l y z ea n dv e r i f ys e c u r i t yp r o p e r t i e so fac e r t a i n s y s t e mi nau n i f i e df r a m e w o r k ? a l lo ft h e s eq u e s t i o n sr e m a i nu n k n o w n a n da r er e a d yt ob e a n s w e r e d s e c u r i t yp r o t o c o l sa r et y p i c a ld i s t r i b u t e dc o n c u r r e n ts y s t e m s ，w h i l ep r o c e s sc a l c u l u si s ap o w e r f u lt o o lt om o d e ld i s t r i b u t e dc o n c u r r e n ts y s t e m s w i t hs o n ga b i l i t yo fd e s c r i p t i o n a n df o r m a ls e m a n t i c s ，p r o c e s sc a l c u l u sc a r lp r e c i s e l yc h a r a c t e r i z et h ei n t e r a c t i o nb e t w e e n d i f f e r e n tp a r t i c i p a n t so fas e c u r i t yp r o t o c 0 1 w h e na p p l y i n gp r o c e s sc a l c u l u s ，w ec a nb e n e f i t f r o mn o to n l yt h eb a s i cv e r i f i c a t i o nt h e o r i e sa n dm e t h o d sf r o mi ta sa na l g e b r am o d e l 。b u t a l s op r o g r a ma n a l y s i sm e t h o d sf r o mi ta sa na b s t r a c tp r o g r a m m i n gl a n g u a g e b u tp r o c e s s i i i c a l c u l u sh a sap o o rs u p p o r tf o rd a t as t r u c t u r e s 。w h i c hl e a d st ou n e a s ym o d e l i n go fm e s s a g e o nt h eo t h e rh a n d ，t h o u g hm o d a ll o g i c sb a s e do nk n o w l e d g ea n db e l i e fc a l le a s i l ym o d e l t h em e s s a g e ss e n ti nt h ep r o t o c o la n dp r i n c i p a l s ，t h e yl a c kam e c h a n i s mf o ri n f e r e n c eo n p r i n c i p a la c t i o n s f u r t h e r m o r e ，t h ep r o c e s so fa b s t r a c t i o no fp r o t o c o ld e p e n d st o om u c ho n t h ei n t e n t i o no ft h ea n a l y z e r , w h i c hm a k e si tf a i lc o n s t a n t l yt og e tc o l t p tr e s u l t s s o ，o u r i n t e n t i o ni st oc o m b i n et o g e t h e rp r o c e s sc a l c u l u sa n dk n o w l e d g ei n f e r e n c e 。m a k i n gu pf o r e a c ho t h e r , t om o d e la n da n a l y z es e c u r i t yp r o t o c o l s t h em a i nr e s u l t sa n di n n o v a t i o n sa r e l i s t e da sf o i l o w s 1 w es t u d i e dt h o r o u g h l yv a r i o u sm e t h o d so ff o r m a l i s mo fs e c u r i t yp r o t o c o l s e s p e c i a l l yt h o s ew h i c hb a s eo np r o c e s sc a l c u l u s a n dw es t u d i e dt w op r a c t i c a lc a s e s f i r s l w e a n a l y z e dt h ea u t h o r i t yo ft h ep r o t o c o lk e r b e r o sb a s e do na ne x t e n s i o no fs p i c a l c u l u s s e c o n d ，w ea n a l y z e dt h ep r o p e r t i e sl i k ea u t h e n t i c t i o na n da n o n y m i t yo ft h ep r o t o c o li k pb a s e d o at h ea p p l i e dp i c a l c u l u s 2 w ee s t a b l i s h e dag e n e r a lm o d e lg s p mf o rf o r m 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 w h i c hi sb a s e do np r o c e s sc a l c u l u sa n di sc o m b i n e dw i t hk n o w l e d g ei n f e r e n c eo fp r i n c i p a l s t om a k eu pf o r t h ep o o rs u p p o r tf o rd a t as t r u c t u r e s b yu s i n gg s p m ，w ec a n p r e c i s e l yd e p i c t t h es e c u r i t yp r o t o c o l sa n dc h a r a c t e r i z ea n dv e r i f yv a r i o u ss e c u r i t yp r o p e r t i e su n d e rau n i f o r m f r a m e w o r k t h e p r o c e s s c a l c u l u s p a r t o f g s p m d e p i c t s t h e e v o l v i n ga c t i o n so f t h e p r i n c i p a l s p a r t i c i p a t e d ，a n dt h el o g i cp a r te n a b l e sk n o w l e d g ei n f e r e n c eb a s e do n as e r i e so fr u l e s t h e e m b e d d e di n f e r e n c es y s t e mc a nb ee x t e n d e db ya d d i n gn e wi n f e r e n c er u l et oa n a l y z et h e p r o t o c o l sm o r ed e e p l y i ng s p m i ti sn ol i e c dt om o d e lt h ei n t r u d e r , w h i c hb e t hm a x i m i z e s t h ea b i l i t yo ft h ei n t r u d e ra n d s i m p l i f i e st h ea n a l y s i sp r o c e s s 3 a n a l y z ea n dv e r i f ys e c u r i t yp r o t o c o l sb a s e do ng s p m ( a ) b a s e do ng s p m ，w ed e f i n e dt w oc o n c e p t ：o n e s t e pr e a c h a h i l i t ya n dm u l t i s t e p r e a c h a b i l i t y , b yu s i n gw h i c hw ef o r m a l i z e dt h ep r o p e r t yo fs e c r e c y a n dw es t u d i e dt h e t m n p r o t o c o la sa ne x a m p l e ( b ) w ep r o p o s e dt h el a b e l e dt r a n s i t i o ns y s t e ma st h es e m a n t i c sf o rg s p m ，a n df o r - m a l i z e dt h ep r o p e r t yo fa u t h e n t i c t i o n a n dw es t u d i e dt h en e e d h a m - s c h r o c d e r p u b l i c k e y p r o t o c o la sa ne x a m p l e ( c ) w ep r o p o s e dg s p m + 船av a r i a n to fg s p m 。i nw h i c hw ef o r m a l i z e dt h ep r o p e r t i e s o fn o n - r e p u d i a t i o na n df a i r n e s sf o rf a i re x c h a n g ep r o t o c o lb yu s i n gt h ei d e ao fg a m e a n d w es t u d i e dnc e r t i f i e de - m a i lm e c h a n i s m m dm e c h a n i s ma sa ne x a m p l e ( d ) w ed i s c u s s e dt h ef o r m a l i s mo fo t h e rs e c u r i t yp r o p e r t i e so fs e c u r i t yp r o t o c o l s 4 w ep r o p o s e dab i s i m u l a t i o nr e l a t i o ni no r e v a d a n tg s p m + a n dt h ed e f i n i t i o n so f s e c r e c ya n da u t h e n t i c t i o n a n das i m p l ec a s ew a ss t u d i e d 毒 事 ； 5 t os o l v et h ep r o b l e mo fi n f i n i t eb r a n c h i n gi ng s p mt r a n s i t i o ng r a p h ，w ea d o p 【e d t h es y m b o l i ct e c h n i q u e w h e nw a i t i n gf o ra l li n p u tp a t t e r n 。p n n c i p a l sc h a r a c t e r i z et h er u e s s a g e sw h i c hc o u l d b eg e n e r a t e db yt h ee n v i r o n m e n ti n t of i n i t eg r o u p sc o r r e s p o n d i n gt of i n i t e s u b s t i t u t i o n ，b yc h o o s i n ga s u b s t i t u t i o nt op r o c e e da n dr e c o r d i n gt h es u b s t i t u t i o ni nt h et r a n s i t i o n s ，t h ei n f i n i t eb r a n c h i n gp r o b l e mw a ss o l v e d t h es y m b o l i ct e c h n i q u e i sa d o p t e di n t o t h er e a c h a b l er e l a t i o n sb a s e do ng s p m ，t h el a b e l e dt r a n s i t i o ns y s t e ma n dt h eg a m em o d e l i tw a sd e m o n s t r a t e db yp r a c t i c a le a s es t u d y s y m b o l i ct e c h n i q u eh a sb e e nt h eb a s eo fo u r v e r i f i c a t i o nt 0 0 1u n d e rd e v e l o p m e n t 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 ，s e c u r i t yp r o p e r t y ，p r o c e s sc a l c u l u s ，s y m b o l i ct e c h n o l o g y v 上海交通大学 学位论文原创性声明 本人郑重声明：所呈交的学位论文，是本人在导师的指导下， 独立进行研究工作所取得的成果。除文中已经注明引用的内容外 本论文不包含任何其他个人或集体已经发表或撰写过的作品成果。 对本文的研究做出重要贡献的个人和集体，均己在文中以明确方式 标明。本人完全意识到本声明的法律结果由本人承担。 学位论文作者签名：弘辱红 日期：妒年3 月t ，e l 上海交通大学 学位论文版权使用授权书 本学位论文作者完全了解学校有关保留、使用学位论文的规定， 同意学校保留并向国家有关部门或机构送交论文的复印件和电子 版，允许论文被查阅和借阅。本人授权上海交通大学可以将本学位 、论文的全部或部分内容编入有关数据库进行检索，可以采用影印、 缩印或扫描等复制手段保存和汇编本学位论文。 保密口，在一年解密后适用本授权书。 本学位论文属于 不保密口。 ( 请在以上方框内打“4 ”) 学位论文作者签名：7 殳禾肛指导教师签名：学多彦 日期：矿羁年3 月口日日期：夕年月o 日 1 1 引言 第一章绪论 随着网络技术应用与发展逐步渗透到许多关键部门，特别是政府，军事机构等， 以及电子商务的兴起与广泛应用，信息安全已变得日益重要 安全协议是信息安全的基础在个分布式的互联网网络环境中，人们只有通过安 全协议来具体实现安全共享网络资源的需求协议本身的正确性和安全性至关重要， 直接关系到整个系统的安全 ， 但是，实际上安全协议的正确性和安全性却不容乐观，已有的安全协议往往被证 实并不如设计所期望的那样安全，网络系统面临着各种攻击手段的威胁即使不考虑。 与实现相关的协议缺陷和密码系统被成功破译的可能性复杂的网络环境还是使得攻 击者可利用安全协议自身的缺陷来实施各种各样的攻击1 1 2 1 目前已经发表甚至已投 入使用的不少安全协议在发表甚至实用几年或几十年后却被发现是有漏洞的，最著名 的是n s p k ( n c e d h a m s c h r o c d e rp u b l i ck e y ) 协议在发表使用十六年后被发现存在中 间人攻击的问题 3 1 因此，安全协议是否能达到它所要求的安全目标是一个非常关 键的问题 安全协议的设计极易出错，即使参加协议的主体只有两三个，交换的消息只有三 五条，设计一个正确的、符合安全目标的协议也十分困难安全协议设计与分析的困 难在于【4 l ； 安全协议所要确保的各种安全性质本身是十分微妙的例如，1 1 9 使表面上十分简 单的“认证性”，实际上也十分微妙关于认证性的定义，至今存在各种不同的观 点； 安全协议的运行不是独立的，协议运行在复杂的、充满恶意的环境中，攻击者处 处存在如何完整而精确地刻画安全协议的运行环境是一项艰巨的任务； 攻击者采用的手段是多种多样的。我们不可能完全获知攻击者的能力，但我们希 望在最大限度上对这些能力进行模拟如何描述攻击者的能力，对攻击者和攻击 行为进行分类和分析也是一项艰巨的任务； 安全协议本身具有高度并发的特点，使得安全协议的分析变得更加具有挑战性 对安全协议的分析和验证是保证所设计的协议满足其安全性的重要技术手段目 前，对安全协议进行分析和验证的手段主要有两大类：类是攻击检验方法，另类 是形式化分析方法所谓攻击检验方法就是搜集目前能对协议造成有效攻击的方法， 逐一对安全协议进行攻击，检验安全协议是否具有抵抗这些攻击的能力在分析的过 2 上海变通大学博士论文 程中主要使用自然语言和示意图，对安全协议所交换的消息进行剖析如果发现有效 的攻击，那么说明协议是不安全的实际上，由于安全协议的复杂性，构造对安全协议 的攻击是十分困难的，这一过程很难进行，很难有效地对安全协议进行分析验证而 形式化分析方法则首先对安全协议进行形式化建模，然后借助人工推导或自动分析， 判断安全协议的形式模型是否满足所要求的安全性质形式化分析方法能够全面，深 刻地检测到安全协议中细微的漏洞，有助于发现对安全协议的新的攻击方法，从而便 于对协议进行改进和完善，进而可以得到安全协议设计的一般性准则 安全协议的形式化研究已成为安全协议研究的热点近十几年来。世界各国学者 对其进行了广泛和深入的研究，尤其是美国和欧洲的一些国家在这一关键领域投入了 大量的研究经费和力量【5 1 同时，安全协议的设计和分析也引起了国内研究人员的 高度重视 6 - 9 1 实践证明，借助形式化的分析方法或工具分析安全协议是一种非常必 要而且行之有效的方法 1 2 安全f ，办议 1 2 1 密码学基础 密码学是安全晰议的基础，研究的是对消息的加密和解密 根据密码算法所使用的加密密钥和解密密钥是否相同，可将密码算法分为对称密 码算法和公钥密码算法( 也称非对称密码算法) 另外，密码学中还较多地使用哈希 ( h a s h ) 函数作为辅助的加密算法关于对称密码算法的密码体制称为对称密码体 制，而关于公钥密码算法的密码体制就称为公钥密码体制( 也称非对称密码体制) 如果一个密码算法的加密密钥和解密密钥相同，该算法就是对称密码算法对称 密码的特点是速度快，安全强度高，主要用作数据加密例如。a l i c e 和b o b 共享一个 秘密值k ，其它任何人都不知道k 如果a l i c e 要与b o b 进行秘密通信，a l i c e 可以 把k 作为密钥，用对称加密算法加密她的消息m ，产生的密文我们用( m ) 表示 如果假设密码算法是完善”的，攻击者就不可能知道消息m 由于一般采用概率加 密的方式。所以也不可能通过比较密文而知道一些关于明文的消息另外，攻击者在 不知道和m 时，也不可能构造 m ) 。它只能从网上截获 m ) 。而在另一个时 刻重放这个消息 如果一个密码算法的加密密钥和解密密钥不同，则该算法就是公钥密码算法 使用公钥密码体制的每一个用户都拥有基于特定公钥算法的一个密钥对( p u b k e y ， p r v k e y ) 。公钥p u b k e y 公开，任何人都可以访问，私钥p r v k e y 为所有者保管并严 格保密公钥密码算法主要用于分发密钥和数字签名例如，a l i c e 拥有一个密钥对 ( p u b a ，p 彻a ) ，任何人可以用a l i c e 的公钥p u b a 加密消息m ，产生密文( m 】p 。h ， r； i g , - 章缝建 一 3 但只有a l i c e 拥有自己的私钥p r y 可以解密 m ) h 6 。数字签名是签名者利用自己 的私钥加密要签名的消息，别人可以用签名者的公钥角军密从而验证这个签名数字签 名往往与单向加密的哈希函数联合使用单向的哈希函数是从明文到密文的不可逆函 数，也就是说，只能加密不能还原 保密数据认证和非否认可以通过基本的密码学操作如加密、哈希和数字签名来 实现但是，当这些操作被用于实现安全网络通信时，需要密钥交换、公钥分配等协 议来辅助本文涉及的密码学知识可参见文献【1 0 】 1 2 2 协议 在理解安全协议这一概念之前，首先要了解什么是协议所谓协议就是两个或 两个以上的参与者采取一系列步骤以完成某项特定的任务这个定义包含三层意思； 第一，协议至少需要两个参与者单独的一个人可以通过执行一系列的步骤完成 一项任务。但它不构成协议； f 第二，在参与者之间呈现为消息处理和消息交换交替进行的一系列步骤，“一系 列步骤”意味着协议是从开始到结束的一个序列，每一步必须依次执行； 第三，设计协议的目的是要完成一项任务，因此，通过执行协议必须能够达到这 个目的 密码算法应用于协议中的消息处理，对消息的不同处理方式则要求不同的密码算 法，而对算法的具体化则可定义出不同的协议类型因此，简单地说，安全协议就是 在消息处理环节采用了若干的密码算法的协议由此可见，密码算法和安金协议处于 ” 网络安全体系的不同层次，是网络数据安全的两个主要内容具体而言，密码算法为 网络上传递的消息提供加解密操作和其它辅助算法( 如哈希函数等) ，而安全协议是在 这些密码算法的基础上为各种网络安全性方面的需求提供其实现方案 安全协议可定义为；建立在密码体制基础上的需要达到某些安全性要求的通信协 议，也称密码协议它运行在计算机通信网或分布式系统中，为安全需求的各方提供 一系列步骤，借助于密码算法来达到密钥分配身份认证信息保密以及安全地完成 t 电子交易等目的协议的参与者可能是可以信任的人，也可能是攻击者和完全不信任 的人 在网络通信中最常用的、最基本的安全协议按照其目的可以分成以下四类， 1 密钥交换协议 这类协议用于完成会话密钥的建立一般情况下是在参与协议的两个或者多 个实体之间建立共享的秘密。通常用于建立在一次通信中所使用的会话密钥协 议可以采用对称密码体制，也可以采用非对称密码体制 2 认证协议 4 圭謦窒望查兰堡圭堡塞 认证协议包括实体认证( 身份认证) 协议，消息认证协议和数据目的认证协 议等，甩来防止假冒、篡改、否认等攻击 3 认证和密钥交换协议 这类协议将认证协议和密钥交换协议结合在一起，先对通信实体的身份进行 认证，在成功认证的基础上，为下一步的安全通信分配所使用的会话密钥，它是 网络通信中应用最普遍的一类安全协议 4 电子商务协议 电子商务协议是保证客户和商家之间完成正常，可靠、安全交易活动的规则 与上述协议最为不同的是，电子商务协议中主体往往代表交易的双方，其利益目 标是不一致的，或者根本就是矛盾的电子商务协议不仅要考虑基本的安全性( 如 保密性、认证性，完整性等) ，更要关注其特有的性质( 如交易的可追究性、公平 性货币和商品的匿名性等) 1 2 3 安全性质 不同的安全协议对安全性的要求也是不同的，有时甚至是矛盾的一般地，在设 计安全协议时需要考虑以下一些安全性要求： 保密性；保密性足最经典的安全性质。传统上人们总是把保密性和安全性混淆成 一个概念保密性是指信息存取和信息在传输过程中不能被非法窃取，尤其在涉 及到商业机密以及有关支付等敏感信息时，信息的保密性就显得特别重要 认证性：要使网上交易成功，参与交易的人首先要确认对方的身份，确定对方的 真实身份与对方所称的身份是否一致在电子商务中，方便可靠地确认对方身份 是实现电子交易的一个前提认证性可以分为数据认证和主体认证所谓数据认 证是指数据确实是从所期望的那儿给出的，而主体认证是指当前通信的对方身份 的确认 完整性：要求数据在传输过程或存储过程中，不会受到非法的生成修改和删除， 同时要防止数据传送过程中信息的丢失和重复，并保证信息传送次序的统一 非否认性：在交易信息的传输过程中为参与交易的个人、企业或服务部门提供可 靠的标志，以防止任何一方出现的对自己以前的行为做出抵赖即，要求接收方 能向第三方证明发送方对发出的信息不可抵赖，同时发送方能向第三方证明接收 方对收到的信息无法否认 公平性；即协议应保证交易双方在任何时候得到的利益是公平的例如，考虑商 业合作伙伴在网络上签订合同，一个基本的问题是谁先签任何一方先签可能导 致另一方不签而产生不公平 匿名性。匿名性就是保护客户在商业交易中的一些隐私信息如客户身份购物 第一章结论 5 习惯、购物品种和数量等匿名性虽然是一种商业交易中的需求，但也有其负面 影响一种可行的折中办法屉通过可信任的采购代理来购物，客户的身份等私有 信息保存在代理处，追踪也仅仅到代理为止 1 2 4 安全协议的攻击 由于安全协议自身设计、规范以及说明等诸多的缺陷，使得攻击者有机可乘攻 击者的攻击可分为被动窃听和主动攻击，其中主动攻击的危害更大被动窃听就是非 法搭线窃听，截取通信内容后进行密码分析，还可以用来监视网络通信的信号流，井 确定通信双方的身份而主动攻击就是攻击者非法修改信息系统中交换的消息，可以 通过破译密码来达到目的，也可以在不窃取和篡改信息的同时危及系统的安全性消 息重放攻击是最为基本的而且是常见的攻击，很多其它攻击都是基于此类攻击而加以 实施的 消息重放攻击主要是指攻击者利用其消息再生能力生成诚实用户所期望的消息格 式并重放，从而达到破坏协议安全性质的目的由于消息是协议的主要组成部分，协 议主体的身份认证消息的秘密性都是通过消息的正确传递加以实现的，因此根据攻 击目的对消息进行任意的组合并重放，是攻击者对安全协议实施各种具体攻击往往要 用到的手法 消息重放攻击足最基本，最常用，危害性最大的攻击，s y v e r s o n 根据消息的来源 和去向对消息重放攻击进行了完整的分类l 。其中，根据消息的来源把重放攻击分为 本协议的轮内攻击和本协议的轮外攻击前者是指对一个协议轮内的消息进行重放， 后者是指对一个协议的不同轮次的消息进行重放对于协议的轮外攻击，根据协议的 不同轮次的执行时间是否重叠，又可以分为交叉攻击和典型重放攻击前者不同轮次 的协议执行时间是有重叠的，而后者则没有重叠另一方面，根据消息的去向将重放 攻击分为直接攻击和偏转攻击，前者是指消息的确发给了意定的接收方，但是被延迟 了；后者则是指改变了消息的去向，使消息为非意定的主体接收，这种情况又可区分 为两种，一种是将消息返还给了发送方，称为反射攻击，另一种是将消息发给了协议 合法通信双方之外的任一方，称为第三方攻击在消息重放攻击的基础上还可以实施 多重会话攻击等其它攻击 1 3 安全协议形式化分析 1 3 1 形式化方法 形式化方法是一种以数学为基础的技术，使得在系统设计和实施的不同步骤中达 6上海交通大学博士论文 到可证明的正确性和可靠性，从而给系统开发以一个坚实的基础一般认为形式化方 法是始于2 0 世纪6 0 年代末，当时由于“软件危机 ，人们试图用数学证明程序的正确 性而发展成为各种程序验证方法一直以来，形式化方法成为人们解决软件不可靠的 最大希望 形式化方法的意义在于它能帮助发现其它方法不容易发现的系统描述的不一致， 不明确或不完整，有助于增加软件开发人员对系统的理解，因此形式化方法是提高软 件系统。特别是关键安全性( s a f e t y - c r i t i c a l ) 系统的安全性与可靠性的重要手段 形式化分析一般可以分成三个步骤。 1 ，建模：形式化分析第一步就是为要验证的系统建立一个数学模型，用精确可靠的 方式将要验证的系统抽象成数学模型来表达，从而去掉不重要的细节，便于简单 有效地推理 2 规范：第二步就是利用建立的数学模型将系统所要求的性质形式化地规范表述， 便于形式化地推导和验证 3 验证：在建立的数学模型中推理说明系统的性质足否满足衄好推理过程可以自 动化 形式化方法在协议开发中的应用研究也足始于6 0 年代末人们首先开展丁协议 的各种形式化模型的研究工作，如；p e t r i 网 1 2 1 有限状态机形式语言等在此基础 上。建立了协议的标准形式描述语言，如：e s t e l l e 1 3 1 ，s d l 【3 h 1 ，l o t o sm 1 5 i 等目前，随着形式化技术的日趋完善，网络协议的开发已逐步从非形式化描述手工 方法实现过渡到以形式化描述技术为基础，渗透到网络协议分析，综合，测试等备环 节的软件工程方法同时，已开发出支持协议开发活动中形式化描述、正确性验证 性能分析、自动代码生成和一致性测试等各方面的许多软件工具， 形式化方法应用在电路设计和协议设计上都取得了很大的成绩研究怎样在安全 协议的设计和分析中使用形式化方法，以提高安全协议的可靠性是安全协议的研究 热点 1 3 2 安全协议形式化分析的历