（计算机科学与技术专业论文）认证协议设计与分析方法的研究.pdf

认证协议设计与分析方法的研究 摘要 开放网络和分布系统上不断增长的重要应用对系统安全提出了 l 更迫切的需求。身份认证系统作为系统安全、网络安全的第一道防线， 它的安全性对整个系统的安全具有十分重要的作用。实现身份认证的 方式有多种，其中最安全的方式是设计基于密码技术的身份认证协 议。许多认证协议在公布后被发现有漏洞，因此，如何保证认证协议 是安全的就成为协议研究者的重要任务。 好的认证协议往往需要在设计时有一定的协议设计原则指导，在 设计后能够通过某种方法分析协议满足期望的特性。认证协议分析方 法可分为形式化方法和非形式化方法两种。其中形式化方法能够更全 面、深刻地发现协议漏洞和证明安全性。协议形式化分析方法中影响 比较大的三种方法是：信仰逻辑方法、模型检测方法和定理证明方法。 信仰逻辑方法的主要优点是推理协议结构的新鲜性、使用简单、代价 低，但它不能推理其它安全特性如保密性；模型检测方法基于状态空 间搜索，可以迅速地发现一些简单的攻击，但它只能搜索有限的状态 空间，而且协议没有被发现攻击不能证明协议没有攻击；定理证明技 术使用归纳方法可以帮助发现协议更深层次的结构特性，但它的使用 代价很大。从目前协议分析领域的发展情况来看，三种方法结合分析 协议能够产生更有效的结果。信仰逻辑能够在协议设计阶段帮助确保 协议结构的新鲜性。当然三种方法结合使用的程度，是由协议使用者 需要的安全程度和在证明协议失败上投入的代价来决定的7 本文从协议设计者使用的简便性和大多数攻击与消息重放有关 两个方面出发，将信仰逻辑中主流的类b a n 逻辑作为本文的研究重 点。本文所做的工作主要有以下几点： 1 、对认证协议各种攻击手段进行了分析，从信息采集的角度， 提出了基于遍历的运行模式分析方法； 2 、针对类b a n 逻辑中最容易出错的两个方面即协议理想化阶段 和初始化假设阶段进行了深入地研究，提出使用协议上下文 语法敏感的规则推导方法对理想化过程中直观概念和形式化 概念之间转换的偏差进行修正。( 并通过创造新的规则对该方 法进行了完善和补充，提高了方法的正确性、扩大了方法的 使用范围。对于初始化假设导致逻辑分析基于不正确前提的 情况，文中指出：除非是协议执行前已经成立的、或当前环 境保证的假设，其它假设必须通过正确的推理或证明过程来 得到。文中的上下文敏感语法分析方法也帮助推理了一些曾 经导致著名协议分析出错的初始化假设j n 3 、研究表明，攻击在绝大多数情况下是利用协议中参与方名字、 新的会话密钥、新鲜性标识三者之间关联关系的漏洞以及协 议中出现结构一致的消息而成功实现的。文中针对性地提出 了几条新的协议设计指导原则。 4 、基于协议理想化规则和设计指导原则，本文设计了一个建立 i i 在对称密码体制上的认证协议基本模型n ( 另外，本文在类b a n 逻辑形式化方法中，增加了一些适合处理公 钥认证协议的符号定义和推理规则，并说明在协议分析时若基于公钥 、， 设计的消息满足一定的条件可以被转换成等价的对称钥消息o ) 本文还 针对电子商务应用中认证协议的效率问题进行了研究，并结合公钥和 对称钥的特点，对c c i t tx 5 0 9 协议从安全和提高服务器端性能两个 方面进行了改进设计。 关键词：认证协议，形式化方法，类b a n 逻辑，篷电子商务 1 1 1 r e s e a r c ho nd e s lg na n da n a l y s ism e t h o d s o fa u t h e n t ic a tio np r o t o c o l s a b s t r a c t t o d a y , m o r ea p p l i c a t i o n sr e q u i r et oe s t a b l i s hs e c u r ec o m m u n i c a t i o n o v e ri n s e c u r e o p e n n e t w o r k sa n dd i s t r i b u t e d s y s t e m su r g e n t l y a u t h e n t i c a t i o ni so n eo f t h em o s ti m p o r t a n tp r o p e r t i e si nn e t w o r ks e c u r i t y , i ti su s u a l l ye n s u r e db yd e s i g n i n ga u t h e n t i c a t i o np r o t o c o l sw h i c hu s e c r y p t o g r a p h i ct e c h n i q u e s u n f o r t u n a t e l y , t h e r ea r e s e v e r a le x a m p l e so f a u t h e n t i c a t i o np r o t o c o l st h a tw e r ep u b l i s h e d ，b e l i e v e dt ob es o u n d ，a n d l a t e rs h o w nt oh a v es e v e r a ls e c u r i t yf l a w s s o ，t h em o s ti m p o r t a n tt a s kt o r e s e a r c h e r si sh o wt oe n s u r es e c u r i t yo fa u t h e n t i c a t i o n p r o t o c o l s g o o da u t h e n t i c a t i o np r o t o c o l sn e e dc e r t a i np r i n c i p l e st oh e l pd e s i g n a n ds o m ea n a l y s i sm e t h o d st o v e i l f ye x p e c t e dp r o p e r t i e s a n a l y s i s m e t h o d sc a nb ed i v i d e di n t ot w oc a t e g o r i e s ，o n ei sf o r m a tm e t h o d ，t h e o t h e ri si n f o r l t l a lm e t h o d t h ef e i r m e rc a l ld i s c o v e rf l a w s c o m p r e h e n s i v e l ya n dp r o v es e c u r i t y i th a st h r e ek i n d so f m a i n t e c h n i q u e s ： b e l i e fl o g i c 。m o d e lc h e c k i n g ，a n dt h e o r e mp r o v i n g b e l i e fl o g i cm i g h t h e l pe n s u r ef r e s h n e s sp r o p e r t i e sd u r i n gt h ed e s i g np h a s e ，a n d i ti se a s yt o u s e m o d e lc h e c k i n gm i g h tp i n p o i n ts i m p l ef l a w sq u i c k l yb ys e a r c h i n g s t a t es p a c e b u ti tc a r lo n l yd e a lw i t hl i m i t e ds t a t e s 。a n di ft h i st e c h n i q u e d i s c o v e r sn of l a w , i td o e s n tm e a nt h a tt h ep r o t o c o li ss e c u r e t h e o r e m p r o v i n gc a nh e i p u s p r o v ed e e f e r s t r u c t u r a i p r o p e r t i e sb y i n d u c t i v e m e t h o d b u ti ti sc o s t l y s of a r , ac o m b i n a t i o no ft h r e et e c h n i q u e sm i g h t y i e l d t h eb e s tr e s u l t s h o w e v e r ，t h e d e g r e e o fac o m b i n a t i o ni s d e t e r m i n e db yu s e r sw h ow i l lb a l a n c es e c u r i t ya n dc o s t i n 协i sp a p e r o u rr e s e a r c hf o c u s e so na n a l y s i so fb a n 1 i k el o g i c o n er e a s o ni st h a tt h et e c h n i q u ei se a s yf o rp r o t o c o ld e s i g n e r st ol e a r n t h eo t h e rr e a s o ni st h a tm a n yp r o t o c o la t t a c k sa r eb a s e do nm e s s a g e s r e p l a y m y m a i nw o r k sa r el i s t e da sf o l l o w s 1 ，b ya n a l y z i n g v a r i o u sa t t a c k so na u t h e n t i c a t i o np r o t o c o l s a n a n a l y s i s m e t h o da b o u t r u n n i n g m o d e so ft h e p r o t o c o l s i s p r o p o s e d 。w h i c hw i l l s e a r c ha l li n f o r m a t i o nt h a ta t t a c k e rc a n c o l l e c t ； 2 t w o a s p e c t s o fb a n i i k e l o g i c ， i d e a l i z a t i o na n di n i t i a l a s s u m p t i o n s ，a r ep r o n et oe r r o r t om a k ep r o t o c 0 1i d e a l i z a t i o n p e r f e c t ，a c o n t e x t - s e n s i t i v em e t h o di su s e d t or e d u c et h e d e v i a t i o nd u r i n g 订a n s f o r m a t i o nf r o m d i r e c t d e s c f i p t i o n t o i d e a l i z e dp r o t o c 0 1 an e wr u l ei sc r e a t e dt oi m p r o v et h i sm e t h o d s ot h a tt h ec o r r e c t n e s so ft h em e t h o di se n s u r e d t oe n s u r ei n i t i a l a s s u m p t i o n s 。w er e q u i r et h a ta l lt h ea s s u m p t i o n sm u s t b ep r o v e d e x c e p tf o rw h a t h a v eb e e n g u a r a n t e e db e f o r ec u r r e n tp r o t o c o lr u n i nt h i s p a p e r , s o m ea s s u m p t i o n s c a nb ed e d u c e d b y t h e c o n t e x t - s e n s i t i v em e t h o d 3 s e v e r a ln e wg u i d i n g p r i n c i p l e s a r e p r o p o s e d t o h e l pd e s i g n a u t h e n t i c a t i o n p r o t o c o l s t h e s ep r i n c i p l e s a r er e l a t et ot h e m e s s a g e s s t r u c t u r e sa n d t h ea s s o c i a t i o na m o n gt h es e s s i o n k e y ， t h ef r e s hi d e n t i f i e ra n dn a m e so f p r i n c i p a l s o u rr e s e a r c hs h o w s t h a tm a n ys u c c e s s f u la t t a c k sc a l le x p l o i tt h e s et w o a s p e c t s 4 w i t ht h er u l e so fi d e a l i z a f i o na n dt h eg u i d i n gp r i n c i p l e s ，ab a s i c m o d e lo fa u t h e n t i c a t i o n p r o t o c o l s b a s e do n s y m m e t r i c c r y p t o g r a p h y i sp r o p o s e d i na d d i t i o n ，s o m es y m b o l i cd e f i n i t i o na n di n f e r e n c er u l e sa r ea d d e d t ob a n l i k el o g i ct oh e l pa n a l y z ep u b l i c k e ya u t h e n t i c a t i o np r o t o c o l s i n o r d e rt os i m p l i f yt h ea n a l y s i so f p u b l i c k e yp r o t o c o l s ，w et r a n s f o r ms o m e m e s s a g e si np r o t o c o l s t oe q u i v a l e n tt b r m s u s i n gs y m m e t r i cc r y p t o g r a p h y m o r e o v e r ，t h e e f f i c i e n c y o fa u t h e n t i c a t i o n p r o t o c o l s i ne l e c t r o n i c c o m m e r c ei sc o n s i d e r e di nt h i sp a d e r w i t h c o m b i n i n gt h ea d v a n t a g e so f p u b l i c k e yc r y p t o g r a p h ya n ds y m m e t r i cc r y p t o g r a p h y , w eh a v ei m p r o v e d t h es e c u r i t ya n d p e r f o r m a n c e o fc c i t tx 5 0 9p r o t o c 0 1 k e yw o r d s ：a 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 lm e t h o d ，b a n - l i k e l o g i c ，s e c u r i t y ，e l e c t r o n i cc o m m e r c e v 上海交通大学 学位论文版权使用授权书 本学位论文作者完全了解学校有关保留、使用学位论文的规定， 同意学校保留并向国家有关部门或机构送交论文的复印件和电子 版，允许论文被查阅和借阅。本人授权上海交通大学可以将本学位 论文的全部或部分内容编入有关数据库进行检索，可以采用影印、 缩印或扫描等复制手段保存和汇编本学位论文。 保密口，在一年解密后适用本授权书。 本学位论文属于 不保密囱。 ( 请在以上方框内打“”) 学位论文作者签名： 纭勇 日期：。口2 年3 月) 蝈 指导教师签名 上海交通大学 学位论文原创性声明 本人郑重声明：所呈交的学位论文，是本人在导师的指导下， 独立进行研究工作所取得的成果。除文中已经注明引用的内容外， 本论文不包含任何其他个人或集体己经发表或撰写过的作品成果。 对本文的研究做出重要贡献的个人和集体，均已在文中以明确方式 标明。本人完全意识到本声明的法律结果由本人承担。 学位论文作者签名：分式旁 日期：上一。上年3 月z 砂日 第六章基于效率的认证协议设计9 8 6 1x 5 0 9 认证协议改进设计9 8 6 i 1 协议原型9 9 6 1 2 协议改进1 0 0 6 1 3 协议安全性分析1 0 1 6 1 4 协议性能评估1 0 5 6 2d 、结一1 0 6 第七章总结和展望- - 1 0 7 7 1 全文工作总结1 0 7 7 2 进一步工作展望1 0 8 参考文献一1 0 9 附录a ：实验数据一1 2 5 附录b ：名词注释表1 2 6 致谢1 2 7 作者读博期间主要研究课题和撰写的论文1 2 8 图表索弓 图1 图2 - 图3 一 图6 主体分类图 集成的协议环境一 简单并行会话攻击 x 5 0 9 三向身份认证协议 2 2 1 3 9 9 9 符号说明 一、主体符号分类 r ：任意主体； p 、0 、a 、b 、c 、t ：一般主体的名字 s ：服务器名字； l 、z ：攻击者名字； a s ：证书权威机构； 二、密钥符号分类 s 。、s 。：对称钥的加、解密操作符； p 。、p 。：公钥的加、解密操作符； k ：一般意义上的密钥：在对称密码体制下，加解密钥相同都为k ：在公钥密码体制 下，k 对应的私钥为k ： k 月：主体p 、主体q 之间的共事密钥； k 阳 ( 或k 哪) 、k 曲( 或k 幻) 、k 曲( 或k 缸) ：主体s 和a ，a 和b ，s 和b 2 _ n 的共享密钥； 注；k 。也表示证书权碱机构a s 的公钥根据文中的密钥甬途区分， k p 、k q 、k 。、k 6 、k ，：主体p 、q 、a 、b 、s 的公钥； k ；1 、k ；1 、k 、k ；1 、k ：1 ：主体p 、q 、a 、b 、s 的公钥对应的私钥； 三、其它符号定义 m ：消息； x 、y ：泛指消息公式； x 。、y 。：指主体a 的消息； x ，y ：公式x 和y 的串联 c a 、c b ：主体a 、b 对应的证书： ! = ：不等于； n 。、n b ：主体a 、主体b 产生的随机数，一种用于验证协议新鲜性的一次性临时值 形式： x t 。、t 。：主体a 、主体b 产生的时间戳，一种用于验证协议新鲜性的一次性临时值 形式： “p q ：消息”：是协议中每一步消息被发送的典型形式，表示p 发送消息给q ： 【x ) k ：是消息加密的基本形式，表示使用密钥k 对信息x 加密： i x k ：表示使用私钥k 。对消息x 进行签名； x 。y ：表示两方密码协议中x 是发起方，y 是响应方 p ( q ) 表示在协议执行时主体p 假冒成q ； g ( a ：b ) ：表示用密钥a 对消息b 进行加密。 四、与类b a n 逻辑相关的符号定义 p ；x ：表示p 相信x ： pi x ：p 说过x ，即p 发送过包含x 的消息： p 司x ：p 看到x ，即p 接收到包含x 的消息； pj x ：p 控制x ，即p 对x 有仲裁权，x 可以绝对信任p ； p 、q 共享密钥k ，若k 是好的密钥，则除p 、q 以及p 、q 共同信任的主体 其他人都不可能知道k ； x 、y 的组合； x ) ：表示用密钥k 对x 进行加密； # ( x ) 或f r e s h ( x ) ：x 是新鲜的，即x 在这以前没有出现过 k i - - p ：密钥k 是p 的公钥； x p = q ：x 是只被主体p 、q 知道的秘密。 j k 占随砩 p 年 双向认证协议，如g o n g 双向认证协议 7 4 1 。 ( 4 ) 根据认证胁议实现的功能分为两种： g l ：身份认证协议只保证参与方在认证过程中具备正确的身份，而不保证认 证过程之后参与方之间通信的身份鉴别性和私密性： g 2 ：身份认证协议在认证参与方身份的同时，分配了参与方共享的秘密会话 钥，用于保证未来通信的身份鉴别性和私密性。 在实际系统中，身份认证之后往往是数据信息的交互过程，这就需要一定的机制来保证 整个通信过程中各参与方的合法身份。g 2 类型的认证协议通过在认证过程中分发新的共享 会话钥对随后通信中参与双方交互的信息进行加密，有效地实现了这一目标。同时义保证了 交互信息的私密性。因此，本文把g 2 类型的认证协议作为重点分析的对象。 认证协议是安全通信的基础，因此协议是否被正确实现将直接关系到整个系统的安全。 虽然，系统的安全还与其它一些因素如密码算法的强度c 6 5 j 相关，但在本文我们不打算对这 些方面进行讨论，而假设它们满足安全的需求。由于i n t e r n e t 设计者的初衷是考虑资源共 享，因此i n t e r n e t 是一个充分开放的网络，t g p i p 协议中没有涉及任何安全内容，这使得 网络环境一般是不安全的，很容易成为各种各样攻击的目标。攻击者可能是一些合法成员， 他们能够读、修改和删除事务，甚至能够控制系统，也可能是竭力破坏协议设计目标的敌意 入侵者 8 8 】。在不安全网络中，根据主体行为可以把主体划分为两类：可信主体和不可信主 体( 参见图卜1 模型) 2 8 。可信主体的行为与期望的行为一致，不可信主体的行为与期望 的行为不一致，往往破坏协议，然而其他主体却认为该行为是正确的。 区 2 囡 p r i n c i p a l sw i t h o u ti n t r u d e r p r i n c i p a l sw i t hi n t r u d e ra n de n v i r o n m e n t ( a ) ( b ) 图卜1 主体分类图 f i g u r e1 1 a t a x o n o m yo fp r i n c i p a l s 同样，判定密码协议实际提供的安全与协议在设计时被要求的安全是否一致也是一件很 困难的事情 7 0 。即使忽略以下两种情况的攻击：( 1 ) 通过快速破译代码实施的攻击：( 2 ) 2 卜海交通大学博士学位论文 协议实现过程中产生的缺陷，协议仍经常受到些攻击，这些攻击即使经过仔细检奇也是不 易被发现的，这种攻击在协议运行的环境发生变化时出现的可能性更大。目前协议设计者已 经设计出很多密码协议，但许多协议在发表后不久就被发现有漏洞。n s 认证协议 9 9 1 在1 9 8 1 年被d e n n i n g 和s a c c o 发现存在以下安全缺陷 9 8 1 ：当主动攻击者用一个已被破译的旧会话 密钥冒充新的会话密钥时，形成了有效攻击。当然，认证防议的攻击手段还有许多，如 9 2 1 中指出的n s 公钥协议在假设通信一方是不诚实时将受到插入攻击 4 0 】、【1 5 】中指山的反射 攻击以及其它情况下的协议失败 6 5 1 1 等等。据g a v i nl o w e ( 对协议失败进行研究的著 名专家) 估计，一半以上的公开协议事实上不能保证它们的安全设计目标 6 6 。 造成密码协议失败的最主要原因是协议的设计者对安全需求的定义研究得不够透彻 f 7 0 1 、缺乏避免密码协议失败的专门技术( 6 0 ，以及对设计出来的密码协议缺乏足够的安全 分析和验证。另个原因是目前还没有一套成熟的理论作为密码协议设计的指导原m u 9 7 1 。 这两方面原因都造成了认证协议容易出错达不到预期的设计要求。因此，我们很有必要对 设计的认证协议进行分析，判断它们是否符合设计要求、能否达q 预定的安全目标。为此， 本人博士期间主要研究如何分析和设计安全的认证协议。 1 2 密码技术概述f 1 0 8 l 认证协议基于的密码体制大体上可分为两种：对称密码体制和公钥密码体制【1 0 9 1 f 1 1 0 1 。 对称密码体制中数据的加密和解密采用相同的密钥，这个密钥是通过安全的方式建立的，在 大型分布式系统中往往是通过k d c ( 密钥分配中心) 进行密钥分发。在d 个用户进行保密 通信的系统中，共需要分发n + ( n - 1 ) 2 个对称密钥，常见的对称密码算法有d e s 9 1 1 、i d e a 等。在公钥密码体制中，数据的加密和解密采用不同的密钥，公钥被存放在大家都能访问到 的一个地方( 如l d a p 服务器) ，用户拥有自己的私钥并负责保证该密钥的私密性从公钥 推导对应的私钥在计算上是不可行的。在n 个用户进行保密通信的系统中，共需要分发n 个密钥。在实际使用的场合，往往利用证书权威机构颁发的公钥证书来证明被认证主体的公 钥和身份。常见的非对称密码算法有r s a 1 0 8 1 1 0 、数字签名标准d s s 9 0 等。在密钥分 发量方面，相同用户规模的网络使用非对称密码系统大大减少了密钥分配量；而在处理速度 方面，对称算法比公钥算法要快得多，因此大规模网络系统密钥分配方案多采用公钥体制， 而在加密大量数据时往往采用对称算法。另外，公钥算法还能提供数字签名功能。对于常见 的认证系统而言，大多数系统基于对称密码体制。而大型分布系统的认证往往是通过有全局 目录的本地网认证实现的( 例如，基于x 5 0 0 目录 8 9 ) ，系统使用公钥密码术 6 7 【6 8 儿6 9 j 的开放认证结构。在电子商务系统中，x 5 0 9 【1 0 2 】三向强认证协议就是基于公钥密码体制实 现的。本文在讨论公钥密码协议时，总假定c a ( 证书权威机构) 是可信任的。 1 3 认证协议的分析方法 身份认证协议的安全主要包括两个方面：一致性和保密性。我们用以下两个协议来帮助 理解。 3 上海交涵人学博士学位论立 单同认证协议1 ： ( 1 ) p q ：p ， k k ( 2 ) q p ：q ， k ) k 月 由于( 1 ) p z ( q ) ：p ， k ) k w ( 2 ) z ( q ) 一p ：q ， k k 此协议中会话钥k 的保密性得到了保证，但身份认证的一致性却是失败的。 单向认证协议2 ： ( i ) p q ：p ， k ，p ) k ：1 ( 2 ) q p ：q ， k ，q k ：1 由于( 1 ) p z ( q ) ：p ， k ，p k ? ( 2 ) z ( p ) 一q ：p ， k ，p k ：1 z 从( 1 ) 中得不到消息 k ，q ) k ：1 ( 3 ) q p ：q ， k ，q k ： 此协议的设计目标之一是分配一个只被p 、q 共享的密钥k ，但由于k 是公开的，攻 击肴z 若在协议执行中截获第一条消息，就能够得到此共享密钥k ，因此协议满足了身份 认证的一致性，但会话钥k 的保密性却是失败的。 判定协议是否取得保密性( 即不暴露机密信息给台法接收者之外的任何人) 、是否执行 了正确的身份认证( 即相互证实对方身份的真实性) 这两个基本目标，或者说判定协议是否 能够被具备截获、重放、修改消息能力的主动搭线者破坏，是一个十分困难的问题 8 7 。 协议分析是揭示认证协议存在漏洞的重要途径。在分析认证协议的安全时，常用的方法 是攻击检测方法，即对认证协议施加各种可能的攻击来测试其安全陛 4 0 1 1 1 4 1 1 9 4 1 。认证协 议分析主要从三个方面进行：( 1 ) 协议中采用的密码算法：( 2 ) 算法和协议中采用的密码方 案；( 3 ) 协议本身。对密码算法和密码方案的研究不是本文的主题，本文主要研究第三种情 况即对协议本身的攻击，而假设协议中采取的密码算法和密码方案均是安全的。 对协议本身的攻击可以分为：( 1 ) 被动攻击；( 2 ) 主动攻击。两者的最大区别在于： 被动攻击者往往是对协议执行的部分或整个过程实施窃听，但并不影响协议的执行；而主动 攻击者试图改变协议执行中的某些消息以达到获取信息、破坏系统或获得对资源非授权访问 的目的。因此，主动攻击对密码协议来说具有更大的危害性。 对认证协议进行分析的攻击检测方法是一种非形式化的分析方法，它是早期密码协议分 析的主要研究方法。该方法的成功很大程度上要依赖于已知的各种攻击方法对协议攻击的有 4 上海交通大学博士学位论文 效性。事实上，我们不可能发现针对认证协议的所有攻击方法，这种非形式化分析方法只能 通过发现协议中存在已知的缺陷而证明协议是不安全的，而不能用于证明协议是安全的，因 此它无法全面客观地分析密码协议，很容易导致不安全的协议经分析是安全的错误结论。 另外一种分析方法是对认证协议进行形式化分析 1 1 l 】 1 1 2 1 1 1 1 3 】【1 1 4 1 1 5 】【1 1 6 1 1 7 】 1 1 8 f 1 1 9 1 ，这在八十年代末九十年代初开始成为研究热点。这种方法的出发点是希望将认 证协议形式化，而后借助于人工推导，甚至计算机的辅助分析，来判别密码协议是否安全可 靠。这种方法和一般的非形式分析方法相比，它能全面、深刻地检测到认证协议中细微的漏 洞。形式化分析方法不仅能发现现有的攻击方法对协议构成的威胁，还能在分析过程中发现 认证协议存在的新漏洞，从而不断地丰富认证协议的攻击方法集合。 1 4 论文章节安排 本文结合国家9 7 3 课题“信息与网络安全体系结构研究”( 编号：g 1 9 9 9 0 3 5 8 0 i ) 、国家 重点科技项目( 攻关) 计划“信息网络的安全测评技术”( 编号：2 0 0 0 a 3 2 0 6 ) 、国家自然 科学基金项目“双向认证系统的研究及i n t e m e t 上的电子支付系统”( 编号：# 6 9 7 7 3 0 1 3 3 、 国家八六三计划“安全电子支付系统中的关键技术”( 编号：8 6 3 3 0 6 z t 0 2 0 6 3 ) ，对身份 认证协议分析和设计的形式化方法进行了研究。 以下是本论文内容的安排情况： 第一章： 从网络通信和i n t e m e t 上不断增长的重要应用对安全的迫切需求出发，提出研究系 统安全的第一道屏障身份认证技术。在分析了各种形式的身份认证方法以后， 进一步明确本文的主要研究内容是如何保证基于密码体制的身份认证协议的安全。 对认证协议安全的两种分析方法( 非形式化方法和形式化方法) 进行了比较，指出 形式化分析方法能够较全面、深刻地检测协议漏洞和证明协议安全。 第二章： 介绍密码协议分析阶段各种形式化方法的发展概况，并说明目前结台使用信仰逻 辑、模型检查和定理证明这三种主流的形式化方法分析协议能够产生最好的结果； 介绍密码协议设计阶段各种形式化方法的发展概况： 介绍当前在协议分析过程中使用的几种主要的形式化描述语言和分析工具。 第三章： 从认证协议受到的各种攻击案例入手，试寻找种能够帮助协议分析者尽可能地找 出协议缺陷的方法。提出了基于遍历的非形式化分析方法。 通过分析复杂的协议攻击方法，进步指出非形式化方法难以满足对各种情况攻击 的分析，只在一定程度上证明了协议的安全。而逻辑分析方法尽管在目前尚有一些 问题，但由于它的发展趋势是语义上的严格证明，因此只要协议理想化过程得当、 前提假设可信，就可以避免许多凭经验做判断带来的失误，证明过程更严密、更科 学和更准确a 因此，开发简单而有效的形式化分析方法应该是今后认证协议分析的 s 上海交通大学博士学位论文 主流方向。 第四章： 基于协议设计者使用的简便性和认证协议中最常见攻击是消息插入和重放两个方 面，提出以简单易用的信仰逻辑作为本文的研究重点，通过对逻辑方法的完善来 帮助协议设计者迅速地解决许多协议缺陷。 通过对类b a n 逻辑方法的分析，指出了该类方法的缺陷主要在弥议理想化和初始 化假设两个阶段。 案例分析说明这两个阶段的问题又多与理想化过程中忽略协议上下文的内容有 关，因此提出理想化阶段要使用上下文敏感的语法分析方法，并对已有的方法进 行了规则增加和完善，使得理想化过程更好地消除了协议直观定义和形式化定义 之间的语义偏差，使用面更广。 通过以上的理想化方法，推出了部分合理的初始化假设，而这些假设在以往的逻 辑证明中往往是导致错误的地方。 第五章： 提出了认证协议设计时最基本的几条指导原则。 针对公钥密码体制的特点，扩充了类b a n 逻辑中定义的逻辑符号集。 没计了三方认证协议的基本模型。 第六章： 针对现实世界中一些应用领域如电子商务对认证协议的高性能需求，结合 ( 1 ) 公钥密码技术密钥分配的便利性和防抵赖的特点； ( 2 ) 对称密码技术的高性能； 从安全和性能两个方面改进设计了x 5 0 9 协议。 第七章： 对全文的工作进行总结： 提出下一步的研究目标。 6 上海交通大学博上学位论文 第二章形式化方法进展 形式化方法在密码协议安全的分析过程中是非常有用的。n e e d h a m 和s c h r o e d e r 在 9 9 】 中最先提出协议错误在正常操作下不太可能被检测出来，需要验证协议正确性的技术【2 9 】。 最先在这个领域开展工作的是d o l e v 和y a o 7 2 、稍后是d o l e v 、e v e n 和k a r p 7 3 1 ；他们在 七十年代末、八十年代初开发了一组多项式时间算法来确定一类受限制协议的安全。d o l e v 和y a o 的工作是十分重要的，第一次开发了协议的多个执行并发运行环境的形式化模型， 以后的绝大多数密码协议形式化分析方面的工作基于这个模型或该模型的变种。 到目前为止，已有许多工具和技术被设计用来分析和验证密码协议的安全。如：b a n 逻辑 5 】、形式化说明语言【2 1 7 】、自动程序如n r l 和i n t e r r o g a t o r 1 1 6 ，和有色p e t r in e t s 2 1 8 】、 【7 9 】、 2 1 9 、【8 0 l 。这些技术的共同特征是强调协议的设计而不是协议中密码算法的强度。 协议失败 6 5 】的分析方法主要可分为三种 8 6 】： l 、构造推理方法。此方法使用基于信仰概念的专门逻辑构造证明，信仰指主体能够秘 密地得到期望的认证结论，试图通过证明失败指出协议的漏洞 1 5 1 0 4 6 ； 2 、构造攻击方法。它利用协议中使用算法的代数特性构造可能的攻击 4 0 11 4 9 4 ； 3 、构造证明方法。此方法从攻击者控制的网络行为的现实模型构造协议不失败的证明 7 5 7 6 7 7 ； 构造推理方法利用模态逻辑，逻辑与分布系统中分析知识和信仰变化的逻辑很类似。构 造推理方法被广泛使用在 5 】【1 4 6 】，许多特定的问题与它们关联【1 0 】【1 5 2 】【1 1 8 】 1 5 3 1 5 4 ， 这些问题涉及：零知识协议的分析、并行会话多角色缺陷的检测、消息和命题到理想化消息 的转换、逻辑没有完备语义的事实、以及新鲜性的建模。 构造攻击方法基于协议算法的代数特性构造了可能的攻击集合。这些方法【7 2 】【1 3 2 4 0 】 】5 5 】 】1 4 1 1 5 6 8 5 1 5 7 1 1 1 5 8 1 1 1 2 5 】的目标是确保协议具有身份认证、正确性或安全特性； 方法与被提议逻辑的正确性无关。它们的主要缺陷是必须检测大量的可能事件。 构造证明方法是第三种分析协议失败的方法。它被产生的目标是避免构造攻击方法的指 数级搜索，把协议分析的范围扩展到可以涉及任意多的参与方和消息。它在寻找可能的攻击 时，与构造攻击方法同样的彻底，同时它采用搜索定理替换搜索而避免了指数级的搜索。构 造证明方法也是基于假设和认证特性的问题形式化，它是对构造推理方法的补充，但它依赖 于特定问题的特性和更精确的描述。构造证明方法形式化建模了协议中执行的实际计算，并 证明了关于这些计算的定理。s n e k k e n e s 在【1 3 0 】中、b o l i g n a n o 和p a u l s o n 在 7 5 4 1 1 1 7 6 以 及b r a c k i n 在【1 5 9 】中采用了这种方法。 当然，还有其它通用的形式化分析方法，如使用p e t r i 网的形式化分析和证明密码协议 的方法【7 8 l 【7 9 】【8 0 1 和最弱前置谓词分析方法1 3 5 】。 下面我们进一步说明协议安全分析的三种主要形式化方法。 1 上海交通人学1 尊上学位论文 2 1 构造推理方法 构造推理方法利用模态逻辑技术，此逻辑与分布系统中分析知识和信仰变化的逻辑相类 似。1 9 8 9 年，b u r r o w s ，a b a d i 和n e e d h a m 设计了第一个说明和验证密码协议的信仰模态逻 辑b a n 5 1 2 0 i ，该逻辑被广泛使用于认证协议的分析。b a n 信仰逻辑属于k d 4 5 模态逻辑 一类，此类逻辑实际上意味着任何事实只是一种信仰，不必在时间和空间上是普遍适用的。 它假定认证是完整性和新鲜性的函数，在协议中使用逻辑规则跟踪这些特征。使用b a n 逻 辑分析协议有三个主要阶段： 第一步是把假设和目标表达为符号语句，使得逻辑能够从一个已知的状态进行到另外一 个状态，在该状态下逻辑能够探知目标事实上是否被实现； 第二步是协议的每一步转换成符号表达式； 最后，应用一组称之为公理的推导规则。公理从假设开始，经由中间的公式，得到认证 目标。 b a n 逻辑主要解决了以下四个方面的问题： ( 1 ) 这个协议能正常工作吗? ( 2 ) 这个协议确切而成功地完成了吗? ( 3 ) 这个协议需要比其它协议更多的假设吗? ( 4 ) 这个协议是否做了一些多余的事情? 例如，在不降低认证协议安全程度的前提下， 是否加密了一些可以用明文传送的信息。 b a n 逻辑通过分析协议参与主体的信仰回答了以上问题，它从认证协议的基本假设出 k f 发，通过逻辑推理得到认证主体的信仰：如一级信仰a - - = a b ，b | = a b ，和二级信 kr 仰a1 一b j a o b ，b f = al a t b 。这样就得出了认证主体之间的逻辑信仰关系，进 而得出认证协议是正确的结论。因为b a n 逻辑是一组非常简单、直观的规则集组成的，所 以该逻辑使用起来非常容易。 自b a n 逻辑被提出以来，它成功地发现了许多著名认证协议的缺陷，如 n e e d h a m - s c h r o e d e r 9 9 】和c c i t tx 5 0 9 1 1 0 2 】协议。它也发现了许多协议的冗余，如 n e e d h a m - s c h r o e d e r ，k e r b e r o s 5 9 ，o t w a y - r e e s 6 2 和c c i t tx 5 0 9 1 0 2 坍议。许多发表的 文章中也使用b a n 逻辑来