（计算机系统结构专业论文）安全协议的形式化方法及其应用的研究.pdf

摘要 网络可以使人们在任意地点和任意时间、以任意方式访问共享网络资源，同时随着 网络的迅猛发展和应用领域的不断扩大，网络面临着越来越多的安全威胁，为了保证网 络的安全运行和资源的有效利用，作为网络安全服务基础的安全协议越来越受到重视， 但由于安全协议本身的复杂性、相关理论和工程技术的不成熟以及人们认识能力的局限 性，使得在现有安全协议中不可避免地存在着安全缺陷。为了设计出更可靠的安全协议， 形式化方法成为描述、设计和分析安全协议的有效工具，并得到相当深入的研究、并获 到比较广泛和成功的运用。目前，在无线局域网的安全协议中不同程度地存在着安全缺 陷，其中在8 0 2 1 1 中的安全机制存在着致命的安全漏洞。近几年来，为了基于可信平 台特性建立未来具有高安全性的计算机系统，可信计算组提出了在计算机的硬件平台上 引入安全芯片架构和通过提供硬件的安全特性来提高系统安全性的安全体系结构。本论 文深入研究了安全协议面向主体的形式描述、设计和分析，并运用本论文中提出的安全 协议面向主体的形式描述、设计和分析方法，分别研究了无线局域网中w a p i 的认证和 密钥协商协议以及可信计算中的o i a p 协议。本论文的贡献表现在： ( 1 ) 在安全协议面向主体的逻辑描述语言的研究中，将主体遵从安全协议相互通信 的过程看成主体通过通信行为传递拥有、知识和信念以及主体的拥有、知识和信念随时 序单调增加的过程；基于拥有、知识、信念、发送、接收和时序建立了描述安全协议的 形式语言；给出它的k r i p k e 语义模型和真值语义解释；在安全协议元素的形式化描述 中，运用面向主体的方法描述了参与安全协议运行的主体的特性及其角色，比较清晰、 准确和全面地描述了安全协议中消息的可辨认性和新鲜性、密钥的特性以及认证与密钥 分发的目的，根据提供的不同安全服务，将安全协议中的密码机制抽象为不同信道；运 用该形式语言以面向主体的方法对n e e d h a m s c h r o e d e r 对称密钥协议进行了形式化描 述；将该语言与c k t 5 对安全协议逻辑描述的表达能力进行了比较。 ( 2 ) 在安全协议面向主体的设计逻辑的研究中，创建了基于面向主体以及知识和信 念逻辑的安全协议设计逻辑，给出了关于知识和信念、安全主体、权威主体、发送、接 收、拥有、消息的可辨认性、消息的新鲜性、消息源和主体身份认证、密钥验证和密钥 协商的公理，给出了三段论推理规则；根据提供的不同安全服务，将安全协议中的密码 机制抽象为不同信道，形式化地描述了细化规则、合成规则、转发规则、规范消息规则、 关联规则、全信息规则和优化消息规则7 个安全协议设计规则；将安全协议的设计分为 安全协议目的的确定、分析主体的角色及其特性、密码机制的确定、安全协议目的的细 化、分析安全协议设计的初始假设、运用规范消息、关联和全信息规则设计单个消息， 根据优化消息优化安全协议7 个步骤：根据给出的设计逻辑、设计规则和设计步骤形式 安全协议的形式化方法及其应用的研究：摘要 化和系统化地设计了一个基于对称密钥机制的安全协议和一个基于挑战响应机制进行 相互身份认证和d i f f i c h e l l m a n 密钥协商机制的安全协议；将该设计逻辑与b s w 逻辑 进行了比较。 ( 3 ) 在安全协议面向主体的分析逻辑的研究中，构建了面向主体的安全协议分析逻 辑，将拥有、信念和知识融合起来更真实地模拟主体在协议运行中的状态，给出基于秘 密和公开密钥密码系统的公理集，给出了兰段论、必然律和理性推理规则；由主体的拥 有集、信念集、知识集和通信行为构造安全协议的计算模型，给出该分析逻辑中形式语 言的真值语义解释，证明了该分析逻辑的可靠性；给出安全协议的分析步骤，通过对 n e e d h a m s c h r o e d e r 协议的分析检验了新的分析逻辑的推理能力，并与b a n 和g n y 逻 辑对该协议的分析结论进行了比较。得出本逻辑比它们有着更强的推理能力的结论。 ( 4 ) 在国家标准无线局域网认证和保密基础设施咄i ) 的研究中，描述了w l a n 中安全协议的特性，分析了它们中存在的安全缺陷，对w a p i 和8 0 2 1 l i 进行了比较， 运用本论文提出的安全协议分析逻辑对w a i 协议进行了形式化分析和改进分析。 ( 5 ) 在可信计算的研究中，描述了可信平台的特性和o i a p 的会话过程，运用本论 文提出的安全协议分析逻辑对o i a p 进行了形式化分析和改进分析。 关键词：安全协议；身份认证； 面向主体的软件工程； 密钥协商；信道；知识；信念；主体； 可信计算；可信平台模块 n 叶 1 i l - r e s e a r c ho nf o r m a lm e t h o d sa n dt h e i r a p p l i c a t i o n sf o rs e c u r i t yp r o t o c o l s h u ad o n g m i n g ( c o m p u t e r a r c h i t e c t u r e ) d i r e c t e db yh o uz i f e n g n e t w o r k sc a nm a k ep e o p l ea c c e s ss h a r e dn e t w o r kr e s o u r c e sb ya n yw a y sa n da ta n y p l a c e a n da n yt i m e ，m e a n w h i l et h r o u g hn e t w o r k sb e i n gr a p i d l yd e v e l o p e da n di t sa p p l i c a t i o nb e i n g g r a d u a l l ye x t e n d e d ，t h e r ee x i s tm o r ea n dm o r es e c u r i t yt h r e a t si nn e t w o r k s ，i no r d e rt o g u a r a n t e et h a tn e t w o r k sa r er u n n i n gs e c u r e l y , a n dr e s o u r c e sc a l lb es e c u r e l yu t i l i z e d ，s e c u r i t y p r o t o c o l s ，a st h eb a s i so fs e c u r i t ys e r v i c e si nn e t w o r k s ，a r ep a i dm o r ea t t e n t i o n ，b u tb e c a u s e s e c u r i t yp r o t o c o l sa r ev e r yc o m p l e x ，i t st h e o r ya n de n g i n e e r i n gt e c h n o l o g ya r en o tp e r f e c t , t o g e t h e rw i t hs c i e n t i s t sa n de n g i n e e r sh a v el i m i t e da b i l i t yt op e r c e i v e ，s ot h e r ee x i s ts e c u r i t y v u l n e r a b i l i t i e si np r e s e n ts e c u r i t yp r o t o c o l s i no r d e rt od e s i g nm o r ev a l i ds e c u r i t yp r o t o c o l s ， t h ef o r m a lm e t h o db e c o m et h ev a l i dt o o lt od e s c r i b e ，d e s i g na n d a n a l y z es e c u r i t yp r o t o c o l s ，i n w h i c ht h el o g i cm e t h o dh a sb e e nr e s e a r c h e dq u i t ed e e p l y , a n dh a sb e e na p p l i e dw i d e l ya n d s u c c e s s f u l l y t h e r ee x i s ts e c u r i t yv u l n e r a b i l i t i e s a td i f f e r e n te x t e n t si nv a r i o u ss e c u r i t y p r o t o c o l so fp r e s e n tw i r e l e s sl o c a ln e t w o r k s ；e s p e c i a l l yt h e r ee x i s tf a t a ls e c u r i t yh o l e si nt h e s e c u r i t ym e c h a n i s m so f8 0 2 1 1 r e c e n t l yi no r d e rt oc r e a t et h ef u t u r ec o m p u t e rs y s t e mi n w h i c ht h eh i g hs e c u r i t yi sb a s e do nc h a r a c t e r i s t i c so ft r u s t e dp l a t f o r m s ，t h et r u s t e dc o m p u t i n g g r o u ph a sp u tf o r w a r dt h es e c u r ea r c h i t e c t u r ew h i c hi sb a s e do ns e c u r ec h i po nh a r d w a r e p l a t f o r m so f c o m p u t e r sa n dc a r li n c r e a s es e c u r i t yg u a r a n t e e so f c o m p u t e rs y s t e m st h r o u g ht h e s e c u r i t yo fh a r d w a r e i nt h ed i s s e r t a t i o n , id e e p l yr e s e a r c ha g e n to r i e n t e df o r m a ld e s c r i p t i o n ， d e s i g na n da n a l y s i sf o rs e c u r i t yp r o t o c o l s ，a n dr e s e a r c ht h ea u t h e n t i c a t i o na n dk e ya g r e e m e n t p r o t o c o lo fw i r e l e s sa u t h e n t i c a t i o na n dp r i v a c yi n f r a s t r u c t u r ea n dt h eo b j e c ti n d e p e n d e n t a u t h o r i z a t i o np r o t o c o lo ft r u s t e dc o m p u t i n gu t i l i z i n gt h ea g e n to r i e n t e dm e t h o d sf o rf o r m a l l y d e s c r i b i n g ，d e s i g n i n ga n da n a l y z i n gs e c u r i t yp r o t o c o l sw h i c hi sp u tf o r w a r di nt h ed i s s e r t a t i o n t h em a i nc o n t r i b u t i o n so f t h ed i s s e r t a t i o ni n c l u d e ， ( 1 ) i nt h er e s e a r c ho ft h ea g e n to r i e n t e dl o g i c a ll a n g u a g et od e s c r i b es e c u r i t yp r o t o c o l s ，i r e g a r dt h ep r o c e s so fa g e n t sb ye x c h a n g i n gm e s s a g e sf o l l o w i n gt h es e c u r i t yp r o t o c o l sa st h e p r o c e s so fe x c h a n g i n gt h e i rp o s s e s s i o n , k n o w l e d g ea n db e l i e fa n da st h ep r o c e s so f m o n o t o n o u s l yi n c r e a s i n gt h e i rp o s s e s s i o n , k n o w l e d g ea n db e l i e ff o l l o w i n gt i m e ；im a k et h e f o r m a ll a n g u a g ef o rs p e c i f i c a t i o no fs e c u r i t yp r o t o c o l sb a s e do np o s s e s s i o n , k n o w l e d g e ，b e l i e f , s e n d i n g ，r e c e i v i n ga n dt i m e ，a n dm a k ei t sk r i p k es e m a n t i cm o d e la n di n t e r p r e t a t i o no ft r u e v a l u e ；d e s c r i b ea g e n t s c h a r a c t e r i s t i c sa n dr o l e sw i t ha g e n to r i e n t e df o r m a lm e t h o d ，q u i t e c l e a r l y , w h o l l ya n de x a c t l y s p e c i f yt h er e c o g n i z a b i l i t ya n df r e s h n e s so f m e s s a g e s ，t h ea t t r i b u t e s i i l 安全协议的形式化方法及其应用的研究：a b s t r a c t o fc o m m u n i c a t i v ec h a n n e l sa n dk e y s ，a sw e l la sg o a l so fa u t h e n t i c a t i o na n dk e ya g r e e m e n t ；i a l s of o r m a l l ys p e c i f yt h en e e d h a m s c h r o e d e rs h a r e dk e yp r o t o c o lw i t ho u rl a n g u a g ea n da g e n t o r i e n t e df o r m a lm e t h o d ；a tl a s tic o m p a r et h er i g h tl a n g u a g ew i t hc k t 5a b o u tt h e i rd e s c r i p t i v e a b i l i t yf o rs e c u r i t yp r o t o c o l s ( 2 ) i nt h er e s e a r c ho f t h ea g e n t o r i e n t e dl 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 ，ip r o v i d ea na g e n t o r i e n t e dl 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 a c c o r d i n gt ot h e i rv a r i o u ss e c u r i t ys e r v i c e s ， c r y p t o g r a p h i cm e c h a n i s m sa r ea b s t r a c t e dt ov a r i o u sc h a n n e l si ns e c u r i t yp r o t o c o l s if o r m a l l y d e s c r i b er e f i n e m e n t sf o rg o a l so fs e c u r i t yp r o t o c o l s ，r e q u i r e m e n t so fs e c u r i t ys e r v i c e sw h i c h v a r i o u sm e s s a g ec o m p o n e n t sn e e d ，a s s o c i a t i o nb e t w e e nm e s s a g e sa n de n v i r o n m e n t si nw h i c h p r o t o c o l sr u n , f u l li n f o r m a t i o no f m e s s a g ec o n t e n t sa n do p t i m i z a t i o no f m e s s a g e s ，a n dir e g a r d t h e ma sd e s i g nr u l e sa n dm e t h o d st op r e v e n ta t t a c k s i nd e s i g ns t e p sf o rs e c u r i t yp r o t o c o l s ，i c o n s i d e rh o wt od e s i g r j ， ， , t h e i rg o a l s a g e n t s r o l e sa n dc h a r a c t e r i s t i c s s e c ，u r i t ymechanismsinitial a s s u m p t i o n sa n dm e s s a g ec o n t e n t sa c c o r d i n gt ot h ed e s i g nl o g i cd e s i g nr u l e sa n d d e s i g ns t e p sa b o v e ，if o r m a l l ya n ds y s t e m a t i c a l l yd e s i g nt h en e ws e c u r i t yp r o t o c o lt h a ti sb a s e d o ns y m m e t r i cc r y p t o g r a p h ya n dt h en e ws e c u r i t yp r o t o c o lt h a ti sb a s e do nc h a l l e n g e - r e s p o n s e m u t u a la u t h e n t i c a t i o na n dd i f f i e - h e l l m a nk e ya g r e e m e n t a tl a s tic o m p a r e0 1 1 1 1 0 9 i ca n dt h e b s w l o g i c ( 3 ) i nt h er e s e a r c ho ft h ea g e n to r i e n t e dl o g i ct oa n a l y z es e c u r i t yp r o t o c o l s , ic o n s t r u c ta n a g e n to r i e n t e dl o g i cf o rv 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 s ，m o r et r u l ym o d e l s t a t e so fa g e n t si n t h ep r o t o c o lr u n b ym e r g i n gp o s s e s s i o n , b e l i e fa n dk n o w l e d g e t h a ni t sp r e c u r s o r s ；im o d e lt h e u n d e r l y i n gc r y p t o g r a p h i cm e c h a n i s m sa sc h a n n e l sw i t hv a r i o u sc h a r a c t e r ，c o n s t r u c tt h e c o m m u n i c a t i v em o d e l 、 ，i t l lp o s s e s s i o ns e t s ，b e l i e fs e t s ，k n o w l e d g es e t sa n dc o m m u n i c a t i v e a c t i o n s ，i n t e r p r e tt r u t h - v a l u es e m a n t i c so ft h en e wf o r m a ll a n g u a g e ，m o r e o v e r ，p r o v et h en e w l o g i cv a l i d ；iv e r i f yd e d u c t i v ea b i l i t yo ft h en e wl o g i cb ya n a l y z i n gt h en e e d h a m s c h r o e d e r p r o t o c o la n dc o m p a r et h ec o n c l u s i o n so fb a n a n dg n yl o g i c st ot h ep r o t o c o l ，l a s t l yi c o n c l u d et h a tt h en e w l o g i ch a ss t r o n g e rd e d u c t i v ea b i l i t yt h a nb a n a n dg n y l o g i c s ( 4 ) i nt h er e s e a r c ho ft h en a t i o n a ls t a n d a r do fw i r e l e s sa u t h e n t i c a t i o na n dp r i v a c y i n f r a s t r u c t u r e ，id e s c r i b et h ec h a r a c t e r i s t i c so fs e c u r i t yp r o t o c o l si nw i r e l e s sl o c a ln e t w o r k ， a n a l y z et h e i rd e f e c t s ，c o m p a r et h ea u t h e n t i c a t i o na n dp r i v a c y p r o c e s st o g e t h e rw i t ht h ed e s i g n o fk e ym a n a g e m e n to ft h ew i r e l e s sa u t h e n t i c a t i o na n dp r i v a c yi n f r a s t r u c t u r ea n dt h es a m e m e c h a n i s mo f8 0 2 1 1 i f o r m a l l ya n a l y z e 血ea u t h e n t i c a t i o na n dk e ya g r e e m e n tp r o t o c o l u t i l i z i n go u ra n a l y t i c a ll o g i c ，a n da n a l y z et h ed e f e c t si ni t ( 5 ) i i l 山er e s e a r c ho ft r u s t e dc o m p u t i n g ii n t r o d u c et h ec h a r a c t e r i s t i c so ft r u s t e d p l a t f o r ma n dt h es e s s i o np r o c e d u r eo fo b j e c ti n d e p e n d e n ta u t h e n t i c a t i o np r o t o c o l ，f o r m a l l y a n a l y z et h ep r o t o c o lu t i l i z i n go u ra n a l y t i c a ll o g i ca n da n a l y z et h ed e f e c t si ni t i v j ， w - - - 图目录 图2 1 对称密钥密码系统的模型9 图2 2 公开密钥密码系统的保密模型1 1 图2 3 公开密钥密码系统认证模型1 2 图2 4 多主体系统的标准结构1 8 图3 1 外延目的的层次：2 3 图6 1w a i 的系统结构示意图7 0 图6 2 w a i 的认证和密钥协商流程图7 0 图6 38 0 2 1 1 i 的认证过程一7 2 图6 4 a p 与s t a 的4 次握手过程7 2 图7 1 完整性报告协议8 4 图7 2 始于静态信任根的系统导入的可递信任8 5 图7 3 口m 的体系结构8 5 表目录 表2 1d e s 、i d e a 和a e s 的比较1 0 表2 2 对称与公开密钥密码系统的比较1 2 表4 1 新逻辑和b s w 逻辑的比较4 6 表5 1 新逻辑和b a n 类型逻辑对n s s k 协议分析结论的比较。6 4 表6 1e a p 协议的比较6 8 表6 2w ：a p i 和8 0 2 1 1 i 的比较7 3 表7 1o i a p 的会话过程8 8 一 l - 4 ：r 声明 本人声明所呈交的论文是我个人在导师指导下进行的研究工作 及取得的研究成果。就我所知，除了论文中特别加以标注和致谢的 地方外，论文中不包含其他人已经发表或撰写过的研究成果。与我 一同工作的同志对本研究所做的任何贡献均已在论文中作了明确的 说明并表示了谢意。 作者签名：群众 日期：嬲争斗 关于论文使用授权的说明 作者签名：牟才一 导师签名。 ，乏1 日期：加眵一玑 第一章引言 在当今世界，现代技术以爆炸态势迅猛发展，以计算机、网络和微电子为代表的电 子信息技术产业迅速渗透到人们工作和生活的方方面面中，从而促进了全球经济的发 展，也改变了人们的生产方式、生活方式和社会文化，使人们进入数字化信息时代，同 时计算机、网络和家电开始走向融合，以无缝方式向人们提供全面的信息服务。网络作 为未来人们共享信息的主要方式，可以使人们在任意地方和任意时间，以任意方式提供 或接受信息服务。在提供和接受信息服务的过程中，如何保证信息的安全，成为近几年 人们关注的焦点，作为信息服务安全保护基础的安全协议，越来越成为信息安全领域的 一个重要研究方向。目前，在无线局域网的安全协议中不同程度地存在着安全缺陷，其 中在8 0 2 1 1 中的安全机制存在着致命的安全漏洞。近几年来，可信计算组提出的可信 计算成为构建未来具有高安全性的计算机系统和网络的基础。 1 1 本文的研究背景 1 1 i 安全协议的发展 1 1 i 1 安全协议的概念与分类 安全协议是指使用密码学技术或提供安全服务的协议，可以实现认证和密钥交换等 安全目的。所谓协议，就是2 个或者2 个以上的参与者为完成某项特定的任务而采取的 一系列步骤。它包含3 个涵义【3 l ，3 2 】； ( 1 ) 协议自始至终是有序的过程，每一个步骤必须执行，在前一步没有执行完之 前，后面的步骤不可能执行； ( 2 ) 协议至少需要2 个参与者； ( 3 ) 通过协议必须能够完成某项任务。 在协议运行前，协议中的每个参与者都必须预先拥有或知道运行协议所需的资源， 都必须预先知道所要完成的所有协议步骤，并同意且遵守它。协议本身必须被明确定义， 不能产生歧义，并且必须是完整的，对每种可能的情况都必须规定具体的动作。 在网络通信中最常用、基本的安全协议按照其完成的功能可以分成以下4 类【3 3 】： ( 1 ) 认证协议 认证是指对主体身份和消息源的证明【1 3 】。认证是最基本的安全服务，是其它安全 服务的基础。认证过程包括标识和验证两个步骤，标识是主体声称确定身份的过程，验 证检验所声称身份的过程。当某个主体声称自己的身份时，认证服务证明该主体所声称 的身份的真实性。在分布式系统中认证可以分为3 种主要类型：消息内容认证、消息源 认证和身份认证。消息内容认证验证接收到的消息内容与发送时的消息内容相同，消息 内容认证可以通过在消息认证码来实现；消息源认证验证所接收到的消息的发送者与该 中国科学院博士学位论文一安全协议的形式化方法及其应用的研究 消息发送域所记录的发送者相同；身份认证验证主体的身份与其所声称的身份相同。消 息源认证是身份认证的一个子情况。目前共有3 种方法来进行身份认证，分别是以知识 为证据的认证、以拥有物为证据的认证和以生物特征为证据的认证。以知识为证据的认 证是指在认证过程中，声称者向验证者证明只有所声称身份的主体生成或知道的有关声 称身份信息的知识，它可分为直接认证和间接认证，直接认证如基于1 3 1 令的认证等，间 接认证过程由可信第三方来验证声称者身份的真实性；以拥有物为证据的认证是指声称 者产生一个只有所声称身份的主体拥有的标识物；以生物特征为证据的认证是指验证者 直接度量声称者确定的特性。基于知识和拥有物的证明可以被运用到网络的所有类型的。 认证需求中，而基于生物特性的证明通常通过具有特定度量功能的主机认证用户的身 份。认证可以通过认证协议来完成1 1 5 1 。 ( 2 ) 密钥交换协议 密钥交换协议是在参与协议的两个或者多个主体之间建立共享的密钥，通常用于 建立在一次通信中所使用的会话密钥，如d i f f i e - h e l l m a n 密钥交换协议； ( 3 ) 认证和密钥交换协议 认证和密钥交换协议将认证协议和密钥交换协议结合在一起，是网络通信中最普遍 应用的安全协议。在认证和密钥交换协议中，先运用认证协议对通信主体的身份进行认 证，如果认证成功，就通过密钥交换协议协商出在随后通信中保证数据机密性的会话密 钥。 ( 4 ) 电子商务协议 电子商务协议是在电子商务过程中，能够保证交易双方的利益不会受到损害的协 议，它关注交易的公平性。常见的电子商务协议有s e t 协议等。 1 1 1 2 重要的安全协议 在过去二十多年里，随着网络的迅速发展和应用领域的不断扩大，用户获得更多的 信息服务和资源的更有效使用成为可能。为了保证网络的安全运行和资源的安全使用， 相当数量的安全协议被描述和实现。其中包括n e e d h a m s c h r o e d e r 协议、w i d e - m o u t h f r o g 协议 3 4 1 、y a h a l o m 协议【3 4 】、o t w a y - r e e s 协议1 3 5 】，n e u m a n - s t u b b l e b i n e 协议 3 6 】、 d a s s 协议【3 7 】、d e n n i n g - s a c c o 协议 3 8 】、w o o - l a i n 协议【3 9 】等。1 9 9 7 年，c l a r k 和j a c o b 4 0 1 对安全协议进行了概括和总结。以下是在安全的发展过程中有着重要地位和影响，或者 在实际中被广泛使用并起着重要作用的安全协议。 ( 1 ) n e e d h a m - s c h r o e d e r 协议 n e e d _ h a m s c h r o e d e r 协议 4 1 1 是由r o g e rn e e d h a m 和m i c h a e ld s c h r e o d e r 于1 9 7 8 年提出的，采用了对称或非对称密钥加密算法和可信第三方，来相互认证两个用户及建 立用于他们随后通信的会话密钥。这些协议成为后来设计和分析新的安全协议的基础， 每当有新的分析安全协议的形式化方法被提出时，都会先通过分析这些协议来验证新的 形式化方法的有效性，同时也被用来说明安全协议设计规则的特点 4 2 1 。1 9 8 1 年d e n n i n g 和s a c c o 3 8 证明了基于对称密钥密码机制的n e e d h a m s c h r o e d e r 协议中存在缺陷，并提 第一章引言 出了改进措施；1 9 9 0 年b o y d 【4 3 】通过实例表明基于对称密钥密码机制的 n e e d h a m s c h r o e d e r 协议中存在缺陷；1 9 9 5 年l 0 w e 【4 4 】证明了基于非对称密钥密码机制 的n e e d h a m s c h r o e d e r 协议中存在缺陷，并提出了改进措施。 ( 2 ) d i 丘i e h e l l m a n 密钥交换协议 1 9 7 6 年d i f f i e 和h e l l m a n 4 5 发表了著名的“密码学的新方向”的论文，这篇论文 定义了公开密钥密码编码学，而这种算法通常被称为d i f f i e h e l l m a n 密钥交换，该协议 的目的是使两个通信主体安全地交换一个密钥用来保证随后通信数据的机密性，它的安 全性依赖于计算离散对数的难度，该协议具有无法防止重放攻击的缺b f i 1 4 1 。 ( 3 ) k e r b e r o s 认证系统 k e r b e r o s 是由麻省理工学院( m i t ) 为雅典娜项目开发的一个认证机制，它基于 n e e d h a m s c h r o e d e r 协议以及由d e n n i n g 和s a c c o 提出的修改协议，使用了对称密码技 术和在线可信的第三方认证服务器，为工作站用户到服务器以及服务器到作站用户提供 认证方法 1 4 ，3 3 1 。 、 ( 4 ) x 5 0 9 公钥证书框架 x 5 0 9 4 6 是国际电话与电报顾问委员会( c c l l 砷建议作为x 5 0 0 目录服务的一部 分，提供安全目录检索服务，最早于1 9 8 8 年发布，1 9 9 4 年批准了第2 版，1 9 9 7 年批准 了第3 版，2 0 0 0 年批准了第4 版。x 5 0 9 基于公开密钥加密和数字签名，定义了一个由 x 5 0 0 目录向它的用户提供的认证框架。x 5 0 9 中定义的证书结构和认证协议已应用到 s m i m e ，i p 安全、s s l 厂r l s 和s e t 等应用中【1 4 】。 1 1 1 3 安全协议的缺陷 安全协议是网络和分布式系统安全的基础，确保这些协议的安全运行是极为重要 的。大多数安全协议只有为数不多的几个消息传递，其中每一个消息都是经过巧妙设计 的，消息之间存在着复杂的相互作用和制约；同时，安全协议中使用了多种不同的密码 体制，安全协议的这种复杂的情况导致目前的许多安全协议存在安全缺陷 3 2 1 。 s g r i t z a l i s 和d s p i n e l l i s 根据安全缺陷产生的原因和相应的攻击方法对安全缺陷进 行了分类 3 3 ，4 7 ： ( 1 ) 基本协议缺陷 基本协议缺陷是指在安全协议的设计中没有或者很少防范攻击者的攻击而引发的 协议缺陷，例如使用公钥密码系统加密交换消息时，不能预防中间人攻击。 ( 2 ) 口令密钥猜测缺陷 口令，密钥猜测缺陷产生的原因是用户往往从一些常用的词中选择其口令，从而导 致攻击者能够进行口令猜测攻击；或者选取了不安全的伪随机数生成算法构造密钥，使 攻击者能够恢复该密钥。 ( 3 ) 陈旧消息缺陷 陈旧消息缺陷主要是指协议设计中对消息的新鲜性没有充分考虑，从而使攻击者能 够进行消息重放攻击，包括消息源的攻击、消息目的的攻击等。 中国科学院博士学位论文一安全协议的形式化方法及其应用的研究 ( 4 ) 并行会话缺陷 并行会话缺陷是指协议对并行会话攻击缺乏防范，从而导致攻击者通过交换适当的 协议消息能够获得所需要的信息。包括并行会话单角色缺陷、并行会话多角色缺陷等。 ( 5 ) 内部协议缺陷 内部协议缺陷是指协议的可达性存在问题，协议的参与者中至少有一方不能够完成 所有必需的动作而导致的缺陷。 ( 6 ) 密码系统缺陷 密码系统缺陷是指协议中使用的密码算法和安全协议导致协议不能完全满足所要 求的机密性、完整性等需求而产生的缺陷。 造成协议存在安全缺陷的原因主要有三个 4 2 1 ： 一 ( 1 ) 对于安全协议的一些目的、需求和概念没有明确的认识和准确的形式化描述，例 如对于认证目的认识没有明确的认识等； ( 2 ) 安全协议运行环境非常复杂性，安全协议运行在一个非常复杂的开放环境中，攻 击者无处不在，并且攻击能力越来越强大，新的攻击手段不断出现，只有采用形式化方 法来描述攻击者的特性、能力和行为，才能真正认识整个攻击环境； ( 3 ) 协议设计者误解或者采用了不恰当的技术，例如在8 0 2 1 1 标准的w e p 算法中错 误使用r c 4 算法。 1 1 2 安全协议形式化研究的发展 1 1 2 1 安全协议的形式化分析 安全协议作为分布式系统安全的基础，只有为数不多的几个消息传递，其中每一个 消息都是经过巧妙设计的，消息之间存在着复杂的相互作用和制约，同时安全协议中使 用了多种不同的密码体制，这样使用非形式化方法来证明一个安全协议是否安全和设计 一个有效的、满足安全需求的以及没有冗余的安全协议是非常困难的，而形式化方法本 身所具有的严格、明确、清晰和反直觉的特点非常适合被用来设计和分析安全协议。安 全协议的形式化分析方法是采用各种形式化的语言或模型，为安全协议建立模型，并按 照规定的假设和分析方法证明协议的安全性 3 2 】。在二十世纪七十年代末和八十年代 初，人们开始将形式化方法运用到安全协议的研究, 9 4 8 ，4 9 1 ，直到九十年代初，当一些 研究人员使用形式化方法发现了安全协议中潜藏的缺陷时，形式化方法在安全协议中的 应用才得到广泛关注【5 0 】，从那时起安全协议的形式化研究一直被认为是分析安全协议 的有效工具，是安全协议研究中最重要的研究问题之一。 近几年来，密码学家提出了许多关于安全协议的形式化分析方法，以检验协议中是 否存在安全缺陷。总的来说，协议的形式化分析技术可以概括为4 类【3 2 ，5 0 】： ( 1 ) 使用通用的、不是专门为分析安全协议设计的形式化描述语言和协议验证工具对 安全协议进行建模和验证； ( 2 ) 安全协议的设计者设计特定的专家系统来制定协议的验证方案并进行协议验证； ( 3 ) 基于密码学系统的代数特性开发协议的形式化模型； 4 第一章引言 ( 4 ) 基于知识与信念的模态逻辑，来建立所分析的协议的安全需求模型。 在安全协议的形式化分析方法中，基于知识和信念推理的模态逻辑方法最受到人们 的重视，它是分析安全协议的最为重要的形式化方法之一。该模态逻辑包含关于消息知 识或信念的描述以及知识或信念演化的推理规则。安全协议的