（计算机软件与理论专业论文）两种安全协议形式化理论的研究.pdf

坐壅查兰堡主兰笙丝圣!， 两种安全协议形式化理论的研究 赵华伟 ( 山东大学网络信息安全研究所，济南，2 5 0 1 0 0 ) 摘要 在本文中，我们探讨了有关两种安全协议形式化理论的若干问题，其中，工 作重点集中在对三方认证密钥交换协议的形式化分析上。 网络技术具有快速实现信息共享的特点，这大大提高了人们通信的效率，给 人们的生活、学习和工作带来了巨大的改观。但与此同时，人们对网络本身具有 的公开性和匿名性所带来的日益严重的信息安全问题也深感不安。 为了解决网络的信息安全问题，人们设计了许多用于开放网络的安全协议来 解决各种安全应用问题。所谓安全协议，就是两个或两个以上的参与者采取一系 列步骤来完成某项特定的安全任务。它包含三层含义：1 协议需要至少两个参 与者。2 参与者之间执行的是消息处理和消息交换交替进行的一系列步骤。3 通 过协议执行必须能够完成某种安全任务。 由于每个安全协议都是为了某种安全应用而精心设计的，协议中的各条消息 问有着微妙的相互制约关系，因此若采用人工方式对协议进行安全性分析。往往 不能发现协议存在的问题，所以必须借助于形式化的方法来完成。形式化方法是 一种用于描述系统性质的数学方法，它主要用于发现一个系统中的歧义性，不一 致性与不完备性。该系统可以大到一个企业级的软硬件系统，也可以小到有若干 条消息组成的协议。对安全协议使用形式化的方法可挖掘出协议消息所表示的 内在含义，对协议的正确性进行验证通过验证，不仅可证明协议是否符合预期 的安全目标，而且对不符合安全目标的协议可分析其缺陷之所在，进而为协议的 设计提供有力的支持。 目前在安全协议形式化的研究领域有两种截然不同的理论：符号理论与计算 理论： 山东大学博士学位论文 在符号理论的形式化中，协议各要素被抽象为赋予了特定含义的符号，然后 通过对这些符号的形式化分析来考察协议的安全性。虽然符号理论为协议的验证 工作提供了强大的证明手段，但是这些证明手段都是在一定的假设下进行的，比 如均假设协议所采用的算法是理想化的，敌手在进行密码分析时得不到任何有用 的信息由于这些假设不仅高估了一些常见算法的强度，同时低估了敌手的攻击 能力，因此符号理论不具有计算可靠性。 在计算理论中，协议各要素被看成位串，协议所采用的算法由函数表示。其 安全性的证明通常是通过构造一个“矛盾归约”的证明得到，这里的矛盾指的是 计算复杂性领域中人们普遍相信的困难问题出现了一个有效解。计算理论通过分 析敌手的攻击能力来考察协议的安全性，更具有实际意义。但是计算理论下的分 析方法难以考察协议各要素的完备性，因此不适于分析协议的逻辑正确性。 在本文中，我们主要以认证密钥交换协议为载体，深入考察了符号理论与计 算理论各自的优缺点，然后提出了若干有关安全协议形式化的新思路，主要的工 作有以下几个方面： 第一，提出了c s 逻辑及其改进方案的不足之处，对c s 逻辑重新进行了扩 展。c s 逻辑在公理方面存在一些不足，比如违背了公钥的公开性原则，知识与 信念的转化是通过非形式化的手段得到的等等，而已有改进方案中有关时间单调 性与消息新鲜性的公理不能正确反映现实。我们通过对逻辑公理的改进与扩展实 现了：1 更准确地描述了有关知识和信念与时间有关的单调性概念。2 对发送 和接收有关密文的知识和信念进行了描述，优化了原有的推理过程。3 改进后的 推理公理描述了知识与信念之间的转化关系，更客观地反映了人类的认知能力。 4 可分析协议要素在一定时间段内的安全需求，为深入了解协议消息的性质以 及设计更优质的安全协议提供了强有力的帮助。 第二，针对b a n 类逻辑的不足，构造了一个新的形式化分析工具m b l 逻 辑。该逻辑的特点在于：1 克服了b a n 类逻辑缺乏有效证明机制的不足，具有 严格的证明体系，可证明在给出的语义模型下推理规则的正确性，说明了逻辑系 统的合理性2 对协议进行简单的处理便可进行安全性分析，不需进行理想化 处理，降低了分析者分析协议的难度。3 可分析协议消息的保密性，使得主体 不必过分依靠可信中心，主要根据自己的判断来确定秘密是与哪个主体共享的， 从而能弥补b a n 类逻辑不能发现由于敌手欺骗可信中心所造成攻击的不足。此 j 山东大学博士掌位论文 外，我们基于m b l 逻辑并采用p r o l o g 语言实现了一个协议的自动化分析工具， 可以大大提高分析协议安全性的效率。 第三，发现了敌手针对认证密钥交换协议的一种新型攻击：敌手利用针对协 议的某种看似“无用”的攻击过程，能够完成另一种严重的攻击，即敌手能够延 续对协议的攻击效果从而实现另一种攻击。由于目前所普遍使用的d o l c v - y a o 敌 手模型无法具体涵盖该类型的攻击，所以我们对d o l e v y a o 敌手模型进行了补充。 第四，分析了设计认证密钥交换协议所需注意的事项，指出设计安全的协议 不仅要保证具备必要的协议要素，还要保证采用正确的密码算法，由此引出了在 计算方法下讨论协议安全性的初衷。然后通过两个攻击游戏模型化了敌手攻击认 证协议的行为，进而通过主体在游戏中的成功概率给出了敌手在实施有关密码分 析的攻击时认证密钥交换协议认证性的定义。该定义充分考虑了敌手实施主动攻 击时协议的安全性，具有实际意义。 第五，结合符号理论中的模态逻辑法与计算理论下的矛盾归约法，提出了一 种安全协议的调和分析法。该方法与符号理论下的方法相比，克服了它们总假设 密码体制是完善的，并且仅考虑敌手的被动攻击的不足，可有效地分析在面对敌 手实施有关密码分析的主动攻击时协议的安全性；与计算理论下的方法相比，该 方法能考察协议各要素的完备性，能有效发现协议在面对重放攻击、平行穿插攻 击等非密码分析的攻击时是否存在漏洞。最后我们给出了采用该方法分析协议的 一个实例。 下一步的工作包括：建立一种设计安全协议的逻辑方法，然后利用p r o l o g 语言建立该逻辑方法的自动化方案，并实现由协议目标来自动定位协议的缺陷； 研究在各种攻击模型下对称钥体制的安全性，以便提出更好的用于安全协议的对 称钥加密方案，以及更全面地分析加密方案的安全性。 关键词：安全协议，符号理论，计算理论，保密性，自动化分析 r e s e a r c ho nt w of o r m a lt h e o r i e so fs e c u r i t yp r o t o c o l s z h a oh h a w e i ( i n s t i t u t eo f n e t w o r ki n f o r m a t i o n & s e c u r i t y , s h a n d o n gu n i v e r s i t y , j i n a n , 2 5 0 1 0 0 ) a b s t r a c t i nt h i sd i s s e r t a t i o n , w ed i s c u s s8 0 m ep r o b l e m sr e l a t e dt ot h et w ot h e o r i e so ft h e f o r m a lm e t h o d si n t h ef i e l do fs e c u r i t yp r o t o c o l s ，a n do u rw o r ki sm a i n l yo nt h e f o r m a la n a l y s i sa b o u tt h r e e - p a r ta u t h e n t i c a t e dk e y - e x c h a n g ep r o t o c o l s w i t ht h ea d v a n c eo ft h ei n t e r a c t ，t h ee f f i c i e n c yo fc o m m u n i c a t i o n si sg r e a t l y i m p r o v e d w h i c hb u l k i l yc h a n g 鼯a p p e a r a n c e so f p e o p l e sm e t h o d so f l i v i n g ，s t u d y i n g , a n dw o r k i n g b u ta tt h es a m et i m e ，t h ep r o b l e mo fi n f o r m a t i o ns e c u r i t yc a u s e db y a n o n y m i t y a n dp u b l i c i t yo f i n t r e n e ta r i s e sp p l e sm i s g i v i n g s i no r d e rt os o l v et h ep r o b l e mo fi n f o r m a t i o ns e c u r i t y , p e o p l ea l 删yd e s i g n e da l o to fs e c u r i t yp r o t o c o l sf o rs e c u r ea p p l i c a t i o n s s e c u r i t yp r o t o c o la r ep r o c e s sh a v i n g t w oo ra b o v ep a r t i c i p a n t st oc o m p l e t eak i n do fs e c u r i t yt a s k i th a st h r e ep o i n t s ： f i r s t l y , p r o t o c o l sh a v et w op a r t i c i p a n t sa tl e a s t s e c o n d l y , p a r t i c i p a n t sm u s td e a lw i t h m e s s a g e sa n de x c h a n g em e s s a g e sb yt u r n s t h i r d l y , p r o t o c o l sm u s ta c h i e v es o m ek i n d o f s e c u r i t y t a s k e l a b o r a t e l yd e s i g n e dm e s s a g e so fp r o t o c o lh a v ed e l i c a t ei n t e r a c t i v er e l a t i o n s h i p ， s oi fw ea n a l y z ep r o t o c o l su s i n gn o n - f o r m a lm e t h o d s ，d e f e c t sa r eh a r d l yt ob ef o u n d c o m m o n l y i no r d e rt os o l v et h ep r o b l e m , w en e e dt or e c u rt ot h em e t h o do ff o r m a l a n a l y s i s f o r m a la n a l y s i si sam a t h e m a t i cm e t h o du s e dt od e s c r i b es y s t e mp r o p e r t i e s a n di t sp u r p o s ei st of i n da m b i g u i t y , c o n g r u i t y , a n di m p e r f e c t i o no fas y s t e m t h e s y s t e mm a yb es ob i ga sae n t e r p r i s es y s t e mi n c l u d i n gs o f t w a r ea n dh a r d w a r e ，o r s o s m a l la sp r o t o c o l si n c l u d i n gs o m em e s s a g e s t h r o u g hf o r m a la n a l y s i sm e t h o d s ，w e c a nd i s c l o s em e s s a g e s i n h e r e n tm e a n i n g s ，a n dv c r i f yp r o t o c o l s r i g h t n e s s i fa p r o t o c o li s n ts e c u r e f o r m a la n a l y s i sm e t h o dc 粕f i n dt h er e a s o na n da d v a n c et h e o p i n i o na b o u tm e n d i n gt h ep r o t o c 0 1 ： j ； 寸 ： ； l *lj，$ ， 山东大学博士学位论文 n o w , t h e r ea r et w od i f f e r e n tt h e o r i e si nt h ef i e l d so fs e c u r i t yp r o t o c o l s f o r m a l a n a l y s i s ：s y m b o lt h e o r ya n dc o m p u t a t i o n a lt h e o r y ： i nt h es y m b o lt h e o r y , a l lk i n d so f m e t h o d sl o o ke a c hp r o t o c o lm e s s a g ea ss y m b o l h a v i n gs p e c i a lm e a n i n g , a n da n a l y z et h e s es y m b o l st o 、惯毋p r o t o c o l s s e c u r i t y s y m b o lt h e o r yc a ns u p p o r tp o w e r f u la p p r o a c h e sf o rp r o t o c o l s v e r i f i c a t i o n ，t h o u g h t h e s ea p p r o a c h e sn e e ds o m ea s s u m p t i o n s f o re x a m p l e ：a l lc r y p t o g r a p h i e sa r e s u p p o s e dp e r f e c t ，a n da d v e r s a r yc a n n o ta c h i e v ea n yu s e f u li n f o r m a t i o ni nt h ep e r i o d o fc r y p t o g r a p h i ca n a l y s i s b u tt h ea s s u m p t i o nd o e s n tc o r r e s p o n dt oa c t u a ln e e d s , b e c a u s ei to v e r r a t e st h ec r y p t o g r a p h y ss e c u r i t y , a n du n d e r e s t i m a t e sa d v e r s a r y s a b i l i t y i nt h ec o m p u t a t i o n a lt h e o r y , m e s s a g ei na p r o t o c o li ss t r i n g so f b i t ，a l le n c r y p t i o n f u n c t i o ni sj u s ta na l g o r i t h m ，a n da l la d v e r s a r yi se s s e n t i a l l yat u r i n gm a c h i n e g o o d p r o t o c o l sa l et h o s ei nw h i c ha d v e r s a r i e sc a n n o td o s o m e t h i n gb a d t o oo f t e na n d e f f i c i e n t l ye n o u g h u s u a l l yas e c u r i t yp r o o fi sr e l a t e dt oai n d u c t i o n , t h a ti s ：i fa l l a d v e r s a r yc o u l ds u c c e s s f u l l ya t t a c kap r o t o c o le a s i l y , h e nh ec o u l ds u c c e s s f u l l ys o l v e ah a r dp r o b l e me a s i l y , b u ti nf a c tt h ep r o b l e mc o u l d n tb es o l v e d ，t h e nt h r o u g ht h e c o n t r a d i c t i o n , w ec a nb e l i e v et h ep r o t o c o li ss 。c u m c o m p u t a t i o n a lt h e o r yi sd i f f i c u l t t oc h e c kw h e t h e rap r o t o c o lh a sn e c e s s a r ym e s s a g e s ，a n dd o e s n ta d a p tt oa n a l y z e p r o t o c o l s l o g i s t i cr i g h t n e s s i nt h i sd i s s e r t a t i o n , t h r o u g ha n a l y z i n ga u t h e n t i c a t e dk e y - e x c h a n g ep r o t o c o l s ，w e s t u d yt h ef l a w sa n dv i r t i i e so f s y m b o lm e t h o da n dc o m p u t a t i o n a lm e t h o d , a n dp u r p o s e s o m en 州i d e a sa b o u ts e c u r i t yp r o t o c o l s f o r m a lm e t h o d s o u rp r i m a r yw o r k i n c l u d e s ： f i r s t l y , w ef i n df l a w so fb o t hc sl o g i ca n di t si m p r o v e ds c h e m e s ，a n di m p r o v e t h el o g i ca g a i n c sl o g i ch a ss o m el i m i t a t i o n s i ni t sa x i o m s s u c ha sv i o l a t i n g p u b l i c - k e y se x o t e r i cc h a r a c t e r , l a c k i n gf o r m a lm e t h o d st ot r a n s f o r mb e t w e e nb e l i e f a n dk n o w l e d g e i na d d i t i o n , i ni t s i m p r o v e ds c h e m e ，s o m ea x i o m sa b o u tt i m e m o n o t o n ya n df r e s h n e s sa r ew r o n g i nt h ep a p e r , w ei m p r o v ec sl o g i ca g a i n , a n d a c h i e v et h ef o l l o w i n gg o a l s ：1 ，t od e p i c tt i m em o n o t o n yc o n c e p t i o no fb e l i e fa n d k n o w l e d g em o r ea c c u r a t e l y 2 ，t od e p i c tk n o w l e d g ea n db e l i e fa b o u ts e n d i n ga n d 山东大学博- a 学位论文 r e c e i v i n gm e s s a g e s ，a n do p t i m i z e f o r m e ri n f e r e n c e p r o c e s s 3 ，t od 印i c t t h e r e l a t i o n s h i pb e t w e e nk n o w l e d g ea n db e l i e fi nt h em o d i f i e di n f e r e n c ea x i o m s , w h i c h i m a g e sh u m a nc o g n i t i v ep o w e r so b j e c t i v e l y 4 , t o b ea b l et op o 硫o u tm e s s a g e s 8 e c l l r er e q u i r o m e n ti nap e r i o do ft i m e ，a n dh e l pt ou n d e r s t a n dm e s s a g e s p r o p e r t i e s a n dt od 鼯i g ns e c u r i t yp r o t o c o l sb e t t e r s e c o n d l y , f a c i n gt h ef l a w so f b a n l i k ei o g i c s s s w eb u i l dan e w f o r m a la n a l y t i c t o o l s - m b ll o g i c ，t h el o g i ch a st h ef o l l o w i n gc h a r a c t e r s ：1 , m b ll o g i ch a ss t r i c tp r o o f s y s t e m , a n dc a np r o v et h er i g h t n e s so fi n f e r e n c er u l e s , o nt h ec o n t r a r yb a n l i k e l o g i c s s sl a c k se f f e c t i v ep r o o fm e c h a n i s m 2 ，t h el o 画cd o e s n t n e e di d e a l i z a t i o n p r o c e s s + 8 0c a nd e p r e s st h ed i f f i c u l t yo fa n a l y z i n gp r o t o c o l s 3 ，t h el o g i cc a l la n a l y z e t h es e c r e c yo f p r o t o c o l s m e s s a g e s ，w h i c hc o u l dh e l pa n a l y z e r j u d g ew h oi ss h a r i n ga s e c r e tw i t hh i mb yh i m s e l f , a n dr e d u c et h ed e p e n d e n c eo nt r u s t e dc e n t e r m o r e o v e r , b a s e do nm b ll o g i ca n du s i n gp r o l o gl a n g u a g e ，w er e a l i z ea na u t o m a t i ca n a l y z i n g t o o l sf o rp r o t o c o l s ，w h i c hc o u l di m p r o v ee f f i c i e n c yo f a n a l y z i n gp r o t o c o l s t h i r d l y , i nt h ep r o c e s so fb u i l d i n gm b ll o g i c ，w ef i n dan e wa t t a c ka b i l i t yo f a d v e r s a r yt oa u t h e n t i c a t i o nk e y - e x c h a n g ep r o t o c o l s ：h ec o u l du s ea n u s e l e s s a t t a c k t oa c t u a l i z ear e d o u b t a b l ea t t a c k , t h a ti sa d v e r s a r yf i r s t l yc a l t yo u ta na t t a c kw h i c hi s b e l i e v e dh a m l l c s sf i r s t l y , b u th ec o u l dc o n t i m mt h ea t t a c ke f f e c tt or e a l i z ea n o t h e r a t t a c kw h i c hc o u l dc a u s es e v e r eb a r r e lt h r o u g hs t u d y i n gt h ea d v e r s a r ya b i l i t y , w ef i n d t h ed o l e v - y a oa d v e r s a r ym o d e lc o u l d n td e p i c tt h i sa b i l i t y , s ow ea d dt h en e w a b i l i t yo nt h eh ed o l e v o y a oa d v e r s a r ym o d e l f o u r t h l y , w ea n a l y z eh o wt od e s i g na $ e c u l 他a u t h e n t i c a t e dk e y - e x c h a n g e p r o t o c o l s ，a n dp o i n to u tas e c l l r ep r o t o c o ln o to n l yr e l yo nn e c e s s a r ym e s s a g e s ，b u t a l s or e l yo ns o u n dc r y p t o g r a p h y , w h i c hg i v e st h ei n i t i a li d e a so fd i s c u s s i n gt h e s e c u r i t yu n d e rc o m p u t a t i o nt h e o r y t h e nw eb u i l dt w og a m e st om o d e la d v e r s a r y s a b i l i t yt oa t t a c kp r o t o c o l s a u t h e n t i c a t i o n , a n dt h r o u g hp r i n c i p l e ss u c c e s sp r o b a b i l i t y , w eg i v et h ed e f i n i t i o no f a u t h e n t i c a t i o ni nt h ef i e l do f c o m p u t a t i o nt h e o r y f i f t h l y , r e c o n c i l i n g t h e o r e m p r o o f m e t h o do fs y m b o lt h e o r ya n d i n d u c i n g t o - e o n t r a d i c t i o nm e t h o do fc o m p u t a t i o nt h e o r y , w ed e s i g nan e wa n a l y t i c m e t h o d i nc o n t r a s tt om e t h o d so fs y m b o lt h e o r y , t h en e wm e t h o dc o u l da n a l y z e k # _ 一 ， lsl ， 山东大学博士掌位论文 a d v e r s a r y sa b i l i t yt oa t t a c kc i p h e rt e x t a n di nc o n t r a s tt om e t h o d sc o m p u t a t i o nt h e o r y , t h em e t h o dc o u l da n a l y z ew h e t h e rp r o t o c o l sh a v i n gn e c e s s a r ym e s s a g e s ，a n dv e r i f y t h e i rs e c u r i t y f i n a l l y , w eg i v ea na n a l y z i n ge x a m p l eu s i n gt h en e wm e t h o d t h en e x tw o r ki n c l u d e ：b u i l d i n gal o g i ct od e s i g ns e c u r i t yp r o t o c o l s ，t h e nu s e p r o l o gl a n g u a g et or e a l i z ea u t o m a t i cd e s i g n i n gs c h e m e ，t h r o u g hw h i c hw ec o u l d l o c a t e p r o t o c o l s f l a w sa u t o m a t i c a l l y ；s t u d y i n gs y m m e t r i c a l k e yc r y p t o g r a p h y s s e c u r i t yi nk i n d so fa t t a c km o d e l i no r d e rt oa d v a n c es o m eb e t t e rs c h e m e st od e s i g n p r o t o c o l s ，a n da n a l y z ep r o t o c o l s s e c u r i t ya l l a r o u n d k e yw o r d s ：s e c u r i t yp r o t o c o l s ，s y m b o lt h e o r y , c o m p u t a t i o nt h e o r y , s e c r e o y , a u t o m a t i ca n a l y s i s 山东大学博士学位论文 4 、口 s i e k 、足7 m k 胁 k o 肘。 q m o m 以伊 ab e t s ( # ) as a y s ( m ) as a i d ( m ) 符号说明和缩略词 主体 可信中心 特指敌手 a 的公钥、私钥 用密钥足对m 加密的密文 彳的n o n c e 密码体制的安全参数 公开消息 保密消息 材具有完整性 表达式 一相信成立 a 刚刚说过 ， 4 曾说过肼 ；i l 一 原创性声明 本人郑重声明：所呈交的学位论文，是本人在导师的指导下，独 立进行研究所取得的成果。除文中已经注明引用的内容外，本论文不 包含任何其他个人或集体已经发表或撰写过的科研成果。对论文的研 究作出重要贡献的个人和集体，均已在文中以明确方式标明，本声明 的法律责任由本人承担。 论文作者签名：叁笠生日，期：尘! 出型三 关于学位论文使用授权的声明 本人完全了解山东大学有关保留、使用学位论文的规定，同意学 校保留或向国家有关部门或机构送交论文的复印件和电子版，允许论 文被查阅或借阅；本人授权山东大学可以将本学位论文的全部或部分 内容编入有关数据库进行检索，可以采用影印、缩印或其他复制手段 保存论文和汇编本学位论文。 ( 保密论文在解密后遵守此规定) 论文作者签名卜塞鲢 导师签名e t 期：必j j 山东大掌博士学位论文 第一章绪论 当今社会，随着计算机技术和互联网技术的日益发展和广泛应用，人们越来 越强烈地感受到无地域性和实时性的网络数字流正在全方位地改变着信息的传 播方式，使之变得更加快捷和高效。 但人们在享受计算机网络技术所带来的梦幻般快捷的通信时，也越来越深刻 地感受到随之而来的一个严重威胁信息的不安全：由于互联网本身具有公开性 和匿名性的特点，使得网上传递的信息可被随意窃听和篡改，人们不仅不能产生 面对面通信时所获得的信任，而且对于所接收信息的真实性和保密性也感到怀 疑。由于计算机技术和互联网技术已经渗入到国家的社会生活、政治、军事和经 济的方方面面，能否很好地解决这些信息安全问题，不仅关系到人们的日常生活， 而且还涉及国家安全问题，因此各国政府和科研机构已将其作为高额投入的焦 点此外，信息安全技术涉及密码学、计算机科学、信息论等各个学科，是一门 综合性研究领域，吸引着国内外大量学者的兴趣，因此也是科学研究领域的一个 重要方向。 1 1 、安全协议的一些基本概念 信息安全领域的一项重要内容就是研究如何保证网络上传输数据的机密性、 完整性、身份或数据来源的鉴别、不可否认性、可追究性、匿名性等功能。这些 目标的实现，通常是运用密码算法，设计一个在网络上运行的两方或多方安全协 谢l 】来完成的随着人们对网络安全需求的日益增强，安全协议作为一种有效的 安全保护手段也受到了越来越多的关注，针对它的研究已经成为信息安全领域的 一项重要分支。 首先我们给出有关安全协议的一些基本概念 1 1 1 、网络协议及会话 网络协议可以看作是通过消息来驱动的：设n 个主体毋，z 组成一个集 合，他们之间通过点对点的连接来传递消息所谓网络协议【刁是这些交互过程的 山东大学博士掌位论文 集合，执行这些过程的主体同步运行，并按照一定的规范处理接收到的消息、产 生新消息。协议可由外部请求触发一方主体开始，然后依靠消息的收发执行下去， 主体所能执行的动作有：接收并处理消息、产生并发出新消息、等待下一条消息 的到达、拒绝执行协议、结束协议。 每个主体可同时运行多个协议的副本。所谓会话，指在主体中运行的某个协 议的副本。会话由主体标示符、通信对方标示符和一个会话标示符来唯一确定， 它们在实际中也指明了存在于通信对方中的对应会话。 1 1 2 、安全协议及分类 安全协议是一类特殊的网络协议。简单而言，安全协议是指那些利用密码学 算法实现某些安全目标或者安全性质的网络协议。 根据安全协议的应用目的，一般可划分为以下四种【3 】： 1 密钥交换协议：为了实现主体间的安全通信，这类协议通过一系列消息 的交互，在两方或多方主体之间共享了一个秘密的临时会话密钥。协议中的密码 算法可采用对称钥算法或公钥算法。常见的密钥交换协议有：d i f f i e h e l l m a a 协 议( 4 , 5 1 、b i o t a 协议 6 1 、k e r b o r o s 协谢“、端端协议n 蜘、m i t 协议【7 1 和g i r a u l t 协议 嘲等等。 2 认证协议：这类协议通过消息的交互来实现通信主体身份的认证或数据 源的认证，来防止敌手的冒名或篡改数据源等攻击。在这类协议中，比较著名的 有f e i g e 、f i a t 与s h a m i r 在1 9 8 6 年提出的基于零知识的身份识别协议 9 1 、s c h n o r r 协议【、o k a m o t o 协议等【1 。 3 认证密钥交换协议：在协商秘密i 临时会话密钥的同时，实现主体认证或 者数据源认证y a h a l o m 协议 1 2 , 1 3 】，n e e d h a m s c h r o e d e r 协议【1 4 1 等均是这类协议 的代表。 4 电子商务协议：是随着电子商务的广泛应用而产生的一种协议。协议的 运行不仅要保证数据的保密性，防止假冒和篡改攻击，而且公平性、不可否认性 也是需要考虑的重要性质常见的电子商务协议有s e t 协议、i k p i 协议。 2 山东大学博士掌位论文 1 1 3 、安全协议的服务 作为一种在公开网络上为信息提供安全保障的手段，安全协议可提供以下几 种安全服务： 机密性：机密性也称为保密性，通常在不同的应用领域有着不同的解释一 个严格的保密性描述需要敌手得不到合法用户活动的任何有用信息，即既不能推 断加密消息的内容，也不能做任何的流量分析。但对于大多数应用而言，这个描 述过于严格。大多数情况下，只要防止攻击者能得到通过可信节点的被保密的消 息就足够了。即敌手能够通过某种方式知道4 向用户口发送了一个消息，甚至 清楚地知道这个消息持续的时间，但无法知道消息的内容。 认证性：是最重要的安全服务之一，许多的安全应用都依赖于该服务它是 用来获取对谁或对什么事情信任的一种方法，包括数据源认证和身份认证两方 面。 数据源认证：接收者能确定消息声称的源地址是消息真正发出的地址例如： 口收到一条自称是发自a 的消息，则该消息就一定是用户a 发出的。但是在该认 证通过时，消息可能已被许多系统重放，且这些系统并没有通过认证数据源认 证与完整性有一些联系，必须确认消息在离开它的信源后没有被篡改。然而，数 据源认证不能免遭消息的复制、重排或者丢失。 身份认证：通过消息的交互来确认对话者的身份它可以是单向的或是双向 的。所谓单向身份认证是指通信双方中只有一方向另一方进行认证；所谓双向认 证是指通信双方相互认证它与数据源认证较为明显的一点区别在于它包含“实 时性”的含义，即身份的认证局限于当前协议的执行阶段。而数据源认证没有该 要求。 完整性：是指数据在传输或者存储的过程中没有损坏( 修改、丢失、重排序 或替换) 。在具体应用的时候，我们是通过针对数据的任何篡改都会被检测出来 来保证数据的完整性在某种意义上，我们认为完整性是协议正确运行的前提， 即每一步正常协议动作的执行都隐含着消息的完整性 不可否认性：主要应用于电子商务协议。对于大多数安全目标，我们总假设 合法用户是诚实可信的，也就是他们将遵循协议规范。但在电子商务协议中，则 是另一种情况。因为利益的驱使，合法主体可能会欺骗通信的对方以便获取利益。 山东大学博士掌位论文 而不可否认性就是讨论如何保护通信的一方不被欺骗。采取的方法是要为用户提 供证据，来证明协议中某些步骤确实已经发生过。 公平性；电子商务中可能会出现这种情况：彳签名后，b 却在即将签名前拒 绝继续执行协议，这样丑就获得了比多的优势因此我们需要考虑如何避免 参加协议的任何一个用户通过半途中止协议来获取比另一方更多的利益，这就是 公平性。一般采用引入可信的第三方并戚增加承诺机制来实现。 1 2 、密码学的相关内容， 密码学技术是信息安全的关键技术，也是为安全协议提供安全服务的基础。 1 2 1 、常用的密码体制 密码学对信息的安全保护主要分为两个方面：保密性和认证性。保密性是防 止敌手破译系统中的机密信息认证性有两个目的：一是验证信息的发送者不是 伪造的；二是验证在传输或存储中的信息没有被篡改、重放或伪造。在密码学中 为了实现这两个方面的安全，通常采用以下两种密码体制： 一加密体制 加密体制从原理上可分为两大类：对称钥体制和公钥体制 1 5 】两种加密体 制的保密性仅取决于相关密钥的保密性，与密码算法的保密性无关。 ， 对称钥体制 对称钥体制的加密密钥和解密密钥是相同的，或者两者能很容易地相互推 出。在这种体制中，需要考虑的主要问题是如何产生满足保密要求的密钥，以及 如何将密钥安全可靠地分配给通信双方。 。 对称钥体制下对明文消息的加密有两种情况：一种是明文消息按字符逐位进 行加密，称为流密码1 1 6 - 1 叼；另一种方式是将明文分组，逐组加密，称为分组密码 1 9 - 2 7 对称钥体制不仅能用于数据加密，还能用于消息认证 公钥密码体制 公钥体制中每