（计算机软件与理论专业论文）instantiation+space逻辑在公钥认证协议形式化分析中的应用.pdf

i n s t a n t i a t i o ns p a c e 逻辑在公钥认证协议 形式化分析中的应用 专业：计算机软件与理论 硕士生：晏青 导师：苏开乐教授 摘要 网络的普及为社会生活带来无限便利的同时，其易攻击性也会导致不 可估量的后果，如何保障网络安全已是当今开放的网络亟待解决的问题。安 全叻、议是网络安全的有效保障手段之一，而安全协议的可靠性问题受到越 来越多的关注。 安全协议形式化分析方法在近3 0 年得到了迅速发展。i n s t a n t i a t i o n s p a c e 逻辑是苏开乐教授提出的用于安全协议形式化证明方法中的模态逻 辑，它将知识推理运用到安全协议形式化分析中，并开发了相应的自动化验 证工具s p v 。 本文将i n s t a n t i a t i o ns p a c e 逻辑应用于公钥认证协议的形式化验证中， 选取了s p l i c e a s 和d e n n i n g s a c c o 两个典型的公钥认证协议，利用该逻辑 系统公理进行了严格、准确地推导和分析，得出了i n s t a n t i a t i o ns p a c e 在公 钥认证协议中对于防止伪装攻击的有效性，同时也指出了该逻辑在验证多 重会话攻击上是不完备的。 在进行公理推导的基础上，本文还利用工具s p v 对更多的公钥认证协 议进行了自动化验证，与协议推导取得了一致的验证结果。通过推导和工具 的互补检验，证明t i n s t a n t i a t i o ns p a c e 逻辑及其工具s p v 在公钥认证协议 验证中的正确性和可靠性。 关键词：安全协议形式化分析，认证协议，i n s t a n t i a t i o ns p a c e 逻辑，知 识理论，伪装攻击，多重会话 i i i t h ea p p l i c a t i o no fi n s t a n t i a t i o ns p a c el o g i ci n f o r m a la n a l y s i so fp u b l i ck e ya u t h e n t i c a t i o n p r o t o c o l s 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 ： f a nq i n g s u p e r v i s o r ：p r o f k a i l es u ab s t r a c t t h ep r e v a l e n c eo fn e t w o r kh a sb r o u g h ti nh u g ec o n v e n i e n c et os o c i a l l i f e ，b u ti t sv u l n e r a b i l i t yw i l ll e a dt od i s a s t e r h o wt oe n s u r et h es e c u r i t y o fn e t w o r kh a sb e e nah e a ti s s u e s e c u r i t yp r o t o c o l sa r ee f f i c i e n tm e a n st o p r o t e c tt h en e t w o r k ，a n dt h es e c u r i t yo fs e c u r i t yp r o t o c o l sh a sb e e nt h ef o c u s t h ef o r m a la n a l y s i sa p p r o a c h e so fs e c u r i t yp r o t o c o l sh a v eb e e nr a p i d l y d e v e l o p e di nt h ep a s t3 0y e a r s p r o f k a t i es uh a sp r e s e n t e dan e wm o d e l o fs e c u r i t yp r o t o c o ll o g i cc a l l e di n s t a n t i a t i o ns p a c ew h i c ha p p l i e sk n o w l e d g e r e a s o n i n gi na n a l y s i so fs e c u r i t yp r o t o c o l s ，a n dt h ec o r r e s p o n d i n ga u t o m a t i c t o o ls p vh a sb e e nd e s i g n e da n di m p l e m e n t e d b u ta st h ef r e s h n e s sa n di m m a t u r i t yo ft h i sl o g i c ；i tc a l l sf o ram o u n to fi n s t a n c e st oc h e c kt h ec o r r e c t n e s s a n de f f i c i e n c yo fi t t h i sp a p e ra p p l i e dp r e c i s e ，c o r r e c td e d u c t i o na n dp r o o fo n2t y p i c a l p r o t o c o l ss p l i c e a sa n dd e n n i n g s a c c ou s i n gt h ei n s t a n t i a t i o ns p a c el o g i c s y s t e ma n dr e v e a l e dt h ee f f i c i e n c yo ft h i sl o g i ci nd e t e c t i n gi m p e r s o n a t i o n a t t a c kb u td e f i c i e n c yo fm u l t i p l es e s s i o n sa t t a c ki np u b l i ck e ya u t h e n t i c a t i o n p r o t o c o l s o nt h eg r o u n do fd e d u c t i o n ，t h ep a p e rc h o s eam o r es e r i a l so fp 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 st ou s et h et o o ls p v f o ra u t o m a t i cv e r i f i c a t i o n a n dg o te x p e c t e dr e s u l t s i td r a w st h ec o n c l u s i o nt h a ti n s t a n t i a t i o ns p a c e l o g i ca n di t sa u t o m a t i ct o o ls p vi sc o r r e c ta n de f f i c i e n ti np u b l i ck e ya n t h e n t i c a t i o np r o t o c o l s k e y w o r d s ：f 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 s ，a u t h e n t i c a t i o np r o t o c o l ，i n s t a n t i a t i o ns p a c el o g i c ，k n o w l e d g et h e o r y ，i m p e r s o n a t i o na t t a c k ，m u l t i p l es e s s i o n s iil卜 第1 章概述 1 1选题背景 随着信息技术的发展，网络已逐渐渗透覆盖了社会牛活的各个领域，网络 的开放性不仅是其带来便利性的基础，同时也是网络通信中安全隐患的根源， 网络通信安全已成为制约网络发展的瓶颈，为了保障存开放的网络环境下主体 问安全可靠的通信，需要约定一系列的网络通信规范和约束，作为通信双方互 相遵循的准则，安全协议应运而生。 安全协议是为保障网络安全而设计，安全协议的运行结果能否达到它预期 设定的安全目标，即安全协议的安全性和可靠性问题是整个网络安全的坚实基 础，近3 0 年来，安全协议的分析技术和方法日益受到关注，主要发展了证明和证 伪两大类方法。证明方法是证明协议能满足某些安全属性，而证伪方法是搜索 协议漏洞，看是否存在着潜在攻击。 形式化技术的发展使得安全协议经过具体的验证之后，可能会检测出该协 议针对所期望的性质来说存在某些缺陷；对这些缺陷的整理有助于总结出一系 列安全协议的设计准则，以指导协议的设计，更有效的保障安全协议的可靠性。 苏开乐教授结合知识推理理论并将其运用于安全协议形式化验证领域，发 展了一套基于i n s t a n t i a t i o ns p a c e 语义模型的验证逻辑体系，该体系中定义的模 态逻辑在本文中称为i n s t a n t i a t i o ns p a c e 逻辑。i n s t a n t i a t i o ns p a c e l 锣_ 辑体系不仅 提供了一套足够完备的公理模式来对协议进行验证，同时也能在算法上实现该 理论，已开发了相应的自动化验证工具s p v 。但是该逻辑理论刚刚提出，且还在 逐步完善过程中，其正确性虽然已部分通过理论的证明，但是还需要通过大量 的实例验证来证明其正确性和可靠性。 本文将针对i n s t a n t i a t i o ns p a c e 逻辑在公钥认证协议中的应用，选取 典型公钥认证协议进行分析和推导证明，并辅以s p v 工具进行验证，以检 验i n s t a n t i a t i o ns p a c e 理论的有效性和可靠性。 2i n s7 弘n t i a t l 0 ns p a c e 逻辑在公钥认证协议形式化分析中的应用 1 2安全协议基础知识 安全协议是双方在网络环境下通信需要遵循的规范和约定，以确保建立双 方的信任和通信的安全通道。安全协议以密码体制为基础，定义了双方通信的 消息格式，通过安全协议的运行一般可以达到以下一些目标：如认证协议的目 标是认证参加协议的主体的身份，还有许多认证协议有附加的目标，即在主体 之问安全地分配密钥或其他各科t 秘密；非否认协议的目标包括确认发方非否认， 即非否认协议向接收方提供不可抵赖的证据，证明收至0 消息的来源的可靠性和 确认收方非否认即非否认协议向发送方提供不可抵赖的证据，证明接收方已收 到了某条消息；电子商务协议的目标除认证性、非否认性之外，还有可追究性、 公平性等等。本文针对的协议主要是采用公钥加密的认证协议。 1 2 1 安全协议系统模型 对安全协议的分析，不能孤立进行，需要考虑其实际的运行环境，为了便于 分析，将安全协议运行的网络环境抽象成如下的模型：将协议及其所处的环境 视为一个系统，在这个系统中，包括发送和接收消息的诚实的主体和一个攻击 者以及用于管理消息发送和接收的规则。协议的合法消息可被攻击者截取、重 放和篡改。攻击者的行为归纳起来表现为以下几种形式：即著名的d o l v e y a o 模 型” 将消息发送到其意定接收者； 延迟消息的送达； 将消息篡改后转发； 将消息与以前接收的消息合并； 改变部分或全部消息的目的地址； 重放消息。 在认证系统中，假设每一个主体与可信服务器之间共享一个秘密密钥，密钥是通 过离线方式建立的。当两个主体要进行秘密通信时，它们要建立一个仅为其所知 第1 章概述 3 的秘密密钥，这个秘密密钥的作用相当于一个秘密通道，不知道密钥的攻击者无 法干扰通信。 1 2 2 重要的安全协议 n e e d h a m s c h i o e d e l 协议2 1 是最为著名的早期的认证协议，许多广泛使用的 认证协议以n e e d h a m s c h r o e d e r 协议为蓝本而设计，它电是安全协议分析的“试 验床”，每当出现一个新的形式化分析方法，都要先分析这几个安全协议，验证 新方法的有效性。本文应用的i n s t a n t i a t i o ns p a c e 逻辑已经通过了n s 协议的形 式化分析。1 9 9 7 年，c l a i k 季w j a c o b 对安全协议进行了概括和总结，列举了一系列 有研究意义和i 实用价值的安全协议他们将安全协议进行如下分类f 3 1 ： 1 无可信第三方的对称密钥协议。属于这一类的典型协议包括以下i s o 系 列协议：i s o 对称密钥一遍单边认证协议、i s o 对称密钥二遍单边认证 协议、i s o 对称密钥二遍相互认证协议、i s o 对称密钥三遍相互认证协 议、a n d r e w 安全r p c 协议等。 2 应用密码校验函数( c c s ) 的认证协议属于这一类的典型协议包括以 下i s o 系列协议：i s o 应用c c f 的一遍单边认证协议、i s o 应用c c f 的二 遍单边认证协议、i s o 应用c c f f l j - - 遍相互认证协议、i s o 应用c c f 的三 遍相互认证协议。 3 具有可信第三方的对称密钥协议属于这一类的典型协议包括n s s k 协 议、o t w a y r e e s 协议、y a h l o m 协议、大嘴青蛙协议、d e n n i n g s a c c o 协 议、w o o l a m 协议等 4 对称密钥重复认证协议属于这一类的典型协议有k e r b e r o s 协议版 本5 、n e u m a n s t u b b l e b i n e 协议、k a o c h o w 重复认证协议等 5 无可信第三方的公开密钥协议属于这一类的典型协议包括以下i s o 系 列协议：i s o 公开密钥一遍单边认证协议、i s o 公开密钥二遍单边认证协 议、i s o 公开密钥二遍相互认证协议、i s o 公开密钥三遍相互认。 4i n s t a n t i a t l 0 ns p a c e 逻辑在公钥认证协议形式化分析中的应用 6 有可信第三方的公开密钥协议属于这一类的典型协议包括：s p l i c e a s 协 议，d e n n i n g - s a c c o 协议，s d c c i t tx 5 0 9 协议，该类协议即是本文的研究 对象。 1 3安全协议分析方法现状 如何保证安全协议能够满足其预期的安全性质，则需要借助安全协议分析 方法来对安全协议的各种性质进行验证。 对安全协议进行分析通常有两种方法，一种是攻击检验的方法；种是形 式化的方法。 攻击检验的方法是采用已知的攻击方法，逐个对协议进行攻击，如果发现 攻击是有效的，那么证明协议是不安全的。攻击检验可以验证协议有无已 知类型的安全漏洞，但不能验证能否对付新出现的攻击。 形式化的方法是采用一种正规的、标准的方法对协议进行分析，以检查协 议是否满足其安全目标。形式化方法基于严格的数学基础，具有精确的语 法和语义，能够检测到安全协议中的细微的漏洞。 目前大量的研究工作都集中在形式化的分析方法上。 1 3 1 安全协议形式化分析思路 安全协议形式化分析的思路为： ( 1 ) 用相应的形式语言来对所要分析的密码协议进行形式化描述，并且用形式 化需求语言来形式化地描述协议安全的需求。 ( 2 ) 将协议的形式化描述和形式化需求提交给具体的形式化系统，再用该系统 的方法来进行验证，验证安全协议是否满足其所说明的安全需求。 1 3 2安全协议形式化描述 针对一个安全协议进行分析时，首先需要使用某种形式语言来对该协议进 行描述。各种形式化方法都有自己的一套形式语言来对安全协议进行形式化描 述。 第1 章概述5 由于不同的形式化系统都以方便自身进行分析为目的而采用不同的形 式化语言，为了克服这种在协议描述上的不统一而导致的不同分析系统在进 行相互交流时的障碍，出现了一种通用性较强的安全协议的形式描述语言一 一c a p s l 。 c a p s l 4 1 ( c o m m o na u t h e n t i c a t i o np r o t o c o ls p e c i f i c a t i o nl a n g u a g e ) 是由 m i l l e n 所开发的运用于安全认证协议和密钥分配协议的高级语言，它被设计为 不同形式化分析工具的形式化输入。c a p s l 的理念是成为协议的任意种形式 化分析二 具的形式化输入的一个单独的通用的协议说明语言。 1 3 3 安全协议的形式化需求 形式化需求语言用来形式化地描述安全协议必须满足的安全特性，并将这 些安全特性作为协议验证时的指标以及协议设计时的指导。由于不同的安全协 议有其不同的需求，因此，在对安全协议的分析过程中，需要对此需求集进行不 断的维护( 包括增、删、改) 。作用于该形式化需求之上的协议分析器，可看作是 作用于该需求语言之上的语义模型检查器，从而可使得形式化需求与形式化分 析二者相互促进、共同发展。 虽然在安全协议的形式化描述和需求方面已经做了一些工作，但此领域仍 然很少涉及。目前人们在安全协议中采用形式化方法进行研究时，主要工作集 中在了对协议安全性的验证方面。 1 3 4 安全协议的形式化验证 1 3 4 1 模态逻辑的方法 模态逻辑由一些命题和推理规则组成。命题表示主体对消息的知识或者 信仰，运用推理规则可以从已知的知识和信仰推导出新的知识和信仰。最著名 的是b a n 及b a n 类逻辑【5 】，其次是用于分析电子商务协议可追究性的k a i l a r 逻 辑 6 ，较新的研究是k i n d r e d 提出的安全协议的生成理论r v 逻辑7 1 。 1 9 8 9 年，b u r r o w s ，a b a d i h e 矛h n e e d h a m 提出了基于信仰的b a n 逻辑5 1 ，是 安全协议分析的一个里程碑。b a n 逻辑的基本思想是通过对认证协议运行过程 中消息的接收和发送来从最初的信仰逐渐发展到协议运行所要达到的目的一一 6 i n s t a n t i a t l 0 ns p a c e 逻辑在公钥认证协议形式化分析中的应用 主体的最终信仰。b a n 的使用基本分为四个步骤： ( 1 ) 给出协议的初始状态及其所基于的假设； ( 2 ) 对协议进行理想化； f 3 ) 形式化说明协议将达成的安全目标； ( 4 ) 根据初始假设和仂、议会话事实，应用推理规则进行推理，验证协议是否满 足其安全目标。 b a n 逻辑只能分析安全协议的认证属性不能分析保密属性，并且其最大问题 是不够完备，g i b a n 逻辑不能查出协议的所有问题：如果b a n 证明一个协议是 有问题的，那么那个协议一定存在问题：如果b a n 逻辑证明一个协议是安全 的，却不能令人信服。许多研究人员对b a n 逻辑进行了大量的扩展和改进，包 括g n y 逻辑 8 】、a t l 矍辑【9 、s v o 逻辑【1 0 等，这些统称为b a n 类逻辑。 1 3 4 2 模型检测方法 模型检测法也叫状态空问搜索法，它是- - g e e 验证有限状态系统的自动化 技术。其基本思想是使用规范语言( 一般采用有限状态自动机) 对系统进行建 模，使用逻辑语言( 一般采用时态逻辑) 对系统需要满足的性质进行描述，使用 状态的搜索算法来确定系统的模型是否满足期望的性质。常用的模型检测工具 有i n t e r r o g a t o r 、n r l 、f d r 、m u r 、s m v 等。 i n t e r r o g a t o r 1 1 是m i l l e n 等人提出的基于状态机技术的协议分析器，也是这 方面最早的协议分析系统。i n t e r r o g a t o r 采用前推搜索，即从初始状态起寻找到 达最终的不安全状态的可能路径。 n r l ( n a v a lr e s e a r c hl a b o r a t o r y ) 是m e a d o w s 等开发的模型检测工具 1 2 】， 也是这类系统中应用最为广泛的协议分析器，n r l 结合了模型检测技术和定理 证明技术。n r l 采用倒推搜索，即从最终的不安全状态起寻找是否存在可到达 初始状态的路径。 1 9 9 6 年，l o w e r 首先使用通信顺序进程( c o m m u n i c a t i o ns e q u e n t i a lp r o c e s s e s - - - - c s p ) 模型5 9 l f d r ( f a i l u r ed i v e r g e n c e sr e f i n e m e n t ，故障偏差精炼检 第1 章概述7 测器) 工具来对密码协议进行分析f 1 3 1 ，并且成功地发现了n e e d h a m - - s c h r o e d e r 公 钥协议中一个近1 7 年来未知的并行话路攻击缺陷。f d r 被j 一、。+ 泛应用于对分布式 数据库和通信协议的分析。m u r 语言是- , 0 e 用来描述非确定有限状态机的高级 语言1 4 】，其许多特征都与一般的程序语言相似。它先将所期望的密码协议的性 质描述为不变式，然后将采用深度优先或者广度优先的方式来穷举搜索所有的 状态，对于每个状态判断所给出的不变式是否保持为真，如果在到达的某个状 态时某个不变式不成立，m u r 0 5 将给出导致该错误的状态序列。 s m vf s y m b o l i cm o d e lv e r i f i e r ) 是美 c a r n e g i em e l l o n 大学计算机学院 的l m c m i l l a n 博士于1 9 9 2 年开发出的模型检测工具。s m v 程序由两部分组 成：有限状态转换系统和c t l ( c o m p u t a t i o nt r e el o g i c ) 公式。将这两部分输入 到s m v 系统并运行s m v 系统后，若有限状态系统满足c t l 所捕述的属性， 则输出真，否则输出假，并同时生成不满足属性的反例。在s m v 中，布尔公 式用高效率的o b d d s ( o r d e r e db i n a r yd e c i s i o nd i a g r a m s ) 来表示和操作，因 此，s m v 能有效地缓解状态爆炸问题。 模型检测的优点是自动化程度高，若协议有缺陷能自动产生反例。但是其 不足之处是容易产生状态空间爆炸问题；需要限定协议参与主体的数目。但是 随着基：f b d d ( b i n a r yd e c i s i o nd i a g r a m s ) 的符号方法的引入，模型检测技术 已由原来只能对几千个状态进行有效处理增到能对1 0 1 2 0 个状态进行搜索。 1 3 4 3 定理证明方法 定理证明是对形式化后的协议模型和规约，运用证明的技术来证明规约是 否在协议模型中满足。该方法是证明公式在所有的模型都成立。其目的是证明 协议满足安全属性，而不是去寻找协议的攻击，所以定理证明方法针对的是安 全协议的正面，而模型检测方法针对的是安全协议的反面。定理证明的方法主 要有p a u l s o n 归纳法、串空间模型、秩函数等。 p a u l s o n 归纳法 1 5 1 j 将协议定义为所有可能事件执行序列的集合，每个执行 序列反映了主体之间可能的通信方式。在证明以前，消息需要转化成协议规 则，在证明过程中，主体可以按照协议规则扩展事件执行序列。使用定理证明 器i s a b e l l e 可以自动产生证明。 8i n s t a n t i a t i o ns p a c e 逻辑在公钥认证协议形式化分析中的应用 串空问是诚实主体和攻击者的串组成的集合【1 6 ，1 7 】。串是协议中主体可以 执行的事件序列，它既可以代表合法主体行为也可以代表攻击者行为。丛是串 空间的子集。在这种模型下，协议的正确性可以表示成不同类型串之间的连接 关系。协议的正确性证明过程是先建立协议规范可能形成的所有丛，然后根据 丛中攻击者串的连接情况，判断协议的安全属性是否满足。p e r r i g 并1 s o n g 等对串 空间模型进行了重要的扩展，将其推广到分析三方安全协议。 秩函数f 1 8 1 是一个把攻击者的知识和协议消息映射成整数的函数。使用秩 函数可把消息分成两类：攻击者可以得到的消息，它们的秩函数的值为大于o 的 整数；攻击者不可以得到的消息，它们的秩函数的值为小于或等于0 的整数。对 于认证属性，认证条件定义为事件e 1 必须先于事件e 2 发生，然后在用c s p 建立 的协议模型中阻一i 二事件e 1 发生，然后通过检查事件e 2 对应消息的秩函数的值来 判断该事件是否会发生，如果秩函数的值小于等于0 ，就说明在e l 不发生的条件 下，e 2 也不会发生，说明认证属性满足，否则就不满足。对于保密属性，就是检 查保密消息的秩函数是否小于等于0 。 定理证明的实施需要定理证明器的支持。现有的定理证明器包括：用户导 引自动推演工具、证明检验器和复合证明器。 定理证明的方法不同于模型检测，其优点是通过状态的简化可以处理无限 状态空间问题，不足之处是该方法难以完全自动化。 i 3 4 4 其他方法 近来也出现了一些其它的形式化方法。比较典型的是s p i 一演算和类型检 查( t y p ec h e c k i n 9 1 方法。 1 9 9 7 年，a b a d i 和g o r d o n 在p i 演算的基础上增加支持安全协议描述和验证 的原语，建立t s p i 演算 1 9 】o 分析安全协议时，安全属性是通过两个系统的观 测等价来实现的。一般来说，一个系统表示协议的并行进程运行模型；另一个系 统表示协议规范的并行进程运行模型。如果第三者不能区分这两个系统的行为， 说明这两个系统是观测等价的，也就是协议是安全的。s p i 的优点是语法描述简 洁，对安全协议的刻画能力很强。但是不足之处是目前还缺乏相应的工具支持。 使用类型检查分析安全协议的属性是a b a d i 提出的2 0 。a b a d i 使用类型 第1 章概述9 检查分析了协议的保密属性，如果协议能通过类型检查，那么协议就不会泄漏 秘密。类型检验方法的优点是只需对协议模型进行静态分析，而不需要遍历大 的状态空间。 1 4研究意义 1 4 1 安全协议设计的困难性 安全协议的设计极易出错，即使安全协议中最基本的认证协议，其中参加 协议的主体只有两三个，交换的消息只有3 5 条，设计一个正确的、符合认证目 标的、没有冗余的认证协议也十分困难。 从1 9 7 8 年n s p k 协议问世以来，至1 l o w e 于1 9 9 6 年发现n s p k 协议的索全缺 陷，已经过去了大约1 7 年之久。安全协议设计的困难性和安全协议分析微妙 性，由此可见一斑。 安全协议设计与分析的困难性在于： 1 安全目标本身的微妙性。仞j 如，表面上十分简单的“认证目标”，实际上十 分微妙。关于认证性的定义，至今存在各种不同的观点； 2 协议运行环境的复杂性。当安全协议运行在一个十分复杂的公开环境时， 攻击者处处存在。要形式化地刻画安全协议的运行环境是一项艰巨的任 务； 3 攻击者模型的复杂性。必须形式化地描述攻击者的能力，对攻击者和攻击 行为进行分类和形式化的分析； 4 安全协议本身具有“高并发性”的特点，因此，安全协议的分析变得更加 复杂并具有挑战性。 1 4 2i n s t a n t i a t i o ns p a c e 逻辑在形式化分析方法中的优势 3 0 年来，为了应对安全协议设计的困难性这一挑战，已设计了不同种类的 形式化分析方法，取得了可喜的成果，但是目前的分析方法还或多或少存在不 足，主要的问题是： 1 0i n s t a n t i a t i o ns p a c e 逻辑在公钥认证协议形式化分析中的应用 1 不完备性：现存的公理系统不够完备，使得某些属性因为这种不完备性而 无法证明。 2 自动化和可扩展性：在d o l e v y a o 模型下证明协议的正确性的理论有很 多，如d u r g i n 的协议组合逻辑( 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 1 】，p a u l s o n 的 归纳法 2 2 】：b l a n c h e t 的p r o v e r i f 2 3 】，等等。但是，它们要么不是完全自动 化实现的，要么是无法有效扩展和处理大规模的工业级的复杂协议的。 苏开乐教授提出的i n s t a n t i a t i o ns p a c e 逻辑力求解决上述两个问题。由于协 议的验证是个不可判的问题2 4 1 ，所以理论上是不存在完备的验证公理系统的， 因此，该逻辑研究的重一0 ，是提供一套公理模式，使得对于验证工业级的复杂协 议的相关安全属性，是足够完备的。该逻辑还解决了自动化验证和可扩展性的 问题。由于该逻辑系统在算法上的可行性，对应的工具s p v ( s e c u r i t yp r o t o c o l v e r i f i e r l 已经开发成功，并且可以验证复杂的协议由于在此语义基础上的公理 集是纯命题逻辑的因此所需要的验证目标可以很方便地转化成可满足性问 题( s a t ) ，从而可以利用工业上快速高效的s a t 求解器求解，使得s p v 可以高效 验证复杂的包括工业级的安全协议性质。 i n s t a n t i a t i o ns p a c e 逻辑虽然在理论上很好地解决了上述两个问题，但是该 理论还处于不断成熟和完善阶段，还未经受大量实例的检验，需要通过实例来 证明其可靠性，以及在实例中发现公理系统中不完备之处，力求逐步完备公理 系统，在1 2 2 中已经指出，安全协议有很多，不可能在文中一验证，本文主 要针对公钥认证协议这一大类协议，选取其中有代表性的协议来进行实例验证， 通过将i n s t a n t i a t i o ns p a c e 逻辑应用于实例中来力求证明其有效性和可靠性。通 过理论推导和实际使用s p v 2 1 2 具进行互补验证，能证明理论和工具在公钥认证 协议中的有效性，则可以在今后的工作中，公钥认证协议这一类协议就可以直 接利用s p v t 具来进行自动化验证，有效地解决了这一类协议的验证问题。 本文的结构安排如下： 1 5 论文组织结构 第1 章概述 第一章介绍本文的选题背景，安全协议的相关知识，以及安全协议形式化 分析方法现状，指出了本文的研究意义； 第二章详细介绍了苏开乐教授提出的i n s t a n t i a t i o ns p a c e 理论逻辑，以及将 认知逻辑应用于安全协议形式化验证中的方法； 第三章是本文的核心工作，即将i n s t a n t i a t i o ns p a c e 理论应用于公钥认证协 议的形式化分析和验证中，进行严格的形式化推导和证明； 第四章是在前一章的基础上，利用i n s t a n t i a t i o ns p a c e 理论的自动化验证工 具s p v 进一步对更多的公钥认证协议进行验证，以进一步确定该理论及工具在 公钥认证协议验证中的可靠性； 第五章总结了本文的研究成果，并提出了对未来工作的一些展望。 第2 章实例化空间 苏开乐教授在f 2 5 ，2 6 ：2 7 t 作的基础上，系统地提出了一个安全协议验证 逻辑的新的语义模型，称为“实例化空间( i n s t a n t i a t i o ns p a c 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 ) 模型上，并 在此语义模型基础上，提出了一系列与安全属性相关的验证公理，并证明了它 们在此语义模型下的正确性。这些公理比现有的一些验证逻辑，如f 2 1 1 中的谓 词s o u r c e 以及2 8 1 中的c h a l l e n g e r e s p o n s ea x i o ms c h e m a 和s e n d r e c e i v ea x i o m s c h e m a ，能刻画更一般的情形。本章将详细介绍整个理论体系的构成，所介绍 概念和方法都是基于苏开乐教授及其实验小组的最新研究成果。安排如下：第 一节先介绍知识推理理论，第二节中介绍加密信息交换模型( c m e ) ，第三节介 绍语义模型“实例化空间f i n s t a n t i a t i o ns p a c e ) ”，第四节给出此模型上的公理系 统。 2 1基于知识理论的推理 苏开乐教授提出了一种基于变量忘记的知识推理方法 2 0 i 。在这一新的推 理框架下，我们可以处理公共知识( 或公理系统) 以及公共知识中的变量的可 观察性问题。并且，可以将知识推理转换成命题逻辑的可满足性问题。 2 1 1 观察理论( o b s e r v a t i o nt h e o r y ) 定义有礼个智能体的观察理论( o b s e r v a t i o nt h e o r y ) f 是一个n + 2 元 组( ke ，0 1 j _ d 。) ，其中y 是有限变量集，o 定义在y 上的公式集，对每个 智能体i ，0 i 是y 的子集。并且y 中的变量称为该观察理论的系统变量( s y s t e m v a r i a b l e s ) ，0 i 中的变量是智能体i 的可观察变量( o b s e r v a b l ev a r i a b l e s ) 。g 称为公 共知识fc o m m o nk n o w l e d g eb a s e ) ；直观上说，它是关于智能体和它们所在的通 信环境的一系列共同假设。为方便起见，有时用e 表示e 中所有公式的合取。 1 4i n s t a n t i a t i o ns p a c e 逻辑在公钥认证协议形式化分析中的应用 2 1 2 可观察公式和变量( o b s e r v a b l ef o r m u l a sa n do b s e r v a t i o n s ) 定义2 1 给定观察理论( vo ，0 1 ：o n ) 和公式妒。对所有isn ，p 被# 2 i 一可 观察的丘o b s e r v a b l e ) ，如果妒是q 上的公式。只表示所有i 一可观察的公式的集 定义2 2 给定观察理论( k o ，0 1 ：0 。) 和公式妒。对所有i n ，定义k 妒为 如下的公式： v o l o e e r ，e 卜。号垆 根据定义，k 咿成立，当且仅当存在i 一可观察的公式q 使得q 成立，且在 公共知识e 下，a 逻辑蕴涵妒。直观上看，妒表示智能体i 能观察到公式妒成 立( 或者简单来说，智能体i 观察到垆) 。 命题2 3 g i v e na no b s e r v a t i o nt h e o r y ( ve ：0 1 ，0 。) a n da ni - o b s e r v a b l e f o r m u l aa e 卜_ q 铮k q 例1 考虑a 舷c e 和b 0 6 之间通信的例子。a l i c e 发送给b d 6 一条消息，b d 6 收到该 消息后发送确认给a 舷c e 。假设a 舷c e 和b o b 都知道如下的公共知识e a b b o b _ r e c v m s g a l i c e s e n d m s g b o b s e n d a c k b o b r e c v m s g a l i c e r e c v a c k b o b s e n d a c k 其中，b o b r e c v m s g 乖, b o b s e n d a c k 是b d 6 的可观察变量，a l i c e s e n d _ m s g 和a l i c e r e c v a c k 是a 跣c e 的可观察变量。由此，得到观察理论 其中 r a b = ( v b ，o a b ，o a ，o b ) 0 a = a l i c e s e n d _ m s g ，a l i c e _ r e c v a c k 0 b = b o b r e c v m s g ，b o b s e n d a c k ) 玖b = o a uo s 第2 章实例化空间 1 5 不难得出o a bf - a l i c e r e c v a c k 心k b a i i c e s e n d m 阳的结论，表示如 果a l i c e4 j c 至0 了b 0 6 的确认，那么a l i c e 观察至j j b o b 观察至1 a l i c e 发送了消息。但 是，不能得出o a b 卜a l i c e r e c y a c k 号k a k b a l i c e r e c v n c 后的结论；也就是 说，即使a 跣c e 收到了b d 6 的确认，a l i c e 也不一定观察到b o b 观察至l j a l i c e 收到 了b d 6 的确认。 2 1 3 观察性和可满足性( o b s e r v a t i o na n ds a t i s f i a b i l i t y ) 给定观察理论( ke ；0 1 0 。) ；其中，o 表示o 中所有公式的合取。 命题2 4 对y 上的任意公式妒和j 一可观察公式o l ，e 卜q 号k 妒当且仅当ea o la 一是不可满足的。 通过上述定理，规范q 号k 妒的验证问题可以转化成eaq 八一妒的可满足 性问题。 在介绍下面的定理之前，需要引入一个符号的定义。给定o 。；的个赋值或 子集盯，和公式，公式q 盯是由对进行如下的赋值变换而来：用t r u e 替换盯 中的变量，用如f s e 替换d p ，一盯中的变量。 命题2 5 对y 上的任意公式妒和i 一可观察公式口，ef - k k j 妒当且仅当对 于q 的每一个赋值盯，如果o 盯aa 盯是可满足的，那么( ea 一妒) o - 是不可满足 的。 根据以上的结论，如果o j 中的变量数很少，那么可以使g s a ts o l v e r 检验 形如q 令k i 心妒的规范。 2 2 加密信息交换模型( 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 m o d e l ) 2 2 1 预备知识一一消息代数( m e s s a g ea l g e b r a l 在协议中，存在三种消息类型：明文消息，组合消息和加密消息密钥属于 明文消息一个消息代数是一个二元组( m ，j i c ) 且j i c m ，加上以下操作组成： 1 6 i n s t a n t i a _ t i o ns p a c e 逻辑在公钥认证协议形式化分析中的应用 逆钥：如果k 瓦，男b 么尼一1 瓦 组合：如果m 1 ：一，仇。m 那么 m l ，m 。l m 分解：如果【m 1 一：m 。】mn 么m l ，m 。m 加密：如果k 瓦，7 n m 且m 不具备 m 7 ) 七一的形式，那么 m ) k m 解密：如果岛- 1 瓦且 m ) 瓦，那么m m 有如下两个假设： 1 如果m 1 ) l = m 2 k 2 那么m 1 = m 2i l k l = k 2 ； 2 如果 m 1 ，：m 。】= 【m ：，m ：，】那么有礼= 仡7 ，且对于o i 咒， 有m i = m ：。 给定一个消息集合m7 ，一个密钥集瓦7 ，和一个消息m o 。一些符号的定义如 下： 1 d ( m7 ) 是一个由消息集m7 通过加密，解密，分解和组合形成的消息集。 2 c l _ ( m7 ) 是一个由消息集m7 通过解密和分解形成的消息集。 3 s u b ( m o ，c 7 ) 是- - m o 通过使用瓦7 中的密钥进行加密和解密形成的消息集。 类似地，定义s u b ( m7 ，疋7 ) = u 。m ，s u b ( m ，瓦，) 4 f r e s h ( m o ) 是由消息m o 产生的消息集。如果m o 是一个新鲜s j n o n c e ，那 么f r e s h ( m o ) 中的消息都是新鲜的。 2 2 2 加密信息交换模型( 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 em o d e l ) ( 或简称 为c m e 模型) 是；n t 的一