（计算机软件与理论专业论文）扩展基于本地会话的安全协议验证逻辑分析tls协议.pdf

扩展基于本地会话的安全协议验证逻辑 分析t l s 协议 专、l k ：计算机软件与理论 硕上生：陈元辰 导师：苏丌乐教授 摘要 安全协议是保证网络安全的重要技术之一，但安全协议自身的缺陷， 往往会导致很，“重的安全问题。如何验证安全协议能否实现其安全目标， 成了研究中的热点问题。近年来，导帅苏丌乐教授提山了一种基于本地会 话的安全协议验证逻辑( l l s ) ，能有效的对协议的安全性进行分析。由于 该理论是一个全新的理论，需要对其进行扩展，以使其能分析更多的协议。 传输层安伞l 办议( t l s ，t r a n s p o r tl a y e rs e c u r i t y ) 是由i e t f 在s s l 3 0 的基础上提出的互联网标准，得到了广泛的应用，其安全性的分析有很高 的研究价值。 本文针对对称密钥协商协议的分析，在l l s 逻辑的基础上进行r 扩 展。本文在l l s 逻辑最核心的( n ，1 ) 一s e c r e c y 定理中加入了对协商密钥的分 析，针对协商密钥协议要认证的安伞规范增加了公理，并对扩展的部分做 了证明。随后，本文使用扩展后的l l s 逻辑分析了t l s | 办议的安全性。 本文首先分析了认证密钥协商协议的实现目标，包括实体认证、密钥认证、 密钥确认、消息完整性等，然后针对t l s 协议给出了一系列的具体的验 证f 1 标，并对这些验证目标进行了验证。t i ，s 协议允许通信双方新建或 重用一个会话，本文对这两种情况分别进行了讨论，并将分析的结果和其 他人的工作进行了比较，说明了l l s 逻辑的正确性和优点以及扩展后的 l l s 逻辑在分析这类协议时的有效性。 关键词：安全协议验证，实例化空间，可观察理论，密钥协商，t l s af o r m a la n a l y s i so ft h et l sp r o t o c o l m a j o r ：c o m p u t e rs o f t w a r ea n dt h e o r y n a m e ：c h e ny u a n c h e n s u p e r v i s o r ：p r o f k a i l es u a b s t r a c t s e c u r i t yp r o t o c o li so n eo ft h em o s ti m p o r t a n tt e c h n o l o g i e st oe n s u r e n e t w o r k ss e c u r i t y b u tt h e ym a yn o tb ea b l et oe n s u r et h ed e s i r e ds e c u r i t y g o a l sd u et ot h el o g i c a lf l a w si nt h ed e s i g no ft h ep r o t o c 0 1 a n di ti sw i d e l y a c k n o w l e d g e dt h a tt h el o g i c a lf l a w si ns e c u r i t yp r o t o c o l sa r eh a r dt oa n a l y z e s e c u r i t yp r o t o c o lv e r i f i c a t i o nh a sb e c o m eah o ti s s u e r e c e n t l yy e a r s ，p r o f k a i l es up r e s e n t san e wp r o t o c o lv e r i f i c a t i o nl o g i c ， c a l l e dl o g i co fl o c a ls e s s i o n s ( l l s ) ，w h i c hi sb a s e do nan e ws e m a n t i c m o d e lc a l l e dl n s t a n t i a t i o ns p a c e t h i sl o g i ci sv e r yu s e f u li nt h ea n a l y s i so f t h es e c u r i t yp r o t o c o l s b e c a u s eo ft h et h e o r yi san e wt h e o r y , i ti sn e e dt ob e e x t e n d e dt oe n a b l ei tt oa n a l y z em o r ep r o t o c o l s t r a n s p o r tl a y e rs e c u r i t yp r o t o c o l i st h ei n t e r n e ts t a n d a r dp r o t o c o lt h a t i e t fd e r i v e df r o m n e t s c a p e ss s l 3 0 i t i s w i d e l yu s e d f o ri n t e m e t c l i e n t s e r v e rc o m m u n i c a t i o n ss e c u r i t y f o rt h ea n a l y s i so fs y m m e t r i ck e y a g r e e m e n tp r o t o c o l ，w ee x t e n dt h el o g i co fl o c a ls e s s i o n s w ea d dt h ea n a l y s i s o fa g r e e m e n tk e yi n ( n ，1 ) - s e c r e c yp r o p e r t ya n dg i v es o m en e wt h e o r e m s a f t e rt h a t ，w ec o m p l e t et h ep r o o fo ft h ee x p a n s i o np a r t t h e nw ea n a l y z et h e t l sp r o t o c o lb yt h ee x t e n d e dv e r i f i c a t i o nl o g i co fl o c a ls e s s i o n s w ef i r s t a n a l y z e dt h eg e n e r a lg o a lf o ra u t h e n t i c a t i o nk e ye s t a b l i s h m e n tp r o t o c o l ，a n d t h e nw eg a v es o m es e c u r i t yp r o p e r t i e sf o rt l sp r o t o c o la n dv e r i f i e dt h e m k e y w o r d s ：s e c u r i t yp r o t o c o lv e r i f i c a t i o n 。i n s t a n t i a t i o ns p a c e ，o b s e r v a t i o n t h e o r y , k e ya g r e e m e n t ，t l s 第1 章引言 随着计算机网络应用的普及，安全问题也变的越来越突出，越来越复 杂。安全协议是解决安全问题的最有效的手段之，其目标是要在不安全 的网络环境中解决些罩要的安全问题，如源认征和目标认证、消息的完 整性、匿名通信、抗抵赖、授权等。 虽然安全协议基f 密码系统来保护阱议的安全性，但是如果协议本身 的设计存在逻辑漏洞，则会产生作常严重的安全问题。但由于安全协议的 复杂性，分析其逻辑上的漏涮十分团难。因此，如何有效的对安全协议的 安全性进行分析，成为了一个非常重要的研究课题。 近年来，导师苏丌乐教授提出了一种新的基于本地会话的安全协议验 证逻辑l l s ( l o g i co fl o c a ls e s s i o n s ) 。该理论在定义了个描述安全协议 分析的加密信息交换( c r y p t o g r a p h i c a lm e s s a g ee x c h a n g e ) 模型的基础上， 给出了一个称为“实例化空间( 1 n s t a n t i a t i o ns p a c e ) ”的安全协议验证逻 辑的语义模型，并提出了一系列与安全性相关的l l s 验证公理。为了验 证多层的认知规范，该理论又引入了可观察理论( o b s e r v a t i o nt h e o r y ) ，从 而可以利用主体的可观察知识束验证防议的安全性质。该逻辑可以方便的 处理任意加密函数任意嵌套形式的消息格式，并具有很好的扩展性。 由于安全协议的验证是一个不可判的问题，理论上不存在完备的验证 公理系统。因此需要分析大量的协议以验证该理论的有效性，发现问题并 进行改进，以使该理论尽可能的完备。同时，由于该理论是一个全新的理 论，也需要对该理论不断进行扩展，使其能分析更多的协议。 传输层安全协议( t l s ，t r a n s p o r tl a y e rs e c u r i t y ) 【1 】是由i e t f 在 s s l 3 0 1 2 的基础上提出的互联网标准，得到了非常广泛的应用，其安全 性的分析有很高的研究价值。 本文针对t l s 协议的分析，在l l s 逻辑的基础上进行了扩展。本文 在( n ，1 ) 一s e c r e c y 中加入了对协商密钥的分析，针对协商密钥的情况增加了 静艇早卜小地会1 【的丘争饥议验i l r 逻辑分忻t l s 悱议 定理，片对扩展的部分做了证明。 本文随后使用扩展后的l l s 逻辑分析了t l s 协议。本文首先分析了 密钥协商协议的实现目标，然后针对t l sm 议给出厂+ 系列具体的验证 目标，并对这些验证目标进行了验证。t l sm 议允许通信双方新建或重 用个会话本文对这两种情况分别进行j ，讨论。片将分析的结果和其他 人的工作进行了比较，说明了l l s 逻辑的i f 确性和优点以及扩展后的l l s 逻辑在分析这类协议时的有效性。 本文共分为六章，第一章是引言，乇要介绍本文所作的工作和本文的 结构。 第二章介绍了安全协议的背景、发展情况以及安全协议分析的系统模 碰，即著名的d o l v e y a o 模型【3 】。 第三章说明了基于本地会话的验证逻辑，包括加密信息交换模型、实 例化空日j 以及l l s 逻辑的验证公理的说明。 第四章对l l s 逻辑进行了扩展，并对扩展部分的诈确性做了证明。 第五章分析了t l s 协议的安全性。该章首先对要验证的t l s 协议做 了简单的介绍，片对该协议进行了形式化。随后本文使用扩展的l l s 逻 辑对t l s 协议新建会话和恢复已有会话时的安全性分别进行了分析。在 本章的最后，我们列举了一些其他人的工作，并和本文的工作做了比较。 第六章对本文的工作做了总结，并对未来的工作提出了些展望。 本文的研究工作得到国家自然科学基会( 6 0 4 9 6 3 2 7 ，6 0 4 7 3 0 0 4 ) 的资 助。 2 第2 章安全协议验证 本章上要介绍安全协议验证的基础知识。内容安排如f ：第节介绍 了安全协议的基本概念。第一：节描述了安全协议分析的系统模型，即著名 的d o l v e y a o 模型【3 1 。第j 节对已有的安全协议形式化分析方法做了简 单的介绍。本章e 要参考了我因这个领域的权威学者冯登国、范红老师 【4 5 6 】和卿斯汉老i ) 币1 7 ，8 】的文章。 2 1 安全协议 安全协议，足以密码学为基础的消息交换协议，其目的是在复杂的网 络环境中提供各种安全服务。密码算法和安全协议处于网络安全体系的不 同层次，足网络数据安全的两个不同内容。密码算法为网络上传递的消息 提供高强度的加解密操作和其他辅助算法( 如h a s h 函数) ，而安全协议 是在这些密码算法的基础上，为各种网络安全性方面的需求提供实现方 案。 安全协议的目标是多种多样的，目前网络通信中最常用的安全协议按 照其目的可以分为一下四类【4 】： ( 1 ) 密钥交换协议。这类协议用于完成会话密钥的建立。般情况下 足在参与协议的2 个或者多个实体之问建立共享的秘密，如用于次通信 中的会话密钥。 ( 2 ) 认证协议。认证协议包括实体认证( 身份认证) 协议、消息认证 协议、数据源认证协议和数据目的认证协议等。用来防止假冒、篡改、否 认等攻击。n e e d h a m s c h r o e d e r 协i , s 1 0 是最为著名的早期的认证协议， 许多广泛使用的认证协议都是以n e e d h a m s c h r o e d e r 协议为蓝本而设计 的。 ( 3 ) 认证密钥交换协议。这类协议将认证协议和密钥交换协议结合在 一起，先对通信实体的身份进行认证，在认证成功的基础上，为f 一步安 和地壮卜本地会i ，的奠令悱议r 验l 小逻辑竹析f l s 悱歧 全通信分配所使用的会话密钥，它是网络通信中应用最普遍的一种安令协 议。常用的认证密钥交换协议有互联网密钥交换协议( 1 k e ) 协 义、分布 式认证安伞服务( d a s s ) 协议等。 ( 4 ) 电子商务协议。该类协议中的t 体往 t 代表交易的双方，其利益 目标是不敛的，或者根本就是矛盾的。凶此，电子商务防议最为关注的 就是公平性，即协议应保i i f 交易双方都不能通过损害对方利益而得到它不 应该得到的利益。常见的电f 商务协议有s e t 阱议、i k p 协议等。 除了卜面提到的安全协议外，早期著名的经典安全阱议还有 o t w a y r e e s 协议、y a h l o m 协议、大嘴青蛙协议等，以及。止j 荤要的实用 协议，如k e b e r o s 防议、c c i t tx 5 0 9 协议等。1 9 9 7 年，c l a r k 和j a c o b 1 0 】 对安伞协议进行了概括和总结，列举了+ 系列有研究意义和实用价值的安 全协议。 2 2 安全协议分析的系统模型 运行安全协议面临的最大问题是其所处的网络通信环境是不安全的， 环境中除了发送和接收消息的诚实的主体外，还有攻击者的存在。在对安 全协议进行分析之| j 仃，需要对协议所处的环境以及攻击者的能力进行限 定。 1 9 8 3 年，d o l v e 和y a o 提出了攻击者模型，即著名的d o l v e y a o 模型 3 】。陔模型将安全协议本身与安全协议所具体采用的密码系统分丌，使 得在研究安全协议时可以专心于安全协议内在的安全性质。该模型约定攻 击者可以： ( 1 ) 将消息发送到其意定接收者： ( 2 ) 延迟消息的送达： ( 3 ) 将消息篡改后转发； ( 4 ) 将消息与以前接收的消息合并： ( 5 ) 改变部分或全部消息的目的地址： ( 6 ) 重放消息。 4 第2 争奠乍叭议验计 陔模型同时还约定了攻击者不对密文进行破译，假定安全协议采用的 加密算法是安全的，这简化了对协议的分析。该模型被证明为最强的黑客 模型，因为它能够模拟任何可能的独立于协议的攻击。迄今为止，大部分 的安全| 办议的研究工作都是基于咳模型的。本文在分析时，不对黑客进行 卣接的模型化，但我们把d o l v e y a o 模型看作是协议运行环境中的部 分。 2 3 安全协议的形式化分析方法 从1 9 7 8 年n e e d h a m s c h r o e d e r 协议【9 的诞生算起，安全蜘议的发展 已经历经了将近3 0 年的发展。安全协议验证从丌始对具体协议的观测、 分析，发展到安全协议验证的形式化分析阶段。 安全防议的形式化分析是采用一种- f 规的、杯准的方法对协议进行分 析，以检查协议是否满足其安全目标。与非形式化分析方法现比，形式化 分析方法可以界定安全协议的边界，更准确的定义安全协议的特性和描述 安全 办议的行为，证明安全协议满足其设计目标，以及证明安全协议在什 么条件下不能满足其设计目标。 根掘冯登国老师【4 】的研究，形式化分析方法可以归纳为3 类，即基 于推理的结构性方法，基于攻击的结构性方法和基于证明的结构性方法。 2 3 1 基于推理的结构性方法 基于推理的结构性方法主要是运用逻辑系统从用户接收和发送的消 息出发，通过一系列的推理公理，推证协议是否满足其安全说明。用于安 全协议形式化分析( s e c u r i t yp r o t o c o lf o r m a la n a l y s i s ) 的逻辑系统可分为2 类：一类是基于知识的( ak n o w sp ) ；另类是基于信仰的( ab e l i e v e sp ) 。 两者的主要区别在于：基于知识的逻辑系统的公理表述为：“i f y o uk n o w p ，t h e n p i s t r u e ”。基于信仰的逻辑系统不涉及p 的正确与否。这些逻辑系 统通常由一些命题和推理公理组成。命题表示主体对消息的知识或信仰， 而运用推理公理可以从己知的知识和信仰推导出新的知识和信仰。 由眨早十奉地会l ，的丘伞悱议验计逻辑分析t l s 脚吐 在这类方法中，最著名的就是b a n 1 2 l & b a n 类逻辑。b a n 逻 辑是种关f 主体信仰，以及用于从已有信仰推知新的信仰的推理规则的 逻辑。这种逻辑通过对认证胁议的运行进行形式化分析，来研究认证双方 通过相互发送和接收消息，能否从最初的信仰逐渐发展到协议运行最终要 达到的信仰。其目的是在+ 个抽象层次上分析分御式网络系统中认证协议 的安全问题。如果在咖议执行结束时，未能建立起关于诸如共享通信密钥、 对方身份等信任时，则表明这协议有安令缺陷。b a n 逻辑的规则十分 简洁和直观、易于使用，因此得到广泛的认町，片成为逻辑形式化分析系 统的标准。 但b a n 逻辑自身也存在很多的缺陷，例如非标准的理想化协议过程， 不合理的假设，不能对知洪进行推理使得b a n 逻辑只能分析协议的认汪 性质，而不能分析协议的保密件质等，这些都限制了b a n 逻辑分析安全 l 力 议的能力。学者们在b a n 逻辑的基础上，不断进行改进，提出了很多 新的逻辑，主要有以下几个方面【4 】： ( 1 ) 对b a n 逻辑自身进行扩充导致了b a n 类逻辑的产，l 三。如g n y 逻辑【1 3 】，a t 逻辑【1 4 ，v o 逻辑 15 】，s v o 逻辑 1 6 ，1 7 1 等； ( 2 ) 为具体的协议设计特定的形式化分析工具，如分析电子商务协议 的k a i l a r 逻辑【18 以及分析与时间相关的协议c s 逻辑【1 9 等： ( 3 ) 突破b a n 及b a n 类逻辑对协议主体的假设的局限性而提出的 k g 逻辑 2 0 l ，以及突破主体信仰与知识的单调性而提出的n o n m o n o t o m i c 逻辑 2 1 】。 目前在这方面最新的研研究是m i t c h e l l 和p a v l o v i c 等提出的组合协议 逻辑( p r o t o c o lc o m p o s i t i o n a ll o g i c ) 2 2 】，该逻辑可以模块化的验证一。个复 杂协议，即先把一个协议分成几个小的模块分别进行验证，然后将分析的 结果进行整合。 6 第2 争奠伞饥议验* 2 3 2 基于攻击的结构性方法 基于攻击的结构性方法也称为基于证伪的方法。这种方法先假定。个 协议的有穷会话b o u n d e ds e s s i o n s ) ，然后在此会话中搜索潜在的攻击漏 洞。该疗法在对协议进行分析时，一般要借助于自动_ 具，如一般目的的 模型检测工具f d r 2 3 和m u r 庐【2 4 】以及特殊目的的n r l 分析器 2 5 1 和 i n t e r r o g a t o r 2 6 。这些方法郁是从协议的初始状态出发，对合法t 体和一 个攻击者的所有i 叮能的执行路径进行穷尽搜索，看能否找到协议可能1 罕在 的错误。 该方法的优点是，( 1 ) 能够自动验证一个系统是否满足其所设计的规 范。( 2 ) 、当规范不被满足或检测出协议存在漏洞时，能够提供导致该结果 的时唰序列，从而可以方便的定位协议中的漏洞。 该方法也同样存在有缺陷，主要表现在，( 1 ) e 体数目的有限性。由 于只能考虑一个协议的有穷会话，所有即使没有发现协议的错误，但当协 议的主体数目增加时仍可能出现错误。( 2 ) 无法解决状态空j b j 爆炸问题， 不能用于分析比较复杂的协议。 2 3 3 基于证明的结构性方法 和基于攻击的结构性方法不同，基于证明的方法不是去寻找协议可能 存在的攻击，而是用数学的方法去证明协议的正确性。这点和基于推理的 方法有些相似，但所不同的是，基于推理的方法是基于公理集和推理规则 的，而证明的方法借助于别的数学方法。 这种方法的好处是，在分析协议时，不受限于协议的大小，不限制主 体参与协议的回合。其缺点足证明过程不能完全的自动化。需要人工进行 “专家式”的干预。而且由f 该方法满足不了完备性，无法保证所有语义 i f 确的定理都可以通过系统证明出来，难以发现协议的漏洞。 该类方法主要有p a u l s o n 归纳法 2 7 1 、串空l 日j 模型( s t r a n ds p a c e s ) 2 8 、 和畦皋卜奉地全l 。的矗牟m 汉验l 一逻辑分析f i sy j 议 s p i 演算 2 9 1 等。 8 第3 章基于本地会话的验证逻辑 本文一 作的基础是导师苏丌乐教授提出的新的基于本地会话的验证 逻辑( l l s ) 该逻辑的研究是在 3 0 3 1 3 2 ，3 3 1 的基础上进行的。咳逻辑基于 一种新的称为“实例化空f u l ( 1 n s t a n t i a t i o ns p a c e ) ”【3 4 的语义模型，该语义 模型是建矗在。种自然的加密信息交换( c r y p t o g r a p h i c a lm e s s a g e e x c h a n g e ) 模型卜的。 本章给出了l l s 逻辑的晚明，第一节介绍了加密信息交换模型；第 二节介绍了“实例化空间”：第j 节给出了系列与安全属性相关的l l s 验证公理：第四节介绍了可观察理论( o b s e r v a t i o nt h e o r y ) 。 3 1 加密信息交换模型 这一节，我们介绍一个消息代数( m e s s a g ea l g e b r a ) 和加密信息交换模 型c m e ( c r y p t o g r a p h i c a lm e s s a g ee x c h a n g e ) 模型，咳模型是实例化空| 日j 的 基础。 3 i i 消息代数 在这个安全协议模型中，存在i 种消息类型：明文消息，组合消息和 加密消息。密钥属于明文消息。个消息代数是一个二元组( m ，瓦) ，其 中尼m 并包含。一个特殊的密钥h a s h ，町作以卜操作： 逆钥( i n v e r s ek e y ) ：若k 庀并且k h a s h ，则k “瓦。 组合( c o n c a t e n a t i o n ) ：若啪，m n m ，则 m l ，m n 】at 。 分解( d e c o m p o s i t i o n ) ：若【坍，m ，】m ，则m ，m ，m 。 加密( e n c r y p t i o n ) ：若k 疋、m m 且m 不是 m 形式，则 m ) m 9 和埏堆卜奉地会i 仙q 奠牟叭议验计逻辑分析t l s 肌c 义 解密( d e c r y p t i o n ) ：若k 一a 1 月 ，玎 。 f ，贝u ，”一。 假定 1 若 i m i ，那么m i = m 2 且k i = k 2 2 若【m l - m 。1 - 【m i m 】，那么对f o i s h 月= nv m t = m ，。 给定个消息集合m ，个密钥集合足和一个消息。给出f 列 符号定义。 1 c l ( a 4 ) 足。个由m 通过加密，解密，分解和组合形成的消息集 合。 2 c l 一( w i 足一个出m 通过解密和分解形成的消息集合。 3 c l + ( m ) 是一个由m 。通过加密和组合形成的消息集合。 4 s u b ( m o ，【) 是一个由消息通过用k 解密和分解形成的消息 集。类似的，我们定义s u b ( m ，瓦) = u 。s u b ( m ，瓦。 5 f r e s h ( m o ) 是一个由产生的消息集合。若嘲，是一个新鲜的 n o n c e 或时戳，那么f r e s h ( m o ) 中的消息都是新鲜的。 3 1 2 加密信息交换模型( c m em o d e l ) 0 加密信息交换模型被定义为一个多元组 = ( m ，e ，a g ，p k ，s k ，l a b e l ，n o n c e ，l n i t r e c v s ，s e n t s ) 其中 m 是一个消息集合。 庀是密钥的集合，是的子集。 e 是个由黑客控制的通信环境。 a g 是通信主体的集合，为方便起见，假定a g m 。 第3 市培卜奉地会矸的验计逻辑 p k 是元组 的集合其中密钥符号k 是角色“的公钥而 k “是对应的私钥。 s k 足元组 的集合，表明是角色和啦共享的秘密。 l a b e l 是标识消息集。通常是时删戳、会话标识数或者随机数。l a b e l 集中的消息通常称为标识消，包, ( 1 a b e lm e s s a g e s ) 。 n o n c e 是一个把主体玎a g u e 映射到a 产生的n o n c e s 或 c h a l l e n g e n u m b e r s 集合的函数。显然，对于所有的6 1 a g u e ) ，可 以得到n o n c e ( a ) l a b e l 。 l n i t 是一个把a a g u e 映射到a 在某个会话最初拥有的明文消 息集的函数。 r e c v s 是。个把主体口a g u e 和每个时间点l ( 自然数) 映射到一 个消息集合的函数，表示( f 到时间点t 收到的消息集合。 s e n t s 足个把主体a a g u e 和每个时| 日j 点t ( 自然数) 映射到一 个消息集合的函数，表示口到时i u j 点f 发送的消息集合。 给定+ 个t 体p a g 和一个n o n c e 或者时间戳( t i m e s t a m p ) 或者会话 标识( s e s s i o ni dn u m b e r ) c ，我们假设p 在协议p 中最多只在。个局部运行 中使用了c 。这样消息c 就可以看成是协议的某个局部运行的标识符号。 定义函数r e c v s 和s e n t s 为 r e c v s ( a ，) = u r e c v ( a ，t s e n t s ( a ，) = u 口s e n t ( a ，t 3 对于每个a a g ，定义k = l n i t ( a ) n 瓦。显然，匕是a 的初始密钥集。 为表示f 的初始密钥集，定义氍= 一( p r k d s h k ) ，其中 p r k = 七一i p k f o rs o m e 口a g ) 和艘挂j 。奉地会l t 【的丘令肌叹验i l 逻辑分析t l sm 泌 s h k = k | s kf o rs o m ea 1 a ! a g 这咀，假定环境p 可以拥有除了a g 中主体的私钥和共亭密钥外的所 有密钥。 定义p o s s 足个函数，对于每个口a g u f e ) 和每个自然数( 时间点) t ，p o s s ( a ，j _ c l ( i n i t ( a ) o r e c v s ( a ，f ) ) 。下面，我们给出c m e 模型的假设 2 1 肘f 每个a a g 和m a 4 ，有 ( a ) 苫m s e n t s ( a ，) ，贝u m r e c v s ( e i + i ) ； ( b ) 若m r e c v s ( a ，) ，贝u m s e n t s ( e ，一1 ) 。 此假设表明环境可以收到每个由毛体发出的消息，而主体收到的 每个消息都由环境发出。 2 若m r e c v s ( a ，t ) ，则存在某个a a g 使得m s e n t s ( a ，f 一1 ) 。 此假设表明环境可以包括除了a g 外的任意主体。 3 对于每个a a g t j e ，s e n t s ( a ，) p o s s ( a ，t 1 ) 。 4 对丁二每个a a g t j e 和r t ，s e n t s ( a ，s e n t s ( a ，f ) 且 r e c v s ( a ，t ) r e c v s ( a ，) 。 5 ( a ) 对于a a g 、k 赶和m m ，若 p k ，则对于 所有不是a 的主体a g t j e ，k 茌i n i t ( a 。 ( b ) 对于口l ，口2 a g 和m a 4 ，若 s k ， 则 m i n i t ( a 1 ) 且m i n i t ( a 2 ) ，但是对于所有不是q 和日2 的主体 a a g u e ，m g l n i t ( a 3 。 上述假设说明环境e 或主体最初不能拥有他不该拥有的密钥，或 者别人产生的秘密消息如c h a l l e n g en u m b e r 。 第3 帝杜卜本地会一的验仆逻辑 下面，我们再引入止匕公式。我们定义 k e y s ( a f l = p o s s ( a t ) n 厄 s e e s ( a ，) = s u b ( r e c v s ( a f ) k e y s ( a ，) 另外，s a i d ( a ，f j 定义为满足下列条件的最小消息集合m ( 1 ) s e n t s ( a ，f ) m ； ( 2 ) 若 m ，m ，】一，i a i j m r m 。m ： ( 3 ) 若 3 , 4 ，且m ，k p o s s ( a ，) ，贝0 m 6 4 。 定义 e n c r ( a ，f ) = “棚 tk p o s s ( a ，f ) 且用p o s s ( a ，t ) l r e c g ( a ，j = ( ，” tk 一p o s s ( a ，) 或七p o s s ( a f ) 且，竹p o s s ( a ，) e n c r ( a ，f ) 是一个a 可以通过加密操作形成的消息集，r e c g ( a ，f ) 是a 可 识别的加密消息集。 f r e s h ( a ，m 。，f ) 定义如下 ( 1 ) m 0 f r e s h ( a ，m o ，) ( 2 ) 若对于某个f ( f _ 1 ， ) 有m j f r e s h ( a ，m o ，) ， 则 【m l ，m 。】f r e s h ( a ，n o ，r ) ： ( 3 ) 若 州r e c g ( a ，f ) ，且m 或k 在集合f r e s h ( a ，m o ，) 中，则 聊 女f r e s h ( a ，m o ，) 。 直觉上，f r e s h ( a ，m o ，t ) 表示若是一个新鲜的消息，那么从日看来， 所有在f r e s h ( a ，n o ，) 中的消息也是。 引理3 1 对于每个a a g u e ) ，若 m ) s e e s ( a ，t ) 成立，则对于某个 订a g u e ) 年t f ， m ) t s a i d ( a ，) n e n c r ( a ，t 。 扫j 挺肚卜本地会l 的扯令叭议验计逻辑分析 l s 叽汶 3 2 安全协议的实例化空间 这罩，我们先介绍验证逻辑l l s 的语义模型：实例化空阳j ( i n s t a n t i a t i o n s p a c e ) 。这个语义模型的直觉意义是，冼议中的每个消息符号的实质是消 息变量，而主体肘协议的某个( 局部) 会话的一次执行，实质就是尉这些变 量进行的次实例化，即给他们赋予具体的消息值。 3 2 1 协议和局部协议 为了描述个协议，首先定义了5 个符号集合：t a t k t n ，i 。和 t g t a t k ，t n ，t l 和k 分别做主体符号( a g e n t t e r m s ) ，密钥符号( k e y t e r m s ) n o n c e 符号( n o n c e t e r m s ) ，杯识消息符号( 1 a b e lm e s s a g e t e r m s ) 并1 1 一。般明文消 息符号( g e n e r a lp l a i nt e x tt e r m s ) 。这些符号也称为原子消息符号( a t o m i c m e s s a g et e r m s ) 或一般消息符号( p l a i nt e x tt e r m s ) 。个消息符号( m e s s a g e t e r m ) 或者是一个原f 消息符号；或者形如【m m 。j 其中每个 m ，( f - l ，n ) 都是+ 个消息符号：也或者形如 肘) 。，其中m 是r 个消 息符号而k 足个密钥符号。 安全协议p 为一个血元组( a g ，p k ，s k ，删r ，b o d y ) ，其中 a g 是一个主体符号集，可以看成是主体在协议定义中扮演的协议 角色： j d k 是元组 的集合，其中密钥符号k 是角色j d 的公钥 而k 一- 是对应的私钥： s k 是元组 的集合，其中消息符号m 是角色p 和q 共享 的秘密通常m 足一个密钥符号并且此时m 足p 和q 的共享密 钥： 删7 1 足。个把每个角色p a g 映射映射到原子消息符号集合的 4 第3 章挂卜木地会i 【的验i l p 逻辑 函数； b o d y 是协议的主要部分，是由元组 的有限序列组成， 其中p 和q 是a g 中的角色，m 足由u 。n i t ( p ) 的原子消息符 号和，k 及s k 中的密钥符号构造而成的消息符号集。 为方便起见，定义n o n c e 为。个函数，使得对每个角色p a g ， n o n c e f p ) = ，r ( j p ) n t n ，也就足说，n o n c e 足一个把角色p a g 映 射到n o n c e 符号集的函数，表示由p 产生的n o n c e s 。 在f 文中，字母p ，q r 代表主体符号k 代表密钥符号，代表n o n c e 或时1 1 日j 戳符号，肘代表消息符号。注意尸不是代表具体的某个宅体，而 是表示t a 中的一。个符号。为了作为区别，我们用p ，f 表示具体的某个主 体。 用m s g ，来表示协议p 中出现的所有消息符号集，它定义为满足下列 条件的最小消息符号集合： 1 u m i n i t ( p ) c m s g l , ； 2 若存在尸，r a g 使 在b o d y 中，则m m 姊： 3 若加密消息符号 m 。m s g v ，则m 和k 都在m s g p 中： 4 若连接消息符号【m ，肘。】在m s g 9 中，则对f = l ，h 有 m 。m s g 7 , 。 角色q 的局部协议( 1 0 c a lp r o t o c 0 1 ) ，用p ( q ) 表示，意思为根据协议p 中的b o d y ，该角色的收发消息的历史过程。它也可以表示为事件序列 一) h ，其中乞是q 的局部历史的长度，对于每个，存在某个 m 懈使得 或 是b o d y 中的成员，而且要么是 s e n d ( m ) ，要么足r e c v ( m ) 。 6 堑竺兰l 世垒堕竺垄竺坐坚竺! ! 堡塑竺堑! 坚坐坚 3 2 2 相关符号 给定个协议尹和一个角色9 ，对于每个，s 七，考虑f f ，j ，“的初始 部分 一用& n 船( q ，) 表示角色q 在p 中的f 步前发送的消息集合， 同理还有r e c v m q ，n p o s s ( ，) s a d ( q d ) , f f l s e e s ( q ，) 。他们的精确定义如 f ： 。触9 ( 9 ，) ：所有满足j p d ( m ) = e ，且 i f 弦j m 的集合。很明显若 ，= 0 ，则s e m s ( o ，) 是个宅集。 。尺。( q ，) ：所有满足r e c v ( m ) = e ，且 ，的m 的集合。很明显 r e c v s ( q o ) 是个空集。 。| p 伽( q ，z ) ：满足f 列条件的最小集合m s g ，, ： ( i ) i n i t ( q ) u r e c v ( q ，) ： ( 2 ) 若f m l ，m ，j ，则对于f f = l ，疗) ，m 量： ( 3 ) 若 m k 且k 1 ，则m 。 。勋谢f 9 ，) ：满足下列条件的最小集合： ( 1 ) s e n d ( q ，) ： ( 2 ) 对于，2 l ，胛，若 肘，m ，】，则m ，a ： ( 3 ) 若 肘k k ep o s s ( q ，) 且m t o s s ( o ，) ，那么m 。 s e e s ( q ，z ) ：满足下列条件的最小集合a ： ( 1 ) r e e v s ( q ，) ： ( 2 ) 对于f = l ，胛，若【肘，m 。】，那么m ： ( 3 ) 若 肘 k r k 一p o s s ( q ，) ，则m 。 。r e c g ( q ，z ) ：满足下列条件的密文集合f 竹j 。m s g p ： 第3 争阜寸。奉地会讯的验u r 逻辑 ( 1 ) m k s p o s s ( q ，) 或 f 吖 。k 1 量p o s s ( q f ) ( 2 ) 满足m 。p o s s ( q ，) 且m 2 p o s s ( q z ) 的那些m l0 m 2 。 直觉上说，若 m j 。r e c g ( q ，f ) _ 那么角色q 能识别出 m ；。是用 密钥k 加密的密文。 3 2 3 实例化函数和实例化空间 为了精确定义实例化函数和实例化空1 日j ，我们给定一个协议p 和 个c m e 模型 z = ( 朋，e ，a g ，p k ，s k ，l a b e l ，n o n c e ，l n i t ，r e c v ，s e n t ) ， 3 2 3 1 实例化函数 给定主体p a g 和一个标识消息c ，我们假设最多只有一个p 的局部 协议运行使用c 杯识。所以，我们可以用二元组( n f ) 表示p 在p 中使用c 的局部运行( 若确实存在的话) 。为方便起见，我们用，p 表示主体和标识 消息的二元组，而c 表示标识消息。 对于每个局部运行= ( p ，c ) ，我们定义。一个消息赋值函数 f ：m s g v 斗m 使得对于每个m m s g v ，厂( m ) 为在运行会话中那个 对应协议p 中的抽象的吖的具体的值。下列是( p ，c ，p ，) 一函数的定义和一 些重要性质。 定义3 2 设p a g ，c 为一标识消息，p 为一角色且，s 如。若以下条件成 立，我们称一个消息赋值函数f ：嬲( 0j m 为( p ，c ，p ，) 一函数。 1 f ( m ) 的类型由m 决定若a a g ，则f ( a ) a g ；对于每个标 识消息符号t m s g p ，f ( t ) l a b e l 。 和睦挂卜本地会【的奠牟m 议验汁逻辑分 斤t l s 饥议 2 ( a ) f ( p ) = p 。 ( b j 肘j 二每个n n o n c e ( p ) f ( n ) n o n c e ( p ) 。 ( c ) 肘于m i n i t ( p ) f ( m ) i n i t ( p ) 。 ( d ) 对于每个，和m p o s s ( p ，) 一r e c g ( p 1 3 ) ，存在一个，使 得厂( m ) p o s s ( p ，) 一r e c g ( p ，) 。 3 肘r 某个标识消息符号m p o