（计算机软件与理论专业论文）密码协议验证与设计中若干关键技术研究.pdf

密码协议验证与设计中若干关键技术研究 摘要 ， f f 我国国务院在1 9 9 9 年1 0 月颁布了2 7 3 号令中华人l e 共平国商川密码管理条例，要 求发展我国自己的安全产品。导致一人批拥有自主版权的安全产品如雨后春笋般不断涌现。 这些产品大多依托对密码协议的实现。由丁密码协议本身是标准化的，开放的。而且所使川 的密码算法亦是公开的。所以产品的安全性人多依赖于这些开放技术。发展对密码协议的验 证和设计自己的可靠的商用密码协议，对保障我国电子商务的安全和商业利益都是1 | 常紧 迫。 形式化的协议验证往往能发现隐藏的逻辑上的漏洞，这种漏洞单纯从协议的直观分忻 是不易发现的。例如对并发协议实例的中间人攻击，选择协议攻击，不同协议的组合攻击， 不破坏安全性但同样能造成严重危害的拒绝服务攻击。 早期的协议验证着眼于认证协议。尽管有人量的研究成果，并且发现了许多未知的攻 击，一些最根本的安全特性分析尚未完全解决，实用的理论和简单可靠的分析工具尚未出现。 当前的安全应用发展很快，许多已经投入实用的密码协议比形式化分析的对象复杂的多，这 些协议为了满足不同的应用场合，往往设计得很通用，很灵活。超出了目前形式化分析理论 和工具的分析能力。或者说这些协议尚未经过验证这一过程。密码协议的广泛应用正在期待 这一领域开拓性的工作。 为此，本人有幸参与了上海市科委发展基金资助的研艽课题“分布计算技术一安全协 议分析与设计”( 9 8 5 1 1 5 0 3 5 ，9 9 5 1 1 5 0 1 4 ) ，该课题旨在跟踪当前世界在形式化协议验证方面 和设计方面的最新研究成果，并提出创新性的分析方法，在商务电子交易的协议设计中做一 些尝试。4 本文作者经过辛勤研究，在以下几个方面取得了一些成绩，通过实例分析和比较， 显示我们方法的可行性和其中某些技术具有一定的领先性： 1 ) 发现了密码协议中消息关联特征，并能抽取关联因子作为分析对象。我们对这两个 概念进行了形式化的定义，利用c s p 分析t 具f d r 2 对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 协议的相关性进行了实例分析发现了有效的攻击，证明了这种方法的可行性。 协议相关性的提出为形式化定义和描述协议的安全特征提出了新的思路。 2 ) 提出协议认证特征的形式化定义一观测等价，观测等价描述了在开放环境中认证协 议的安全目标。同时我们借助d o l e v y a o 的协议模型对满足观测等价的主体动作序列的进 ? 搜索，间接地找到了攻击路径。陋种方法也提供了一种隐式地描述攻击行为的途径。通过对 i 实例分析，我们分别独立地发现了4 条对n e e d h a m s c h r o e d e r 公钥协议的攻击路径和3 条对 s s l 客户认证协议的的攻击路径。这些路径都不同程度地满足观测等价要求。 3 ) 发现了k u d o 逻辑在时间标记分析中的缺陷，提出了改进的时限逻辑体系用于分析 电子商务协议中的时限责任问题：利用我们的新方法发现了k u d o 提出的电子投递协议中的 错误，并对支持时限责任的改进n e t b i n 协议进行了实例分析，说明如何利用我们的逻辑体 系进行实际的协议分析。 4 ) 针对当前的拒绝服务的攻击我们提出如何对密码协议分析防j f 这类攻击的方法。 根据拒绝服务攻击的特点，我们的分析的重点放在对发出方产生消息和接收方解析消息的动 作上，这些动作是实现相关的，在协议规范中有明确的说明。而一般的形式化工作都是在消 息格式和收发上进行高层的抽象。为此我们的工作集中对协议规范进行形式化。借助防j p 拒 绝服务的方法一弱认证的设计要点，利用我们的形式化框架对i s a k m p ，h t r p 状态管理， x 5 0 9 改进协议的分析发现了对他们有效的拒绝服务攻击。l ， f 4 5 ) 我们设计了一种分布式拍卖协议。f 在投标阶段协议中用电子现金作为标书，通过密 码分割和标书承诺将其分布到多个拍卖服务器，保证了n = 2 m + l 的最小容错限定。我们的 标书评定算法保证只有最后赢家的标书被恢复，使得输家利益不受损，实现了最大的保密特 性。数字现金和群签名技术保证了其他的一些安全特点。比较同类工作，我们的方案具有最 大保密特征和最小容错限制。并通过了我们时限逻辑的形式化验证。j 6 ) 我们基于观测等价和协议相关特性的分析方法，开发了一个协议分析的专家系统。 该系统可与用户交互来调整分析过程中的状态，达到加速有效路径的构造。 7 ) 我们实现了一个基于秘密分割和群签名的分布式拍卖系统原型，能完成秘密投标拍 卖的基本功能并体现分布式拍卖关于安全性和容错性的6 点要求。 关键词 密码协议，形武化验证，相关性，观测等价，时限责任，协议规范形式化框架， 拒绝服务攻击，分布式电子拍卖 、 i i e n a c t e ds i n c eo c t o b e r1 9 9 9b yt h ec h i n as t a t ec o u n c i l ，t h e c o m m e r c i a lc r y p t o g r a p h y r e g u l a t i o no fp e o p l e sr e p u b l i co fc h i n a - n o 2 7 3 ”h a sp r o m p t e dt od e v e l o pt h ec r y p t o g r a p h y t e c h n o l o g yo f o u ro w n m a n ys e l f - o w n e dc r y p t o g r a p h i cp r o d u c t ss h o o tu pl i k em u s h r o o m s ，m o s t o fw h i c hf e a t u r ei ne r y p t o g r a p h i c p r o t o c o l si m p l e m e n t a t i o n s i n c et h ec i p h e r s a n dc r y p t o g r a p h i c p r o t o c o l sa r es t a n d a r d i z e d ，o p e nt e c h n o l o g i e s ，t h es e c u r i t yo fo u rp r o d u c t sh e a v i l y r e l i e so nt h e s e o p e nt e c h n o l o g i e s t op r o t e c tt h es a f e t yo fo u rc o u n t r y sc o m m e r c i a li n t e r e s t s ，w ed e d i c a t e do n t h er e s e a r c ho ft h ec r y p t o g r a p h i cp r o t o c o l sv e r i f i c a t i o na n dd e s i g n t y p i c a l l y , f o r m a lv e r i f i c a t i o n o ns e c u r i t yp r o t o c o l sc a nr e v e a lm a n yd e l i c a t el o g i ce r r o r s s u c he r r o r sa r en o tp r o n et ob el o c a t e di ni n t u i t i v ei n f o r m a la n n l y 3 i sa n dc a nr e s u l ti nm a n yd e a d l y w e a k n e s s e s l o g i cl o o pc a l le a s i l yb e c o m et h et a r g e to fm i d d l ea t t a c k ，s e l e c t e dp r o t o c o l sa t t a c k ， c o m p o s e dp r o t o c o l sa t t a c ka n du s u a ld e n y o f - s e r v i c ea t t a c k s t h ee a r l ys e c u r i t yp r o t o c o l sa n a l y s i sf o c u s e do nk e ym a n a g e m e n ta n de x c h a n g e - m a n y p r e v i o u su n k n o w n f a u l t sh a v eb e e nf o u n di na u t h e n t i c a t i o np r o t o c o l s h o w e v e r , s o m es u b s t a n t i a l s e c u r i t yp r o p e r t i e sa n a l y s i sa n dr e g u l a t i o na r ef a rf r o mb e i n gc o m p l e t e d p r a c t i c a la n de a s y u s e d a u t o m a t i ca n a l y s i st o o l sh a v en o te m e r g e dy e t m o r e o v e r , m a n yp r a c t i c a lc r y p t o g r a p h i cp r o t o c o l s a r ef a rm o r ec o m p l i c a t e dt h a nt h el i t e r a t u r ep r o t o c o l s t h e s ep r a c t i c a lu s e ds e c u r i t yp r o t o c o l sa r e o f t e nd e s i g n e dt ob ev e r yf l e x i b l ea n dm e e tt h eg e n e r a lp u r p o s e s ，w h i c hm e a n st h e yh a v eb e y o n d t h e c a p a b i l i t y o fc u r r e n tf o r m a lv e r i f i c a t i o n i no t h e rw o r d s ，t h e i n c r e a s i n g u s eo ft h e c r y p t o g r a p h i cp r o t o c o l sl o o k f o r e w o r dt ot h eb r e a k t h r o u g hi nt h ef i e l d f o r t u n a t e l y , o u rr e s e a r c hg r o u po b t a i n e d t h e s u p p o r tf r o ms h a n 曲a is c i e n t i f i cd e v e l o p c o m m i t t e ef i n a n c i a l l ya n dt e c h n i c a l l yi n1 9 9 9a n d2 0 0 0 ( c o n t r a c tn o 9 8 5 1 1 5 0 3 5 ，9 9 5 1 1 5 0 1 钔 w el a u n c h e dap r o j e c tn a m e d “s e c u r i t yp r o t o c o l sa n a l y s i sa n dd e s i g n f u n c t i o n i n ga sas u b - f i e l d o fd i s t r i b u t e dc o m p u t i n gt e c h n o l o g i e si nd i s t r i b u t e dc a m p u t i 叩t e c h n o l o g yc e n t e r ( d c r c ) t h e p r o j e c t c o n c e n t r a t e so nt h ef o r m a lm e t h o da p p l i c a t i o ni ns e c u r i t yp r o t o c o l sa n a l y s i sa n ds o m e i n n o v a t i v es o l u t i o n st oc r a c kt h ec h a l l e n g eo ft h ef i e l d m u l t i p a r t ye - t r a n s a c t i o np r o t o c o l sd e s i g n i sa n o t h e rc o n c e r no fo u rr e s e a r c h a f t e rs e v e r a ly e a r so ft o u g he x p l o r i n g ，w eh a v em a d el o t so f a c h i e v e m e n ti no u rr e s e a r c h n o w , w ep r e s e n to u tc o n t r i b u t i o ni nt h i st h e s i s s h o r t l yl i s t e db e l o w ： +w ef o u n dt h em e s s a g ec o r r e l a t i o np r o p e r t yi nc r y p t o g r a p h i c p r o t o c o l s ，a n de x t r a c t e dt h e c o r r e l a t i o nf a c t o ra st h ek e yt or e f l e c tt h em e s s a g ec o n t e x t f o r m a l i z i n gt h i sc o n c e p t ，w eu t i l i z e d t h ec s pt o o lf d r 2t o v e r i f y t h ef a m o u sn e e d h a m - s c h r o e d e r p u b l i ck e yp r o t o c o l a n d d e n n i n g s a c c oa u t h e n t i c a t i o np r o t o c o lw i t ht h er e s u l to fs u c c e s s f u la t t a c k s c o r r e l a t i o np r o p e r f y s h o u l db es p e c i f i e da sas u b s t a n t i a lc h a r a c t e r i s t i ci ns e c u r i t yp r o t o c o l 十 w ef o u n da n o t b e rc h a r a c t e r i s t i co fa u t h e n t i c a t i o ni nu n r e l i a b l ee n v i r o n m e n t o b s e r v a t i o n i i i 厂 e q u i v a l e n c e ( o e ) o es p e c i f i e s t h e g e n e r a ls e c u r i t yp u r p o s e i n o p e nc i r c u m s t a n c e a f t e r f o r m a l i z i n gi nd o l e v y a o sp r o t o c o lm o d e l ，w es e a r c ht h ep r i n c i p l e s a c t i o ns e q u e n c e sa n da r e b o u n dt of i g u r eo u tt h ea t t a c kp a t h si m p l i c i t l y w er e a l l yd i di ta n di n d e p e n d e d l yc o n s t r u c t e d4 a t t a c k sa g a i n s tn e e d h a m - s c h r o e d e rp k p r o t o c o la n d 3o n e sa g a i n s ts s lc l i e n ta u t h e n t i c a t i o n p r o t o c 0 1 w ef o u n dal o g i cd r a w b a c ki nk u d o t e m p o r a ll o g i c ，a n dp r o p o s e dan e wt e m p o r a ll o g i c f r a m et o a n a l y s i st e m p o r a la c c o u n t a b i l i t y i n p a y m e n tp r o t o c o l s u t i l i z i n g o u rs c h e m e ，w e s u c c e s s f u l l yl o c a t e dt h el o g i cf a u l ti nk u d o se s u b m i s s i o np r o t o c 0 1 m o r e o v e r , n e t b f l lp r o t o c o l w a se n v i s i o n e dt os u p p o r tt h et e m p o r a la c c o u n t a b i l i t ya n dv e r i f i e di no u rs c h e m e 十 r e f e r r i n gt ot h ed e n y o f - s e r v i c ea t t a c k ，w ep r o p o s e dh o w t ol o c a t et h ev u l n e r a b i l i t yb y f o r m a l l ya n a l y z i n gt h ep r o t o c o ls p e c i f i c a t i o ni n s t e a do ft h ei m p l e m e n t a t i o ns o l u t i o nt oa n t i f l o o d s i n c et h es p e c i f i c a t i o na n a l y s i sd i f f e r sg r e a t l yf r o mu s u a lp r o t o c o la n a l y s i sw e p r o p o s e dan e w f o r m a ls p e c i f i c a t i o nf r a m e ，w h i c hf o c u so nt h em e s s a g e sc o n s t r u c t i o ni n s t e a do fo i lm e s s a g e s p a s s i n g w e a ka u t h e n t i c a t i o nw a s i n t r o d u c e dt os e i n et h ep r i n c i p l e so fa n t i - f l o o d b ya n a l y z i n g t h ei s a k m p , e n v i s i o n e dx 5 0 9a n dh n 甲t r u s t m a n a g e m e n t 叩。：f i c a t i o n ，w ef o u n d t h ep o t e n t i a l d o sa t t a c k so ft h e s ep r o t o c o l s w e p r o p o s e dad i s t r i b u t e da u c t i o np r o t o c o l ( d e a ) t oh a v eas m a c k a ts e c u r i t ym u l t i p a r t y t r a n s a c t i o np r o t o c o ld e s i g n i no u rs o l u t i o n 。c u s t o m e r su s et h e i re c a s ha sb i d st og u a r a n t e et h e n o n r e p u d i a t i o n t h eb i di ss a f e l yp a r t i t i o n e da n dr e c o v e r e db ym u l t i p l eb i d d i n gs e r v e r si no r d e r t o p r o t e c t t h e i n t e g r i t y o ft h eb i da n dt o g a i n t h em = 2 t + lf a u l t t o l e r a n ti nad i s t r i b u t e d e n v i r o n m e n t o u rb i de v a l u a t i o na l g o r i t h mg u a r a n t e et h a to n l yt h ew i n n e r sv a l i db i di sr e v e a l e d a n dt h eo t h e r s i n t e r e s t sw i l ln o tl o s e c o m p a r i n gw i t hr e l a t e dw o r k s ，o u rs c h e m eb e n e f i t s m a x i m u m p r i v a c ya n dm i n i m u m f a u l t t o l e r a n tr e s t r i c t i o n b a s e do nt h eo b s e r v a t i o n e q u i v a l e n c e a n dc o r r e l a t i o np r o p e r t y , w e d e v e l o p e d a o e e x p e r t s y s t e mi m p l e m e n t e du s i n gp r o l o g u s e rc a l li n t e r a c tw i t ha o e t oa d j u s tt h ep r i n c i p a l s s t a t e st o a c c e l e r a t et h ea c t i o np a t h sc o n s t r u c t i o n + w e d e s i g n e d a n d i m p l e m e n t e dt h e d e ap r o t o c o l p r o t o t y p es y s t e m t h i ss y s t e m d e m o n s t r a t e do u t b i d d i n g s o l u t i o ns a t i s f y i n gt h e6s e c u r i t yr e q u i r e m e n t so fs e c r e t eb i d d i n g k e y w o r d s ：c r y p t o g r a p h i cp r o t o c o l s ，f o r m a lv e r i f i c a t i o n ，c o r r e l a t i o np r o p e r t y , o b s e r v a t i o n e q u i v a l e n c e ，t e m p o r a la c c o u n t a b i l i t y , f o r m a l s p e c i f i c a t i o n ，d e n y o f s e r v i c e ，d i s t r i b u t e de l e c t r o n i ca u c t i o n 刚茜 日u吾 随着i n t e r n e t 的发展，开放环境中的电子商务对安全通信的需求日益增强。除了更新传 统的底层网络协议外，密码协议为这类应用提供了基本的安全保障。在人们不断设计出新的 密码协议的同时，对这些密码协议的分析和攻击也在进行。传统的密码协议设计过程通常是 设计人员同时作为协议的分析者，这种分析和规范说明过程往往以直观的自然语言进行描 述。这一过程中分析的对象只能是防范已知的可能攻击，对术知的攻击是无能为力的。 形式化的协议验证则往往能发现隐藏的逻辑上的漏洞，这种漏洞单纯从协议的直观分 析是不易发现的。例如对并发协议实例的中间人攻击，选择协议攻击，不同协议的组合攻击， 不破坏安全性但同样能造成严重危害的拒绝服务攻击。 冈为现代密码体制都是利用公开的密码算法，协议的安全性决定丁：密钥而不是算法的 保密。认证协议在密钥管理和交换中起着重要作用，所以早期的协议验证着眼于认证协议。 尽管有大量的研究成果，并且发现了许多未知的攻击，一些最根本的安全特性分析尚未完全 解决，实用的理论和简单可靠的分析工具尚未出现。当前的安全应_ 【_ f j 发展很快，许多已经投 入实用的密码协议比形式化分析的对象复杂的多，这些协议为了满足不同的应j j 场合，往往 设计得很通用，很灵活。超出了目前形式化分析理论和工具的分析能力。或者说这些协议尚 未经过验证这一过程。密码协议的广泛应用正在期待这一领域开拓性的工作。 密码协议分析和设计是一对孪生兄弟，每个密码协议的诞生一定伴随着相应的分析过 程，而且分析过程往往会伴随协议一生。只要这种密码协议还在继续使用，对他的分析就有 价值。甚至可以说，随着协议存在的时间越长，其应用就越广，其安全隐患可能造成的危害 就会越大。同样，新的分析方法也会指导协议的设计，已有很多学者提出了模块化，形式化 的协议规范的协议设计思想，这样设计出的协议易于分析，而且能避免许多逻辑错误。这也 是刚刚起步的研究，实用的设计方法，特别是自动化的设计与验证： 具才可能引起广大协议 设计者的兴趣。 密码协议是种面向应用层的网络安全协议，她为通信的实体打上包装，穿上盔甲。 防止在不安全网络中攻击者对敏感数据的窃取，保证通信内容的完整性。不同的应用需求对 传统密码协议的设计也提出了新的要求，组通信，匿名通声安全多方计算，不可抵赖的签 名，盲签名，群盲签名数字现金技术的需求对密码协议设计者提出了更高的挑战。虽然这些 概念早已提出，但要把这些理论上讨论的协议实用化还有一段路要走。 本文针对上述问题着重对密码协议的形式化验证做了一些研究。对验证中几个核心问 题进行了深入的讨论，并提出了自己的一些思路和方法。在设计方面，作者尝试了电子商务 中拍卖乖】支付两方面的设计一i ：作。希望本人的 作对这方面的研究贡献一点微薄的力量。 上海交通大学博士学位论文 0 1 论文研究的背景 我国在密码学上的研究已有很长的历史，早期的研究集中在军方和政府部门。随着电 子商务的热潮，民间的信息安全研究已经兴起，许多高等院校和学术机构都开设了专f j 的安 。 全方面的研究。在这些研究中多集中在密码学和信息系统安全方面，在协议验证和对商_ 【 4 的 可靠的密码协议设计方面还有所欠缺。但密码协议的“泛应已是势在必行，1 9 9 9 年在上 海，广卅1 分别成立了c a 证书中心，各种网上购物中心，银行联网，企业上网已是一股潮流。 世界各国从自身利益出发，对安全技术和产品的进出口都进行了严格的控制。我国国 务院在1 9 9 9 年1 0 月颁布了2 7 3 号令中华人民共和国商川密码管理条例，要求发展我国 自己的安全产品。导致人批拥有自主版权的安全产品如雨后春笋般不断涌现。这些产品人 多依托对密码协议的实现。由丁密码协议本身是标准化的，开放的。而且有些这些协议所使 用的密码算法亦是公开的。所以产品的安全性完全依赖于这些开放技术。发展对密码协议的 验证和设计自己的可靠的商用密码协议，对保障我国电子倘纷的安全和商业利益都是非常紧 迫。 为此，本人有幸参与了上海市科委发展基金资助的研究课题“分布计算技术一安全协 议分析与设计”( 9 8 5 1 1 5 0 3 5 ，9 9 5 1 1 5 0 1 4 ) ，该课题旨在跟踪当前世界在形式化协议验证 方面和设计方面的最新研究成果，并提出创新性的分析方法，在商务电子交易的协议设计中 做一些尝试。虽然整个课题组的工作尚未完成，但通过近一年的工作表明，我们在这一领域 的工作是卓有成效的，已有3 名博士生参与了该项目，发表论文1 0 余篇。本人提出的一些 新的分析思路和协议设计方案已被学术刊物所接收。希望我们的工作能丰富我国在这一领域 的研究，进一步推动我国的信息技术发展。这就是我们深入研究该课题的初衷。 0 2 本论文的结构安排 本文以密码协议的形式化分析为主线，针对现有分析方法中的不足，提出了一些创新 性的分析思路。结合课题的研究对一些协议实例的分析得到了较好的结果。同时在我们也 尝试了一些复杂密码协议的设计。其中涉及的关键问题有：如何发现密码协议设计中的规 律，形式化的定义安全。如何隐式的建立攻击模型，但通过对模型的分析攻击行为可以自 动的体现出来。如何对设计中规范说明进行形式化描述，以方便协议的分析。如何对密码 协议的抗拒绝服务进行形式化分析。如何分析时间敏感协议中各个主体的责任性。在设计 方面，我们研究了分布式拍卖并提出了一个具有最小容错限制同时又保证拍卖各项安全特 性的方案。 论文的结构安排如下： 绪论部分主要介绍了本论文研究的背景和相关研究课题的重要意义，以及本文的结构 2 刚舌 安排和作者做的主要贡献； 第一章是与本课题研究相关的一些密码学的基础知识 第二章详细介绍了形式化方法在密码协议分析与设计上的国内外研究现状。包括形 式验证的起源，主要的分析方法分类和各自的特点和不足。 第三章针对认证协议验证中的两个主要问题：安全特征定义和攻击行为描述。第一 节，我们提出了密码协议中的消息相关性，在某些利用随机数和时间标记作为消息关联的 密码协议中，我们定义了关联因子作为特征抽取。通过对关联因子的分析来搜索可能的攻 击。第二节，我们针对身份认证的特点，提出了在开放环境中的观测等价概念，攻击的目 标可以刻画为达到相对被攻击者与被冒充者的观测等价，根据攻击的程度分为强、中、弱 三类。将这种等价状态视为攻击的目标，从而隐式的推出“r 十行为。我们对上述方法都做 了实例分析。证明了这些思路的可行性。 第四章对复杂密码协议中的两个问题做了研究：时间限制责任性和抗拒绝服务特性。 第一节，我们发现了k u d o 逻辑中有关分析时间标记的一个错误，它只对时间签名的责任 性进行了推理而忽视了签名内容的新鲜性。由此我们提出了新的逻辑框架来对时间标记进 行责任分析，发现k u d o 电子投递协议中的时限责任不清的问题。第二节，针对密码协议 可能遭受的拒绝服务攻击，这是一种特殊不破坏协议安全性的攻击。它的攻击对象往往是 产生消息的主体动作，而不是消息本身。而现有的分析工具却把分析对象往往限定在消息 的发送和接收事件上，为此我们提出了一套协议规范的形式化框架，结合抗拒绝服务的设 计目标，重点分析了消息产生和解析的过程。通过几个实例分析发现了一些未知的潜在攻 击。 接下来我们在第五章中设计并实现了一个分布式拍卖协议和。拍卖协议是从两方交易 走向完全多方交易的中间协议，1 ：1 的拍卖是两方协议，n ：m 的拍卖则是多方参与的电子 市场。分布式的电子拍卖可以通过容错解决集中式服务中可能带来的单点故障，更重要的 是可以防止出错服务方的欺骗。我们的方案利用秘密分割将标书分解成多份，发往各个服 务器。并且对分割的标书使用了一种新评比算法保证了只有出价最高者的标书得以恢复保 证了输家利益不受损。 论文的附录a 介绍了我们自行开发的一个中基于相关性与观测等价的协议分析工具 a o e 和对n e e d h a m s c h r o e d e r 公钥协议和s s l 客户认证协议的分析结果。附录b 介绍了第 五章内容d e a 原型系统的设计与实现。 最后是总结与展望，总结了本文研究的内容和成绩，展望了本课题未来需要深入研究 的内容。 上海交通大学博士学位论文 0 3 本论文研究的成绩和贡献 总的来看，本文作者经过长时间的认真研究，在以下几个方面取得了一些成绩，通过实 例分析和比较，显示我们方法的可行性和其中某些技术具有一定的领先性： 1 ) 发现了密码协议中消息关联特征，并能抽取关联因子作为分析对象。我们对这两个 概念进行了形式化的定义，利用c s p 分析工具f d r 2 对n e e d h a m s c h r o e d e r 公钥协议和 d e r m i n g - s a c c o 协议的相关性进行了实例分析发现了有效的攻击，证明了这种方法的可行性。 协议相关性的提出为形式化定义和描述协议的安全特征提出了新的思路。 2 ) 提出协议认证特征的形式化定义一观测等价，观测等价描述了在开放环境中认证协 议的安全目标。同时我们借助d o l o r y a o 的协议模型对满足观测等价的主体动作序列进行搜 索，间接地找出攻击路径。这种方法也提供了一种隐式地描述攻击行为的途径。通过对实例 分析，我们分别独立地发现了4 条对n e e d h a m - s c h r o e d e r 公钥协议的攻击路径和3 条对s s l 客户认证协议的的攻击路径。这些路径都不同程度的满足观测等价要求。 3 ) 发现了k u d o 逻辑中在时间标记分析中的缺陷，提出了新的改进的时限逻辑体系用 于分析电子商务协议中的时限责任问题：利用我们的新方法发现了k u d o 提出的电子投递协 议中的错误，并对支持时限责任的改进t b i l l 协议进行了实例分析，说明如何利用我们的 逻辑体系进行实际的协议分析。 4 ) 针对当前的拒绝服务的攻击，我们提出如何对密码协议分析防止这类攻击的方法。 根据拒绝服务攻击的特点，我们的分析的重点放在对发出方产生消息和接收方解析消息的动 作上，这些动作是实现相关的，在协议规范中有明确的说明。而一般的形式化工作都是在消 息格式和收发上进行高层的抽象。为此我们的工作集中对协议规范进行形式化。借助防止拒 绝服务的方法一弱认证的设计要点，利用我们的形式化框架对i s p 黜i p ，h t t p 状态管理，x 5 0 9 改进协议的分析发现了对他们有效的拒绝服务攻击。 5 ) 我们设计一种分布式拍卖协议。在投标阶段协议中用电子现金作为标书，通过密码 分割和标书承诺将其分布到多个拍卖服务器，保证了n = 2 m + l 的最小容错限定。我们的标 书评定算法保证只有最后的赢家的标书被恢复，使得输家利益不受损，实现了最大的保密特 性。数字现金和群签名技术保证了其他的一些安全特点。比较同类工作，我们的方案具有最 大保密特征和最小容错限制。并通过了我们时限逻辑的形式化验证。 6 ) 我们基于观测等价和协议相关特性的分析方法，开发了一个协议分析的专家系统a o e 分析器。该系统可与用户交互来调整分析过程中的状态，达到加速有效路径的构造。 7 ) 我们实现了一个基于秘密分割和群签名的分布式拍卖系统原型，能完成秘密投标拍 卖的基本功能并体现分布式拍卖关于安全性和容错性的6 点要求。 4 第一章密码协议相关技术 1 1 密码学基础 1 1 1 消息和加密 第一章密码协议相关技术 消息被称为明文。用某种方法伪装消息以隐藏它的内容的过程称为加密，加了密的消息 称为密文，而把密文转变为明文的过程称为解密。图1 1 表明了这个过程。 图1 1 加密和解密 明文用m ( 消息) 密文用c 表示，它也是二进制数据，有时和m 一样大，有时稍大( 通 过压缩和加密的结合，c 有可能比m 小些。然而，单单加密通常达不到这一点) 。加密函数 e 作用于m 得到密文c ，用数学表示为： e ( m ) = c 相反地，解密函数d 作用于c 产生m d ( c ) = m 先加密后再解密消息，原始的明文将恢复出来，下面的等式必须成立： d ( e ( m ) ) = m 1 1 2 算法和密钥 密码算法也叫密码，是用于加密和解密的数学函数。( 通常情况下，有两个相关的函数： 一个用作加密，另一个用作解密) 如果算法的保密性是基于保持算法的秘密，这种算法称为受限制的算法。受限制的算法 的保密性已远远不够。大的或经常变换的用户组织不能使用它们，因为每有一个用户离开这 个组织，其它的用户就必须改换另外不同的算法。如果有人无意暴露了这个秘密，所有人都 必须改变他们的算法。而且，受限制的密码算法不可能进行质量控制或标准化。每个用户组 织必须有他们自己的唯一算法。 + 现代密码学用密钥解决了这个问题，密钥用k 表示。k 可以是很多数值里的任意值。 密钥k 的可能值的范围叫做密钥空间。加密和解密运算都使用这个密钥( 即运算都依赖于 密钥，并用k 作为下标表示) ，这样，加解密函数现在变成： e x ( m ) = c 上海交通大学博士学位论文 d k ( c ) = m 这些函数具有下面的特性( 见图1 _ 2 ) ： d x ( e k ( m ) ) = m 图1 2 使用一个密钥的j n 解密 图1 3 使用两个密钥的j j n 解密 有些算法使用不同的加密密钥和解密密钥( 见图1 3 ) ，也就是说加密密钥k 1 与相应的 解密密钥k 2 不同，在这种情况下： e 日( m ) = c d l ( 2 ( c ) = m d r 2 ( e n ( m ) ) = m 所有这些算法的安全性都基于密钥的安全性；而不是基于算法的细节的安全性。这就意 味着算法可以公开，也可以被分析，可以大量生产使用算法的产品，即使偷听者知道你的算 法也没有关系；如果他不知道你使用的具体密钥，他就不可能阅读你的消息。 密码系统由算法、以及所有可能的明文、密文和密钥组成的。 1 1 2 1 对称算法 基于密钥的算法通常有两类：对称算法和公开密钥算法。 对称算法有时又叫传统密码算法。就是加密密钥能够从解密密钥中推算出来，反过来也 成立。在大多数对称算法中，加解密密钥是相同的。 对称算法的加密和解密表示为： ， e k ( m ) = c d k ( c ) = m 对称算法可分为两类。次只对明文中的单个比特( 有时对字节) 运算的算法称为序列 算法或序列密码。另一类算法是对明文的组比特并行运算，这些比特组称为分组，相应的 + 算法称为分组算法或分组密码。现代计算机密码算法的典型分组长度为6 4 比特这个长 度大到足以防止分析破译，但又小到足以方便使用( 在计算机出现前，算法普遍地每次只对 6 第一章密码坍议相关技术 明文的一个字符运算，可认为是序列密码对字符序列的运算) 。 1 1 2 2 公开密钥算法 公开密钥算法( 也叫非对称算法) 是这样设计的：用作加密的密钥不同于用作解密的密 钥，而且解密密钥不能根据加密密钥计算出来( 至少在合理假定的长时间内) 。之所以叫做 公开密钥算法，是因为加密密钥能够公开，即陌生者能用加密密钥加密信息，但只有用相应 的解密密钥才能解密信息。在这些系统中，加密密钥叫做公开密钥( 简称公钥) ，解密密钥 叫做私人密钥( 简称私钥) 。 用公开密钥k 加密表示为 e k ( m ) = c 虽然公开密钥和私人密钥是不同的，但用相应的私人密钥解密可表示为： d k ( c ) = m 有时消息用私人密钥加密而用公开密钥解密，这用于数字签名( 见1 2 5 节) ，尽管可能 产生混淆，但这些运算可分别表示为： e k m k ，y ，x ，c 表示y 向 x 发送第k 轮消息m k ，消息内容为c 。x 表示x 收到了这个消息。k a i l e r 的方法能显式地表达信任，而不象b a n 逻辑一样将这种信任隐含在假设中。句子 t r u s t r ( p , q ) 表示在上f 文r 中，p 相信q 。t r u s t 是指如果qs a i d x ，p t r u s t s q ，r a 0p 相信 x 。在分析中转发的消息被视为直接来自消息产生源，只要中间媒介不能识别消息的内容。 一个值得注意的假设是主体能够区别不同会晤中的消息，没有这一点，无关的消息历史 可能导致信仰状态的不一致。k g 逻辑中有一条判定消息唯一接受者的规则： x m i ，x ，y ，c ) ；x 障 z ；j i ，0 x i - v y s 2 一 s 1 ) ；驴，k l p e s ；i k j ；y ( j 0 成立。 第二章密码