（计算机科学与技术专业论文）安全协议模型检验技术研究与实现.pdf

独创性声明 本人声明所呈交的学位论文是我本人在导师指导下进行的研究工作及取得 的研究成果。尽我所知，除了文中特别加以标注和致谢的地方外，论文中不包含 其他人已经发表和撰写过的研究成果，也不包含为获得国防科学技术大学或其它 教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任 何贡献均已在论文中作了明确的说明并表示谢意。 学位论文题目：塞垒盐达搓型拴验挂盎盈塞生塞塑 学位论文作者签名： 望鱼釜日期：知。z 年k 月3 0 日 学位论文版权使用授权书 本人完全了解国防科学技术大学有关保留、使用学位论文的规定。本人授权 国防科学技术大学可以保留并向国家有关部门或机构送交论文的复印件和电子 文档，允许论文被查阅和借阅；可以将学位论文的全部或部分内容编入有关数据 库进行检索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论文。 ( 保密学位论文在解密后适用本授权书) 学位论文题目：塞全盐遮搓型挂坠挂垄壁塞盏塞理 学位论文作者签名：垒! 重垒 作者指导教师签名 日期：? 口吃年j z 月5 口日 日期：2 o 工年，2 月3 0 日 国防科学技术人学研究生院学位论文 摘要 随着计算机网络通信的迅猛发展，安全协议的重要性越来越得到重视。安全协议负责 密钥分发和身份认证，一旦其自身出现漏洞，那么将会对通信的安全造成威胁。模型检验 方法在对安全协议的验证中体现出了巨大的优越性。 本课题的研究目的是采用模型检验工具对安全协议进行验证。本文研究了验证安全协 议的各种形式化方法，详细研究了符号化模型检验工具s m v 的工作机制：确定了使用s m v 作为工具对安全协议进行模型检验，验证了认证版n e e d h a m s e h r o e d e r 公钥协议和w o oa n d l a m 兀对称钥协议。 通过使用s m v 对n e e d h a m s c h r o e d e r 公钥协议进行建模和验证，理解了符号化模型检 验和小系统模型的原理，并发现了一个协议漏洞，该漏洞与g a v i nl o w e 用f d r 所发现的 相一致。 为了突破小系统模型的局限性，我们使用s m v 验证w o oa n dl a m 兀对称钥协议时， 建立了允许诚实的通信实体运行两次协议的模型，在这个模型上发现了一个已知的协议漏 洞，攻击者利用诚实通信实体的两次运行，成功地进行了攻击。 在对s m v 的大量使用中，我们发现了s m v 的一个b u g 和其产品说明书中所忽略的一 些值得注意的问题。 文章主要介绍了安全协议的概念、分类和性质，安全协议的形式化验证方法，以及小 系统模型的原理；重点分析和研究了符号化模型检验工具s m v 的原理和语法及其对安全 协议进行模型检验时的工作机理，而且使用s m v 对n e e d h a m s c h r o e d e r 公钥协议和w o o a n dl a m 对称钥协议进行了形式化建模与模型检验，发现了它们的安全漏洞。 关键词：安全协议，形式化方法，b a n 类逻辑，模型检验，s m v ，小系统模型 国防科学技术火学研究生院学位论文 a b s t r a c t a tt h ep r e s e n tt i m e ，f o l l o w i n gt h ei n u n d a n t d e v e l o p i n g o fc o m p u t e rn e t w o r ka n d c o m p u n i c a t i o n ，t h ei m p o r t a n c eo fs e c u r i t yp r o t o c o l sb e c o m e sm o r ea n dm o r ee v i d e n t s e c u r i t y p r o t o c o l st a k ec h a r g eo fd i s t r i b u t i n gk e y sa n da u t h e n t i c a t i n gi d e n t i t y o n c et h e r ei saf l a wi na s e c u r i t yp r o t o c o li t s e l f , t h es e c u r i t yo fc o m m u n i c a t i o nw o u l df a c ed a n g e r t h em e t h o do fm o d e l c h e c k i n gh a ss h o w n i t sa d v a n t a g ei nt h ev e i l f i c a t i o no fs e c u r i t yp r o t o c o l s n eo b j e c to ft h i sp a p e ri st ov e r i f ys e c u r i t yp r o t o c o l sw i t hm o d e lc h e c k i n gt o o l s w e r e s e a r c hd i f f e r e n tk i n d so ff o r m a lm e t h o d s ，p a r t i c u l a r l ys t u d yt h em e c h a n i s mo fs y m b o l i cm o d e l c h e c k i n gt o o ls m v a n df i n a l l yw ed e c i d et oa d o p ts m va st h et o o lf o rt h em o d e lc h e c k i n go f s e c u r i t yp r o t o c o l s 、m t hs m vw em o d e lc h e c kt h ea u t h e n t i c a t i o nv e r s i o no fn e e d h a m s c h r o e d e rp u b l i ck e yp r o t o c o la n dw o oa n d l a m1 7s y m m e t r i ck e yp r o t o c 0 1 d u r i n gt h em o d e l i n ga n dv e r i f i c a t i o no ft h ea u t h e n t i c a t i o nv e r s i o no fn 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 lw i t hs m v , w eg e tm o r ec o m p r e h e n s i o no nt h et h e o r yo fs y m b o l i cm o d e l c h e c k i n ga n ds m a l ls y s t e mm o d e l ，a n df i n a l l yf i n daf l a wi nt h i sp r o t o c o lt h a tc o r r e s p o n d sw i t h t h eo n et h a tg a v i nl o w ef o u n dw i t hf d r i no r d e rt ob r e a kt h r o u g ht h el i m i t a t i o no fs m a l ls y s t e mm o d e l f o rt h ev e r i f i c a t i o no fw o o a n dl a i n | 7s y m m e t r i ck e yp r o t o c o lw i t hs m v , am o d e li sb u i l tu p a nh o n e s ta g e n ti nt h em o d e l i sa l l o w e dt o p a r t i c i p a t e i nt w op r o t o c o l s f i n a l l yaf l a wi sf o u n dt h a ta ni n t r u d e rc a n s u c c e s s f u l l yc o m m i ta l l a t t a c kw h e nt h er e s p o n d e ri sa l l o w e dt op a r t i c i p a t ei nt w op r o t o c o l s s i m u l t a n e o u s l y w h i l em o d e l i n ga n dv e r i f y i n gs e c u r i t yp r o t o c o l sw i t hs m v , w ef i n dab u go fs m va n d s o m eo t h e rp r o b l e m s w h i c ha l ei g n o r e db yt 1 1 ea u t h o r si nt h eh a n d b o o ko f s m v f i r s t ，t h i sp a p e ri n t r o d u c e st h en o t a t i o n ，c a t e g o r i e sa n dp 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 ，a n d f o r m a lm e t h o d st ov e r i f ys e c u r i t yp r o t o c o l sa n ds m a l ls y s t e mm o d e l t h ee m p h a s i si st h e r e s e a r c ha n da n a l y s i so ft h ep r i n c i l c l eo ft h em o d e lc h e c k i n gm e t h o d w es t u d yt h em e c h a n i s m a n ds y n t a xo fs y m b o l i cm o d e lc h e c k i n gt o o ls m v m o d e lc h e c kt h ea u t h e n t i c a t i o nv e r s i o no f n e e d h a m s c h r o e d e rp u b l i ck e yp r o t o c o la n dw o oa n dl a m 玎s y m m e t r i ck e yp r o t o c 0 1 f l a w sa r e f o u n di nb o t hc a s e s k e y w 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 ，b a n - t y p el o g i c ，m o d e lc h e c k i n g ，s m v ， s m a l ls y s t e mm o d e l 国防科学技术火! 学研究生院学位论文 第一章绪论 1 1 课题背景 近年来，计算机网络得到了迅猛发展，信息安全问题也就变得越来越关键。要保证信 息的安全性，仅仅依赖于良好的加密算法是不够的。在实际应用中，还需要有可信的机制 为各个独立的通信实体分发密钥，并且在通信实体之间进行身份认证，这就迫使人们研究 设计出了各种加密协议，或者称作安全协议 1 。这些协议主要完成密钥分发和身份认证任 务。 通常所说的协议，就是指两个或者两个以上的实体( 参与者) 为完成某特定任务而相 互约定的步骤和规则。 协议有三个特点：第一，协议是通信实体之间有序的过程，每个实体的每一步骤必须 按照顺序执行：第二，协议起码要有两个参与者：第三，协议的执行是为了完成某项任务， 而不是空操作。 协议的通信双方在相距很远的情况下进行相互通信时，都要确定一下对方的身份，或 者对方是否合法的通信实体。例如在共享资源的计算机环境中，用户之间要通过用户名 口令来认证各自的身份。这种方法对于所有用户在一个控制台或是通过安全连接的环境中 是足够的。但是，在当今的高度共享数据及计算资源的网络中，这种简单传递的信息可能 被攻击者篡改或重放。安全协议对计算机网络通信的安全性提供了某种程度的保证。 安全协议本身的目的是保证信息的安全，但如果安全协议本身存在漏洞怎么办? 攻击 者会利用这些漏洞，伪装成合法通信者，窃听秘密或者更改信息对通信系统所涉及的业 务领域造成巨大危害，尤其是诸如政府、金融、军事这样的安全攸关的机构。这就要求确 保安全协议本身的正确性，即安全之上的安全。协议的漏洞在设计的时候往往难于发现， 多数都是在使用中或者验证中发现的。单纯的攻击检验法，即穷举各种已知形式的攻击的 方法，不能发现未知的攻击方式，是不够充分的。形式化方法大大地推动了协议验证的发 展。形式化方法主要有基于逻辑、基于模型检验、以及其他诸如基于专家系统、定理证明、 代数项重写等通用的形式化技术的方法。其中，模型检验方法在协议验证中越来越受到重 视。g a v i nl o w e 在1 9 9 6 年使用模型检验工具f d r 对简化的认证版n e e d h a m s c h r o e d e r 公 钥协议进行了验证，成功地发现了一个协议漏洞。 s m v ( s v m b o l i cm o d e lv e r i f i e r ) 是一个功能强大的符号化模型检验工具，在复杂电路设 计的验证中得n t 广泛的应用。在安全协议的验证方面，s m v 也有强大的优势。它具有语 法简单、描述全面等特征，其语法形式与高级语言c 非常接近。 1 2 课题内容与意义 选择好相应的模型检验工具后，对安全协议进行模型检验的一般过程是： 1 ) 建立模型，对所要检验的系统进行抽象，将其描述为有穷状态迁移系统； 2 ) 给出有穷状态迁移系统所要验证的性质的命题描述； 3 ) 遍历有穷状态迁移系统中的所有可达的状态，判断其是否满足所要验证的系统性 第l 页 国防科学技术人学研究生院学1 1 i ) ：论文 质。 课题研究的具体内容和方法是： 1 ) 了解安全协议的基本分类、基本原理和性质以及对安全挤议进行验证的一般方法； 2 ) 了解模型检验的基本原理，熟练掌握模型检验工具s m v ，掌握线性时序逻辑l t l ( l i n e a rt e m p o r a ll o g i 【c ) ： 3 ) 使用s m v 编写程序，对n e e d h a m s c h r o e d e r 公钥协议和w o oa n d l a mn 协议建模， 给出它们的安全性质的形式化刻画，进行验证。 在课题研究中，我们对安全协议有了比较深刻的了解，学习到了安全协议的若干性质， 这些性质正是我们所要验证的协议的安全性质。掌握了g a v i n l o w e 提出的用小系统模型对 协议进行模型检验的方法，以及对安全协议进行模型检验的建模原则和技巧。 我们熟悉了模型检验的基本原理和符号化模型检验工具s m v 的使用，在对s m v 的使 用中，发现了一些s m v 说明书中忽略的问题和未知的b u g ，这些问题在对协议的建模验证 中尤其值得注意。 使用小系统模型方法，用s m v 对n e e d h a m - s c h r o e d e r 公钥协议的简化版进行模型检验 后，发现了一个利用消息重放完成的攻击，与g a v i nl o w e 用另一模型检验工具f d r 所发 现的攻击相一致； 为了不拘泥于小系统模型，我们放宽了实体的协议运行次数的限制，对w o oa n dl a m 兀协议进行模型检验，发现了w o o 和l a m 的所描述的一个攻击。 1 3 本文的组织结构 在第二章中，将介绍数据加解密技术、安全协议、安全协议的分类以及安全协议的漏 洞：在第三章中，将介绍安全协议验证的若干技术，重点介绍了b a n 类逻辑的特点和缺 陷，还介绍了用基于专家系统、代数项重写方法进行协议验证的特点：第四章研究了本课 题所选用的形式化方法一模型检验，以及本课题所选取的模型检验工具符号化检验 工具s m v ；第五章中，使用s m v 在小系统模型上验证了n e e d h a m s c h r o e d e r 公钥协议， 在更加宽松的模型上验证了w o oa n dl a mi i 对称钥协议：第六章对全文进行总结，并且 展望了将来的工作方向。 第2 页 国防科学技术人学研究生院学位论文 第二章安全协议 2 1网络时代的计算机安全 在计算机网络系统中，网络安全的重要性是显然易见的：如果系统存在安全漏洞，那 么系统很容易遭受外界攻击而造成严重的后果；如果缺乏必要的身份认证体系，那么通信 实体之间很难相互信任，通信也就失去了它的可靠性。 在当今网络时代，由于系统自身的安全缺陷，加之网络的开放性和黑客的入侵，系统 的安全性面临极大的挑战，因而我们必须提高安全意识。首先，我们必须了解系统所面临 的安全威胁以及系统被攻击的手段。 系统所面临的安全威胁主要来源与四个方面： 1 ) 信息泄漏( 重要信息被未授权用户获得) ： 2 ) 信息的伪造与篡改； 3 ) 资源窃取； 4 ) 系统遭受蓄意破坏。 系统遭受的攻击，如果是建立在入侵者获得已经存在的通信通道或伪装身份与用户建 立通讯通道的基础上的，则包括消息窃听，身份伪装，消息伪造与篡改，消息重放等手段。 为了实施这些攻击手段，入侵者必须能进入系统中。在很多情况下，系统入侵者是系统的 合法用户之一；而对于那些非合法用户，最简单直接的方法就是破解一合法用户的密码， 另外，网络病毒，网络蠕虫以及一些特洛伊木马程序也是入侵系统的重要手段。 知道了系统被攻击的手段，我们所设计的系统就应当尽量克服这些安全漏洞：首先系 统应当保障通信通道的安全，避免通道被人监听；其次系统应当引入认证机制防止身份伪 装与消息的伪造；最后必须保证每次通话是一次新的通话，避免消息重放攻击。而对于系 统的合法用户，应当使用不易破解的密码，并且要定期更换密码。 为了使通信系统的安全机制达到上述的要求，即机密性、完全性、抗否认性、可用性， 必须将系统建立在三个安全技术上：加解密技术、认证机制和系统登录控制。加解密技术 不仅仅用于明文的加密和解密，而且还是认证机制以及数字签名的支柱；认证机制由两部 分组成：认证系统和密钥分发系统，分别负责通讯双方身份的验证和通讯双方会话密钥的 分发。系统登录控制由于与协议本身关系不大，本文暂不涉及。 2 2 数据加解密技术 数据加密就是利用密钥，对原来可读的明文信息进行翻译，译为密文或密码的代码形 式。该过程的逆过程为解密，即将该编码信息转化为其原来的形式的过程【2 】。 在网络应用中加密的作用就是防止有价值信息在网络上被拦截和窃取。一个简单的 例子就是密码的传输。计算机密码极为重要，许多安全防护体系是基于密码的，密码的泄 漏就会导致安全体系的全面崩溃。通过网络进行登录时，所键入的密码就不能以明文的形 式被传输到服务器，因为网络上的窃听是一件极为容易的事情，所以用户的密码很有可能 第3 页 国防科学技术人学研究生院学位论文 会被黑客侦听并窃取，如果用户是r o o t 用户或a d m i n i s t r a t o r 用户，那么后果将是极为严 重的。 解决这个问题的一个关键方法就是加密加密后的数据即使被黑客截获，也是不可读 的，除非加密密钥十分简单或加密方式十分脆弱，容易被黑客破解。总之，使用加密之后， 黑客不会轻易获取所传输的秘密数据。 随着时代的发展，加解密算法不断改进。对应于对称钥和公钥两种加解密技术，最常 用的有两种加密算法：对称钥加密算法( d e s ，即d a t ae n c r y p t i o ns t a n d a r d ) 3 】和公钥加密 算法( r s a ，由r i v e s t 、s h a m i r 和a d e l m a n 共同设计) 4 1 。 d e s 加密算法是由美国i b m 公司w t u c h m a n 和c m e y e r l 9 7 1 1 9 7 2 年研制成功，1 9 7 7 年1 月1 5 日由美国国家标准局颁布为数据加密标准。d e s 加密算法是为二进制编码数据 设计的，它将“位的明文加密为6 4 位的密文，密钥的长度是6 4 位( 实际可用密钥长度是 5 6 位) 。d e s 算法中的加密和解密所用的密钥相同只是加密函数不同于解密函数，设加 密函数是f ( k ，m ) ，其中k 是密钥，m 是明文，则加密过程是f ( k ，m ) 专 m ) k ， m ) k 是密文： 设解密函数是i ( k ， m ) k ) ，则解密过程是l ( k ， m ) k ) 专m 。不过d e s 加密算法仍存在两 个缺陷：一是5 6 位的密钥不太可能提供足够的安全性；二是算法由于s 盒的设计原理的 未公开陛而可能隐藏陷阱。进入9 0 年代，又出现了其他几种加密算法：i d e a 加密算法( 6 4 位分组，12 8 位密钥，8 圈循环) ，b l o w f i s h ( 6 4 位分组，最大到4 4 8 位可变长密钥) ，r c 5 ，r c 2 加密算法( 可变长密钥加密算法) 等。 另一类是公钥加密算法r s a 。关于r s a 算法的描述大致如下： 1 ) 选择两个太素数p 和q ，通常要求每个均大于1 0 1 0 0 。 2 ) 分别计算n = p q ，珥p 1 ) ( q 1 ) 。 3 ) 选取一个和z 互素的数，记为d 。 4 ) 找到一个e ，满足e d = l ( m o d z ) 。在这里，对于p , q 的选取还有以下的几点建议： n ) p 和q 在长度上应仅差几个数位， ( 2 )( p 1 ) 和( q 1 ) 都应包含一个较大的素数因子， ( 3 )( p 1 ) 和( q 1 ) 的最小公约数应当比较小；另外，d 不能太小， 可以证明，如果e m 而秘密密钥( 即解密密钥) k d = 。这样我们便可以清楚的 说明r s a 算法的加密和解密过程。举个例子，假设b 希望收到从其他发送方发来的消息 是保密的，并且只有b 可解的，这时，b 通过计算生成一对密钥，k e 和k d 。然后b 发布 它的公钥k e ，并且保留它的私有密钥k d 。当然，b 也可以直接将k e 发给通讯方，或者将 k e 发给一个维护用户公钥数据库的公钥分发服务系统，当任意方a 想给b 发送密文时， a 首先向公钥分发服务系统提出请求，公钥分发服务系统从用户公钥数掘库中取出b 的公 钥k e ，并将它送给a 。这时，a 将消息m 加密e ( k e ，m ) - - ) m ，后者是传送的密文。当 b 收到密文 m k o 时，b 用自己的私有密钥k d 解密d ( k d ， m k 。) 专m ，得到明文。 2 3 安全协议密码协议 不管安全系统采用对称钥体制还是公钥体制，它们都会涉及到密钥的管理和分发问题。 如果这方面存在安全漏洞，那么，不论密文加密的效果多么好，通信的安全性也毫无保证。 第4 页 国防科学技术人学研究生院学位论文 对于对称钥加密通信，加密密钥和解密密钥是相同的，将这个通信密钥分发给通信双方的 任务是通过认证服务机制来完成的：对于公钥加密通信公开密钥的分发涉及到公开密钥 的授权和公开密钥的认证的问题。分发密钥的同时，各个通信实体都要完成一个确信：对 方是否诚实实体，也就是说身份是否正确可信，这就要求相互之间进行身份认证。 这些就要靠使用安全协议来完成。 所谓协议就是两个或者两个以上的参与者为完成某项特定的任务而采取的一系列步 骤。这个定义包含三层含义： 1 ) 协议自始至终是有序的过程，每一个步骤必须执行，在前一步没有执行完之前， 后面的步骤不可能执行； 2 ) 协议至少需要两个参与者： 3 ) 通过协议必须能够完成某项任务。 安全协议： 在网络环境中完成主体身份认证和密钥分发等任务的具有安全功能的协议。 密码协议： 在计算机通信环境中，利用加密解密技术来分发密钥、身份认证、传输秘密数据等等。 目前，绝大部分安全协议都利用到了密码技术。许多情况下安全协议与密码协议这两 个概念相互通用。我们这里约定安全协议就是密码协议，本文统一称作安全协议。 安全协议的参与者可以是可信任的通信实体，也可以是攻击者或完全不信任的通信实 体。 安全协议包含某种密码算法。 按照其完成的功能，可以将网络通信中最常用的、基本的安全协议分为以下三类【5 ： 1 ) 密钥交换协议 一般情况下是在参与协议的两个或者多个实体之间建立共享的秘密，通常用于建立在 一次通信中所使用的会话密钥。协议可以采用对称密码体制，也可以采用非对称密码体制， 例如d i f i l e h e l l m a n 密钥交换协议。 2 ) 认证协议 认证协议中包括实体认证( 身份认证) 协议、数据源认证和数据目的安全协议等，用 来防止假冒、篡改、否认等攻击。 3 ) 认证和密钥交换协议 这类协议将认证和密钥交换协议结合在一起，是网络通信中最普遍应用的安全协议。 常见的有n e e d h a m s c h r o e d e r 公钥协议、k e r b e m s v e r s i o n5 协议、分布认证安全服务( d a s s ) 协议、i t u tx 5 0 9 安全协议、w o oa n dl a m 协议等等。 我们研究的安全协议主要是第三种，即认证和密钥交换协议。这是因为在一般情况下， 认证的目的是为了在通信实体之间确认身份后建立共享的秘密这些共享的秘密供实体之 间以后进行的通信使用，例如用作数据传输时使用的对称密钥。所以大部分安全协议都是 认证和密钥交换协议。 最经典的认证和密钥交换协议首推n e e d h a m s c h r o e d c r 公钥协议【6 】。在该协议的一次 完整运行中，参与运行的合法通信实体有三个：服务器s ，该服务器对于协议中的其它通 信实体来说是无条件可信的，负责密钥分发：启始者a ，负责发起一次与响应者进行的认 1 再顶一 国防科学技术大学研究生院学位论文 证。响应者b ，负责响应a 发起的一次协议。它们三者之间的通信关系图如下 映 s ：服务器，a ：启始者，b ：响应者 图i ：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 公钥协议的运行流程为：a 向服务器s 发送服务请求，说明自己想 与b 进行身份认证，建立共享秘密；s 将b 的公钥p k b 以密文的方式发送给a ：a 产生 一个临时值n a ，将n a 和自己的身份信息用前面得到的p k b 加密，作为请求信息发送给b ： b 收到a 的请求后向s 发送服务请求，从s 那里得到a 的公钥p k a ；然后b 产生一个临时 值n b ，连同前面得到的n a 一起，用p k a 加密，发送给a ，作为响应者的应答；最后，a 将收到的n b 用p k b 加密发送给b ，这样a 、b 之间就相互确信了对方的身份并且共享 了临时值n b ，协议的运行就完成了。 为使描述更加清晰我们采用消息序列的方式来表示协议： ( i )a s ：a ，b ( 2 ) s 斗a ： p k b ，b ) p b - ( 3 ) a b ： n a ，a ) p k b ( 4 )b _ s ：b a ( 5 ) s b ： p k a , a m ( 6 ) b 斗a ： n a ，n b m ( 7 ) a 斗b ： n b ) m 其中n a ，n b 为a 、b 产生的临时值，n b 还用作协议结束后a 、b 之间的共享秘密： p k a 和p k b 分别为a 、b 的公钥；p k s 1 为s 的私钥，用于加密发出的消息，a 、b 收到这 样的消息后用s 的公钥p k s 进行解密。 从n e e d h a m - s c h r o e d e r 公钥安全协议的消息序列中可以看出，服务器s 只负责向a 和 b 分发密钥，而不直接参与a 、b 之间的身份认证，如下所示 ( 1 ) a _ + s ：a ，b ( 2 ) s 斗a ： p k b ，b ) p k ；- j ( 4 )b s ：b a ( 5 ) s b ： p k a ，a 列 第6 页 国防科学技术人学研究生院学位论文 可以看出，服务器s 响应a ( b ) 的请求，然后将b ( a ) 的公钥以密文形式回答给a ( b ) ，就是说负责向a 和b 发布双方的公钥。a 与b 之问在进行认证时，其消息传递并 不真正涉及到s 。所以，在研究n e e d h a m s c h r o e d e r 公钥协议时，如果不考虑密钥分发的 安全特性，只考虑协议在认证方面的特性，那么就可以将以上( 1 ) 、( 2 ) 、( 4 ) 、( 5 ) 四个消息 省略，只列出( 3 ) 、( 6 ) 、( 7 ) 这三个消息。这样协议就可以简化为认证版的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 公钥协议的消息序列如下： ( 3 ) a 寸b ： n a ，a p k b ( 6 ) b _ a ： n a ，n b p k a ( 7 ) a - b ： n b ) p k b 2 4 当前流行的各种安全协议 当前流行使用的安全协议比较多，这是因为许多协议被提出后都被发现有安全漏洞， 所以人们就对己经提出的协议进行修正，或者提出更加完善的协议。安全协议在设计上目 前还没有统一的标准，只能以是使用了对称钥加密技术还是公钥加密技术、协议中的通信 实体是否有可信的第三方( 即服务器) 来区分 6 。即使同时依照这两个条件来分类，还是 无法区分出一些特殊的协议。 2 4 1没有可信第三方的对称钥协议 这类协议只有两个通信实体，依靠相互间发送用共享密钥加密的认证消息来进行认 证a 例如i s os y m m e t r i ck e yt w o p a s sm u t u a la u t h e n t i c a t i o np r o t o c o l i s ox c 称, n i z i n 双向认证协议： ( 1 ) a 斗b ：t e x t 2 ，( t a i n a l ，b ，t e x t l ) k a b ( 2 ) b _ + a ：t e x t 4 ， t b l n b ，a ，t e x t 3 k a b a 、b 之间共享对称钥k a b ，其中的t e x t l 、t e x t 2 、t e x t 3 、t e x t 4 依赖于具体的实现， t a ln a 的含义是采用时间戳t a 或者临时值n a 。 2 4 2 使用密码检查函数c c f s ( c r y p t o g r a p h i cc h e c kf u n c t i o n s ) f l t j 协议 这类协议使用一些密码检查函数爪a b ( x ) ，对x 进行加密。爪曲( x ) 根据k a b 的值，返回 x 的h a s h 函数值。例如i s ot w o p a s sm u t u a la u t h e n t i c a t i o nw i t hc c f s 带c c f s 的i s o 两遍双向认证协议： ( 1 ) a 斗b ：【t a l n a ，t e x t 2 ， t a i n a ，b ，t e x t l ) ，k a b ( 2 ) b a ：【t b | n b ，t e x t 4 ， r b n b ，a ，t e x t 3 ) ，k 。b 收到消息的通信实体将密文解密，并将其与明文内容进行比较( 具体方法因实现而 异) ，完成认证。 巧万贡一 国防科学技术人学研究生院学位论文 2 4 3 具有可信第三方的对称钥协议 这类协议使用对称钥加密，并且都有一个可信的第三方，即服务器s 。s 与其他的每 个通信实体之间都共享两两不相同的对称密钥。当通信实体之间想进行身份认证时，就向 s 发出请求，由s 处理、转发请求消息，最后完成认证，并相互都拥有了由s 分发的共享 的对称钥。 例如n e e d h a m s c h r o e d e r 对称钥协议： ( i )a 呻s ： a ，b ，n a ( 2 ) s a ： n a ，b ，k a b ， k a b ，a k b 。) k 。； ( 3 ) a 斗b ： k a b ，a ) k b s ( 4 ) b a ： n b ) k a b ( 5 ) a 寸b ：f n b 一1 k a b 2 4 4 对称钥重复认证协议 这类协议进行重复认证，就是说要反复地、不止一次地进行认证。最常用的是著名的 k e r b e r o sv e r s i o n5 协议。该协议在w i n d o w s 2 0 0 0 的安全基础架构中得到了使用，是比较成 熟比较稳定的协议。协议的消息序列如下： ( 1 )c a ： ( 2 )a c ： ( 3 )c 斗g ： ( 4 )g 斗c ： ( 5 )c _ s ： u ，g ，l 1 ，n 1 u ，t c g ， g ，k c g ，t s t a r t ，t e x p i r e ，n 1 k 。 s ，l 2 ，n 2 ，t c g ，a c g u ，t c s ， s ，k c s ，t s t a r t ，t e x p i r e ，n 2 k c g t e s ，a c s ( 6 ) s _ + c ： i k c s 在这个协议中，客户c 在与服务器s 进行通信之前，必须先经过两个服务器认证：首 先要向k e r b e r o s 认证服务器a 发送门票请求，得到门票分配许可证后，c 向门票分配服务 器g 发送门票许可证，然后g 将相应的门票返回给c ，其中包含c 与s 之间的通信密钥， c 将门票发送给s ，s 接收到门票，经检验后确认c 的身份，客户c 就可以使用门票中的 密钥与服务器s 进行通信了。 2 4 5 没有可信第三方的公钥协议 这类协议用公钥加密技术通信。没有一个可信的第三方提供密钥分发服务。靠通信实 体x 利用对方y 不知道的、自身的私钥k x i 或者加密请求和应答消息，对方y 接到后， 用x 公开的相应的公钥k x 解密，完成认证。 例如i s op u b l i ck e yt w o - p a s sm u t u a la u t h e n t i c a t i o np r o t o c o l - - i s o 公钥两遍双向认证 第8 页 国防科学技术人学研究生院学位论文 协议： ( 1 ) a b ：c e r t a ，【t a i n a ，t e x t 2 ， t a i n a ，b ，t e x t l k ：1 ( 2 ) b 斗a ：c e r t a t bn h ，t e x t 4 ，( 【t bn b ，a ，t e x t 3 ) k ： 这个协议与前面讲述的1 s o 对称钥两遍烈向认证协议的愿* 就在丁消息的加密方法，这里是用的公 钥加密技术。 2 4 6 具有可信第三方的公钥协议 这类协议使用公钥加密技术，其中有一个可信的第三方进行密钥分发服务。最著名的 就是前面2 3 中提到的n e e d h a m s c h r o e d e r 公钥协议，这罩不再重复叙述。 2 4 7 其它协议 还有一些协议无法归入以上的分类。这些协议混和使用了对称钥和公钥加密技术。例 如e k e ( e n c r y p t e dk e ye x c h a n g e ) 协议： ( 】) a 斗b ： k a ，p ( 2 ) b 斗a ：“r k 。 p ( 3 ) a 斗b ： n a ) r ( 4 ) b 呻a ： n a ，n b r ( 5 ) a b ： n b r 这个协议混和使用了对称钥和公钥加密技术：k a 是a 的公钥，a 将其用a 、b 之间 共享的对称钥p 加密传给b ，b 再用k a 加密另一个对称钥r ，并将这个密文用p 加密传 给a ，然后a 、b 之间共享对称钥r ，用r 交换临时值n a 和n b ，这样就完成了身份认证。 还有一些诸如此类的不能严格划分的协议，大多是混和使用了公钥和对称钥技术，这 里就不一一列出了。 安全协议虽然种类繁多，但是在实际使用中，用得比较多的还是那些有可信第三方的 公钥协议，使用对称钥的协议则比较少。这是因为对称钥协议要首先假设通信实体之间已 经共享了对称钥k a b ，这一点在应用中是很难的而且这个对称钥一般要先使用公钥认证 协议来分发，才能共享，所以归根结底，实际中多数都是使用公钥加密方法来分发密钥和 认证身份。实际应用中的公钥认证协议一般都有一个可信服务器，甚至不止一个，这样能 够保证公钥分发的可信性。 所以，本文主要围绕具有可信第三方的公钥认证协议进行研究。 2 5 安全协议的漏洞 安全协议本身是用来完成秘密信息的安全传递的，因而安全协议是否安全则是至关重 第9 页 国防科学技术人学研究生院学位论文 要的，这是安全之上的安全。 类似于法律系统，法律是保障人民群众的安全的因而法律系统本身首先要具备完备 性和公正性。 但是，目前的实际情况却表明：安全协议的正确性或者说安全性不容乐观。即使我们 不考虑与实现相关的协议缺陷和密码系统被成功破译的可能性，安全协议也可能存在一些 未知的漏洞，攻击者可以使用直观上难以发现的攻击序列，冒充协议中的诚实的通信实体。 目前已经发表甚至投入实用的安全协议不少，但许多协议在发表甚至使用几年或十几年后， 却被发现存在安全漏洞。 例如s h a m i rr i v e s t a d e l m a n 三遍协议【6 7 ，该协议的消息序列如下： ( 1 ) a 呻b ： m ) k 。 ( 2 ) b _ a ：“m k a k b ( 3 ) a b ：f m k b 这个协议设计时的初衷是保证通信实体能够在不安全的通信频道传输数据，其特点是 通信实体之间事先不共享任何秘密，包括对称钥和公钥。通信实体只保存自己的一个密钥， 供加密和解密用，即通信实体x 加密和解密时都使用k x 。 启始者a 要与响应者b 共享秘密m ，就将m 用自己的密钥k a 加密传给b ：b 把接收 到的密文再用自己的密钥k b 加密，返回给a ；a 将其用k a 解密后，消息就成为以k b 为 密钥的密文，a 将其传给b ：b 用k b 解密，得到m ，完成认证，并且与a 共享了秘密m 。 这里的一个假定是：对m 进行多重加密解密时，得到的密文形式与加密解密顺序无关。即 “m k a k b = “m k b k a 。 这个协议存在一个漏洞【6 】：入侵者i 截留a 对的消息b ，通过重放、即不另行加密， 直接返回给a a 解密之后将自认为与b 共享的秘密m 传送给了入侵者i 。入侵者i 的攻 击序列如下： ( 1 ) a i ( b ) ： m ) k 。 ( 2 ) i ( b ) 一a ： m k 。 ( 3 )a _ i ( b ) m i 成功地冒充了响应者b ，与a 共享了秘密m 。 该协议的另一个漏洞是入侵者可以在冒充响应者b 接收a 的第一个消息后冒充b 以启始者的身份发起与a 的另一次协议。攻击序列如下： ( 1 ) a - + i ( b ) m k 。 ( 1 ) + i ( b ) - 4 , a ： m k a ( 2 ) + a - + i ( b ) m ( 2 ) i ( b 1 一a ：b o g u s 第1 0 页 国防科学技术人学研究生院学位论文 ( 3 ) a i ( b ) ： b o g u s k 。 可以看出，协议的设计者往往无法保证安全协议的f 确性，设计出的协议难免存在一 些漏洞。利用这些漏洞，入侵者可以轻松地冒充诚实的通信实体参与通信，窃取秘密。安 全协议的漏洞对网络中的通信安全已经构成了巨大的威胁。 既然任何协议在其使用过程中都有可能发现潜在的漏洞就是说发现那些在设计时没 有注意到的漏洞，那么我们就要想方设法对已经设计完成的协议进行分析检验，而不是只 停留在设计的层次上。在设计的层次上，可以制定无数的设计原则，但协议最终是要投入 使用的，所以对已经设计完成的协议进行分析检验是必不可少的工作。 第1 1 页 国防科学技术人学研究生院学位论文 法。 第三章安全协议的检验方法 安全协议有很多的检验方法。总的来说，可以分为两大类：非形式化方法和形式化方 3 1 非形式化方法 非形式化方法的特点是：检验时不把协议用形式化方法表示出来，而是采用直观的分 析检验方法f 8 1 。 最直接的非形式化方法是让实践来检验。就是说在设计完成后，将协议投入使用。在 大量的实践中，如果协议的确存在漏洞，在一定的时间内、在大量的实际应用中，一般会 被发现的。 但是这种方法是一种懒惰的、甚至是冒险的方法。前面绪论中已经详细阐述过协议漏 洞的危害，如果真的在实践中出现了漏洞，很多损失都是无法弥补的。例如，假定某操作 系统o s 已经采用某个协议p 进行网络通信中的身份认证，那么在使用中p 出现漏洞后 该操作系