（计算机软件与理论专业论文）串空间理论在电子商务协议形式化分析中的应用.pdf

南京邮电大学硕士研究生学位论文 摘要 摘要 电子商务协议是保障电子商务安全的一种重要手段。非否认性和公平性是电子商务协 议的重要性质，但相对于认证协议和密钥分配协议的保密性和认证性，电子商务协议及其 非否认性和公平性的形式化研究还不够充分。 论文对串空间模型的丛理论、诚实理论和认证测试理论进行深入的研究，并在此基础 上探讨了将串空间模型应用于电子商务协议安全性形式化分析的方法。为了能反映电子商 务协议中加密、签名、完整性保护等多种安全机制，扩展了密码原语，以满足分析复杂安 全协议的需要。根据电子商务协议主体利益目标不一致、攻击主要来自内部的特点，扩展 了攻击模型，对主体处理消息的能力进行了形式化的定义。为了解决电子商务协议中协议 主体动态确定，协议执行路径不唯一确定的问题，扩展了串空间中结点间的因果依赖关系， 来描述协议随着协议步骤的不断执行而使协议执行结果发生改变的内在逻辑关联。 论文应用扩展的串空间模型对安全电子支付协议s e t 的安全性进行了较为全面的分 析，首次应用形式化的分析方法对s e t 的保密性、认证性及完整性进行了严格的论证。同 时由于s e t 协议无法满足交易公平性的缺陷，提出了s e t 协议的一个改进版本，该版本 能满足数字商品交易的公平性。 关键词：电子商务协议，认证协议，形式化分析，串空间，公平性 南京邮电大学硕士研究生学位论文a b s t r a c t a b s t r a c t e l e c t r o n i cc o m m e r c ep r o t o c o li st h em o s ti m p o r t a n ts e c u r i t ym e a n st ot h ee l e c t r o n i c c o m m e r c e t h o u g hn o n r e p u d i a t i o na n df a i m e s sa r ev i t a lp r o p e r t i e si ne l e c t r o n i cc o m m e r c e p r o t o c o l ，r e s e a r c h e so ne l e c t r o n i cc o m m e r c ep r o t o c o la n di t sn o n r e p u d i a t i o na n df a i r n e s sa r e n o ts u 衢c i e n tc o m p a r e dw i t ht h o s eo ns e c r e c ya n da u t h e n t i c a t i o no fa u t h e n t i c a t i o np r o t o c o l s b a s i n go nd e e pr e s e a r c ho nb u n d l et h e o r y , h o n e s t yt h e o r ya n da u t h e n t i c a t i o nt e s tt h e o r yi n s t r a n ds p a c em o d e l ，t h i sp a p e r , p r o b e si n t ot h em e t h o dt h a tu s e ss t r a n ds p a c et o a n a l y s i s e l e c t r o n i cc o m m e r c ep r o t o c o l s i no r d e rt od e s c r i b ee n c r y p t ，s i g n a t u r e ，h a s ha n do t h e rs e c u r i t y m e c h a n i s m ，t h i sp a p e ri m p r o v e sc r y p t o g r a ma n t i t y p et oa n a l y z ec o m p l e xp r o t o c o l s 。t h i sp a p e r e x t e n d sa t t a c k e rm o d e la n dd e f i n e sp r i n c i p a l sa b i l i t i e sf o rm e s s a g eh a n d l i n g sb a s e do nt h e f e a t u r e st h a ti ne l e c t r o n i cc o m m e r c ep r o t o c o l s ，p r i n c i p a l s b e n e f i t sa r en o tc o n s i s t e n t ，a n da t t a c k s a l w a y sc o m ei n s i d e t or e s o l v et h ep r o b l e m st h a tp r i n c i p a l sa r ed y n a m i c a l l yc h o s e na n dt h a t p r o t o c o l sp a t hi sn o to n l y , t h i sp a p e re n h a n c e sc o n s e q u e n c ea m o n gn o d e sa n dd e s c r i b e sl o g i c r e l a t i o n s h i pi nw h i c hp r o t o c o l ss t e p sg o i n go nc a nc h a n g ee x e c u t er e s u l t s t h i sp a p e ru s e se x t e n d e ds t a n ds p a c em e t h o dt o a n a l y z es e tt h o r o u g h l y , a n df o rt h ef i r s t t i m e ，u s e sf o r m a l i z e dm e t h o d st os t r i c t l yp r o v es e c r e c y , a u t h e n t i c a t i o na n di n t e g r i t y m e a n t i m e ， t h ep a p e rp r e s e n t sam o d i f i e de d i t i o nt os e t , w h i c hs a t i s f i e sf a i r n e s sf o rd i g i t a lm e r c h a n d i s e k e y w o r d s ：e l e c t r o n i cc o m m e r c ep r o t o c o l ，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 la n a l y s i s ，s t r a n d s p a c e ，f a i r n e s s 南京邮电大学学位论文独创性声明 本人声明所呈交的学位论文是我个人在导师指导下进行的研究 工作及取得的研究成果。尽我所知，除了文中特别加以标注和致谢的 地方外，论文中不包含其他人已经发表或撰写过的研究成果，也不包 含为获碍南京邮电大学或其它教育机构的学位或证书而使用过的材 料。与我同工作的同志对本研究所做的任何贡献均已在论文中作了 明确的说明并表示了谢意。 磷究生签名：起整盎嚣期：醯璺! 留 南京邮电大学学位论文使用授权声明 南京邮电大学、中国科学技术信息研究所、国家图书馆有权保留 本人所送交学位论文的复印件和电子文档，可以采用影印、缩印或其 他复制手段保存论文。本人电子文档的内容和纸质论文的内容相一 致。除在保密期内的保密论文外，允许论文被查阅和借阌，可以公布 ( 包括刊登) 论文的全部或部分内容。论文的公布( 包括刊登) 授权 南京邮电大学研究生部办理。 研究生签名：。_ 救导师签名：撇目期：遥扭& 南京邮电大学硕士研究生学位论文 第1 章绪论 1 1 安全协议形式化分析 1 1 1 安全协议的基本概念 第l 章绪论 安全协议( 又称密码协议) 是建立在密码体制基础上的一种高互通信的协议，它运行 在计算机通信网络或分布式系统中，为安全需求的各方提供一系列步骤，借助于密码算法 来达到密钥分配、身份认证、信息保密以及安全地完成电子交易等目的【l 】。 在通信网络中最常用的、最基本的安全协议按照其功能可以分为以下四类： ( 1 ) 密钥建立协议：建立共享会话秘密，如d i f f i e h e l l m a n 协议【2 1 。 ( 2 ) 认证建立协议：向一个实体提供对他想要进行通信的另一个实体身份的某种程度的 确信，n e e d h a m s c h r o e d e r 协议例。 ( 3 ) 认证的密钥建立协议：与另一身份己被或可被证实的实体之间建立共享秘密，如 o t w a y r e e s 协议【4 】，k e r b e r o s 协议【5 1 等。 ( 4 ) 电子商务协议：确保电子商务各参与方之间信息流的交互有规可循，从而保证各方 的利益和安全，并能控制风险。目前常用的电子商务协议有s e t 协议、s s l 协议等。 安全协议的目标就是要保证某些安全性质在协议执行完毕时能够得以实现，这些安全 性质主要有认证性、机密性、完整性、非否认性、公平性等。 1 1 2 安全协议形式化分析 安全协议是许多分布式系统安全的基础，确保这些协议的安全运行是极为重要的。大 多数安全协议只有为数不多的几个消息传递，其中每一个消息都是经过巧妙设计的，消息 之间存在着复杂的相互作用与制约，而且安全协议中往往使用多种不同的密码体制，此外 协议设计者对协议运行环境的安全估计不足或采用不当的技术，以上这些都会导致设计的 安全协议存在安全漏洞与缺陷并引发攻击者对协议进行各类的攻击行为，从而破坏协议的 安全性。 安全协议的安全性是一个很难解决的问题，许多广泛应用的安全协议后来都被发现存 在安全缺陷。如著名的n s p k 协议自1 9 7 8 年问世以来，到l o w 于1 9 9 6 年发现n s p k 协议 的安全缺陷，已经过去了大约1 7 年之久。安全协议设计的困难性和安全协议分析的微秒 南京邮电大学硕上研究生学位论文 第l 章绪论 性，由此可见一斑。因此，从安全协议的分析和设计角度来看，我们都不能够存在轻信和 盲从心理，而应当对协议的安全性作出认真的分析。协议的安全分析是揭示安全协议是否 存在漏洞的重要途径。 目前，对安全协议进行分析的方法主要有两大类：一类是攻击检验方法；一类是形式 化的分析方法。 攻击检验方法也称为非形式化分析方法，这种分析方法就是搜集使用目前的对协议的 有效攻击方法，逐一对安全协议进行攻击，检验安全协议是否具有抵抗这些攻击的能力。 在分析的过程中主要使用自然语言和示意图，对安全协议所交换的消息进行剖析。这种方 法只能停留于发现协议中是否存在着己知的缺陷，而不能全面客观地分析安全协议，所以 容易导致不安全的协议经分析是安全的这样错误的结论。这是安全协议早期的主要分析方 法。 2 0 世纪9 0 年代初以来，安全协议的形式化分析成为研究热点。形式化的分析方法是 将安全协议形式化后，借助于人工推导，甚至计算机的辅助分析，来判别安全协议是否安 全可靠。形式化与非形式化分析方法相比，它能全面、深刻地检测到安全协议细微的漏洞。 形式化分析方法不仅能够发现现有的攻击方法对协议的威胁，而且通过对安全协议的分 析，能够发现协议中细微的漏洞，从而发现对安全协议新的攻击。 到目前为止，安全协议的形式化分析方法大致可分为以下三类： ( 1 ) 推导构造法：运用逻辑系统从用户接收和发送的消息出发，通过一系列的推理公理 推证协议是否满足其安全说明。用于安全协议形式化分析的逻辑系统可区分为两类：一类 是基于知识的，比如b a n 逻辑【6 】；另一类是基于信仰的，比如k a i l a r 逻辑【7 1 。 ( 2 ) 攻击构造法：从协议的初始状态开始，对合法主体和一个攻击者的所有可能的执行 路径进行穷尽搜索以期找到协议可能存在的错误。用这种方法对协议进行分析时一般要借 助自动工具，比如c s p 法【8 】。 ( 3 ) 证明构造法：证明协议满足其安全性要求，比如串空间【9 】。 1 2 国内外研究现状 形式化分析协议的工作，普遍认为是从d o l e v 和y a o 于1 9 8 3 年的研究开始的【i o j 。他 们主要贡献有两点：一是将协议本身与协议所具体采用的密码系统分开，在假定密码系统 是“完善的基础上讨论认证协议本身的i f 确性、安全性、冗余性等课题。从而，研究人 员可以专心的研究协议的内在安全性质。二是建立了攻击者模型，攻击者能获取、修改、 和删除网上传递的消息，或执行某些动作如加解密等。此后的协议形式化分析模型大多基 - 2 - 南京邮电大学硕j ：研究生学位论文第1 章绪论 于此或是此模型的变体。如i n t e r r o g a t o r 、n r l 协议分析器】和l o n g l e y r i g b y 工具。 直到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 逻辑之后，这一领域才引起 了人们广泛关注。b a n 逻辑是一种基于主体知识的逻辑推导方法，b a n 逻辑简单、直观 便于掌握和使用，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 逻辑存在初始假设的确定非形式化、理想化步骤非形式化、缺乏精确定义的语法基础等局 限，后来许多文献都对b a n 逻辑进行了必要的改进和扩展，如g y n 逻辑【12 1 、a t 逻辑、 v o 逻辑【14 1 、s v o 逻辑【1 5 】等，这些逻辑都统称为b a n 类逻辑。 1 9 9 6 年l o w e 在文献【8 】中证明了可用r u s c o e 的模型检测程序f d r 发现对 n e e d h a m s c h r o e d e r 协议的一个中间人攻击行为，这引发了人们将协议形式化分析研究的热 点集中于d o l e v y a o 模型的状态探测和定理推证技术上。m i t c h e l l 和s t e m 1 6 】使用d i l l 的 m u r 矽模型检测程序对n e e d h a m s c h r o e d e r 协议、t m n 协议和k e r b e r o s 协议进行了分析； 基于进程代数c s p ，l o w 和r o s c o e 分别发展了不同的理论和方法，把大系统中协议安全 性质的研究约化为小系统中协议安全性质的研究；m i l l e n 开发的c a p s l ( c o m m o n a 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 ) 为协议形式化分析工具提供通用说明语言， 标志着不同形式化分析技术的日趋成熟与集成。 1 9 9 8 年f a b r e g a ，h e r z o g 和g u t t m a n 建立了串空间模型，将安全协议形式化分析技术 推向一个新的高度。串空间模型是一种结合定理证明和协议迹的混合方法，由于它的高效、 严谨、直观等特点，受到广泛推崇。它不仅可以用于证明安全协议的正确性，还可以用于 构造攻击，揭示安全协议的内在缺陷。其他的定理证明方法如s p i 演算【1 7 】、p u a s o n 归纳法、 s c h n e i d e r 秩函数等也有广泛的发展和应用。 安全协议另一个十分活跃的分支是伴随着电子商务的发展，安全电子商务协议、公平 交换协议的逐渐成熟和多样化。但是，与认证协议相比，电子商务协议的形式化分析明显 不足，我们有必要把更多的形式化技术运用到它们的分析中去。本质上，任何分析认证协 议的形式化方法都可应用于电子商务协议的分析，不同之处在于，分析电子商务协议时， 我们可能需要创建新的假设公理、推理规则、以及不同的入侵模型等等。在这方面的主要 研究成果有：s s c h n e i d e r 运用c s p 技术分析了z g 在线t t p 不可否认协议【l 剐；z h o u 和 g o l l m a n n 运用s v o 逻辑分析了他们自己的z g 在线t t p 协议【l9 】；b e l l a 和p a u l s o n 运用归 纳方法对z g 在线1 v r p 协议的分析【2 0 】；s h m a t i k o v 和m i t c h e l l 利用有限状态模型检测器 m u r # 对a s w 乐观合同签字协议的分析【引】； 南京邮电大学硕上研究生学位论文 第l 帮绪论 中国科学院的卿耨汉、范红、冯登圜教授等对认证协议及逻辑分析方法也进行了深入 的研究，同时也开始了应用形式化方法对电子商务协议的安全属性进行分析，如周典萃、 卿斯汉等用k a i l a r 逻辑及改进的k a i l a r 逻辑分析了z g 在线t t p 协议的磁l 。 以上的研究仅限于用逻辑推导法或状态探测法对简单的电予商务协议进行形式化分 析，然而应用串空间模型对电予商务形式化分析的研究还不多。正是基于这个观察，所以 本文尝试将串空间理论引入到电子商务协议的分析。 在众多的形式化分析技术中，本文选择串空间理论，是因为它在协议分板上有瞪大优 点：( 1 ) 数据项的假设有清晰的语义；( 2 ) 明确规定了入侵者的行为能力；( 3 ) 能同时分析秘 密性和认证性；( 4 ) 详细洞察了协议正确的原因。串空间技术弥补了逻辑推导法初始化假设 和理想化过程非形式化的缺陷以及状态探测法不可避免的状态空间爆炸问题，有比较简 洁、直观的证明方法，是目前形式化分析领域内最具完整体系的理论。它的丛理论、诚实 理论和认证测试理论共同组成了一个多样性的协议分析技术簇。串空间理论还在协议的自 动化生成、混合协议的安全性方面作出了有价值的成果。 本文选择串空间理论，希望通过对串空间理论的扩展实现两个目标：( 1 ) 具有分析复杂 协议的能力；( 2 ) 具有分析电子商务协议公平性、非否认性的能力。 1 3 本文工作 本文在安全协议形式化分析领域，重点研究了以下内容： ( 1 ) 对串空间模型方法进行了深入的分析和研究，掌握丛理论、理想诚实理论和认证测 试理论进行协议分析的方法。分别应焉理想诚实方法及认证测试方法对y a h a l o m 协议的保 密性和认证性进行了较为详尽的分析，并针对分析得出的代数缺陷，对y a h a l o m 协议进行 了改进。 ( 2 ) 对串空间模型分析的代数结论与实际攻击的关系进行了研究，同时对认证协议的设 计提出了几点启发式规则。 ( 3 ) 深入研究电子商务协议，分析电子商务协议的特点。 ( 4 ) 扩展串空间模型，使之能够对电子商务的安全牲进行分析。 ( 5 ) 应用扩展的串空间模型对实用的s e t 协议进行了分析，并针对s e t 协议不能满足 交易公平性的缺陷提嵩了s e t 协议的一种改进方案。 南柬邮电大学硕士研究生举位论文第1 章绪论 1 4 论文组织结构 全文共分为六章，其组织如下： 第一章简要介绍了安全协议及安全协议形式化分析方法的基本概念，对相关背景和国 内外研究现状进行了广泛的研究，阐述了论文研究的理论价值和意义。 第二意详细论述了串空间理论的概念，分析协议的原理和方法，并以y a h a l o m 协议的 分析为例，深入剖柝了串空间理论分析机密性翻认证性的机理。 第三章论述了安全电子商务协议的基本概念、安全属性，介绍了s e t 协议及k m 协议， 用于后续章节的分析。 第四章原理性地阐述了电子商务协议的特点并对串空间模型进行了扩展，使之能够分 柝电子商务协议的保密性、认证性、葚# 否认性、公平性。这些扩展主要包括密码原语的扩 展、攻击模型的扩展以及因果依赖关系的扩展。 第五章应用扩展的串空闽模型对s e t 协议的安全性进行了详尽的分析，并针对s e t 协议不能满足交易公平性的缺陷提出- j - s e t 协议的一种改进方案。 第六章对所做的研究工作进行了总结，并对研究课题提出了进一步的展望。 南京邮电大学硕士研究生学位论文第2 章串宅问模型 第2 章串空间模型 f a b r e g a ，h e r z o g 和g u t t m a n 于19 9 8 年建立了串空间( s t r a n ds p a c e ) 模型i 引，将安全协议 的形式化分析技术推向了一个新的高度。串空间模型是一种结合定理证明和协议迹的混合 方法，由于它具有高效、严谨、直观等特点，受到广泛推崇。随后，g u t t m a n 等又对串空 间模型进行了广泛的扩展，提出了理想与诚实的概念【2 3 】以及认证测试方法【2 4 】，使得应用串 空间模型分析协议的安全属性变得更加简捷直观。同时，他们还对应用串空间模型分析混 合协议【2 5 】和串空间方法的自动化分析技术f 2 6 1 等方面进行了深入的研究。 2 1 串空间模型基础 串空间模型是一种新的密码协议形式化模型，其基本结构要素为：结点，表示实体( 协 议参与者) 间交互消息的状态：串，表示协议运行中同一实体的结点序列；串空间，表示协 议运行中合法和非法实体的串的集合；丛，表示协议的一轮完整运行的串集合。用子项关 系和结点关系刻画了串空间模型中的两类基本关系，其中子项关系描述了项( 即实体间收发 的消息) 的结构，而结点关系则描述了结点间实体收发消息的顺序逻辑。 2 1 1 串空间模型的基本概念 1 项及子项关系 令集合a 中的元素为协议主体交换的消息，称a 的元素为项( t e r m ) 。a 通过原子项 ( a t o m i ct e r m ) 进行加密和连接操作生成。 下面构造集合a ： ( i ) t c _ a 是正文集合，表示原子消息。 ( 2 ) 彭c a 是密钥集合，其中茁与t 是不相交集。r 中有一个一元算子i n v r k 。 假设i n v 是单射，它将非对称密码系统中的密钥对中的一个映射为另一个；将对称密钥映 射为自身。 ( 3 ) 两个二元算子 e n c r r a a j o i n - a x a 寸a 根据传统习惯将i n v ( k ) 写成k ，将e n c r ( k ，m ) 写成 m ) k ，将j o i n ( a ，b ) 写成a b 。设k 是一个 南京邮电人学硕士研究生常位论文第2 章串窄问模型 密钥集合，用- 1 表示茁中所有元素的逆元素集合。 项中的重要关系是子项关系，记为c 。t oc t 。表示t 。是t 的子项。子项关系描述了实 体之间收发消息的结构。 定义2 1 子项关系可以递规定义为满足下列关系的最小关系： ( 1 ) 鑫ca ； ( 2 ) ac g k ，如果a c g ； ( 3 ) a c g h ，如果a c g v a c h 。 在安全协议中，主体可以发送项，也可以接收项。在串空间模型中，用加号表示发送 顼，减号表示接收项。 定义2 2 符号项是一个二元组 ，其中a a 且o = + ，一) ，记符号项为+ t 或一t 。 ( ：a ) 是符号项的有限序列集合，记( ：a ) 中的元素为 e 2 串和串空间 定义2 3 定义a 上的串空间为一个集合以及它的迹映射t r ：寸( ：a ) 。- 串空间是一个二元组( ，t r ) ，其中的是个串的集合，这晕的串可以用来表示任何 序列。t r 表示由到么中元素组成的序列的一个映射，我们称其为迹映射，映射的像称为 原像的迹。通常省略掉迹映射，只用表示一个串空间。迹映射可以不是单射，例如在模 拟重放攻击时，需要区分具有相同迹的对应不同时间段的串。 定义2 4 构造串空间的方法如下： ( 1 ) 结点是二元组 s ，其中s 且i 为满足l _ i _ 是，( 专u 警) 的一个子图，这里 _ c c j ；cc 尊，且满足： ( 1 ) c 是有限无环圈； ( 2 ) 若n 2 n c ，且t e r m ( n 2 ) 为负，则存在唯一的结点n l ，使得1 1 i 专( ? n2 ； ( 3 ) 若n 2 n c ，且n l 琏2 ，英i1 1 l cn2 。 以上定义给出了个通信进程的形式化模型，它具有以下性质： ( 1 ) 一个串既可以接收消息，也可以发送消息，但不能同时发送和接收消患，通信是否 同步共不重要。 ( 2 ) 当个串接收消息m 时，存在唯一的一个结点发送m ，且发送m 后立即被收到。 ( 3 ) 当一个串发送消息m 时，可能存在多个串立即接受到m 。 用以下的记号约定：若n n c ，则称结点n 在丛c = 谢c ，( ocu j c ) 中，记为n c ； 若串s 中所有的结点均属于n ，则称串s 在丛c 中。 设c 为丛，定义s 串的c 高度，记为c - - h i g h t ( s ) ，是满足 s ，c 的最大的i 的值。 s 在e 中的迹为c - - t r a c e ( s ) = ( t r ( s ) ) l ，o s ) 。) ，其中氆= c - - h i g h t ( s ) 。 定义2 6 设s 是一个边的集合，即sc 叶uj ，定义_ m - - m a k = k 公理2 2 对于m o ，mo ，m l ，1 1 1 1 e an k ，k 盯， ( 1 ) mo m i - - mo m l jm o 2m o m l2m l ： ( 2 ) mo m l mo ) k ； ( 3 ) mo m l 仨ku t ； ( 4 ) mo ) k 仨ku t 。 在实际的安全协议中，消息代数中存在更多的关系，即项与项之间存在等式关系，是 自有假设中所不允许的。例如，在现实中消息的合成通常是一个满足结合率的算子。更为 严重的是，在实际的密码系统中，公里2 1 是不成立的。即存在不平凡的等式 m ) k = m ) k t 。 对于任意加密代数a ，存在一个自由加密代数a 和满射万：a a ，并且万和a 在同 构的意义下是唯一的，这与泛代数( u n i v e r s a la l g e b r a ) l 里论中的自有代数的定义是一致的。 今后对安全协议的正确性进行证明时，应用的是自由代数a 上的串空间。如果安全协议的 某个性质在a t 上不成立，则在该协议的这个性质在a 上也不成立。反之则不一定成立，因 为安全协议的失败可能利用a 中的关系，但这种关系在a 。中却不成立。然而，通过考虑自 由代数可以获取一些有用的信息，排除一些由于安全协议本身的结构所导致的弱点，这与 消息代数的某些性质是不相关的。 2 1 3 攻击者 攻击者的能力由两部分描述，一部分是攻击者初始时已知的密钥集合，另一部分是攻 击者串的集合，使攻击者可以由他截获的消息生成新的消息。 攻击者集合由密钥集合酢组成，包含初始时已知的密钥，如所有的公丌密钥，攻击者 及其同谋拥有的所有的秘密密钥，攻击者与其他协议主体共享的对称密钥等。其中，也可 9 南京邮电大学硕：_ 匕研究生学位论文 第2 章串窜问模型 能包含所谓“丢失的密钥 ，鞠攻击者先翦成功地通过密码分析所获得的密钥。 攻击者所具有的原子行为由下面定义的攻击者迹描述，它总结了攻击者丢弃消息、生 成消息、连接消息，以及攻击者应用 邈所知道的密钥进行密码运算的能力。攻击者对协议 的攻击，通常需要联合应用下述几个原子行为。 定义2 。? 攻击者迹包括如下内容： ( 1 ) m 正文消息： + 协，其中t t ： ( 2 ) k 。密钥： ； ( 4 ) s 。分解： ； ( 6 ) d 。解密： 。 上述攻击者迹的集合，使攻击者可能发送的值在连接、加密以及相关的逆运算下是封 闭的。 定义2 8 渗透串空间( i n f i l t r a t e ds t r a n ds p a c e ) 是一个二元组( ，p ) ，其中是一个串空 间，p c 满足如下条件：耐所有的p p ，t r ( p ) 是一个攻击者迹。 p 中的串称为攻击者串。即串s e 是攻击者串，如果s p 。结点1 1 是攻击者结点，如 果它所在的串是攻击者串。除此之外的串与结点，将它们称为正则串与正则结点。 不能假设渗透串空间能够识别所有类型为m 的攻击者迹，否则串空间模型就无法表述 随机的临时值。通常假定，渗透串空间对许多芷文值缺少m 串。这样，合法的协议主体才 可以应用这些正文值作为新鲜的临时值。 2 1 4 正确性概念 串空间模型提出时，主要针对的是认证协议及密钥分配协议的分析。这类协议所要满 足的安全属性主要是认证性、机密性和新鲜性等。在文献 2 7 中，w o o 季i l a m 把上述耳标分 别转化成对应属性和保密属性。 对于某一个数据项x ，称一个安全拚议保证了对主体8 酶对斑性是指：每一次主体b 作 为响应者应用x 完成一个回合协议时，对于b 来说他时在与a 通信；于是，存在以主体a 作 为发起者应用x 的唯一的一个回合协议，对于a 来说他是在与b 通信。 称数摆项x 在丛c 中具有机密性，如果下述条件满足：对于任何n e c ，都有t e r m ( n ) x 。 7 0 南京邮电大学硕士研究生学位论文第2 章串窀问模型 2 。1 5 实例分析 本节以n s p k 为例介绍串空间模型分析协议安全属性的原理以及一般方法。n s p k 协 议的详细分析过程可以参阅文献 9 】。 n s p k 认证协议的目的是使通信双方安全地交换两个彼此独立的秘密。n s p k 协议的 简化形式如下： ( 1 ) a 寸b ： n 。，a k 女 ( 2 ) b 斗a ： n 。，n6 ka ( 3 ) a 专8 ： n 6 ) k 6 在应用串空间模型进行协议分析之前，先将项代数进一步具体化如下： ( 1 ) 标志符集合t 一冬t ，通常用a ，b ，表示主体的标志符。 ( 2 ) 映射k ：t 一。_ r 。这个映射将每个主体和他的公开密钥进行绑定。依照传统习 惯用k 。表示k ( a ) ，并假设这个映射是单射的，即若k 。- - k 。则有a = b 。 采| 雳如下记号： t 一中的变量用a ，b 表示；盯中的变量用k ，k - 表示：1 、t 一。中的变量用n ，m 表 示，即不是标志符的正文消息。其他字母，例如，g ，h ，表示a 上的变量。 定义2 9n s p k 协议中的正则串定义为如下形式： ( 1 ) 发起者串s ei n i t a ，n 口，n6 】，与它对应的迹为 i n i t a ，n 。，n 。】表示了所有具有上述迹的串的集合，与这种串对应的主体是a 。 ( 2 ) 响应者串s er e s p a ，n 半，n 6 】，与它对应的迹为 r e s p a ，n 口，n 。】表示了所有具有上述迹的串的集合，与这种串对应的主体是b 。 如图2 1 所示是个描述n s p k 协议中主体行为的丛示意图。图中，a 下方的列表示 发起者串，b 下方的歹l j 表示响应者串，分别表示协议信息交换中发起者和响应者的行为。 协议假定双方都知道对方的公开密钥。发送者a 首先生成临时值n 。，与其标志符连接， 用响应者b 的公开密钥加密后发送给b 。b 生成临时值n 。，与n 。级联后用a 的公开密钥 发送给a 。因此，b 通过证明他能读第一条消息购应了发起者a 的请求。最后，发起者a 返回用响应者b 公开密钥加密的临时值n 。 南东邮电大学预士研究生举位论文第2 章串空间模型 图2 1n s p k 协议 在串空闻模型中，通过证明串空间中发送包含某个数据项的消息的串是唯一的，说明 该数据项的新鲜性。其他包含该数据项的串只是配合发送串完成消息的接收和消息的进一 步处理；通过证明串空间中不包含消息未经接收就可以被发送的攻击者串，说明攻击者不 可能正确地猜测某些数据值。用串空间证明协议的基本方法是：首先，在丛中根据需要构 造一个结点集，这个结点集一般是包含主体用来验证消息新鲜性的i 琏时值或会话密钥等关 键消息；其次，考虑这个结点集的最小元属于哪一种串；最后，对于其余串，分情况判断 该最小元是否属于这个串，如果最小元属于该串，说明这个关键数据项起源不是唯一的， 协议有缺陷。 文献1 9 1 0 0 分析得出，在n s p k 空间中若存在c 高度为3 的响应者串r e s p a ，n 。，n 。】 且n 6 在空i 日- 1 0 e 唯一起源，则存在一个c 高度为3 的发起者串i n i t a ，n 。，n 。】。但是由于 响应者的身份无法确定，于是存在l o w 对n s p k 的攻击。图2 。2 说襞了n s p k 存在的安全 缺陷。图中攻击者p 采取了两回合的行动，发起者a 希望与p 进行了一次会话，p 利用这 个机会冒充a 与b 进行会话。 a 图2 2 攻击n s p k 协议的一种方法 南京邮电大学硕士研究生学位论文 第2 章串空麓模型 2 2 理想与诚实 理想对于描述某些具有特定性质的消息的集合是非常有效的。例如，在保密性的分析 中，理想被用来描述豳秘密信息生成的消息集合，该集合是封闭的且攻击者无法有效地进 入该集合。在认证性分析时，理想被用来描述由认证项组成的消息集合，该集合不霹能由 攻击者通过推导关系全部得到。 2 2 1 理想与诚实 定义2 。羹o 设k c ，定义集合a 的一个繇理想秀a 的一个子集l ，对任意h e i ，g a 和k k ，以下条件满足： ( 圭) h g ，魏g 至； ( 2 ) h k i 。 我们将包含h 的最小隆理想记作王鬣 h 】。 由上面的定义和定义2 1 可知，g c h 当且仅当h i k 隐】。 命题2 1 设s c _ a ，则有i k 【s 】= u 膦lk 【x 】。 定义2 重l 通常称一个项是简单项，当且仅当它不能表示成a b 的形式，其中a ，b e a 。 或者可以说，一个项是简单的当且仅当它属于集合t 或搿，或具有形式 h ) l 。 命题2 2 设s c _ a ，k ，k c 茁且对于任意s es ，s 都是简单的，并且不具有形式 g ) k 。 于是，如果 h j k i k 【s 】，则有h i k 【s 】。 命题2 3 设s c _ a ，k e 鬈，k c 彭且对于任意s es ，s 都是简单的，并且不具有形式 g k 。 于是，如果 h k i k 【s ( k ek ) ，则有k 毯k 。 命题2 。4 设s _ c a ，k c 彭且对于任意s s ，s 都是简单的。于是，如果g h l i ( 【s 】， 则有g ik 【s 】成立，或者h ik 【s 】成立。 命题2 。s 设c 是a 上的一个丛，如果m 是集合 m 最c ：t e r m ( m ) l 中的一个极小元， 则m 是i 的一个入口点。 定义2 薹2 定义集合i c _ a 关于丛c 是诚实的，如果个攻击者结点p 是l 的入囹点， 则p 是一个m 型攻击者结点或k 型攻击者结点。 定理2 。l 设c 是a 上的个丛，s c t ur ，k 冬整量彭s 0k 一，于是l l ( 【s 】是诚实的。 推论2 1 设c 是个丛，茁= s uk ，且s nk 。= 。如果存在一个结点m 联c ，使 得t e r m ( m ) i k 【s 】，则存在一个正则结点n c ，使得n 是l k 【s 】的个入因点。 南京邮电火学硕士研究生学位论文 第2 章串窄问模型 推论2 2 设c 是一个丛，k = suk ，且snr 。= 矽。且不存在一个正则结点m ec 是ik 【s 的一个入口点。于是，任何形女i g k ( k es ) 的项都不起源于一个攻击者结点。 在分析协议保密性的过程中，s 是包含协议运行过程中需要保密的信息。k 包含的是密 钥空间中除去攻击者无法得到的密钥的集合，就是攻击者可能知道的密钥。这样，i 。 s 】 就是所有需要保密的消息用攻击者可能知道的密钥处理后的消息的集合。m 节点或k 节点 实际上是说攻击者不能由得到的消息推导出的信息。这样，如果i 。 s 】是诚实的，就保证了 s 中的消息攻击者不能够由推导得到。 而在分析协议的认证性时，认证的方式都是由认证者产生一个特定的可以代表身份的 消息( 认证项，常用的方法包括数字签名、消息认证码、加密等方式) 使得验证者可以有效 的验证消息的产生者的身份。如果协议能够实现认证目的，那么对于认证项中的所有简单 的子项，攻击者不可能由推导关系全部得到。换句话说，如果协议的认证性可以满足，那 么攻击者不可能通过截获的消息和他所具有的推导能力构造有效的认证项。 2 2 2 应用理想与诚实分析y a h a l o m 协议 y a h a l o m 协议是由t b u r r o u w 等人于1 9 8 9 年提出的一种基于单钥体制的经典认证协 议。参加协议的主体是通信双方a 、b 和认证服务器s 。其目的是通过认证服务器s 在通 信双方之间安全地分配会话密钥。 y a h a l o m 协议具体描述如下： ( 1 ) a j b ：a ，n 。 ( 2 ) bjs ：b ， a ，n 。，n 6 ) k 缸 ( 3 ) s a ： b ，k 曲，n 。，n6 ) k 。， a ，k 曲) k 缸 ( 4 ) a b ： a ，k 曲) k 缸， n6 ) k 曲 在应用串空间模型进行协议分析之前，先将项代数进一步具体化如下： ( 1 ) 标志符集合t 一。t ，通常用a ，b ，表示主体的标志符。 ( 2 ) 映射k ：t 。一r 。将每个主体和他与服务器共享的密钥进行绑定。下面在讨论 协议时，依照传统习惯用k 表示k ( a ) 。此外，假设映射a 专k 。是单射映射，并假设 k 珊= k ：，即该协议中应用的是对称密码。 采用如下记号： 南京邮电大学硕士研究生学位论文第2 章串窄问模型 t 。中的变量用a ，b 表示：r 中的变量用k ，k 表示；1 、t 。中的变量用n ，m 表 示，即不是标志符的正文消息。其他字母，例如，g ，h ，表示a 上的变量。 定义2 1 3 协议中的正则串定义为如下形式： ( 1 ) 发起者串s e i n i t a ，b ，n 。，n 6 ，k ，h 】与它对应的迹为 + a n 。，- b k n 。n 6 ) k 。h ，+ h n6 ) i 其中a 、b t 。，n 。、n6 t 。i n i t a ，b ，n 。，n6 ，k ，h 】表示了所有具有上述迹的串的 集合，与这种串对应的主体是a 。 ( 2 ) 响应者串s e r e s p a ，b ，n 。，n 6 ，k 与它对应的迹为 其中a 、b e t 一。，n 。、n 6 t 。r e s p a ，b ，n 。，n6 ，k 】表示了所有具有上述迹的串的 集合，与这种串对应的主体是b 。 ( 3 ) f j 艮务器串s es e r v a ，b ，n 。，n 6 ，k 】与它对应的迹为 其中a 、be t 。，n 。、n6 t ，k 仨心j p ，k 仨 k 。：a et 。册。) 且k