基于strand空间模型的安全协议分析与设计方法研究.pdf

山东大学 硕士学位论文 基于strand空间模型的安全协议分析与设计方法研究 姓名 莫笑丽 申请学位级别 硕士 专业 计算机应用技术 指导教师 史清华 20050405 山东大学硕士学位论文 摘要 因特网因其开放的协议彻底改变了计算机网络 同时也带来了新的风险和 威胁 保护计算机网络最好的方法就是使用快速的自动化程序阻止攻击者的入 侵 手工的不能防止未知类型攻击的方式是不能起到充分保护的作用的 使用 基于共享攻击信息以及机构间合作的主动安全管理的方法可以解决这个问题 安全区域协作是一个建立在可信区域相互合作和协同的框架 它能够保护系统 免遭潜在的攻击并通过交换安全信息和区间合作来预报和响应攻击 在这种动 态的强安全体系结构中 为了保护网络中传送的区域策略免受攻击 需要建立 安全通信系统 密码算法和安全协议是其核心 然而 攻击一个成熟的密码算 法的代价比攻击一个有缺陷的安全协议所需的代价要巨大的多 往往个人或小 团体艚以完成 安全协议往往是攻击者的首先攻击目标 因此 分析 设计安 全有效的安全协议是计算机通讯领域中一个极为重要的研究课题 安全协议是很多分稚式系统安全的基础 它负责密钥分发和身份认证 安 全协议自身的漏洞会对通信的安全造成严重的威胁 现有的许多协议在设计上 普遍存在着某些安全缺陷 安全协议的形式化分析检验技术就成为目前研究的 热点 但现有的各种方法主要用于分析某个具体的安全协议的安全性 而不是 致力于在设计之初就确保协议的安全性 因此使用形式化方法指导安全协议的 设计 对于满足复杂任务的密码协议有着重要的意义 在形式化方法中 基于S t r a n d 空间模型的安全协议分析 可以利用该模型 中包含的确切的因果关系信息 使对协议安全性质的证明十分简洁 认证检验 是T h a y e r 丌发出的手工验证密码协议的方法 可以通过使用加密和随机数达到 认证和新鲜性 同时他也提出了使用认证检验这种安全协议的形式化分析方法 来指导安全协议设计的可能性 并对现有的一些协议作了再现 本文通过对基于S t r a n d 空间模型理论的研究 提出围绕认证检验在安全通 信或电子商务中建立具体情况下特定安全目标的协议 设计的过程既是通过 s t r a n d 空 日J 和认证检验对可信主体证明的过程 本文第四部分创建了A T S P a nA u t h e n t i c a t i o nT e s t b a s e dS e c u r eP r o t o c 0 1 作 为利用认证检验技术设计安全协议的实例 首先确立明确的设计目标 即在一 山东大学硕士学位论文 个三方协议交换中为指定主体提供认证和两两之间的机密性 A T S P 必须同时 提供不可否认保证 这里不考虑公平性 然后设计相应的输入检验满足A T S P 的所有认证属性 设计验证的结果完成一个简单的电子商务事务 验证其达到 购买请求 授权支付以及接收支付款项的基本安全性能 总之 本文是安全通信中 向建立具体安全目标安全协议的一个尝试 通 过设计输入检验 输出检验以及自发检验 使得协议设计的过程简洁明了 并 达到了预期的安全目标 由于协议的设计过程同时也是使用s t r a n d 空间模型进 行验证的过程 通过形式化分析可以帮助了解A T S P 是否做了不必要的事 从 而减少了协议的冗余 提高了通信效率 关键词 安全协议设计 S t r a n d 空间模型 认证检验 山东大学硕士学位论文 A B S T R A C T D u et oi t so p e np r o t o c o t h eI n t e m e th a sr e v o l u t i o n i z e dc o m p u t e rn e t w o r k s b u t t h i sr e v o l u t i o nb r i n g sn e wr i s k sa n dt h r e a t s T h eb e s tw a yt 0p r o t e c tc o m p u t e r n e t w o r k si st o p r e v e n t a t t a c k e r sf r o m i n t r u d i n g u s i n g f a s ta u t o m a t e d p r o c e d u r e s T h i sp r o b l e mc a nb es o l v e db yu s i n ga c t i v es e c u r i t ym a n a g e m e n t b a s e d o ns h a r i n gi n f o r m a t i o na b o u ta t t a c k sa n dc o o p e r a t i o nb e t w e e n0 瑁a l l i z a t i o 璐 S e c u r e Z o n e C o o p e r a t i o n a f r a m e w o r kt h a te s t a b l i s h e sm u t u a lc o l l a b o r a t i o na n d c o o p e r a t i o nb e t w e e nt r u s t e dz o n e s c a np r o t c c ts y s t e m sa n dn e t w o r k sf r o mp o t e n t i a l a t t a c k s I nt h i sp o w e r f u ls e c u r i t ya r c h i t e c t u r e w en e e dt oe s t a b l i s h s e c u r i t y c o m m u n i c a t i o ns y s t e mt op r o t e c ts e c u r i t yi n f o r m a t i o ne x c h a n g e da m o n ge a c hz o n e C i p h e ra l g o r i t h ma n ds e c u r i t yp r o t o c o la r ei t sc o r e B u ti tn e e dm u c hg r e a tp r i c et o a t t a c kam a t u r ec i p h e ra l g o r i t h mt h a nad e f e c t i v es e c u r i t yp r o t o c 0 1 S ot h ea n a l y s i s a n dd e s i g nf o re f f i c i e n ts e c u r i t yp r o t o c o li sm o r ei m p o r t a n tr e s e a r c hp r o b l e mi nt h e f i e l do f c o m p u t e rc o m m u n i c a t i o n T h ef u n d a m e n to fm a n yk i n d so fd i s t r i b u t e ds y s t e mi ss e c u r i t yp r o t o c o l w h o s e r o l e sa r ed i s t r i b u t i n go fk e ya n dA u t h e n t i c a t i o n O n c es o m ef l a w sa r ef o u n di ni t t h e s e c u r i t yo fc o m m u n i c a t i o nw i l lb et h r e a t e n e ds e r i o u s l y T h e r ea r eal o to fs e c u r i t y f l a w si nt h ed e s i g no fm a n ye x i s t e dp r o t o c o l s T h et e c h n o l o g yo fa n a l y z i n ga n d c h e c k i n gf o rs e c u r i t yp r o t o c o l sb e c o m e st h eh o ts p o to f r e s e a r c ha tp r e s e n t B u tt h e p r e s e n tm e t h o d s a r em a i n l yu s e dt oa n a l y z es e c u r i t yo fs o m es p e c i f i cs e c u r i t y p r o t o c o l n o te n s u r et h es e c u r i t yj u s ta tt h eb e g i n n i n go fd e s i g n i n g S ot h eu s a g eo f f o r m a lm e t h o d sf o rd e s i g nf o rs e c u r i t yp r o t o c o lh a sm a g n i f i c e n tm e a n i n g e s p e c i a l l y f o rt h er e q u i r e m e n to f s o m ec o m p l e xc i p h e rp r o t o c 0 1 I nf o r m a lm e t h o d s s e c u r i t yp r o t o c o la n a l y s i sb a s e do nS t r a n dS p a c eM o d e lC a l l m a k eu s eo fe x a c tc a u s a lr e l a t i o ni n f o r m a t i o nt om a k et h ep r o v eo fs e c u r i t y p r o p e r t i e sv e r yc o n c i s e T h a y e rh a sd e v e l o p e da m e t h o d c a l l e dt h e a u t h e n t i c a t i o n t e s t m e t h o d t h a tc a l lb eu s e db yh a n dt ov e r i 每c r y p t o g r a p h i cp r o t o c o l s I tC a n a c h i e v ea u t h e n t i c a t i o na n dr e c e n c yb ye n c r y p t i o na n dr a n d o mn u m b e r A tt h es a m e t i m e s t r a n ds p a c ea n da u t h e n t i c a t i o nc a r l a l s ob eu s e dt og u i d et h e p r o t o c o l d e v e l o p m e n lp r o c e s s T h a y e rs a i dl e a d i n gt on e wp r o t o c o l sb yt h e mi sa l s op o s s i b l e T h r o u g hs t u d y i n gt h ea p p r o a c ho fp r o t o c o la n a l y s i sb a s e do nS t r a n dS p a c e M o d e l i nt h ep a p e rw ep u tf o r w a r dh o wt oc o n s t r u c ts p e c i a l p u r p o s ep r o t o c o l sf o r I I I 山东大学硕士学位论文 s p e c i f i cs i t u a t i o n s i ns e c u i ec o m m u n i c a t i o no re l e c t r o n i cc o n l l n e r c e u s i n g a u t h e n t i c a t i o n A n dt h ep r o c e s so f d e s i g ni st h ep r o v e dp r o c e s sf o rt r u s t e ds u b j e c t sb y s t r a n ds p a c ea n da u t h e n t i c a t i o n W ed e s c r i b eap r o t o c o ld e s i g np r o c e s s a n di l l u s t r a t ei t su s eb yc r e a t i n gA T S P a n A u t h e n t i c a t i o nT e s t b a s e dS e c u r eP r o t o c 0 1 F i r s t o u re x a c td e s i g ng o a l sf o rA T S P a r et Op r o v i d ea u t h e n t i c a t i o na n dp a l r w i s ec o n f i d e n t i a l i t yf o rc e r t a i nv a l u e si na t h r e e w a yp r o t o c o le x c h a n g e A T S P m u s ta l s o p r o v i d en o n r e p r d i a t i o n g u a r a n t e e s H o w e v e r w eg i v e n oa t t e n t i o nt of a i r n e s s T h ed e s i g np r o c e s si s o r g a n i z e da r o u n dt h ea u t h e n t i c a t i o nt e s t s am e t h o df o rp r o t o c o lv e r i f i c a t i o nb a s e do n t h es t r a n ds p a c et h e o r y T h ea u t h e n t i c a t i o nt e s t sd i c t a t eh o wr a n d o m l yg e n e r a t e d v a l u e ss u c ha Sn o u n c e sm a yb ec o m b i n e dw i t he n e r y p t i o nt oa c h i e v ea u t h e n t i c a t i o n a n df r e s h n e s s A T S Po f f e r sf u n c t i o n a l i t ya n df o u rk i n d so f s e e u r i t yg u a r a n t e e s T os u mu p o nt h eb a s i so fs t r a n ds p a c et h e o r y b ya n a l y z i n gp r o c e s st o w a r d s s p e c i a lg o a l sa n dd e s i g no fo u t g o i n ga u t h e n t i c a t i o nt e s t i n c o m i n ga u t h e n t i c a t i o nt e s t a n du n s o l i c i t e da u t h e n t i c a t i o nt e s t w ea c h i e v ee x p e c t e ds e c u r i t yg o a l s T h ep r o c e s si s c o n c i s e M e a n w h i l e t h ed e s i g np r o c e s so f p r o t o c o li sa l s ov e r i f i c a t i o nb ys t r a n ds p a c e m o d e l w h e t h e rA T S Ph a sd o n ea n y t h i n gu n n e c e s s a r yC a nb eS e e nb ya n a l y s i so f f o r m a lm e t h o d T h u st h er e d u n d a n c yo fp r o t o c o li sd e c r e a s e da n dt h ee f f i c i e n c yo f c o m m u n i c a t i o ni Si n c r e a s e d K e y w o r d s S e c u r i t yP r o t o c o lD e s i g n S t r a n ds p a c em o d e l a u t h e n t i c a t i o n 原创性声明和关于论文使用授权的说明 原创性声明 本人郑重声明 所呈交的学位论文 是本人在导师的指导下 独立进行研究所取得的成果 除文中已经注明引用的内容外 本论 文不包含任何其他个人或集体己经发表或撰写过的科研成果 对本 文的研究作出重要贡献的个人和集体 均已在文中以明确方式标明 v 本声明的法律责任由本人承担 论文作者签名 整丝塑日期 关于学位论文使用授权的声明 本人完全了解山东大学有关保留 使用学位论文的规定 同意 学校保留或向国家有关部门或机构送交论文的复印件和电子版 允 许论文被查阅和借阅 本人授权山东大学可以将本学位论文的全部 或部分内容编入有关数据库进行检索 可以采用影印 缩印或其他 复制手段保存论文和汇编本学位论文 保密论文在解密后应遵守此规定 论文作者签名 世导师签名 盥日 期 山东大学硕士学位论文 1 前言 随着互联网技术的应用和发展 信息共享应用日益广泛和深入 近年来 随着电子商务和电子政务的应用 大规模分布式系统迅速发展 使得信息安 全问题日渐突出与复杂 信息安全问题己深入到国家的政治 军事 文化和 意识形态等领域 成为国内外政府和工业界高额投入的焦点 另一方面 信息 安全研究涉及密码学 计算机科学 信息论 计算机技术和代数学等多个学 科 是一个综合性研究领域 吸引了国内外大量学者的学术研究兴趣 成为 学术研究领域一个重要的研究方向 1 1 1 1 1 计算机网络信息安全问题与安全协议 I 1 1 1 安全问题 安全问题是计算机网络的丌放性和信息控制的矛盾结果 在M a r c e l D e k k e r 报告 S e c u r i t yo fI n t e m e t 网络信息安全性包括 保密性 c o n f i d e n t i a l i t y 完整性 I n t e g r i t y 和可用性 A v a i l a b i l i t y 等 随着电子商务应 用 提出了新的安全需求 如 可追究性 A c c o u n t a b i l i t y 不可否认性 N o n r e p u d i a t i o n 和匿名性 A n o n y m i t y 等 数据保密性是指只有授权用户才能 读取受保护的数掘 它是安全通信中最基本需求之一 完整性是保证数掘不 被篡改和毁坏 在电子商务中 数据的完整性尤为重要 可用性是与服务相 关的概念 缺乏可用性即是 拒绝服务 这些是传统的安全需求 可追究性是指可以提供有效的证据证明数据被转移 产生和读取等 非否 认性是指主体不能否认进行了某些操作 如发送或读取数据 它们是在电子 商务中特别重要的安全需求 是保证商务交易可顺利进行的基础 匿名性用 于特定环境保护用户的权益 如在电子选举中 必须保证选举人的匿名性 随着信息技术日益在社会各个领域应用深入 这些安全需要越来越重要 而 且新的安全需求不断出现 由于互联网的开放性 网络中传送的数据可以被任意地产生 伪造 修 山东大学硕士学位论文 改和窃听等 从而破坏信息的相关安全性质 所谓的网络安全攻击就是指违 反安全性的行为 为了保护网络中的传送的数据免受攻击 需要建立安全通信系统 安全 通信系统的核心包括 密码算法和安全协议 常用密码算法包括 对称密码 也称为私钥密码 非对称密码 也称为公 钥密码 哈希函数和M A C M e s s a g e A u t h e n t i c a t i o nC o d e 函数等 密码算法的 原子运算是单向函数 上面几种密码算法是满足一些特殊性质的单向函数 采用密码技术的主要目的是防止对手破译系统中的机密信息 主要用于 抵御被动攻击 而认证则是防止主动攻击的重要技术 对于开放环境中的信 息系统安全有重要作用 认证主要有两种目的 一是验证通信实体的身份是 否真实 称为身份认证 二是验证信息的完整性 此为消息认证 主要是保 证数掘在传送和存储过程中未被篡改 重放或延迟等 与安全协议有关的认 证理论主要是哈希函数和数字签名 哈希 H a s h 函数是将任意长的数字串M 映射成一个较短的定长输出字符串H 的函数h h M 易于计算 称H h M 为 M 的哈希值 也称其是输入M 的数字指纹 D i g i t a lF i n g e rP r i n t 若杂凑函数h 为单向函数 则称其是单向杂凑函数 常用的杂凑算法如M D 5 S H A S e c u r e H a s hA l g o r i t h m 等 数字签名是实现认证的重要工具 在信息安全等方面有重要应用 如身 份认证 数掘完整性 不可否认性 匿名性等 数字签名一般采用公钥密码 体制束实现 一个签名体制由签名算法和验证算法两部分组成 其中签名算 法或签名密钥是秘密的 只有签名人掌握 验证算法则是公开的 以便他人 进行验证 常用的签名体制有R s A 签名体制 E I G a m a l 签名体制 D S S 签名 标准等 1 1 2 安全协议 协议 P r o t o c 0 1 是两个或两个以上的参与者为完成某项任务而采取的一 系列步骤 包括几层含义 协议是有序的过程 即每一步骤必须依次执行 在前一步未完成前 后面步骤不能执行 协议至少需要两个参与者 协议有 一个目标 完成某些任务 例如 计算机网络中广泛使用通信协议 2 山东大学硕士学位论文 将计算机网络中可以用于保护数据安全性的通信协议称作安全协议 安 全协议通过适当地使用密码技术以保护数据安全性 因此 安全协议也称为 密码协议 在本文中 为方便叙述 我们同时使用这两个术语 在不会引起 误解时 有时也简称为 协议 安全协议的类型 目前 还没对安全协议详细和严谨的分类方法 事实 上 从不同的角度可以对安全协议进行不同分类 根据安全协议的目标 可 分为认证协议 包括消息认证和实体认证 建立共享秘密 密钥或保密数据 协 议和认证的秘密建立协议等 根掘安全协议所使用密码算法可分为 对称安全协议 非对称安全协议 混合安全协议以及其他多方计算安全协议等 按照安全协议包含角色的数量可分为 双方安全协议 具有两个角色 的安全协议 多方安全协议 具有三个或三个以上角色的安全协议等 安全通信系统的安全性依赖于多种因素 密码算法的安全强度对于整个 安全系统的安全性当然是至关重要的 然而 安全系统的安全性还依赖于密 码系统所使用的环境 安全协议 一个不安全的安全协议可以使攻击者不用击 破密码体制而成功进行攻击 安全系统代表了密码系统和安全协议的完美结 合 事实上 实际应用中由安全协议产生的安全缺陷远比密码系统带来的安 全性缺陷更为普遍和严重 这是因为攻击一个成熟的密码算法的代价是非常 巨大的 往往个人或小团体难以完成 然而 攻击一个有缺陷的安全协议只 需非常小的代价 而且这种攻击更难被发现 所以造成的后果更严重 因此 安全协议往往是攻击者的首先攻击目标 随着基于I n t e m e t 应用的发展 越来 越多的安全协议被用于解决各种问题 网络安全协议的缺陷会给网络带来严 重的安全问题 而造成难以估量的损失 因此 分析 设计安全有效的安全 协议是计算机通讯领域中一个极为重要的研究课题 1 2 安全协议的安全性与形式化方法 在一般情形下 安全协议的安全性与所用的密码算法是可能相关的 例 如 一些所谓承诺协议和依赖于概率计算的协议等 这些安全协议不使用一 般意义上的对称密码系统或非对称密码 而使用所谓伪随机函数提供概率上 山东大学硕士学位论文 l l 一 一 安全性 协议的本身构成概率算法的一部分 因此 这类安全协议安全性与 所用算法密切相关 目前广泛使用的一类安全协议通常独立于所用的密码算法 可将密码算 法视为 黑箱 这类安全协议所用密码算法往往可替换 他们的安全性可独 立考虑 可在假设所用密码算法安全条件下 分析这类安全协议的安全性 这类安全协议的典型代表是认证协议和建立共享秘密协议 1 2 1 安全协议的脆弱性 实际应用中 造成网络安全协议缺陷的原因是多方面的 但总的说来主 要可分为两类情况 一是由于协议设计缺乏标准规范 协议实现者没有充分 了解协议设计者的意图 因而产生缺陷 二是协议设计者没有充分研究通讯 环境及安全需求 协议设计本身是不J 下确的 通常一个安全协议形式上看是非常简单的 仅含有几个角色和少量的消 息交互步骤 然而 保证设计的安全协议的正确性决不是一件容易的事情 看似简单的安全协议 往往隐藏着不易发现的漏洞 一些山密码学家设计的相信是 安全 的安全协议后来被发现有致命的 缺陷 并且这些缺陷是在假设所用密码算法是绝对安全的条件下 即协议设 计本身的缺陷 这样的例子在文献中大量存在 例如 典型的例子 N e e d h a m S c h r o e d e r 公开密钥协议在公丌三年以后才被发现有致命的缺陷 C C I T TX 5 0 9 草案的认证协议 后来发现攻击者可以用一个过期的会话密钥使 合法主体相信是新的会话密钥 K e r b r o s 协议和S S L S e e u r e S o c k e tL a y e r 协议 的早期版本都被发现存在不同程度的缺陷 而这些仅是其中部分例子 还有 大量其他例子存在 G r i t z a l i s 和D S p i n e l l i s 根据安全缺陷产生的原因和相应的攻击方法将安 全缺陷分为以下六类 1 基本协议缺陷 是指在安全协议的设计中没有或者很少防范攻击者的攻击 2 口令 密钥猜测缺陷 这类缺陷产生的原因是用户往往从一些常用的词中选择口令 从而导致攻 山东大学硕士学位论文 击者能够进行E l 令猜测攻击 或者用户选取了不安全的伪随机数生成算法构 造密钥 使攻击者能够恢复该密钥 对于口令的猜测既可在线进行 也可离 线进行 3 陈 日 s t a l e 消息缺陷 主要是指协议设计中对消息的新鲜性没有充分考虑 从而使攻击者能够进 行消息重放攻击 包括对消息源的攻击 对消息目的的攻击 4 并行会话缺陷 协议对并行会话攻击缺乏防范 从而导致攻击者通过交换适当的协议消息 能够获得所需要的信息 包括并行会话单角色缺陷 并行会话多角色缺陷等 5 内部协议缺陷 协议的可达性存在问题 协议的参与者中至少有一方不能够完成所有必须 的动作而导致的缺陷 6 密码系统缺陷 协议中使用的密码算法不合适或对密码算法的实现不当 而导致协议不能 完全满足所要求的机密性 认证等需求而产生的缺陷 应该指出的是 随着 攻击手段与技术的不断翻新 以上缺陷并不能涵盖网络安全协议在实际应用 中的所有可能出现的漏洞 目前人们还经常提到的攻击方式有类型攻击和中 闻人攻击 前者指攻击者用一种类型的消息字段代替另外一种类型的消息字 段 后者指攻击者用伪造的消息代替通信实体发送的消息 安全协议设计和安全性分析的困难性主要体现在以下几个方面 1 安全协议通信环境的复杂性 大规模网络环境是一个开放的环境 环境 中可能包含许多的恶意攻击者 他们可以察看 修改和删除通信信息 这些 攻击者还可能联合起来进行协同攻击 设计协议必须考虑攻击者执行的各种 攻击 充分地分析攻击者的攻击能力 2 参与安全协议主体的大量性 协议运行的并发性和交错性 在大规模网 络环境中 参与协议运行的主体是大量的 其中包括非诚实主体 不同主体 同时运行协议 产生大量并发的 交错的会话 这些会话可能互相干扰 而 被攻击者利用 因此 协议设计者不能仅根据协议单一运行的情况判断其安 全性 山东大学硕士学位论文 因此 一个实用的密码协议必须经过严格的安全性检验和分析 否则 可能对网络安全性产生难以估量的损害 1 2 2 安全协议安全性分析与形式化方法 二十多年来 人们在安全协议的设计与分析方面己作了大量的工作 主 要集中在以下三个方面 1 安全协议的分析方法 2 安全协议的自动化分析语 言和工具 3 安全协议的设计方法 其中大部分工作集中在前两个方面 即 对现有协议进行分析和验证 也称之为协议的后序 e x p o s O 分析与验证 就安全协议的分析与设计人们提出了很多方法 这些方法各有其优缺点 它们都只能分析某一类具体的安全协议 还没有一个被业界普遍接受的 实 用的分析 设计方法 随着信息安全技术的提高和电子商务 移动通信的快 速发展 出现了许多新的安全协议 它们往往具有比较复杂的结构 这就为 网络安全协议的分析与设计提出了更高的要求 另外 目I j 的方法只能分析 证明一个安全协议的不安全性 不能证明协议的安全性 更无从分析和评测 其安全性 他们缺乏完善的数学描述 不能就其正确性进行严谨的理论证明 更为明显的一个问题就是现有的各种方法主要用于分析某个具体的安全协议 的安全性 而不是致力于在设计之初就确保协议的安全性 目 j i 对安全协议进行分析的方法主要有两大类 一类是攻击检验方法 一类是形式化的分析方法 所谓攻击检验方法就是使用目I j i 己知的对协议的 有效攻击方法 逐一对安全协议进行攻击 以检验安全协议是否具有抵抗这 些攻击的能力 在分析的过程中主要使用自然语言和示意图 对安全协议所 交换的消息进行剖析 由于新的攻击方法层出不穷 因此很难保证协议的安 全性 形式化的分析方法是采用各种形式化的语言或者模型 为安全协议建 立模型 并按照规定的假设和分析多自动化转换工具及相应的形式化输入语 言 同时人们也研制了一系列的自动化协议分析工具以确保分析过程的自动 化 实践证明 形式化方法是安全协议安全性分析最为可靠和有效的途径 形式化方法在计算机安全领域的应用已有很长的历史 广泛应用于安全 模型 流分析 软件测试认证 硬件认证 结构分析和安全协议分析等 其 中 形式化方法在安全协议分析领域的应用是最为成功的例子之一 运用形 6 山东大学硕士学位论文 I l I 式化分析方法发现了原先不知道的许多安全协议缺陷 一个可实际应用的安全协议必须经过安全性分析 形式化分析可以帮助 协议设计者明确 协议是否正确 协议是否比其他协议需要更多的安全假 设 协议是否有多余的东西 基于I n t e r n c t 的通信 通信效率是至关重要的 协议的冗余会导致通信效率低下 形式化分析方法可帮助了解安全协议是否 做了不必要的事 从而提高效率 协议的形式化分析还可便安全协议描述更 为清晰明确 可规范协议的设计方法 避免由于模糊导致协议实现产生漏洞 近年来使用形式化方法指导安全协议的设计的研究日益增多 这对于满 足复杂任务的密码协议有着重要的意义 特别是T h a y e r 等在2 0 0 0 提出的 S t r a n d 空I 日J 模型 S t r a n dS p a c e s M o d e l 5 67 l 使用图的形式来描述协议 利用 该模型中包含的确切的因果关系信息 使得协议安全性质的证明十分简洁 T h a y e r 丌发出的手工验证密码协议的方法 认证检验 同时提出使用认证检 验这种安全协议的形式化分析方法来指导安全协议设计的可能性 并在f 34 1 中 对已有协议作了协议再现 使用S t r a n d 空 日J 和认证检验方法指导安全协议的设计过程 可以快速的 导出新协议 新协议的j 下确性紧随丌发过程得以证明 因此这项研究具有重 要的理论意义和实际应用价值 1 3 研究工作概要与论文安排 1 3 1 目前相关的工作 W o o 和L a m 关于协议设计的论文1 18 1 集中于怎样从一条 完整的信息 中 安全的移出信息 这种方法的局限性在于 第一 通过创建一条完整的信息 协议来达到给定的目标 但没有给出对复杂协议的指导 二 安全删除信息 的应用方面还很模糊 其早期论文 l7 的协议设计过程亦有缺陷 B u t t y a ne ta 1 在 嘲中描述了一个B A N 逻辑 声称能够从中激发一种设计 方法 但很难从他们给出的例子中抽象出这种方法 P e r r i g 和S o n g 的自动化协议产生器A P O t 撸1 使用启发式应用 A P G 使用A t l e n a 2 0 l 应用S t r a n d 空间模型来过滤协议 只保留符合规范的 那些 A P G 没有使用协议独立来分解设计过程 然后再将两方子协议合成协 7 山东大学硕士学位论文 议的方法 A b a d i 与N e e d h a m 在 2 1 1 有关于密码协议的大量的信息 如什么使其正确 怎样设计 然而不是很系统 也没有建立在协议目标和正确性理论的基础上 1 3 2 课题内容与特点 课题研究的具体内容是 1 熟悉网络安全的一般技术 了解安全协议的基本原理 基本分类和性 质以及对安全协议进行验证的一般方法 2 深入研究S t m n d 空问模型和认证检验理论 3 围绕认证检验具体组织协议设计过程 课题研究的特点是 1 使用S t r a n d 空问模型作为协议设计的基本模型 S t r a n d 空间模型是一 种教新的协议分析模型 它把协议的描述和安全属性都转化为图的结构 有 利于借助图的理论和算法 近两年该理论迅速发展 已被广泛用于协议分析 同时 T h a y e r 指出它在指导安全协议设计方面的理论价值 这方面的研究必 将有其实际应用价值 本课题便是在这一方面的一个尝试 2 认证检验是基于S t r a n d 空间理论的协议验证 可以通过使用加密和随 机数达到认证和新鲜性 课题通过创建A T S P a nA u t h e n t i c a t i o nT e s t b a s e d S e c u r eP r o t o c 0 1 说明协议设计过程 整个设计过程实际上是围绕认证检验来组 织 最终的协议结果能够完成一个简单的电子商务事务 并验证其达到购买 请求与授权支付这些基本的安全性能目标 3 使用认证检验的协议设计过程遵循下列步骤 1 将协议要达到的一些精确的目标公式化 涉及主体中一部分子集的协 议目标由只包含这部分主体的子协议构成 2 对每一个目标 选择一个认证检验模型来完成 设计一条只满足这条 认证目标的t r a n s f o r m i n g 边 使用不相交加密保证子协议是独立的 3 再将子协议组合成一条单一协议 可以自由选择组合 并证明其正确 芦 一9 3 山东大学硕士学位论文 2S t r a n d 空间模型 基于通过推广或完善协议模型以提出有效的安全协议分析理论的思想 T h a y e r H e r z o n 及G u t t m a n 提出了S t r a n dS p a c e 模型 该模型把以往使用过的 许多安全协议形式化分析的思想及技术合理融为一体 首先 我们约定 l l 使用以下符号描述协议 1 以A B 等大写英文字母表示协议主体 2 符号N A 表示主体A 生成的随机数 3 符号l 表示主体A 的公钥 4 符号K A 表示主体A 的私钥 5 符号K A B 表示主体A 和B 之间共享的 对称 密钥 6 符号 M K B 表示将消息M 以主体B 的公钥加密 2 1 消息项 原子项集合是一组文本项T 和一组密钥项K 的并集 其中 文本项T 包 括主体名 随机数 银行账号等 密钥项K 包括一组与T 不相交的密钥 在 非对称密码系统中 k l 表示公钥 私钥对中密钥K 的对应成员 而在对称密 码系统中Ko K 项集合 A 可递归地定义为 如果m 是一个文本项或密钥项 那么m 是一个项 如果m 是一个项 k 是一个密钥项 那么 m k 是一个项 表示加密 如果m l 和m 2 是项 那么m l m 2 是一个项 表示连结 如果项a l 出现在项a 2 中 那么a l 是a 2 的子项 即子项关系c 12 可定义为 如果t T 那么a c t 当且仅当a t 如果k K 那么a 亡k 当且仅当a k a C E g k 当且仅当a C g 或a 酚k a C g h 当且仅当a C g 或a C h 或a g h 如果t o C t t o 不是一个连结项 并且对每个t l t o 若满足t o c t lc t 则 t 是一个连结项 那么项t o 是t 的分量 显然 分量或者是原子项 或者是加 9 山东大学硕士学位论文 密项 如果项a 1 能够从项a 2 中不经解密操作就提取出来 那么a l 是a 2 的内项 即内项关系仨 1 2 0 I 定义为 如果t T 那么a t 当且仅当a t 如果k K 那么a E k 当且仅当a k 征值 k 当且仅当a g k a g h 当且仅当a g 或a 仨h 2 2S t r a n d S t r a n d 空间和B u n dI e 2 2 1S t r a n d 和S t r a n d 空间 协议主体在协议执行期I 日J 可以采取的动作的集合A c t 包括发送 s e n d 和 接收 r e c e i v e 等 在协议执行过程中 每个事件是一个二元组 其中 a c t i o n E A c t 表示动作 a r g u E A 是动作的变量 为简单起见 将发送事件 和接收事件 分别表示为符号项 a 和 并将符号项的有限序 列的集合表示为 A 协议为参与者的每个角色定义事件序列 一个S t r a n d 就表示角色的一个 实例的动作序列 而S t r a n d 空间是集合 和映射t r 一 A 1 1 2 1 S t r a n d 上的每个节点是一个二元组 s 其中s E i 是满足ls i S l e n g t h s 的整数 节点n s 在S t r a n ds 上记作n s 显然 每个节 点属于唯一一个S t r a n d N 表示节点的集合 2 如果n 其中a 是符号 或一 那么t e r m n o a 相应地 称节点n 为正 节点或负节点 3 如果n I n 2 N 那么n l n 2 意味着t e r m n 1 a 并且t e r m n g 一a 即节点n l 发送消息a 并且节点n 2 接收该消息 4 如果n I n 2 N 那么n l n 2 意味着n I 和n 2 出现在同一个S t r a n d 中 并且i n d e x n 2 i n d e x n 1 l 即在该S t r a n d 中 事件n l 后紧随事件1 1 2 5 项t 来源于节点n E N 当且仅当s i g n n 且t c t e r m n 并且对 O 山东大学硕士学位论文 于在同一S 拄a n d 中的n 的任何前驱节点n t a t c r m n 6 项t 唯一来源于节点n 当且仅当t 来源于唯一的n N 随机数和 其它新鲜生成的项通常具有唯一来源 也可以用N 表示有向图洲 E 该图的顶点是节点集合 E 一u 等 是 包括n I n 2 和n l 等n 2 其中I l l n 2 N 两种类型的关系的边集合 2 2 2B u n d I e B u n d l e 代表协议在某种配置下 如协议允许的开始者和响应者的数目 的执行 B u n d l e 1 2 C N c E 是N 的子图 其中E 卜u 是边的集合 N c C N 是与E 中的边相关联的节点的集合 并且以下性质成立 1 非空并且是有限图 4 2 如果I l l C 且s i g n n l 产一 那么存在唯一的节点n 2 满足n 2 一n l C 3 如果n I C 且n 2 j n I 那么n 2 警n l e C 4 C 中不存在环 如果对某个S t r a n dS 中的每个节点n 均有n E C 那么S t r a n ds e C 设S 是一个S t r a n d 空间 节点n l n 2S 那么n I s n 2 当且仅当在S 中 存在零个或多个由1 1 1 到n 2 的边一和等的序列 即 s 表达了原因优先关系 2 1 显然 如果C 是一个B u n d l e 那么 c 是一个偏序关系 并且C 中节点 的任一非空子集都有 c 最小成员1 1 并且n 是正节点 2 3 利用S t r a n d 进行协议说明 一个协议中通常包括若干角色 例如 开始者 响应者和服务器等 每 个角色的动作序列都是由协议通过一系列的参数 如主体名 随机数等 预 先定义的 角色和参数列表的绑定给出了该角色的一个实例 协议的一次执 行形成一个B u n d l e 其中合法主体的S t r a n d 被限制为预先定义的踪迹类型 r o l e p a r a m e t e rl i s t l 合法主体的S t r a n d 被称为规则的S t r a n d B u n d l e 中也 包含映射到入侵者踪迹的S t r a n d 这些S t r a n d 被称为入侵者S t r a n d 以公钥体制下的相互认证协议N e e d h a m S c h r o e d e r L o w e 协议 N S L 协议 山东大学硕士学位论文 为例 其标准符号定义如下 1 A B N A K B 2 B A N A