（计算机软件与理论专业论文）基于串空间理论的安全协议分析.pdf

郑州大学硕士学位论文 摘要 安全协议提供安全服务，是保证网络安全的基础。近年来，安全协议越来越 多地用于保护因特网上传输的各种交易，保护针对计算机系统的访问。由于验证 安全协议自身的安全性是十分困难的。因此，必须借助形式化方法，对安全协议 进行分析。 在众所多的形式化分析方法中，串空间模型是一种结合定理证明和协议迹的 混合方法，将安全协议的形式化分析技术推向一个新的高度，由于其高效、严谨、 直观的特点而受到广泛推崇。本文在对串空间模型研究的基础上，首次以串空间 理论中的“理想”和“诚实”为工具，对改进的n s s k 协议从机密性和认证性两 个方面进行了严格的证明。结果表明，改进的n s s k 认证协议实现了协议设计的 目标，是正确有效的。 安全协议的正确性主要体现在一致性和机密性两个方面。虽然串空间模型在 协议分析过程中比其它形式化方法更为简洁和直观，但在分析协议为什么不正确 及如何改进方面，同其他形式化分析方法一样，显得分析能力较弱。针对这一问 题，本文在认证测试的基础上，提出了参数一致性矩阵的概念。利用参数一致性 矩阵对安全协议的一致性进行分析，与原有的分析过程相比更为直观、简单，有 效地揭示协议失败的原因，并针对这些原因给出相应的改进思路。 关键词：安全协议；串空间；认证测试；参数一致性矩阵 郑州大学硕士学位论文 a b s t r a c t s e c u r i t yp r o t o c o lp r o v i d i n gs e c u r i t ys e r v i c e s , t o 吼玳n e t w o r k ss e c u r i t y i n r e c e n ty e a r s ，m o r ea n dm o l es e c u r i t yp r o t o c o li su s e df o rp r o t e c t i n gt h ei n t e m e t t r a n s m i s s i o no ft r a n s a c t i o n sa n dt h ea c c e s st oc o m p u t e rs y s t e m s h o w o v c r , v e r i f y i n g t h ec o r r e c t n e s so fs e c u r i t yp r o t o c o li sv e r yd i f l k ：i i l t t h e r e f o r e ，w em u s tr e l y0 1 1 f o r m a lm e t h o d st oa n a l y s et h es e c u r i t yp r o t o c 0 1 a m o n gl o t so ff o r m a la n a l y s i sm e t h o d s ，t h es t r a n ds p a c em o d e li sac o m b i n a t i o n o ft h e o r e mp r o v i n ga n dp r o t o c o lt r a c e , p u s h e sf o r m a la n a l y s i st e c h n o l o g yo fs e c u r i t y p r o t o c o lt oan e wl e v e l s t r a n ds p a c em o d e li sw i d e l yr e s p e c t e db e c a u s eo fi t sh i g h e f f i c i e n c y , ar i g o r o u s ，i n t u i t i o n i s t i cf e a t u r e i nt h ef o u n d a t i o no f r e a c h i n gs t r a n ds p a c e t h e o r y , i ti st h ef i r s tt i m et oa n a l y s et h em o t t l e dv e r s i o no fn s s kp r o t o c o lf r o mt h e a s p e c t so fb o t hc o n f i d e n t i a l i t ya n da u t h e n t i c a t i o n , u s i n g “i d e a l a n d h o n e s t o f s t r a n ds p a c et h e o r y t h ea n a l y s i sp r o v e dt h ec o r r e c t n e s so ft h em o d i f i e dn s s k p r o t o c 0 1 t h ec o l t e c t l l e s so fas e c u r i t yp r o t o c o lm a i n l yi n c l u d e sa g r e e m e n ta n ds e c r e c y a l t h o u g h , c o m p a r i n gw i t ho t h e rf o r m a la n a l y s i sm e t h o d s ，s t r a n ds p a c em o d a li sm o r e i n t u i t i o n i s t i ca n ds i m p l e , b u ti na n a l y s i n gw h yp r o t o c o li si n c o r r e c ta n dh o wt o i m p r o v ei t ，s t r a n ds p a c em o d e li sa sw e a ka so t h e rf o r m a lm e t h o d s i nv i e wo ft h i s p r o b l e m ，t h i sp a p e rp r o p o s e dt h ec o n c e p to f t h ep a r a m e t e r - a g r e e m e n t - m a t r i xb a s e d0 1 1 a u t h e n t i c a t i o nt e s t s c o m p a r i n gw i t ho r i g i n a lm e t h o d ，i ti sm o r ei n t u i t i o n i s t i ca n d s i m p l et oa n a y l s es e c u r i t yp r o t o c o l s ，c a nr e v e a lt h er e a s o n sf o r t h ef a i l u r eo f p r o t o c o l s a n dt h ec o r r e s p o n d i n gi m p r o v e m e n ti d e a sa i m e da tt h ec a u s e s k e y w o r d s ：s e c u r i t yp r o t o c o l ；s t r a n ds p a c e ；a u t h e n t i c a t i o nt e s t s ； p a r a m e t e r - a g r e e m e n t - m a t r i x i l 郑州大学硕士学位论文 第一章绪论 1 1 安全协议验证的研究背景 计算机网络正以前所未有的速度发展和普及，并向各个领域渗透，电子商务 和电子政务也正在蓬勃兴起，计算机网络已经成为人们日常生活的一个重要组成 部分。随着人们对网络需求的增加，网络本身所存在的安全问题变得越来越突出， 也越来越复杂，解决安全问题对许多网络应用来说己是头等大事。从目前解决安 全问题的方式来看，安全协议是解决网络安全问题的最有效的手段之一。 安全协议，也称作密码协议，是以密码学为基础的消息交换协议，其目的就 是为了在复杂的、不安全的网络环境中提供各种安全服务，目前在计算机网络中 应用得非常广泛。安全目标是多种多样的，例如，认证协议的目标是认证参加协 议的主体的身份，此外，许多认证协议还有一个附加的目标，即在主体之间安全 地分配密钥或其他各种秘密。非否认协议的目标有两个：一个是确认发送方非否 认( 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 f r e c e i p t ) ，亦即非否认协议向发送方提供不可抵赖的证据，证明接收方己收到了 某条消息。目前用于电于商务的安全协议功能除了实现认证性、非否认性之外， 还有可追究性、公平性等等。 n e c d h a m - s c h r o c d c r 协 2 ；【l 】( 简称n s 协议) 是最为著名的早期的认证协议， 许多广泛使用的认证协议都是以此协议为蓝本而设计的。n s 协议可分为对称密 码体制和非对称密码体制下的两种版本，分别简称为n s s k 协议和n s p k 协议。 这些早期的经典安全协议是安全协议分析的“试验床”，亦即每出现一个新的形 式化分析方法，都要先分析这几个安全协议，验证新方法的有效性。同时，学者 们也经常以它们为例，说明安全协议的设计原则和各种不同分析方法的特点。 经验表明，设计和分析一个正确的认证协议是一项十分困难的任务。即使只 讨论最基本的认证协议，其中参加协议的主体只有2 3 个，交换的消息只有3 巧 条，设计一个正确的、符合认证目标的、没有冗余的认证协议也十分困州2 捌。 迄今所知的许多协议都存在这样或那样的安全缺陷，其中的原因是多方面的，例 如缺乏正确设计认证协议的指导原则；对认证协议进行非形式化的推理分析；缺 郑州大学硕士学位论文 乏有力的分析认证协议的形式化工具；没有考虑到针对认证协议的多种攻击类 型；对认证协议施加太多或太强的假设等。 安全协议设计与分析的困难性在于：( 1 ) 安全目标本身的微妙性。例如，表 面上十分简单的“认证目标”，实际上十分微妙。关于认证性的定义，至今存在 各种不同的观点：( 2 ) 协议运行环境的复杂性。实际上，当安全协议运行在一个 十分复杂的公开环境时，攻击者处处存在。我们必须形式化地刻画安全协议的运 行环境，这当然是一项艰巨的任务；( 3 ) 攻击者模型的复杂性。我们必须形式化 地描述攻击者的能力，对攻击者和攻击行为进行分类和形式化的分析；( 4 ) 安全 协议本身具有“高并发性”的特点。因此，安全协议的分析变得更加复杂并具有 挑战性。 因此必须借助形式化的分析工具，证明安全协议的正确性。对安全协议的形 式化分析始于1 9 8 3 年韵d o l o r 和y a o 。自此以后，许多学者围绕安全协议和安 全协议的形式化分折开展了大量的研究。一方面，随着计算机网络应用范围的扩 展，针对各种应用目的的具有特定的安全性质的安全协议被开发出未；另一方面， 针对安全协议及其特定的安全性质，各种有效的形式化方法不断提出并得到扩 展。 1 2 安全协议验证的研究现状 到目前为止，人们已经开发了许多安全协议。根据这些协议应用目的的不同， 可以将它们分为不同的类型： ( 1 ) 无可信第三方的对称密钥协议。属于这一类的典型协议有以下i s o 系 列协议 4 1 ：i s o 对称密钥一遍单边认证协议；i s o 对称密钥二遍单边认证协议； i s o 对称密钥二遍相互认证协议；i s o 对称密钥三遍相互认证协议；a n d r 鄂v 安 全r p c 协谢5 1 等。 ( 2 ) 应用密码校验函数( c c f ) 的认证协议。属于这一类的典型协议包括 以下i s o 系列协议 6 1 ：i s o 应用c c f 的一遍单边认证协议；i s o 应用c c f 的二 遍单边认证协议；i s o 应用c c f 的二遍相互认证协议；i s o 应用c c f 的三遍相 互认证协议。 ( 3 ) 具有可信第三方的对称密钥协议。属于这一类的典型协议包括n s s k 协谢”、o t w a y - r e e s 协议【7 1 、y a h l o m 协议f 引、大嘴青蛙协i ! ；【引、d e n n i n g s a c c o 2 郑州大学硕士学位论文 协议【9 】、w o o - l a m 协议【1 0 l 等。 ( 4 ) 对称密钥重复认证协议。属于这一类的典型协议有k e r b e r o s 协议版本 5 协议、n e u m a a - s m b b l c b i n e 协议f l i l 、k a o - c h o w 重复认证协议【1 2 1 等。 ( 5 ) 无可信第三方的公开密钥协议。属于这一类的典型协议有以下i s o 系 列协议【1 3 1 ：i s o 公开密钥一遍单边认证协议、i s o 公开密钥二遍单边认证协议、 i s o 公开密钥二遍相互认证协议、i $ o 公开密钥三遍相互认证协议、i s o 公开密 钥二遍并行相互认证协议、d i f f i e - h e i l m a n 协谢1 卅等。 ( 6 ) 具有可信第三方的公开密钥协议属于这一类的协议有n s p k 协议1 】 等。 针对各种类型的安全协议及其安全性质，人们提出了多种形式化方法来进行 相应的分析验证。这些形式化方法大体上可分为：通用形式化方法。如，l o t o s 、 有限状状态机、p c t r i 网、最弱前置谓词w p 等。基于知识和信念推理的模态逻 辑方法。如，k a i l a r 逻辑、b a n 逻辑以及b a n 类逻辑。基于通信状态规模型的 研究方法。如，c s p 和c s p 的模型检测工具f d r 。定理证明分析方法。如，串 空间( s t r a n ds p a c e ) 方法。 1 3 本文工作 本文对串空间模型及其在协议的形式化验证方面，做了详细的介绍、分析和 研究，在此过程中所做的主要工作有： 1 研究了运用串空间模型分析协议的基本方法和过程： 2 运用串空问理论中“理想”和“诚实”的概念，对改进的n s s k 协议进行 了正确性证明； 3 针对串空间模型在协议分析中的不足，在认证测试的基础上提出了参数一 致性矩阵的概念： 4 运用参数一致性矩阵对协议的一致性进行分析。与原有方法相比，找出了 协议失败的原因并给出改进的方向。另外，分析过程的形式化也有利于协议分析 自动化工具的实现。 1 4 章节安排 本文共分为六章： 郑州大学硕士学位论文 第一章，主要介绍了安全协议形式化分析的背景、现状以及各种常用的形式 化方法 第二章，主要介绍了安全协议中使用到的密码体制、安全协议的基本概念、 系统模型以及在协议形式化分析中的基本假设。 第三章，详细介绍了串空问模型的基本概念、定义、定理，以及使用串空间 模型分析协议的一般过程。 第四章，利用串空间模型中“理想”和“诚实”，对改进的n s s k 协议的安 全性进行分析。 第五章，提出了基于认证测试方法的参数一致性矩阵概念，并使用参数一致 性矩阵对o t w a y - r e c s 协议进行分析，分析结果表明该方法的有效性。 第六章，对全文的工作进行总结，并对下一步的工作进行了展望。 4 郑州大学硕士学位论文 2 1 密码学基础 第二章安全协议形式化分析 2 1 1 密码学简介 密码学是网络信息安全科学和技术的最为直接的学科基础，密码学是保证信 息安全性的关键技术。密码学( c r y p t o g o r a p h y ) 有着漫长、丰富的历史，它研究 如何把信息转换成一种隐蔽的方式并阻止其他人理解获得。在过去，密码学用于 在重要的交流活动中来确保隐蔽性，如在间谍活动和反间谍活动之间，或外交官 和总部联系之间等。密码学方法分为两类：一类叫隐写术( s t e g a n o g r a p h y ) ，另 一类叫密码编码学。前者是将秘密信息隐藏在大量无用的信息当中，信息的冗余 度较大，后者是通过各种文本转换的方法使得信息为外部不可理解。本文所涉及 到的密码学是指密码编码学，以下称为密码学。 现代密码学是一门跨越多个学科的科目，涉及到许多理论和工程领域的知 识。它可以被看作是信息论理论，却使用了大量的数学领域的工具，如众所周知 的数论和有限域知识；密码学也可以说是工程学的一个分支，不同的是它必须应 对一些活动频繁的、高度智慧的、怀有恶意的敌人的攻击。早期的密码学采用两 种方法：把给定的信息的字母打乱顺序进行重排，或者使用一组字母替换另一组 字母，比如说著名的恺撒密码和h i l l 密码，进行这种操作需要一个密码本 ( e o d e b o o k ) 。现代的密码学，由于使用了计算机对信息进行处理，所以与传统 的密码编码学有了很大的不同，操作的对象从以前的字母或者文字变成了计算机 内部表示的0 、l 序列，通信双方进行交互传递的信息也不再是字母或者文字， 而是可以被计算机理解的0 、l 序列。近几十年来，随着计算机和网络的普及， 密码学取得了惊人进展，它的使用范围和功能越来越广，从保密性和认证性，扩 充到了匿名性、不可否认性等等。 2 1 2 基本概念 原始的未被处理过的信息，也就是需要使用密码学技术被保护起来的信息， 称为明文( p l a i n t e x t ) 。原始信息使用了密码学技术转换之后所产生的信息，也州 做加密后的信息，称为密文( c i p h e r t e x t ) 。对原始明文信息使用密码学技术转换 郑州大学硕士学位论文 成密文的过程，称为加密( e n c r y p t i o n ) 操作加密的逆向过程，即把密文信息 恢复成原始明文信息的过程，称为解密( d e c r y p t i o n ) 操作。加密操作和解密操 作的另外两种说法是e n c i p h e r i n g 和d e c i p h e r i n g 。把原始明文信息加密成为密文 信息的过程之中所使用的类似于钥匙的额外附加信息，称为加密密钥( 通常使用 字母k 表示) 。把密文信息解密恢复成原始明文信息的过程之中所使用的类似于 钥匙的额外附加信息，称为解密密钥( 通常使用字母表示) 、把原始明文信 息加密成密文信息的具体步骤和方法，称为加密算法。加密密钥和解密密钥是相 同的，或者两者之间容易互相导出的密码体制，称为私钥密码体制。加密密钥和 解密密钥是不同的，且两者之间难于互相推导的密码体制，称为公钥密码体制。 2 1 3 密码体制 在私钥密码体制中，加密过程和解密过程使用的密钥相同或者解密密钥容易 从加密密钥导出。在这种系统中，加密密钥或者解密密钥暴露将会使得整个加密 体制被攻破。因此，私钥系统密码的一个严重缺陷就是在任何密文传输之前，会 话通信的双方必须使用一个严格安全的信道预先协商加密和解密密钥。在实际 中，达到这一点是很难的。在私钥密码体制中，使用最为广泛也最为著名的就是 2 0 世纪8 0 年代公布的数据加密标准d e s ( d a t ae n c r y p t i o ns t a n d a r d ) 和2 0 0 0 年 公布的高级加密标准a e s ( a d v a n c e de n c r y p t i o ns t a n d a r d ) 。私钥密码体制的优 点在于速度快，硬件实现比较容易，因为大部分的操作都是逻辑和置换。在现实 生活中，银行的a t m 机一般都使用d e s 加密体制。 在公钥密码体制中，任何密钥都是成对的，一个专门用于加密，另一个用于 解密。加密密钥和解密密钥的地位是对称的，但是内容是不相同的，并且在现有 的时间和空间内从任意一方推出另一方是很困难甚至是不现实的。使用任意一方 进行加密的信息都可以，而且只能用相对应的另一方进行解密恢复出原有的明文 信息。公钥密码体制的另一个重大作用在于实现数字签名，也就是对密码持有者 身份的证明，因为用他的私钥加密( 此过程称为签名) 的信息只能使用他公开发 布的与之私钥匹配对应的公钥才可以解密( 此过程称为验证) 还原为原有信息。 这是公钥密码体制的一个伟大创新，使用这个特点就可以为每个人确定一个身 份，而不需要使用传统的手工签名等方法来鉴别和证明身份。公钥密码体制的思 想提出以后，各种算法的公开密钥体制和数字签名方案纷纷出台。其中最著名的 6 郑州大学硕士学位论文 是由r i v e s t 、s h a m i r 和a d l e m a n 在1 9 7 8 年提出的r s a 体制【1 5 1 。r s a 体制是一 种基于数论中大合数分解的困难性的公钥密码体制，是历史最悠久、应用最广泛 的公钥密码体制。另外就是基于离散对数求逆困难性问题建立起来的e i g a m a l 体制和椭圆曲线密码体制( e c c ) 。公钥密码体制的优点在于安全性和应用广泛 性，但缺点是运算速度太慢，不适合直接用于加密和签名。在现实的网络中，公 钥密码体制的应用己经非常广泛，比如p e m ( p r i v a c ye n h a n c e dm a i l ) 、s - m i m e 、 p g p 、x 5 0 9 等。 综合私钥密码体制和公钥密码体制各自的优点和缺点，在密码学的解决方案 中经常使用公钥密码体制来交换私钥密码体制中所使用到的加密密钥，比如 d i f f i e - h e l l m a n 密钥交换算法，而在签名的解决方案中则引进了h a s h 函数，只 对签名信息的h a s h 结果( 固定长度的信息) 进行签名操作。 2 2 安全协议 2 2 1 基本概念 安全协议运行过程之中的参与者，称为主体，这里的主体的概念很广泛，可 能是人，也可能是一个程序，或者是一个服务器。协议的运行由一些相互独立的 有先后顺序的动作序列和步骤构成，这种独立的动作序列被称为一个角色或者身 份。每个角色的功能是独立的，但相互之间是关联的和交互的，比如发起者、响 应者等等。在协议中，主体与角色的概念是不尽相同的，一个主体可能就代表一 个角色，同样也可能扮演多个角色和身份。从发起者发起一个协议开始，到最终 协议的结束，称为协议的一轮运行。一轮协议的运行当中所涉及到的参与者的数 目，或者角色不一定恰好符合安全协议的规定，其中那些破坏协议的正常运行， 或者不遵守协议规定步骤的参与者称为攻击者( 或者叫做攻击者角色) ，其他的 参与者称为诚实参与者( 或者叫做诚实角色) 。协议的一个参与者a ( 这里也可 以使用主体或者角色代替) 向另外一个参与者b ( 这里也可以使用主体或者角色 代替) 传递一个消息，称a 的动作为发送，b 的动作为接收，a 称为消息的发 送者，b 称为消息的接收者。一个安全协议p 在运行过程中，假如有攻击者( 攻 击角色) 存在，并且没有被系统或者诚实角色所察觉，同时攻击者在参与过程之 中并没有利用任何密码学上的漏洞，称安全协议p 被攻破，即前面安全协议p 郑州大学硕士学位论文 存在设计上的漏洞。 2 2 2 系统模型 网络通信环境是安全协议运行的物理基础，这个通信环境中存在许多未知 的、不确定的、不安全的因素。安全协议设计和分析的困难性原因之一就在于安 全协议运行环境的异常复杂性，攻击者无时无刻不存在，手段和能力无法具体估 计和量化，刻画安全协议的运行环境和形式化描述攻击者的能力比较困难。安全 协议的形式化分析最主要的问题在于评价和模拟这个环境，对网络上存在的主动 或者被动攻击者的模型进行具体化。如果将安全协议及其所处的环境视为一个系 统，那么在这个系统中，一般而言包括发送和接收信息的诚实的主体和一个攻击 者( 把所有的攻击者都看作是一个团伙) ，以及消息发送和接收的规则，如图2 1 所示。协议的合法消息可被攻击者截取、重放和篡改。攻击者将所有己知的消息 放入其知识集合k s ( k n o w l e d g es e t ) 中，诚实主体之间交换的任何消息都将被 加入到攻击者的k s 中，并且，攻击者可对k s 中的消息进行操作，所得消息也 将加入到k s 中，攻击者可进行的操作至少包括连接、拆分、加密和解密。 图2 1 安全协议系统模型示意图 一个被动攻击者可以在线窃听敏感信息，而一个主动攻击者则可截获数据 包，并对其进行任意的修改，甚至可以伪装成通信主体，欺骗诚实主体与其迸行 非法的模拟通信。加密手段可以有效地阻止主动入侵，因为在不知道密钥且无法 破解密码体制的前提下，对密文的丝毫改动都将导致解密运算失败，从而有效阻 止攻击者的破坏企图，此时攻击者能做的仅仅是阻止消息送达或者准时送达目的 地。归纳起来，攻击者的行为能力一般表现为以下八种形式： ( 1 ) 猜测协议中传递的消息； 郏州大学硕士学位论文 ( 2 ) 将消息完整地转发出去； ( 3 ) 延迟消息的准时送达； ( 4 ) 对消息施行加密运算后转发； ( 5 ) 对消息施行解密运算后转发； ( 6 ) 将消息与以前接收的消息合并后转发； ( 7 ) 阻止消息被准确地送达目的地； ( 8 ) 将以前接收的消息重放出去。 在认证系统中，假设每一个主体与可信服务器之间共享一个秘密密钥，密钥 是通过离线( 比如信函或者电话) 方式建立的。当两个主体要进行秘密通信时， 它们要建立一个仅为互相所知的秘密密钥，这个秘密密钥的作用相当于一个秘密 通道，不知道密钥的攻击者无法干扰通信。 综上所述，我们使用以下几个主要部分来刻画安全协议的系统环境模型：诚 实的参与者( 包括个人，可信服务器，组织等) ，诚实参与者的能力( 发送和接 收消息，以及对消息进行加密和解密运算) ，攻击者( 包括个人，程序，组织等) ， 攻击者能力( 上面所描述的八种能力) ，加密体制( 包括公钥体制和私钥体制) ， 网络通信实体，全局时钟，明文消息空问，密文消息空间。任何一种研究分析安 全协议的方法都必须要对上述要素进行考虑，并给出具体的描述或者假定。 2 2 3 安全协议缺陷 许多安全协议只包含为数不多的几条消息传递，其中每一条消息都是经过巧 妙设计的，消息之间存在着复杂的相互作用和制约；同时，安全协议中经常会使 用多种不同的密码体制，这样就导致安全协议非常复杂、精致，更有可能存在着 无法估计和判断的安全缺陷( 安全漏洞) 。造成安全协议存在安全缺陷的原因主 要有两个：一是协议设计者误解或者采用了不恰当的技术；二是协议设计者对环 境要求的安全需求研究不足。因此，对安全协议的安全性进行分析和研究是一个 重要的课题。 实际应用的安全协议产生缺陷的原因是多种多样的，很难有一种通用的分类 方法将安全协议的安全缺陷进行分类。g r i t z a l i s 和s p i n e l l i s 协1 根据安全缺陷产生 的原因和相应的攻击方法把安全协议的缺陷分为如下六类： ( 1 ) 基本协议缺陷：是指在安全协议的设计中没有采取或者只采取很少防 9 郑州大学硕上学位论文 范攻击者攻击的措施，文献【1 7 】的认证密钥交换协议存在这种安全缺陷； ( 2 ) 口令密钥猜测缺陷：这类缺陷产生往往是因为用户从一些常用的单词、 词组中选择他的密钥口令，从而导致攻击者能够采取字典攻击的手段进行口令 猜测攻击；另外的可能是因为用户选取了不安全的伪随机数生成算法构造密钥， 使得一些强大的攻击者能够恢复该密钥，文献【1 8 1 9 雏2 1 1 中协议可能存在这种安 全缺陷； ( 3 ) 陈旧消息缺陷：主要由于在安全协议设计时没有充分考虑消息的时间 相关性，从而使攻击者能够进行消息重放攻击，包括消息源的攻击、消息目的的 攻击等等，文献f 毖2 如中的协议己经被发现存在这种安全缺陷； ( 4 ) 并行会话缺陷：也叫应答机会话缺陷、多角色漏洞，主要是由于攻击 者可以通过交换适当的消息从而获得他真正想得到的消息，文献2 1 中给出了存 在这种缺陷的协议范例； ( 5 ) 内在性缺陷：由于协议的消息可达性存在问题，安全协议的参与者中 至少有一方不能够完成所有必须的动作而导致的一种协议缺陷，文献【卅中给出 了存在这种缺陷的协议范例； ( 6 ) 密码体制缺陷：这是一种根本性的安全协议缺陷，因为安全协议的可 靠性在很大程度上就依赖于密码算法的安全和可靠，如果安全协议中所使用的密 码算法存在根本性缺陷，则必将导致协议参与各方之间所有交互的加密消息都可 能会被解密，由此造成攻击者可以非常容易或者有很大可能的充当合法的角色参 与协议，欺骗诚实的角色。 2 3 形式化分析的基本假定 如前面所述，安全协议的形式化分析首先需要对安全协议系统模型，以及攻 击者能力进行具体的刻画。不同的形式化方法对系统模型的要素有不同的描述和 假定，这里给出一些关于加密运算、运行环境和攻击者能力方面的基本假定： ( 1 ) 加密数据无碰撞性假定。无碰撞包含3 层意思：任意两条不同的明文 消息使用相同的密钥加密后不会产生相同的密文消息，任意两条不同的明文消息 使用任意两个不相同的密钥加密后不会产生相同的密文消息，相同的明文消息使 用任意两个不相同密钥加密后不会产生相同的密文消息； ( 2 ) 加密数据完整独立性假定。假定认为一个加密消息块无法被拆分成数 0 郑州大学硕士学位论文 个小的加密块，同样一个加密消息块无法由数个小的加密块连接拼凑而成，而且 一条消息中的两个加密块可以被区分开来，被认为是两次分别到达； ( 3 ) 加密体制完备性假定。假定认为任意的加密消息块只能被拥有解密密 钥的主体理解，并认为在有限时间和空间内，或者加密消息失去价值之前是不会 被攻击者理解的： ( 4 ) 攻击者身份未知假定。安全协议的运行主体中包含了诚实的参与者和 攻击者，任意一个参与者都可能充当着攻击者的角色，但不可能在某一轮协议的 运行中所有的参与者都是攻击者角色，当他( 它) 完全遵循安全协议的规定参与 协议时就是一个诚实的角色，当他( 它) 不完全遵守安全协议规定参与协议时就 充当了攻击者的角色； ( 5 ) 攻击者具有对消息进行加密和解密运算的能力，还具有对连接消息项 进行拆分的能力；此外，攻击者了解协议的运行规则，可以根据己知的知识合理 ( 合理指的是不能肆意破解加密消息) 推导隐藏知识；一般而言，攻击者还可以 得到协议运行中参与主体之间传递的消息，并可以参与到协议的运行当中。 2 4 形式化分析方法 针对各种类型的安全协议及其安全性质，人们提出了多种形式化方法来进行 相应的分析验证。这些形式化方法大体上可分为：通用形式化方法、基于知识和 信念推理的模态逻辑方法、基于通信状态机模型的研究方法以及定理证明分析方 法。 通用形式化分析方法 比较典型的用来分析安全协议的通用形式化方法有l o t o s 2 5 1 、有限状状态 机【碉、p e m 网【2 7 1 、最弱前置谓词w p 2 8 1 等。 基于知识和信念推理的模态逻辑方法 该方法将安全协议看作一种分布式的运算过程，用于协议分析的逻辑通常包 含于一种协议描述语言中，用这种语言的句子来描述协议主体知道什么，信任什 么；同时用语言中的推理规则来对这些语句进行推导，从而生成新的语句。分析 的过程就是将安全目标用语句描述出来，按照协议规格说明和初始条件来推导， 看能否得到安全目标的语句。 郑州大学硕士学位论文 最有影响的逻辑系统是b a n 逻辑【2 卅以及b a n 类逻辑 3 0 1 。b a n 逻辑以及 b a n 类逻辑都属于信念逻辑，它是要证明某个主体相信某一公式，因而只能用 来分析密钥发布协议和认证协议的保密性、完整性、认证性等性质。而电子商务 协议中的可追究性的目的在于某个主体要向第三方证明另一方对某个公式负有 责任，亦即不可否认性。鉴于此，k a i l a r 提出了新的可用于分析电子商务协议中 的可追究性的形式化分析方法【3 “，称为k a i l a r 逻辑，用于验证c a m e g i em e l l o n 的i b s 协议。 与b a n 逻辑相比，k a l l a r 逻辑更自然，应用也更广泛，但也同样存在着应 用的局限性。周典萃等指出k a i l a r 逻辑的局限性主要在于其不能分析协议的公平 性瞰1 ，鉴于此，文献【3 3 1 提出了一种新的形式化方法，用于分析电子商务协议的 可追究性和公平性。这种新的逻辑可用于对m e d v i n s k y 和n e u m a n 提出的电子支 付协议进行分析，也可用于对j z h o u 和g o l l m a n 提出的电子合同签订协议的可 追究性和公平性进行分析。 基于通信状态机模型的研究方法 模型检测技术是验证有限状态系统的自动化分析技术，是一种安全协议的自 动验证工具。其基本思路是：用状态迁移系统构造一个运行该协议的模型，同时 结合一个能与协议交互作用的通常意义下的入侵者模型，用模态时序逻辑公式 描述系统的性质，然后利用状态探测工具检测系统是否进入一个不安全状态，从 而说明是否存在对协议的一个攻击。 应用模型检测技术的最早的协议分析系统是m i l l e n 的i n t e r r o g a t o r p 4 1 。 i n t e r r o g a t o r 被用来成功地发现了许多已知的协议缺陷，例如n e e d h a m s c h r o e d c r 对称密钥协议所存在的缺陷。 1 9 9 5 年，r o s c o c 3 5 1 首先提出了使用c s p 和c s p 的模型检测工具f d r ( f a i l u r e s d i v e r g e n c e sr e h n e m e n tc h e c k e r ) 来对密钥发布协议进行验证的思路。 之后，l o w 一3 6 】首先使用c s p 模型和f d r 工具来对n e e d h a m s c h r o e d e r 公钥协 议进行分析，并首次成功地发现了该协议所存在的中间人攻击。f d r 还被用来 对n e t b i l l 协议和d i g i c a s h 协议的原子性进行了分析。此外，t i v l n 协议和s e t 协议也采用f d r 进行了分析。 基于定理证明的方法 郑州大学硕士学位论文 用于分析安全协议的定理证明方法与程序正确性的证明相似，把对安全协议 的证明规约为证明一些循环不变式。k e m m e r e r 最早使用了i n aj o 3 7 1 规格语言及 相应的形式验证系统对安全协议进行分析之后，l a r r yp a n l s o n 在通用证明工具 i s a b e l l e l 3 8 1 的辅助下使用一种归纳的方法对安全协议的安全性质进行分析。 m e a d o w s 等开发的n r l ( n a v a lr e s e a r c hl a b o r a t o r y ) 3 9 , 4 0 协议分析器结合了模 型检测技术和定理证明技术。此外，d u t e r t r e 用p v s 4 1 1 来进行安全协议的分析； b o l i g n a n o 利用定义证明器c o q 对c s e 一4 2 1 进行了验证。 1 9 9 8 年，t h a y e r 等人提出串空间( s t r a n ds p a c e ) 方法 4 3 1 ，之后不久就给出了 将串空间用于验证安全协议的认证性和秘密性的方法。2 0 0 4 年，t h a y c r 等人再 次对串空间模型进行了扩展，将串空间与信任管理结合起来 4 4 1 ，从而使得串空 间模型有可能应用于除了基本的认证性和秘密性之外的其它安全协议属性。 与以往提出的协议形式化分析方法不同的是，串空间机制包括了一个描述因 果结构的偏序关系和一个类递归证明方法，并提出了与所分析的具体协议不相关 的攻击者能力边界的概念。串空间的特点是协议模型简洁且比较容易证明协议的 正确性。归纳起来，串空问协议形式化分析方法的优点体现在以下方面： ( 1 ) 给出了一些数据项的清晰语义( 如：要保证会话密钥的新鲜性，则该 会话密钥只能出现在一轮协议中) ，语义清晰是证明结果准确的重要前提保证。 ( 2 ) 给出了攻击者可能行为的一个详细模型，并与串空间模型基本定理不 相关，从而可将开发用于界定攻击者能力的一般性定理的工作与研究串空间模型 的工作分开进行。 ( 3 ) 给出了正确性的多种定义，包括秘密性和认证性的说明与推证，从而 为正确性证明方法的开发提供多种可能的方向。 ( 4 ) 使分析者能够更为深入细致地了解协议为什么是正确的，以及所需的 假设。证明过程是简洁的，可人工完成，并有助于更准确地识别出协议的相关条 件。 郑州大学硕士学位论文 第三章串空间模型 3 1 串空间模型简介 1 9 9 8 年，f a b r c g a ，h e r z o g 和g u t t m a n 建立了串空间( s t r a n ds p a c e ) 模型， 将安全协议的形式化分析技术推向一个新的高度。串空问模型是一种结合定理证 明和协议迹的混合方法，由于它具有高效、严谨、直观等特点，受到广泛推崇。 它不仅可以用于证明安全协议的正确性，还可以用于构造攻击，揭示安全协议的 内在缺陷。 为了集中精力分析安全协议本身的安全性，总是假设使用的密码系统是完善 的( p e r f e c t ) 。与其他形式化方法相比，串空间模型具有以下特点：( 1 ) 临时值 和会话密钥等数据项具有新鲜性，并且仅在安全协议的一次运行中出现。对于这 个假设，串空间模型给出了清晰的语义解释。( 2 ) 串空间模型精确地描述了系统 中攻击者的可能行为。在串空间模型下，可以给出与具体安全协议无关的攻击者 能力描述。( 3 ) 在串空间模型下，安全协议正确性的含义既包括认证性，也包括 机密性；扩展了b a n 类逻辑的分析范围。( 4 ) 串空问模型是人们对安全协议的 正确性和所作的假设有更深刻的认识。串空问模型对安全协议正确性的证明比较 简单，可以更准确地确认所做的假设。 在串空间模型中，串是参与安全协议的主体可以执行的事件序列。对于诚实 的主体，该事件序列是根据协议定义，由发送事件和接收事件组合而成的，其中 的密钥和临时值等数据有特定的值。一个串只代表一个主体在协议的一次运行中 的行为，与其他主体的行为和协议的另一次运行无关。不同主体的行为用不同的 串表示，如果一个主体参与了协议的多次运行，则需要用多个串表示。串空间模 型中还定义了攻击者串，描述攻击者的行为。所谓攻击者串，指攻击者发送和接 收消息的事件序列，模拟攻击者所具有的基本能力。攻击者具有的基本能力包括 接收一个对称密钥和用该密钥加密的消息，然后发送解密该消息后的明文；接收 两个消息，然后发送这两个消息的链接；发送攻击者知道的数据项。攻击者的有 效行为可以用多个链接的攻击者串表示。 串空间是由协议主体，包括诚实主体和攻击者的串所组成的串集合。可以将 一个串空间理解为，在协议的生命周期里所有的合法行为和攻击者的所有可能行 4 郑州大学硕士学位论文 为组合的集合。 3 2 串空间基础知识 3 2 1 基本概念 令集合a 中的元素为协议主体根据协议原则可能交换的消息，称a 中的元素 称为项( t e r m ) ，项中最重要的是子项( s u b t c r m ) 关系，记为亡。t o r - t l 表示t o 是 t l 的子项，其递归定义如下： ( 1 ) 如果a c t ，当且仅当a = t ，其中t e t ； ( 2 ) 如果a t - k ，当且仅当a = k ，其中k e k ； ( 3 ) 如果a c g k ，当且仅当a c g 或者萨 g ) b ( 4 ) 如果a c g h ，当且仅当a e g 或者a c h 。 在安全协议中，主体可以接收项，也可以发送项。在串空间模型中，用加号 表示发送项，减号表示接收项。 定义3 1 符号项：符号项是一个二元组 o ，驴，其中a e a 且o = + ，一) ，记 符号项为+ f 或- f 。( a ) + 是符号项的有限序列集合，记( a ) + 中的元素为 。加号表示发送项，减号表示接收项。 在具体应用中，将带符号的项看作是基本项，也就是说，项是可以有子项的。 定义3 2a 上的一个串空间为一个集合且在该集合上存在迹映射：t r ：斗( a ) + 。集合中的元素称为串。 定义3 3 对一个固定的串空间，有： ( 1 ) 结点是二元组 ，其中s e e ，i 是整数且满足1 _ i _ i c n g t h ( t r ( s ) ) ，结点 集合记为n ，称 属于串s 。显然，每个结点属于唯一的一个串。 ( 2 ) 如果n = ( s ，i ) e n ，则i n d e x ( n ) = i ，且s h a n d ( n ) = s 。串s 的迹的第i 个有符号 项t e r m ( n ) 定义为( 砸s ) ) i ，即串s 的迹中的第i 个符号项；无符号项u n st e r m ( n ) 定义为 ( ( 叫s ) ) i ) 2 ，即串s 的迹中的第i 个符号项的无符号部分。 ( 3 ) 如果1 1 1 ，n 2 e n ，那么n l 寸n 2 ，意味着存在a e a ，使得t e r m ( n 1 户+ a ，且 t e r m ( n 2 ) = - a 。这类边记录了串间的一种因果连接，意味着n i 发送消息a ，n 2 接收消 郑州大学硕士学位论文 息a 。 ( 4 ) 如果1 1 i ，n 2 n ，那么n l n 2 ，意味着n l ，n 2 发生在同一个串上，n l 是1 1 2 在串s 上的直接因果前驱。有i n d e x ( n i ) - - i n d e x ( n 2 ) - l 。 ( 5 ) 一个无符号项t 出现在n n 中，当且仅当t r t e r m ( n ) 。 ( 6 ) 令i 为无符号项集合节点n n 是i 的入口点( e n t r y p o i n t ) ，当且仅当