（计算机软件与理论专业论文）安全协议的形式化分析技术与方法的应用研究.pdf

南京邮电大学硕二l 研究生学位论文摘要 摘要 安全协议是用来保证电子商务等网络通信安全的重要工具。形式化方法是当今分析 安全协议的一类主流方法，但是不同的形式化方法各有优劣，且应用形式化方法研究安 全协议在理论和实践上还不够充分。 论文对b a n 逻辑进行了较为全面地介绍，并在此基础上探讨了将其应用于协议认证性 形式化分析中的优势和具体方法。为分析y a h a l o m 协议认证性，论文给出了y a h a l o m 协议 基于s v o 逻辑的模型，并通过详细的推理分析了y a h a l o m 协议的认证性质。 为了进一步分析协议的机密性等性质并对协议本身进行更深入研究，论文引入串空 间理论，接着对其中的丛理论、攻击者行为定义、“理想 和“诚实等概念作了深入 剖析。然后，利用串空间方法建立b a n - y a h a l o m 协议的形式化模型，并全面分析了其安全 性质，证明了其中的安全缺陷并找出其原因，随后提出了积极的修改方案并对协议进行 修改。 为使对安全协议的分析能逐渐自动化，论文详细介绍了使用模型自动校验器s p i n 的 基本方法，以及p r o m e l a 语言的关键技术。以n s p k 协议为例，论文提出了利用s p i n 进行协 议建模的基本思想、算法和技术，并深入介绍了建立n s p k 协议模型的具体方法，模型仿 真执行的结果也反映出文中所述的建模方法是可以收到良好效果的。 关键词：安全协议，形式化分析，b a n 逻辑，串空间，s p i n 南京邮电大学硕士研究生学位论文 a b s t m c t a bs t r a c t s e c u r i t yp r o t o c o li sa ni m p o r t a n tm e o x i st og u a r a n t e et h es a f e t yo fn e t w o r kc o m m u n i c a t i o n l i k ee l e c t r o n i cb u s i n e s s f o r m a lm e t h o d st a k et h em a i ns t r e a mi na n a l y z i n gs e c u r i t yp r o t o c o l s b u td i f f e r e n tf o r m a lm e t h o d sb e h a v ed i v e r s e l y ；m o r e o v e r , i ti ss t i l ll e s ss u f f i c i e n tb o t h t h e o r e t i c a l l ya n dp r a c t i c a l l yw h e nu s i n gf o r m a lm e t h o d st os t u d ys e c u r i t yp r o t o c o l s t h i sp a p e ri n t r o d u c e sb a n l o g i cc o m p r e h e n s i v e l ya n dd i s c u s s e si t sa d v a n t a g ea n dd e t a i l e d m e t h o d so fa p p l y i n gt h i st h e o r yt oa n a l y z i n ga u t h e n t i c a t i o np r o p e r t i e so fp r o t o c o l s i no r d e rt o s t u d yt h ea u t h e n t i c a t i o nc h a r a c t e ro fy a h a l o mp r o t o c o l ，t h i sp a p e rm a k e sac o m p l e t em o d e lo f t h i s p r o t o c o lb a s e do ns v ol o g i c a n dt h e n i t sa u t h e n t i c a t i o np r o p e r t yi sp r o v e dt h r o u g h e l a b o r a t ed e d u c t i o n f o rd e e p e rr e s e a r c hi n t os o m ei n t e r n a lc h a r a c t e r sl i k es e c r e c ya n ds of o r t h ，t h i sp a p e ri m p o r t s s t r a n ds p a c et h e o r y , a n dt h e nm a k e sap r o f o u n da n a l y s i so fc o n c e p t i o n ss u c ha sb u n d l e ， d e f i n i t i o no fa t t a c k e r sb e h a v i o r , h o n e s ta n di d e a l s s u b s e q u e n t l y , f o r m a lm o d e lo fb a n y a h a l o mp r o t o c o li se s t a b l i s h e db ys t r a n ds p a c em e t h o d ，w h i c hi sl a t e ru t i l i z e dt oa n a l y s ei t s s e c u r i t yp r o p e r t i e sc o m p l e t e l y t h i sp a p e rn o to n l yp r o v e ss e v e r a ls e c u r i t yd r a w b a c k so fb a n y a h a l o mp r o t o c o l ，b u ta l s op u t sf o r w a r da c t i v es t r a t e g i e st om o d i f yt h i sp r o t o c 0 1 f o rt h es a k eo fa u t o m a t e da n a l y s i so fs e c u r i t yp r o t o c o l s ，t h i sp a p e rf i n a l l yd i s c u s s e st h e f u n d a m e n t a lp r i n c i p l e sa n de s s e n t i a lt e c h n o l o g i e so fu s i n gt h ee x c e l l e n tm o d e lc h e c k e rs p i n t o s e tn s p kp r o t o c o la sa ne x a m p l e ，t h i sp a p e rp r o p o s e ss o m eb a s i ci d e a l s ，a l g o r i t h m sa n d t e c h n i q u e si nm o d e l i n gp r o t o c o l sb ys p i n t h em o d e lo fn s p kp r o t o c o ld e p i c t e db yp r o m e l ai s a l s op r o v i d e db yd e t a i l e d d e s c r i p t i o ni nt h i sp a p e r s i m u l a t i o no ft h i sm o d e lr u n sa se x p e c t e da n d r e f l e c t st h a tm e t h o d sp r e s e n t e dm a k eg o o de f f e c t sw h i c hm a ya l s ob ea p p l i e di nm o d e l i n go t h e r p r o t o c o l 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 la n a l y s i s ，b a nl o g i c ，s t r a n ds p a c e ，s p i n i i 南京邮电大学学位论文独创性声明 本人声明所呈交的学位论文是我个人在导师指导下进行的研究 工作及取得的研究成果。尽我所知，除了文中特别加以标注和致谢的 地方外，论文中不包含其他人已经发表或撰写过的研究成果，也不包 含为获得南京邮电大学或其它教育机构的学位或证书而使用过的材 料。与我一同工作的同志对本研究所做的任何贡献均已在论文中作了 明确的说明并表示了谢意。 研究生签名：佘躲 南京邮电大学学位论文使用授权声明 南京邮电大学、中国科学技术信息研究所、国家图书馆有权保留 本人所送交学位论文的复印件和电子文档，可以采用影印、缩印或其 他复制手段保存论文。本人电子文档的内容和纸质论文的内容相一 致。除在保密期内的保密论文外，允许论文被查阅和借阅，可以公布 ( 包括刊登) 论文的全部或部分内容。论文的公布( 包括刊登) 授权 南京邮电大学研究生部办理。 研究生签名：么叁塑导师签名：趑日期：圭苎垒竺塑步月 南京邮电大学硕士研究生学位论文第1 章绪论 第1 章绪论 1 1 安全协议的形式化研究概述 自从d o l e v 和y a o 两位学者在1 9 8 3 年指出：可以将安全协议本身和其所采用的密码系 统分开独立研究后【l 】1 2 1 ，安全协议的正确性、安全性和冗余性等课题的研究就在假定密 码系统是“完善 的情形下展开了，使得安全协议本身逐渐发展成为一个相对独立的分 支学科。文献 2 的贡献不仅如此，另一个质的贡献在于提出了一个重要的理念：安全协 议的潜在攻击者可以掌握整个通信网络中的知识，从而控制协议的正常运行。这一假设 随着9 0 年代后i n t e r n e t 迅速发展逐步得到认可。 在此基础之上，一系列基于知识与信念推理的模态逻辑方法和基于定理证明的方法 等被相继推出【3 】1 4 ，其中最著名的就是b a n 逻辑推理方法。b a n 逻辑开创了安全协议形式 化分析的先河，其简单、易用的特点至今仍然使得很多学者对之青睐。然后，l o w e 在 1 9 9 6 年首次采用c s p ( 通信顺序进程) 方法和自动化模型校验器f d r 对安全协议进行形式 化分析，这为有限状态的协议模型验证开辟了新的道路。此后，g u t t m a n 等人在推出串空 间这种结合定理证明和协议迹的混合方法之后，把安全协议的形式化分析推向了新的高 度。 。1 2 国内外研究现状 形式逻辑和集合论为b a n 逻辑和串空间理论奠定了坚实的基础，因此国内近些年来比 较成熟的研究主要侧重于安全协议的证明和理论推导【5 l ，并取得了一定的成果，如文献 6 主要就针对协议中各主体的行为进行了扩展定义并对相关定理进行了部分修改和完善。 诸如此类的理论成果都使人们对安全协议本身性质及其网络环境的认识更加深入，也保 证了安全协议在应用上变得更加可靠。但是由于缺少成熟的工具，国内在安全协议的自 动化检测领域的研究却并不多见，主要是靠人工进行逻辑推理和定理证明来分析检测协 议的各种性质1 7 j 。 而国外近些年来在安全协议领域的研究，无论在理论还是在技术上都有不少长足的 进步，且理论成果也不断地促进了技术的革新和进步，如著名的a t h e n a 工具的研发就受 到了串空间理论的深刻影响。安全协议的自动化模型检测技术在a c m 于2 0 0 2 年授予 “s p i n ”软件系统奖之后有了一定的飞跃，而且在此之后的研究变得更为方便了。近年 南京邮电大学硕士研究生学位论文第1 章绪论 来s p i n 这一强大系统在对协议的建模、测试、改进以及设计方面的实际功效受到了广泛 关注，各种实验表明使用该工具对协议安全性进行检测和验证的效果很好。总之，结合 各种方法对已有安全协议进行检测和改进已经成为现在的热点问题，此领域的研究必将 在以后蓬勃发展。 1 3 本文工作概要 本文在安全协议的形式化研究领域，重点研究了以下内容： ( 1 ) 对b a n 及b a n 类逻辑进行了较为深入地研究，掌握从形式化逻辑假设到安全性 质推理的基本过程。使用b a n 类逻辑中的s v o 逻辑对y a h a l o m 协议建模，并对其认证性 质作出具体的分析证明。将原始的b a n 逻辑和s v o 逻辑进行对比，并提出对b a n 类逻辑 的几点修改建议。 ( 2 ) 深入研究串空间模型方法，对丛理论、“理想”和“诚实”理论等概念进行了 全面地剖析。分别应用这些理论衍生出的方法对b a n - y a h a l o m 协议的保密性和认证性进 行了详尽的分析，并针对分析得出的代数缺陷，提出几点修改原则，然后对b a n y a h a l o m 协议进行了修改且分析了改进后协议的特点。 ( 3 ) 深入了解模型建模工具的发展，着重研究s p i n 系统及其对应的p r o m e l a 语言。 重点提出了对n s p k 协议进行建模设计的思想和算法，并阐述使用p r o m e l a 语言实现模型 的关键技术。接着使用s p i n 对该模型进行行为模拟和属性校验。 1 4 论文组织结构 全文共分为五章，其组织如下： 第一章简要介绍了安全协议及安全协议形式化分析方法的基本概念，对相关背景和 国内外研究现状进行了广泛的研究，阐述了论文研究的价值和意义。 第二章详细论述了b a n 逻辑的概念及其分析协议的原理和方法，并以y a h a l o m 协议 的分析为例，深入剖析了s v o 逻辑分析协议认证性的机理。 第三章全面论述了串空间模型及其分析安全协议的基本方法，并用这些方法分析 b a n y a h a l o m 协议的认证性和机密性。最后提出改进b a n y a h a l o m 协议的方法。 第四章原理性地阐述了模型自动校验器s p i n 的特点，并对p r o m e l a 语言关键技术的 使用作了全面论述。对n s p k 协议进行了详细建模，再用s p i n 仿真执行该模型，并对其 进行了模型校验检测。提出了一系列有建设性的协议建模思想和方法，尤其是对潜在入 南京邮电大学硕士研究生学位论文 第1 章绪论 侵者的行为能力作了细致的描述。 第五章对所做的研究工作进行了总结，并对研究课题提出了进一步的展望。 南京邮电大学硕二e 研究生学位论文第2 章b a n 类逻辑的理论与应用 第2 章b a n 类逻辑的理论与应用 本章将首先介绍b a n 逻辑【8 】( b a n 由率先提出b a n 逻辑的三个作者名字的英文首字母 构成，以下的s v o 逻辑等也是如此) 提出的背景和理论基础【9 】，进而自然地引出b a n 类逻 辑；然后对b a n 类逻辑中比较成功的s v o 逻科1 5 1 进行系统地论述，并应用s v o 逻辑完成 对y a h a l o m 协议的认证性建模和分析。 2 1b a n 逻辑的基本概念 2 。1 1b a n 逻辑提出的背景 虽然d o l e v 和y a o 较早就在文献 2 中指出应当把对协议本身安全性的研究同对协议 所使用密码安全性的研究分丌来讨论，但是他们并没有在文章中给出一个切实可行的计 算方法。尽管d o l e v 和y a o 很有远见地指出了应当用形式化的方法来研究协议的安全 性，但是他们所提出的方法仅仅是对加密解密的一种描述，本质上并没有与密码系统完 全地脱离开来。事实上，文献 2 很重要的一个贡献是讨论了影响协议安全性的计算时间 的复杂度，这对后来的一些模型检测工具的设计和开发有着积极的指导意义，这一点本 文将在后续的章节论述模型检测工具s p i n 在协议建模方面的优势的时候有所涉及。 文献 8 的提出真j 下地对安全协议形式化分析产生了决定性影响，直至今日，这一理 论及其衍生出的形式逻辑仍被广泛地使用。文献 1 0 就很清楚地总结了b a n 逻辑的优 势，b a n 逻辑不仅可以很容易地被其他协议认证方式所利用，更可以在协议的自动化设计 方面发挥重要作用。可以说b a n 逻辑检验安全协议认证性的威力是其最大的价值之一。 微软公司的邮件收发系统( m i c r o s o f to u t l o o k ) 更是把用户的认证功能同通信链接的安 全性共同放在了首要的位置，文献 1 1 很明确地说明了这一点，在这篇文章中作者不仅 花了很大篇幅介绍了这一系统在用户认证上所采取的4 种方法，也推荐了配合用户认证 协议使用的3 种服务架构。由此可见协议认证性的重要性，下面将着重介绍b a n 逻辑是 如何进行安全协议的认证的。首先本文将简要介绍b a n 逻辑的数学基础，详细的内容读 者可参考文献 9 。 2 i 2 形式逻辑基础 1 。蕴含式及蕴含式的几个性质 南京邮电大学硕士研究生学位论文第2 章b a n 类逻辑的理论与应用 定义2 1 当且仅当p dq 是一个重言式时，我们称“p 蕴含q ”，并记作p 睁q 。 下面简述本文中b a n 逻辑所主要用到的4 个性质： ( 1 ) 设a ，b ，c 为合式公式，若a l b 且a 是重言式，则b 必是重言式。 证明：根据定义2 1 ，a db 永真，所以当a 为真时，b 必为真，得证。 ( 2 ) 若a b b ，b l j c ，则a b c ，即蕴含关系具有传递性。 证明：由公式( a3b ) 八( b3c ) i ja3c ，由题设和性质( 1 ) ，即得：a3c 为重言 式。得证。 ( 3 ) 若a l jb ，且a i c ，则a b ( b a c ) 。 证明从略，由真值表法即可得此性质。 ( 4 ) 若a i b ，且c i j b ，则( a v c ) i j b 。 证明：因为a 3 b 为真，且c 3 b 也为真，故而由合式公式真值转换表可得：( - 1 a v b ) 八( 1 c v b ) 也为真。即；( - 1a a1 c ) v b 为真，亦即：a v c 3b 为真。 所以有结论( a v c ) l j b 。得证。 2 推理理论 定义2 2 设a 和c 是两个命题公式，当且仅当a3b 为一重言式，即a i jc ，称c 是 a 的有效结论，或c 可由a 逻辑地推出。 b a n 逻辑所采取的方法最终都可以归结为运用一定的命题假设逻辑地推出一些目标公 式，即达到定义2 2 所论述的目的。b a n 逻辑中涉及到的推理理论无外乎数理逻辑中的基 本知识，其基本原则均由以下几种方法所涵盖，下面作简要叙述。 ( 1 ) 真值表法 对所有命题变元作全部的真值指派，这样就能对应所有前提和结论的全部真值，列 出这个真值表，即可看出结论是否为前提的有效结论。 ( 2 ) 直接证法 直接证法就是由一组自i 提，利用一些公认的推理规则，根据已知的等价或蕴涵公 式，推演得到有效的结论。 p 规则：前提在推导过程中的任何时候都可以引入使用。 t 规则：再推导过程中，如果有一个或多个公式，重言蕴涵着公式s ，则公式s 可以 引入推导之中。 这里要说明的一点是，在b a n 及b a n 类逻辑的推导过程中往往用到最多的仍然是t 规则，因为在推导过程中将不断地引入前面已得结论作为推导的前提，而p 规则并不是 那么广泛地被使用。 南京邮电大学硕士研究生学位论文 第2 章b a n 类逻辑的理论与应用 ( 3 ) 间接证法 定义2 3 假设公式h l ，h 2 ，h m 中的命题变元为p l ，1 2 ，p n ，对于p l ，p 2 ，p n 的一些真值指派，如果能使h la h 2 a a h m 的真值为真，则称公式h i ，h 2 ，h m 是相 容的。如果对于的每一组真值指派使得h i a h 2 a h m 的真值均为假，则称公式h l ， h 2 ，h m 是不相容的。 间接证法就是要证明一组前提h l ，h 2 ，h m 和所要推出的结论c 的反面1 c 是不相 容的，也就是说它们不能同时为真，如此便可推出h l a h 2 a a h m l j c 。间接证法具有 很好的机器自动操作性，但是由于b a n 逻辑的不够严谨，故而采用较少。 3 谓词逻辑 谓词逻辑主要反映的是主语所代表的客体性质及其和客体谓词之间的动作关系，其 中客体常用量词作限定，牵涉到多个主体的时候，这显得尤其简洁高效。 谓词逻辑在b a n 逻辑中采用较少，但二元谓词在协议建模中会显得方便而有效，虽 然本文仍主要涉及命题逻辑的基本推证，但谓词逻辑很可能是未来可以扩展的一个方 面。在下面的叙述中本文将具体地举例说明这一点。 2 1 3b a n 逻辑的扩展假设 b a n 逻辑是最早的也是最有影响的认证协议形式化分析方法，它是一种基于信念的模 态逻辑。在应用b a n 逻辑时，首先需要进行“理想化步骤”，将协议的消息转换为b a n 逻辑的合式公式，再根据具体的情况进行合理假设，由逻辑推理的规则根据理想化协议 的假设进行推理，推断协议能否完成预期目标。 1 b a n 逻辑构件的扩展语法 ( 1 ) p i = x ：主体p 相信公式x 是真的； ( 2 ) pa x ：主体p 接收到了包含x 的消息，即存在某主体q 向p 发送了包含x 的消 息； ( 3 ) p i x ：主体p 曾今发送过包含x 的消息； ( 4 ) p i j ix ：主体p 对x 有管辖权； ( 5 ) 拌( x ) ：x 是新鲜的，即x 没有在当前回合前作为某消息的一部分被发送过，x 一 般被当作临时值看待； ( 6 ) p 山q ：k 为p 和q 之间的共享密钥，且除p 与q 以及他们相信的主题之 外，其他主体都不知道k ； 南京邮电大学硕上研究生学位论文第2 章b a n 类逻辑的理论与应用 ( 7 ) 与p ：k 为p 的公开密钥，且除p 和他相信的主题之外，其他主体都不知道 相应的解密密钥k ； ( 8 ) p ；坠q ：x 为p 和q 的共享秘密，且除p 和q 以及他们相信的主题之外，其他 主体都不知道x ； ( 9 ) x ) k ：用密钥k 加密x 后得到的密文： ( 1 0 _ ) y ：x 和秘密y 合成的消息。 从以上的语法定义可以看出b a n 逻辑之所以能获得成功，原因就在于其定义的语法 构件已经相当原子化了，所以对于那些一般只有2 到3 条语句的安全协议来说，其实还 是够用的。但是在后面的分析中我们将看到b a n 逻辑的缺陷所在也正是在于它的语法定 义显然还不那么非常地细化，或者说还不很接近于经典形式逻辑的定义。 举例进行论述，例如：( 1 ) p l - = x ；这句话虽然在文字解释上已经非常简练了，但是如 果要翻译成形式逻辑的语法，则可以这样： b ( m ，n ) ：m 相信n t ( n ) ：n 是真的 通过和的总结归纳，则上述语法构件( 1 ) p l = x 可以写成： b ( p ，x ) 八t ( x ) 这样就完全可以用形式逻辑的语言来描述b a n 逻辑的语法构件，后面的b a n 类逻辑 也是存在着方面的问题，但是尽管如此，b a n 逻辑已经比其他的各种形式化分析工具要简 便且易用。实际上，另_ 方面本文认为：如果完全要是用上述的办法对协议进行形式化 描述的话，也未必就很好，诸如：( 5 ) 撑( x ) ；这样的语法构件如果要完全按照标准的逻辑 来描述的话，那么可以这样来刻画： s e n t ( a ) ：消息a 被发送过； b e l o n g ( a ，a ) ：消息a 属于a 的子集； p r e s e n t b o u t ( a ) ：消息a 是属于当前回合的消息； p r e v i o u s b o u t ( a ) ：消息a 是属于以前回合的消息； t e m p ( a ) ：消息a 可以作为临时值 于是我们可以把# ( x ) 这样短短的一句话细化并且扩展为： ( vm ) ( 1s e n t ( x ) 八b e l o n g ( m ，x ) 八p r e s e n t b o u t ( m ) a1p r e v i o u s b o u t ( m ) 八t e m p ( x ) ) 很显然，这种扩展并没有简化推导的步骤：相反，这样的语法定义很可能会增加后 面推理规则的复杂度和不可操作性，因为像诸如b e l o n g ( a ，a ) 这样的谓词其实并没有更多 地涉及到基于其他语法或者语义推导，仅仅会在描述几个简单定义的时候用到。况且这 南京邮电大学硕士研究生学位论文第2 章b a n 类逻辑的理论与应用 也不会成为b a n 逻辑所规定的目标公式之一。因此下面仍沿用经典的方案进行论述，但 本文这种有意义的细化和扩展可能对未来的研究会有好处。 2 b a n 逻辑的推理 b a n 逻辑的推理规则很简单，只有大约不到2 0 条的推理逻辑。因为下文运用到的 s v 0 逻辑继承了b a n 逻辑的大部分精华，且其推理规则较b a n 逻辑更为全面和有效，文献 1 0 也清楚地指明了这一点，故在此并不作赘述，后面论述s v 0 逻辑时将具体阐述。 在此本文要指出的是正是由于b a n 逻辑是基于信任关系建立的，所以推理规则的建 立和扩展都要非常地谨慎，一些过分的假设和推理规则将会直接影响推导的结论。然而 也正是由于b a n 逻辑假设参与协议的主体是诚实的，所以它本身就避免了很多其他形式 化逻辑内部固有的缺陷，进而使推理变得简洁有效。尽管有些不尽如人意的地方，但是 b a n 逻辑的提出毕竟开创了形式化分析和证明安全协议各个特点的先河，直至后来对串空 间模型的提出都具有很重要的影响，文献 1 2 就清楚地说明了这一点。 2 2b a n 类逻辑 2 2 1b a n 类逻辑的基本概念 在实际中，b a n 逻辑在分析某些协议和协议攻击时，功能还不够完善，对协议中某 些性能的推理能力有限。于是各国学者又提出许多修改和扩充意见，其中较为成功和著 名的就是s v o 逻辑【i3 1 ，其他比较有影响的包括g y n 逻辑，a t 逻辑，v o 逻辑。 g y n 逻辑虽然在某些方面对b a n 逻辑进行了一些改进，诸如：可用来分析某些应 用单向函数的密码协议；增加了“拥有密钥”的表达式等等，但是g y n 逻辑中并不包含否 定形式，而经典的形式逻辑当中否定形式是一个很重要的语法定义，就像本文在上一小 节所指出的那样，显然它的粒度并不比b a n 逻辑更细；不仅如此，更重要的是g y n 逻 辑本身过于复杂，非常不利于简化分析的过程，所以g y n 逻辑基本上已经被很多学者所 抛弃。而后来的a t 逻辑和v o 逻辑使得b a n 逻辑有了长足的进步。a t 逻辑包含了详细 的计算模型，增加了模型论语义，v o 逻辑细化了认证协议的认证目标。这两个重要的特 点均被后来的学者广泛应用，文献 1 4 】就是进一步扩展了a t 逻辑所增加的计算模型，使 得安全协议的自动化设计和建模有了很大的突破。以上的特点均被s v o 逻辑所吸收采 用，下面对文献 1 3 】中所阐述的s v o 逻辑的语法做详细地归纳和介绍。 2 2 2s v o 逻辑的语法 南京邮电大学硕t 研究生学位论文第2 章b a n 类逻辑的理论与应用 s v o 逻辑沿用了b a n 逻辑和a t 逻辑所使用地大部分记号，仍用符号| _ ，么，l ， i ，i j i ，群，三分别表示相信( b e l i e v e s ) 、接收至l j ( r e c e i v e d ) 、发送过( s a i d ) 、刚发送过 ( s a y s ) 、管辖( c o n t r o l s ) 、拥有( h a s ) 、新鲜( f r e s h ) 与等价( e q u i v a l e n t ) 。另外，s v o 逻辑的系 统中还含有一下其特有的符号： ( 1 ) ：主体收到的、不可识别的消息。 ( 2 ) 詹：密钥k 对应的解密密钥。 ( 3 ) ( x p k ：加密消息 x ) k ，其中p 是发送者。 ( 4 ) x 】k ：用密钥k 对消息x 签名后所得到的签名消息，即【x 】k _ x ， h ( x ) ) k 。其中 h 为散列函数。 ( 5 ) y ：合成消，g v ，其中p 是发送者( p 常被省略) 。 ( 6 ) p k v ( p ，k ) ：k 为主体p 的公开加密密钥，只有p 才能理解应用密钥k 加密的消 息。 ( 7 ) p k a ( p ，k ) ：k 为主体p 的公开签名验证密钥，k 用于验证应用k _ 1 签名的消息来自 于p 。 ( 8 ) p k k p ，k ) ：k 为主体p 的公开协商密钥( 或参数) 。 ( 9 ) s v ( x ，k ，y ) ：应用密钥k 可以验证x 是y 的签名，即 x ) k = h ( 。 ( 1 0 ) p 山q ：k 是p 和q 之间的“好的”共享密钥，但p 和q 可能都不知道k 。 ( 1 1 ) p 卜生专q ：k 是p 的、适合于与q 通信的非确认共享密钥( u n c o n f i r m e dk e y ) ， 即p 与q = ( p 七与q ) 八( p ，k ) 。 ( 1 2 ) p 卜生专q ：k 是p 的、适合于与q 通信的确认共享密钥( c o n f i r m e dk e y ) ，即 p 斗q = ( p 七与q ) 八( p ，k a ( q i 鼍q g k ) ) 。 类似于与a t 逻辑，s v 0 逻辑也将语言划分为集合t 上的消息语言m t 和公式语言f t 。 其中t 为原子术语集，由主体、共享密钥、公开密钥、私有密钥及一些常量符号构成， 这一点和后面章节中所要论述的串空间模型很相似。 定义2 4 消息语言m t 是由以下规则生成的最小语言： ( 1 ) 若x e t ，则x em r ； ( 2 ) 若x l x n e m t 且f 为函数，则f ( x i ，x n ) m t ； ( 3 ) 若q ) e f t ，则( p m t 。 定义2 5 公式语言f t 是由以下规则生成的最小语言： ( 1 ) 若x e m t 且p 为主体，则p ，k ，p i x ，p i x ，p i = x ，撑( x ) f t ； ( 2 ) 若p ，q 为主体且k 为密钥，则 南京邮电大学硕士研究生学位论文 第2 章b a n 类逻辑的理论与应用 p l 专q ，p k v ( p ，k ) ，p k o ( p ，k ) ，p k 6 ( p ，k ) ，p 3 k f t ； ( 3 ) 若x ，y m t 且k 是密钥，则s v ( x ，k ，f t ： ( 4 ) 若c p e f t 且p 为主体，则p | _ 叩，p l j q f t ； ( 5 ) 若叩，。f f t 则_ 1 平，甲八甲眯其他连接词可通过和定义) 。 s v o 逻辑自身的两条推理规则是： m p 规, 贝l j ( m o d u sp o n e n s ) 由甲和q 3 甲可以推导出甲； n e e 规s t j ( n e c e s s i t a t i o n ) ：由k 可以推导出 - - p i 三c p 。 其中3 表示蕴涵，h 的含义下面的定义2 6 可以解释。 定义2 6 若q 是某个协议的初始化假设集合( 包含各主体的初始信念、接受消息、理 解消息和解释消息) ，而r 是某一公式集合，则s v o 逻辑中对结论的一个证明指，存在一 个长度有限的公式序列：f i ，f 2 ，f n ，使得r 为 f 1 ，f 2 ，f n ) 之子集，且对于v i l ， 2 ，n ，f i 满足以下3 个条件之一： ( 1 ) f i 是某个公理的实例化； ( 2 ) f i 是某个假设( f i q ) ； ( 3 ) f i 可以由它前面的某些公式通过应用m p ，n e c 规则得出。 若q 卜r 在s v o 逻辑中存在证明，则也称结论q 卜r 成立。若阽西，则我们可以将 卜r 简记为卜r 。 下面总结归纳文献 1 3 】中所阐述的s v o 逻辑的公理，这是后面本文所要涉及的协议 建模分析的核心基础： ( 1 ) 信任公理3 条： 硒( p - q o a p - t p ) 三( p i _ ( 平八甲) ) r ip = c p 八p l 三( c p3 甲) 3p l _ 甲 r 2p - 03p l = ( p l - c p ) ( 2 ) 消息来源公理2 条 r 3 ( p 山q a r a x q k ) 3 ( q i x a q 9 k ) r 4p k o ( p ，i ( ) 八r 么x 八s v ( x ，k ，y ) 3q l y ( 3 ) 密钥协商公理2 条 r sp k 6 ( p ，k p ) 八p i 岛( q ，k q ) 3p 卜茎屿q 甲- q j ( f o ( k p ，k q ) f o ( k q ，k p ) ) 这里的f o 是某个密钥协商函数。 ( 4 ) 接收公理3 条 ： 南京邮电大学硕十研究生学位论文第2 章b a n 类逻辑的理论与应用 i bp 么( x l ，x 2 ，x n ) 3p 么x l i b( p 么 x ) k 八p ，k ) 3 p z i x r 9p 1 k 3 p i x ( 5 ) 消息拥有公理3 条 r i o p 1 x3p ，x r l lp 3 ( x l ，x 2 ，x n ) 3p ，x l r 1 2( p ，x l 八八p ，x n ) 3 ( p ，f ( x l ，x 2 ，x n ) ) ( 6 ) 消息理解公理l 条 r 1 3p i - ( p 3 f ( x ) ) 3p i - ( p 3 x ) ( 7 ) 消息发送公理2 条 r 1 4p i ( x 1 ，x 2 ，x n ) 3 ( p l x i 八p ，x j ) r 1 5 p i 鼍x l ，x 2 ，x n ) 3 ( p i ( x l ，x 2 ，x ) a p i = x i ) ( 8 ) 管辖公理l 条 r 1 6 ( p i j i t p a p i = 9 ) 3q ( 9 ) 消息新鲜性公理2 条 r t 7 撑( x i ) 3 撑( x l ，x 2 ，x n ) r l8 拌( x i ) 3 撑( f ( x l ，x 2 ，x n ) ) 这里的消息函数有一点必须注意，一定确保x i 的系数在函数f 中有意义，即x i 必须 占一部分权重。比如：若髯( x 1 ) ，则对f ( x l ，x 2 ，x 3 ) = 0 * x l + x 2 * x 3 x 3 ，这样x l 在这里对整 个公式就没有意义，这样的函数就不能使用公理r 1 8 。 ( 1 0 ) i 临时值验证公理1 条 r 1 9 ( # ( x ) a p i - - x ) 3p i = x ( 1 1 ) “好的”共享密钥对称性公理 r 2 0p 卜笠专q 兰o 山p 2 3s v o 逻辑的应用 应用s v o 逻辑对一个认证协议进行形式化分析一般都要经过三个步骤：( 1 ) 给出该协 议的出世假设集合，即用s v o 逻辑语言表示出各主体的初始信念、接受到的消息、对所 收到的消息作出合理的解释和理解；( 2 ) 给出该协议可能或应该达到的目标集，并同样要 用s v o 逻辑形式化地描述出来；( 3 ) 分析、推理、证明，考查利用初始假设是否能经过有 限步的推导得到步骤( 2 ) 中所希望达到的目标结论。下面开始应用s v o 逻辑形式化地分析 y a h a l o m 协议。 南京邮电大学硕士研究生学位论文第2 章b a n 类逻辑的理论与应用 2 3 1y a h a l o m 协议白os v o 逻辑建模 y a h a l o m 协议是t b u r r o u w 等人于1 9 8 9 年提出的一种基于单钥体制的经典认证协 议。协议的参与主体是通信双方a 、b 和认证服务器s 。整个协议所要达到的目的是通过 认证服务器s 在通信双方a 和b 之间安全地分配会话密钥。 y a h a l o m 协议具体描述如下： ( 1 ) a 专b ：a ，n 。 ( 2 ) b - - - s - b ， a ，n a ，n b k b s ( 3 ) s a ： b ，k a b ，n a ，n b k 私， a ，k a b ) k b s ( 4 ) a 专b ： a ，k a b k b 。， n b k 。b 协议的议论完整的交互过程如图2 1 所示。 图2 1v a h a l o m 协议的交互过程 首先给出y a h a l o m 协议中关于主体a 的初始假设集合如下： p 1a i - a 卜兰与s p 2a i 三b 卜马s p 3 a - 拌( n a ) p 4a 么( b ，k a b ，n a ，n b k 越， a ，k a b k b , ) p sh i - a 么( b ，k a b ，n a ，母b k 部， a ，k a b k b s ) p 6a - - s v ( b ，k a b ，n 。，n b k 越，k 鹊，( b ，k a b ，n 。，n b ) ) p 7 a - b i ( a ，k 。b k b s ， n b k 曲) p sa t - ( s i i k a b ) p 9 a i = ( s l b ，k 。b ，n 。，n b k 越， a ，k a b k b 。) p 1 0a - ( s i 群( k 。b ) ) 根据p 5 a - a 么( b ，k 。b ，n 。，木b ) k 笛， a ，k 。b k b s ) 和r 8 ，由n e c 规则可得： p l la i - a 么( b ，k a b ，n a ，宰b k 硒) ； 再由p la i - - - a 卜马s 和s v o 逻辑语法的定义可得： a l 三( a 卜丝js ) a ( a ，k 舔) x ( s l ( s ，k 鹅) ) ，因此通过凡运算有： p 1 2a i - a ，k 舔； 南京邮电人学硕士研究生学位论文第2 章b a n 类逻辑的理论与应用 再由r 8 加上p i i 和p 1 2 可推出： p 1 3a i - a 1 ( b ，k a b ，n a ，幸b ) ； 由p 1 3 和r l o 及r l l 两条公理自然推出： p 1 4a i - ( a 1 ( b ，k a b ，n a ，+ b ) 3 a a k a b ) 有了p 1 3 和p 1 4 ，再加上r l 公理和m p 规则，可得： p 1 5a i - a ，k a b 由p l 和p 5 ，参照文献【1 5 】等中的扩展定义，我们可以补充如下定义， p 1 6a i = ( ( s l p k 6 ( a ，k 曲) ) 八a 么( b ，k a b ，n 鼬幸b k 笛， a ，k a b ) k b s ) 3p k a ( a ，k a b ) 这是完全符合逻辑的，因为p l 的模型公式是非常强的条件； 事实上，我们完全可以认为a i = ( a 卜屿s d p k a ( s ，k a s ) ) ，再由p 9 ，p 5 和p 6 ，根据 公理，可得： p i ta i - ( s i p i ( a ，) ；再运用p 5 和公理，有： p i sa i - ( ( s i p k 6 ( a ，k a b ) ) a 么( b ，k a b ，n 。，木b k 鹅， a ，k 曲 k b 。) 于是根据p 1 8 和p 1 6 ，由公理r l 及m p 规则，自然有： p 1 9a i = p k 6 ( a ，k 0 类似地，由p 2 和p 7 ，仍然可以补充定义： p 2 0a i = b 么( a ，k a b k b s ， n b k a b ) ：9p i ( b ，) 这里不再是认证服务器和参与协议的主题交互了，所以本文定义p 2 0 也是合理的建模 方式，于是再次运用p 7 和公理r i 及m p 规则，直接导出： p 2 1a i - p k 6 ( b ，k 0 p 1 9 和p 2 l 联合并加上凡公理，可得： p 2 2a i = ( ( p 磁( b ，k b ) 八p & ( a ，) ) 再由r 5 公理及m p 规则，推出下式： p 2 3a i = ( ( p k 6 ( b ，k 。b ) ap k 6 ( a ，i l b ) da 丝一b ) 再次运用r l 公理和m p 规则，最终有： p 2 4a i = a 堡鸟b p 1 2 和p 2 4 联合，由s v o 逻辑语法的定义式，推出： p 2 5a i - a 卜丝6 二专b 这样p 2 5 式已经达到了一个目标结论，即主体a 相信k 曲是适合于a 和b 通信的非确 认的共享密钥。再由p l 、p 8 、p 9 和p l o 我们可以得出： p 2 6a | _ ( 撑( n a ) 3 撑( k | b ) ) 又根据p 3 和公理r i 及m p 规则，推出： 南京邮电大学硕- i