（计算机应用技术专业论文）基于线空间模型的安全协议形式化分析.pdf

东南大学博士学位论文 摘要 安全协议，又称密码协议，是指运行在计算机网络或者分布式系统环境下，依赖应用密 码学技术完成身份认证、密钥分配或者电子交易等任务的协议。它的正确性是网络和分布式 系统应用安全的基础，针对这些协议进行形式化分析长期以来一直是安全领域的重要研究课 题。 安全协议形式化分析的目标是协议的关联性、保密性，以及与电子商务相关的不可否认 性，公平性和时限性等，论文的研究工作主要针对其中的基本属性关联性和保密性展开。 大部分已有的分析方法或者采用信仰逻辑等推理技术，或者采用状态检测等定理证明技术， 前者分析能力较弱，而后者存在状态爆炸问题。因此。目前研究的一个趋势是综合应用多种 分析手段，取长补短，以达到晟好的分析效果。与之相对应，论文提出了一种新的基于挑战 一响应的分析方法，该方法采用线空间模型作为底层的语义模型、采用认证逻辑作为基本分 析手段，并融合了a t h e n a 算法、认证测试等多种技术。全部研究内容可以划分为四个层面， 分别是建立语义模型、提出分析手段、设计自动化工具和协议分析应用。 在语义模型方面，采用线空间模型作为底层语义模型，给出了协议关联性和保密性的明 确的形式化定义。将保密性分析分解为显式泄密和隐性泄密问题，其中隐性泄密分析依赖于 关联性的判断；而关联性的分析被总结为协议s t r a n d 之间的存在关系和s t r a n d 参数的一致性 问题。 在分析手段方面，充分利用认证逻辑，a t h e n a 算法、认证测试等现有研究成果，并从中 提取出新鲜性、唯一生成，测试和n o n c e 验证等共有的概念，指出安全协议本质上是协议主 体采用密码学方法通过挑战一响应来对协议其他方的存在做出判断。同时完成一些数据如会 话密钥的协商的过程，挑战一响应是协议分析中最小的有效单位。在此基础上，提出了一种 新的形式化分析方法。 在自动化工具方面，采用p r o l o g 语言设计并实现了一个基于认证逻辑的协议分析工具， 可以有效推导并判断协议在特定的目标上是否满足需求，在自动化工具设计领域进行了初步 但有益的尝试。 在协议分析应用方面，针对五个具有代表性的安全协议给出了形式化的分析。对于有缺 陷的协议，给出了错误的根本原因和可能导致的攻击；对于正确的协议，给出了形式化的理 论证明。通过实际应用，演示并验证了论文所提理论和方法的正确性和有效性 总的来说，论文针对安全协议的形式化分析进行了深入的研究，提出的方法很好地解决 了分析能力和易操作性之间的平衡问题，新的分析方法既具有线空间模型的分析能力，又具 有认证逻辑方法的易用性。 关键字：网络安全协议分析挑战一响应线空间模型 a b s t r a c t a b s t r a c t s e c u r i t yp r o t o c o l s ，a l s oc a l l e dc r y p t o g r a p h i cp r o t o c o l s ，a r ep r o t o c o l st h a tu s ec r y p t o g r a p h yt o a u t h e n t i c a t ep r i n c i p a l s d i s t r i b u t ek e y so rt r a u s a e te l e c t r o n i cb u s i n e s s f o rt h e i rc o r r e c u l e s sa r et h e t h e o r e t i c a lb a s i so ft h es e c u r i t yf o ri n t e r a c ta p p l i c a t i o n sa n dd i s t r i b u t e d s y s t e m s ，t h ef o r m a l a n a l y s i sh a sb e e nah o tr e s e a r c ht o p i cf o ral o n gt i m e t h eo b j e c t sf o rf o r m a la n a l y s i sa l ep r o t o c o l s s e c u r i t yp r o p e r t i e si n c l u d i n gc o r r e s p o n d e n c e ， s e c r e c y , e l e c t r o n i cc o m m e r c er e l a t e dn o n r e p u d i a t i o n , f a i r n e s sa n dt i m e l i n e s s t h ew o r ki nt h i s d i s s e r t a t i o no n l yf o c u s e st h ef u n d a m e n t a ls e c u r i t y p r o p e r t i e s ，i e c o r r e s p o n d e n c ea n ds e c r e c y , m o s to f t h ee x i s t i n gf o r m a lm e t h o d sa d o p te i t h e rt h er e a s o n i n gt e c h n o l o g i e ss u c ha sb e l i e f l o g i e so r t h e o r e mp r o v i n gt e c h n o l o g i e ss u c ha ss t a r ee x p l o r a t i o n , a n df a c et h ep r o b l e m so fw e a ka n a l y s i s p o w e ra n ds t a t ee x p l o s i o np u z z l e sr e s p e c t i v e l y t os o l v et h ep r o b l e m s ，o n eo f t b en e w t r e n d so f t h e r e s e a r c h e si st h es y n t h e s i z i n go fd i f f e r e n tt e c h n i q u e sf o rb e s te f f e c t s a c c o r d i n gt ot h i s ，an e w m e t h o db a s e do nc h a l l e n g e - r e s p o n s ei sp r o p o s e di nt h i sd i s s e r t a t i o n , w h i c ha p p l i e ss t r a n ds p a c e m o d e la su n d e r l y i n gs e m a n t i cm o d e la n da u t h e n t i c a t i o nl o g i c b a s i ca n a l y s i sm e t h o d s o m eo t h e r t e c h n i q u e si n v o l v e db ya t h e n aa l g o r i t h ma n da u t h e n t i c a t i o nt e s t sa r ea l s oa p p l i e d t h ew h o l ew o r k i n c l u d e sf o u rp a r t s ，笛e s t a b l i s h m e n to fs e m a n t i cm o d e l ，p r o p o s a lo fa n a l y s i sm e t h o d ，d e s i g no f a u t o m a t i ca n a l y s i st o o l ，d e m o n s t r a t i o na n da p p l i c a t i o n so f t h en e wt h e o r y s t r a n ds p a c em o d e li sa p p l i e d 笛t h eu n d e r l y i n gs e m a n t i cm o d e l b a s e do nw h i c hc l e a rf o r m a l d e f i n i t i o n so fc o r r e s p o n d e n c ea n ds e c r e c ya r eg i v e n t h ea n a l y s i so fs e c r e c yi ss p l i ti n t ot w op a r t s e x p l i c i t - i n f o r m a t i o n l e a k a g ea n a l y s i sa n di m p l i c i t - i n f o r m a t i o n l e a k a g ea n a l y s i s ，w h i l et h e l a t t e ri sb u i l tu p o nc o r r e s p o n d e n c ea n a l y s i s a n dt h ec o r r e s p o n d e n c ei sc o n c l u d e d 髂t h ee x i s t e n c e r e l a t i o n s h i po f s t r a n d sa n dt h ea g r e e m e n to f s t r a n dp a r a m e t e r s an e wm e t h o db a s e do nt h es e m a n t i cm o d e la n df o r m a ld e f i n i t i o n si sp r o p o s e dh e r e w h i c h s y n t h e s i z e st h ei d e a so fs o m ee x i s t i n gm e t h o d si n c l u d i n ga u t h e n t i c a t i o nl o g i c ，a t h e n aa l g o r i t h m , a u t h e n t i c a t i o nt e s t sa n de t e s o m ec o m m o nc o n c e p t so ft h e s er e s e a r c h e ss u c ha sf r e s h n e s s , u n i q u eo r i g i n a t i o n ，t e s t sa n dn o n c ev e r i f i c a t i o na r ea b s t r a c t e d ，b a s e do nw h i c hf o r m a ld e f i n i t i o n o fc h a l l e n g e r e s p o n s ei sp r o p o s e d a st h er e s u l t , s e c u r i t yp r o t o c o li ss p e c i f i e da st h ep r o c e d u r eo f c h a l l e n g e r e s p o n s eu s i n ga p p l i e dc r y p t o g r a p h y , n o to n l yt oc o n f i r mt h e e x i s t e n c eo fo t h e r p r i n c i p a l sb u ta l s ot on e g o t i a t ea b o u ts o m ed a t as u c h 笛s e s s i o nk e y s c h a l l e n g e r e s p o n s ei st h e m i n i m a la n de f f e c t i v eu n i tf o ra n a l y s i s as i m p l el o g i cb a s e da u t o m a t i ca n a l y s i st o o li sa l s op r o p o s e di nt h i sd i s s e r t a t i o n , w h i c hi s i m p l e m e n t e dw i t hp r n l o gl a n g u a g ea n dc a l lm a k el o g i cr e a s o n i n gf o rs p e c i f i cs e c u r i t yg o a l e f f e c t i v e l y t od e m o n s t r a t ea n dp r o v et h ec o r r e c t n e s sa n de f f e c t i v e n e s so ft h en e wt h e o r ya n dm e t h o d ， i l 东南大学博士学位论文 s o m er e p r e s e n t a t i v ep r o t o c o l sa l ea n a l y z e d f o rf l a w e dp r o t o c o l s ，t h er o o tc a u s e sa n dp o t e n t i a l a t t a c k sa r ed e s c r i b e di nd e t a i l s f o rc o r r e c tp r o t o c o l s ，f o r m a lp r o o f sa l eg i v e n i nc o n c l u s i o n ，t h o r o u g hr e s e a r c h e so i lt h ef o r m a la n a l y s i so fs e c u r i t yp r o t o c o l sa r em a d ei n t h i sd i s s e r t a t i o n ，a n dt h en e wt h e o r ya n dm e t h o dp r o p o s e dh e r eb a l a n c et h ea n a l y s i sa b i l i t ya n d o p e r a b i l i t yw e l l w h i c ho w nn o to n l ys t r a n ds p a c em o d e l sp o w e r , b u ta l s oa u t h e n t i c a t i o nl c l g i c s u s a b i l i t y g e y i o r d s ：n e t w o r ks e c u r i t y ；p r o t o c o la n a l y s i s ；c h a l l e n g e r e s p o n s e ；s t r a n ds p a c em o d e l i l l 东南大学博士学位论文 图表目录 图1 1 协议安全属性。2 图1 2 研究层次图6 图2 1 回放攻击分类法l l 图3 1k e r b c r o s 协议图2 0 图3 2k e r b e r o s 节点s s 偏序关系2 2 图3 3o r 协议攻击图2 4 图3 4n s 和n s l 协议一2 8 图3 5n s 协议攻击图2 8 图4 1b a n 类逻辑3 5 图4 2n e s s c r 对b a n 逻辑的质疑3 6 图4 3o r b a n 协议攻击图。3 9 图4 4m m r i 的两种形式4 2 图4 5m m r l 的第三种形式4 2 图4 6 目标分解示意图4 3 图4 7 基本分析树一4 4 图4 8k e r b e r o s 验证分析树4 5 图4 1 0 系统结构和流程4 8 图4 1 1 分析器界面5 0 图5 1c 忍似历的三种类型。5 7 图5 2 三个协议片断5 9 图5 3 c 攻击 图5 4 - c 攻击6 3 图5 5 - r 攻击“ 图5 6 - c 攻击“ 图5 7 一r 攻击“ 图5 8 ( 尬k a 一r 攻击6 5 图5 9 协议的正确性分析。6 5 图6 1o r 和o r - b a n 协议线空间图6 9 图6 2 n s 和n s l 协议线空间图7 2 图6 , 3s t a 接入鉴别流程图7 5 图6 4w a p i 安全接入协议7 7 图6 5w a i 三方认证关系7 9 目录 表格目录 表1 1 国外安全协议分析研究主要群体5 表3 1 a t 对n s 和n s l 协议的分析2 9 表4 1b e l i e v e _ 5 亿k a b ) 的子命题列表一 表4 2 分析器谓词表。 表4 3 核心b a n 逻辑库 4 7 4 8 表4 4k e r b e r o s 初始假设和理想化结果4 9 表5 1v o 认证目标的描述5 5 表5 2 c r ( a 啪过程中的主体标志参数一致性分析6 2 表6 1w a i 公钥证书格式7 6 v 1 1 1 东南大学博士学位论文 a s u a t b a n c s p c r g n y i s o m a c m b n r o n r r n s n s l o r p h y s s m s v 0 m v o w r a i 、) l ，a p l w p i 缩略词表 a u t h e n t i c a t i o ns e r v i c eu n i t a t l o g i c ，a l le x t e n s i o no f b a nl o g i c b a nl o g i c ，al o g i cf o ra u t h e n t i c a t i o np r o t o c o l s c o n c u r r e n ts e q u e n c ep r o c e s s c h a l l e n g e r e s p o n s e g n yl o g i c ，a l le x t e n s i o no f b a nl o g i c i n t e r n a t i o n a ls t a n d a r do r g a n i z a t i o n m e d i u ma c c e s sc o n 仃o l m bl o g i c ，a l le x t e n s i o no f b a n l o g i c n o n - r e p u d i a t i o no f o r i g i n n o n - r e p u d i a t i o no fr e c e i p t ap u b l i ck e yp r o t o c o lp r o p o s e db yr n e e d h a ma n dm s c h r o e d e r ar e v i s i o no f n sp r o t o c o lp r o p o s e db yg l o w e o t w a y - r e e sp r o t o c o l p h y s i c a ll a y e r s s u a n ds p a c em o d e l s v ol o g i c ，a ne x t e n s i o no fb a n l o g i c t r u s t e dt h i r dp a r t y v ol o g i c ，a ne x t e n s i o no f b a nl o g i c w i r e l e s sj o c a ja r e an e t w o r ka u t h e n t i c a t i o nj n f r a s t r u c t u r e w i r e l e s sl o c a la r e an e t w o r ka 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 e w i r e l e s sl o c a la r e an e n 帕r l 【p r i v a c yi n f r a s t r u c t u r e i x 东南大学学位论文独创性声明 本人声明所呈交的学位论文是我个人在导师指导下进行的研究工作及取得的 研究成果。尽我所知，除了文中特别加以标注和致谢的地方外，论文中不包含其 他人已经发表或撰写过的研究成果，也不包含为获得东南大学或其它教育机构的 学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已 在论文中作了明确的说明并表示了谢意。 n 研究生签名： 拯：】_ 日期：竺2 ：! ：当 东南大学学位论文使用授权声明 东南大学、中国科学技术信息研究所、国家图书馆有权保留本人所送交学位 论文的复印件和电子文档，可以采用影印、缩印或其他复制手段保存论文。本人 电子文档的内容和纸质论文的内容相一致。除在保密期内的保密论文外，允许论 文被查阅和借阅。可以公布( 包括刊登) 论文的全部或部分内容。论文的公布( 包 括刊登) 授权东南大学研究生院办理。 躲翩签浏捌 第1 章绪论 第1 章绪论 信息科技的迅速发展使i n t e m e t 成为最为重要的信息存储和传播的工具而作为一种战 略资源，信息的应用也从原来的军事、科技、文化和商业等领域逐步渗透到社会的每个角落， 在社会生产、生活中的作用日益显著。在这种分布式的互联网环境中，各种终端之间通过安 全协议来实现信息的交换和共享。因此，安全协议的设计是否正确、协议的实现是否满足安 全目标，直接关系到网络应用的安全性和可靠性。 1 1 研究背景 安全协议( s e c u r i t yp r o t o c o l c r y p t o g r a p h i cp r o t o c 0 1 ) ，又称密码协议，是指运行在计算 机网络或者分布式系统环境下，依赖应用密码学技术完成身份认证、密钥分配或者电子交易 等任务的协议，主要可分为密钥交换协议、认证协议以及电子商务协议等类型。其中密钥交 换协议主要用于在协议参与各方之间协商、分配会话密钥；认证协议主要用于鉴别协议参与 对象，确认交互数据的来源和目标；电子商务协议是较新型的网络协议，其目标是在参与协 议的各方之间公平地完成交易。安全协议的分类并不严格，例如密钥交换协议必须同时是认 证协议，不能确认会话密钥的来源，或者不能确认分配密钥的目标主体，都是没有意义 的。 安全协议是各种分布式系统安全的基础，确认其正确性极为重要。然而，它的设计并不 是一项简单的工作，许多经过研究人员多番推敲并确信无误，甚至己作为标准发布的协议， 最终仍被发现存在缺陷。安全协议存在的缺陷大致可以分为以下几种类型 g s 9 7 ： 基本协议缺陷：在安全协议设计中未考虑或者较少考虑攻击者攻击行为而引发的协 议缺陷。 口令密码猜测缺陷：选择了易被猜测的1 3 令，如使用了常用词汇或者不安全的伪随 机数生成器。 陈旧消息缺陷：指在协议设计时没有考虑消息的新鲜性，使得攻击者能够进行消息 重放攻击。 并行会话缺陷：协议对并行会话攻击缺乏防范，从而导致攻击者通过交换适当的协 议消息就能够获得所需要的信息。 内部协议缺陷：协议的可达性存在问题，协议的参与者中至少有一方不能完成所有 必需的动作。 密码系统缺陷：协议使用的密码算法的安全强度无法达到保证协议保密性和认证性 的要求。 在早期的协议设计过程中通常采用攻击检验的方法来检查协议的安全性。所谓攻击检 验方法是指收集并使用目前已有的对协议行之有效的攻击方法逐一对新安全协议进行攻击， 检验新安全协议是否具有抵抗这些攻击的能力。虽然这种分析方法具有一定的效果，但是由 1 东南大学博士学位论文 于它严重依赖于对已有攻击手段的知识，并且缺乏分析协议抵御未知攻击能力的手段所以 形式化的分析方法逐渐受到人们的关注。 形式化的协议分析方法是指采用各种形式化的语言或者模型，为安全协议及其所需满足 的安全属性建立模型，并按照前提假设来分析、验证协议的安全性。这种形式化方法有助于 【f f 0 3 ： 界定安全协议的边界，即协议系统与其运行环境的界面。 更准确地描述安全协议的行为。 更准确地定义安全协议的特性。 证明安全协议满足其规范说明，或者指出协议在什么条件下不符合其说明。 图1 1 协议安全属性 安全协议形式化分析的对象是协议的各种安全属性，根据对象的不同，安全协议分析目 前有两个主要的研究方向： 一是针对普通安全协议进行分析，分析的侧重点是协议的基本属性关联性和保密性。 其中关联性是指任何一个协议主体都能确认是在与自己所希望的主体进行交互，保密性是指 在协议的任何一次执行中都没有发生有价值信息被泄密的情况。以a 、b 两方协商会话密钥 为例，关联性是指a 能确认当前在与自己进行协议交互的是b ；保密性则是指，当协议执行 完毕，a 和b 所要协商的会话密钥没有泄漏。 二是针对电子商务应用中的不可否认协议进行分析。作为一种特殊的密码协议，不可否 认协议既有一般安全协议的性质，又有其特有的属性。不可否认协议分析的侧重点是不可否 认性、公平性和时限性。不可否认性是不可否认协议的基本性质，它要求协议能在通信事件 发生后防止某些实体否认通信事件的发生。根据公平程度的不同，公平性可分为强公平性和 弱公平性。强公平性要求只要数据传输成功，收发双方都应该收集到所需的证据；弱公平性 则要求如果实体没有收到所需的证据，而其他实体收到了所需的证据那么它能获得证据来 证明这个事实。时限性是实用的不可否认协议应该具有的另一个重要性质，要求协议保证诚 实的协议实体在协议的任何阶段都能采取措施在有限时间内结束协议的运行，以免实体在不 知道协议是否己结束的情况下需要无限期地维持协议状态以维持协议的公平性；时限性要求 协议结束后实现的公平性级别不低于实体开始结束协议时的公平性级别。 事实上，这两个研究方向所涉及的安全属性并不是同一层面上的概念。如图i 1 ，关联性 和保密性是所有安全协议的基本属性，是不可否认性得以满足的前提。论文所作研究工作针 对安全协议的基本属性展开，不涉及不可否认协议的分析研究。 2 第1 章绪论 1 2 安全协议分析现状 从上个世纪8 0 年代初提出d o l e v - y a o 模型 d y 8 3 1 ，到基于知识信仰的b a n 逻辑 b a n 9 0 ，再到n r l 协议分析器 m e a 9 4 、p a u l s o n 的归纳法 p a u 9 8 等等，安全协议的形式化 分析一直是研究的热点，并已取得了一定的成果，这些研究成果大致可以被划分为以下三类 【g s g 9 9 ： 基于攻击结构的方法( a t t a c k - c o n s t r u c t i o nm e t h o d s ) 包含三种子类型，分别是基于通 用目的验证语言的方法、基于代数简化理论模型的方法和基于专用目的专家系统的方法。 基于通用目的验证语言的方法( g e n e m lp u r p o s ev a l i d a t i o nl a n g u a g e s ) 采用有限状态机、谓词逻辑、模型检测等通用技术，将安全协议分析与其它程序正确性 证明等同处理。这种类型的分析方法虽然也是安全协议分析技术的重要组成部分，但是由于 没有考虑安全协议的特性，具有很大的局限性。 基于代数简化理论模型的方法( a l g e b r a i cs i m p l i f i c a t i o nt i l r 甜cm o d e lm e t h o d s ) 这种类型的方法将消息表示为代数表达式，将协议建模为表达式的转化、简化规则的集 合，并通过分析特定状态的可达性来判断协议是否安全。其中具有代表性的工作包括 d o l e v - y a o 模型和m e a d o w s 模型 m e a 9 2 。 基于专用目的专家系统的方法( s p e c i a lp u r p o s ee x p e r ts y s t e m ，s c e n a r i ob a s e dm e t h o d s ) 基于这种类型方法的分析系统通常从不安全状态着手，搜索从协议初始状态到该不安全 状态的路径，如果搜索到说明协议存在漏洞，反之认为不存在。这一类型方法的最大问题在 于只能用于发现协议漏洞，而无法保证协议的安全性，并且缺乏分析未知攻击的能力。其中 具有代表性的工作是m i l l e n 开发的i n t e r r o g a t o r m i l 9 5 ，它是一种基于协议状态转化模型、采 用p r o l o g 语言实现的软件系统。 基于攻击结构的方法需要探索协议执行的状态空间，随着协议参数数目的增加，协议空 间也随之呈指数级增长。因此当这种增长超过一定程度，其操作所需的时间和空间就会超过 可用资源这种情况被称为状态空间爆炸( s t a t es p a c e e x p l o s i o n ) ，它是基于攻击结构的方 法以及所有其它基于状态空间检测分析技术的方法所共同面临的问题。 基于推理结构的方法( i n f e r e n c e - c o n s t r u c t i o nm e t h o d s ) 这类方法从根本上来说是一系 列基于知识或者信仰的命题和推理规则，它将协议所要满足的安全需求描述为特定的逻辑结 论。分析人员需要从初始假设条件出发，根据协议主体接收和发送的消息进行推导，如果能 推理出所需要的逻辑结论，认为协议满足安全需求，否则认为协议有缺陷。这类方法的典型 代表是b a n 逻辑，它是m r r o w s ，a b a d i 和n e e d h a m 于l9 8 9 年提出的一种关于主体信仰和 如何从已有信仰推理出新的信仰的逻辑。其出发点是研究认证双方能否通过相互发送和接收 消息来从最初的信仰逐渐发展到协议运行最终要达到的目的认证双方的最终信仰；如果 在协议执行结束时能建立关于会话密钥，对象身份等的信任，说明协议正确，否则表明该协 议有安全缺陷。b a n 逻辑被用于对n e e d h a m s c h r o e d e r ，k e r b e r o s 等多个著名协议进行分析， 并找出了协议中已知的和未知的缺陷，取得了极大的成功。加上b a n 逻辑简洁直观、易于 使用因此得到了广泛的认可。b a n 的成功也极大地激发了密码学研究者对安全协议形式分 东南大学博士学位论文 析的兴趣，并导致许多衍生分析方法的产生。 然而，基于推理结构的方法忽视了协议保密性的问题，缺乏明晰的语义，并且在一些情 况下甚至无法清楚表示逻辑推理所要证明的命题。 基于证明结构的方法( p r o o f - c o n s t r u c t i o nm e t h o d s ) 为了解决攻击结构和推理结构方 法所存在的问题，尤其是搜索空间的指数级膨胀问题，一些新的基于证明结构的协议分析方 法被提出，其中具有代表性的包括： d b o l i g n a n o 提出的h u m a n g a d a b l e 证明法 b o l 9 6 1 该方法使用通用的形式化技术，与基于模态逻辑的推理结构性方法相比，可以更自由、 粒度更细地描述协议、协议假设以及协议认证相关的属性；而与其它形式化方法，尤其是 m e a d o w s 模型相比，晟重要的区别在于h u m a n r e a d a b l e 证明法侧重证明的简洁性和可读性， 而不是证明的自动化。在该方法中，所有协议主体被分成四类a 、b 、s 和s p y ，并被明 确建模为可靠主体和不可靠主体( 即攻击者) 。 l c p a u l s o n 的归纳法，以及在此理论基础上利用l s a b e l l e p a u 9 4 实现的协议分析器 p a u l s o n 归纳法综合应用了基于推理结构方法的关于消息的思想和基于攻击结构方法关 于事件( e v e n t ) 的定义，将协议归纳定义为所有可能事件的迹( t r a c e ) 的集合。可以为所有 的攻击行为和密钥丢失情况建模。 s s c h n e i d e r 提出的采用c s p 语言实现的认证属性的分析和验证的通用方法 s c h 9 7 】 该方法架构在通用c s p 语义框架基础上，将认证协议描述为协议主体对消息的发送和接 收，很好地解决了协议描述的简洁性与根据协议的描述进行形式化推理的便捷性之间的平衡 问题。 f j t f l b r e g a ，j c h e r z o g 和j d g u n m a n 等人提出的线空间模型【f h g 9 8 】【f h g 9 9 】 线空间模型( s t r a n ds p a c em o d e l ，简称s s m ) 为协议分析研究人员提供了一种新的分析 思路。线空间模型借助图论的方法描述协议的执行过程协议主体的行为序列构成s u - a n d ， 而线空间则是所有s t r a n d 的集合；不同协议主体的s t r a n d 之间通过消息数据的收发相互关联 从而形成线束( b u n d l e ) ；在线束的基础上，节点之间的偏序关系使得存在极小元，从而又产 生了一种类似于p a u l s o n 归纳法的协议安全性的证明方法。线空间模型的贡献不仅在于提出 了一种协议正确性的证明方法，还体现在为其它形式化方法提供了支持。 基于证明结构的方法的共同特点是为安全协议建立形式化模型，并应用定理证明相关的 技术证明协议的正确性。 从学术群体的分布来说，目前在安全协议形式化分析领域比较活跃的群体有 f f 0 3 ：以 m b u r r o w s 和m a b a d i 为代表的美国d 画t a le q u i p m e n t c o r p o r a t i o n ，代表性成果是b a n 逻辑； 以c m e a d o w s 和e s y v e r s o n 为代表的美国海军研究实验室( n a v a lr e s e a r c hl a b o r a t o r y ) ，设 计实现了n r l 协议分析器c a s p e r 编译器，提出了s v o 逻辑；以g l o w e 为代表的英国l e i c e s t e r 学院，主要研究成果是对认证形式的分类和定义，提出了a g r e e m e n t 致性的概念，并首先 将f d r 应用于安全协议的分析；以s s c h n e i d e r 为代表的英国l o n d o n 学院，将c s p 应用于 认证协议的验证，提出了秩幽数( r a n kf u n c t i o n ) 的概念：以a w r o s c o e 为代表的英国o x f o r d 第1 章绪论 学院，将c s p f d r 应用于协议的建模和分析：以j m i l l a n 为代表的美国c a r n e g i em e l l o n 学 院提出i n t e r r o g a t o r ，将专家系统用于协议的形式化分析；以s d s t o l l e r 为代表的美国i n d i a n a 大学( 现任职于s t o n yb r o o ku n i v e r s i t y ) ，提出了协议分析的攻击限定法【s t 0 0 2 】；以 e j t f a b r e g a 、j c h e r z o g 和j d g u t t m a n 为代表的美国m i t r e 公司，提出线空间模型、认证 测试【g f o o 】 g f 0 2 】【g u t 0 2 】等；以l c p a u l s o n 为代表的英国c a m b r i d g e 学院等，提出协议验证 的归纳法；以d s o n g 和a p e r r i g 为代表的美国c a l i f o r n i a 大学( b e r k e l e y ) ，提出协议验证的 a t h e n a 算法 s o n 9 9 1 【s b p 0 1 ；以d b o l i g n a n o 为代表的美国i b m 公司，提出h u m a n r e a d a b l e 证明法；等等。国内主要是以冯登国、卿斯汉等为代表的中科院软件所信息安全国家重点实 验室。除了这些群体外，还有许多有实力的科研人员在从事这一领域的研究。 表1 1 国外安全协议分析研究主要群体 在这些学者及其研究团体的共同努力下，协议形式化分析研究已经取得了一定的进展和 成果，并且有较多的分析方法被提出。由表】- l 可以看出，大部分分析方法或者采用信仰逻 辑等推理技术，或者采用状态检测等定理证明技术。这两类方法都存在着一定的局限性：以 b a n 逻辑为例，研究人员发现由于在初始假设形式化表达上的不足，b a n 逻辑并不能保证 协议的正确性，而b a n 逻辑的各种改进版本( 如a t 逻辑、g n y 逻辑、v o 逻辑、s v o 逻辑 等等，统称为b a n 类认证逻辑) 则都面临着描述能力与可操作性之间的矛盾。而其它基于 状态空间检测的分析技术，由于协议执行空间的状态是无限的即使应用了各种裁减技术， 仍然不可避免地存在着状态爆炸的问题从无限状态空间到有限状态空间的映射要求必须对 5 东南大学博士学位论文 协议的主体数或者并发的协议执行轮数进行限制。 线空间模型是这些研究成果中较新的分析理论，它可以准确地描述协议的执行过程，并 可以被用于协议安全目标的形式化定义，因此得到了很大的重视。围绕线空间模型，研究人 员提出了a t h e n a 算法、认证测试等新的协议正确性验证方法。但是，由于线空间模型本身主 要用于协议正确性的证明，因此在协议错误的查找方面能力较弱；另方面，目前的这些应 用方法往往没有脱离逻辑推理和定理证明这两条基本技术思路，仍然存在前面所说的分析能 力和状态爆炸的问题( 详细分析见3 3 节) 。 因此，目前研究的一个趋势是多种分析技术的融合，依照这个思路，论文以线空间模型 作为底层的语义模型，以改进的认证逻辑作为分析手段，综合a t h e n a 算法、认证测试等多种 技术，提出了一种新的基于挑战一响应的协议分析方法。 1 3 论文研究内容 安全协议形式化分析这一研究工作是一项系统工程，首先需要明确的是什么样的协议是 正确的，也就是需要给出协议正确性的形式化定义；其次，如何去证明协议的正确性，所提 出的证明方法应该具有一定的通用性，并且便于使用；然后，结合所给出的形式化分析方法， 需要对辅助分析工具展开研究；最后，提出分析方法的目的在于应用，方法的正确性必须通 过实践的考验。 与之相对应，整