（计算机应用技术专业论文）基于svo逻辑的电子商务协议形式化分析与研究.pdf

基于s v o 逻辑的电子商务协议形式化分析与研究 摘要 电子商务协议形式化分析是电子商务研究的一个重要方面，电子商务协议是面向电子商 务的密码协议，安全的电子商务协议是保证电子商务活动正常开展的基础。进行电子商务协 议的形式化分析研究具有重大理论意义和现实的应用价值，是顺利开展电子商务应用的技术 保障。 形式化的方法是分析安全协议的主要方法。目前己经有很多研究安全协议的理论和方 法，其中比较著名的有可证明安全理论、b a n 类逻辑以及模型检测和定理证明的方法等。 本文主要对基于逻辑的形式化方法与模型检测技术及其在电子商务协议形式化分析中 的应用进行了系统研究，重点对s v o 逻辑方法在电子商务协议时限性形式化分析中的应用 进行了研究。总的来说，从理论到实践两个层面上研究了电子商务协议的形式化分析的相关 技术。本文所做的工作、技术难点和创新之处如下： ( 1 ) 首先从电子商务安全出发，对电子商务协议及其协议形式化分析的国内外研究现 状进行了综述。 ( 2 ) 研究了b a n 逻辑和其相关形式化协议分析的方法、步骤，对b a n 的公理规则 进行了部分扩展。同时对s v o 逻辑进行了部分扩展，使该逻辑可以分析电子商务协议的时 限性。 ( 3 ) 对模型检测工具s p i n 进行了详细的介绍，通过研究p r o m e l a 语言，发现该语言 对时间段的模拟依然比较困难，但是通过编程技巧，可以模拟时间段的一些特性，从而模拟 检测协议的时间特性。 ( 4 ) 利用公钥密码机制对k e r b e r o s 身份认证协议进行了改进，并利用扩展的b a n 逻 | 辑准确地描述并证明了改进后的k e r b e r o s 身份认证协议的安全性。 ( 5 ) 通过研究n 7 _ g 协议和i s l 协议，根据它们各自的优缺点，构造了一个新的基于 b 2 c 电子商务协议，使其具有了匿名性、公平性、时限性等特性。 ( 6 ) 运用扩展后的s v o 逻辑，将该电子商务协议属性抽象化，并分析验证其是否具 有时限性，证明出协议具有时限性。通过模型检测工具s p 矾的模拟检测，说明新协议具有 时限性。分析结果表明，对s v o 逻辑的改进是有效和成功的。 关键词：电子商务协议，形式化分析，s v o 逻辑，时限性，模型检测 中图分类号：t p 3 9 3 0 8 i v t h e a p p l i c a t i o ns t u d yo n f o r m a l i s mo fe l e c t r o n i c c o m m e r c ep r o t o c o l sb a s e do ns v ol o g i c a b s t r a c t f o r m a la n a l y s i so fe - c o m m e r c ep r o t o c o l si sa ni m p o r t a n ta s p e c to fl - - o o r n i h e r c es m d 蚋e e - c o l l u n e r c ep r o t o c o l si sac r y p t o g r a p h i cp r o t o c o lo fe , - c o m n l e r c e ，as e c u r ee - c o m m e r c ep r o t o c o l i st h ef o u n d a t i o no f e - c o m m e r c e s t u d yo i lf o r m a la n a l y s i so f 沁o l u i n e r c ep r o t o c o l sh a sp r o f o u n d e f f e c t sb o t hi nt h e o r ya n dr e a l i z a b l ea p p l i c a t i o n , i t st h et e c h n i c a li n d e m n i f i c a t i o nf o re - c o m m e r c e o p e r t i o n f o r m a lm e t h o d sa r et h em o s ti m p o r t a n tm e t h o d st o a n a l y s i s a r l v e r i f y t h e s e c u r i t y p r o t o c o l s s u c h t h ep r o v a b l et h e o r y , b a n sl o g i c m o d e lc h e c k a n dt h e o r e mp r o v e s t h ed i s s e r t a t i o nm a i n l ys t u d i e st h ea p p l i c a t i o n so fl o # ca n dm o d e lc h e c k i n gm e t h o d si n f o r m a la n a l y s i so fe - c o m m e r c ep r o t o c o l s ，e s p e c i a l l ys t u d i e so ns v o1 0 9 i cm e t h o da n dt h e a p p l i c a t i o no fs v ol o g i co ne - c o m m e r c ef o r m a la n a l y z i n go ft i m e l i n e s s i ng e n e r a l ，t h ea u t h o r s t u d i e st h er e l a t e df o r m a la n a l y s i st e c h n o l o g yo fe - c o m m e r c ep r o t o c o l sf r o mt w oa s p e c t s ，t h e o r y a n da p p l i c a t i o n t h em a i nw o r l 岱a n dr e s u l t sa r ea sf o l l o w s ： ( 1 ) s u mu pt h es t a t u so ft h er e s e a c hi ne l e c t r o n i ce o m m e r c ep r o t o c o l sa n df o r m a la n a l y s i s m e t h o d ( 2 ) s t u d i e st h ea d v a n t a g e sa n dd i s a d v a n t a g e so hb a nl o g i c ，a n d e x t e n d sp a r to f “i o m m l s s t u d i e st h ea d v a n t a g e sa n dd i s a d v a n t a g e so bs v ol o 舀c ，a n di m p r o v ep a r to f d i s a d v a n t a g e st of o r m a l l ya n a l y z et h et i m e l i n e s so f e c o m m e r c ep r o t o c o l s ( 3 ) i n t r o d u c e st h ew o r ko fm o d e l - c h e c k i n gt o o ls p i n t h r o u g hs t u d i e si t sm o d e ll a n g u a g e p r o m e l a , w ed i s c o v e ri ti sv e r yd i f f i c u l tt oc o m p l e t e l ys i m u l a t et h et i m es e c t i o u , b o tw e s i m u l a t ep a r t so ft h et i m es e c t i o nb y $ o l l l ep r o g r a m m es l e i g h t st os i m u l a t et h et i m e c h a r a c t e r i s t i co f p r o t o c o l s ( 4 ) i m p r o v e sk c t b e r o sa u t h e n t i c a t i o np r o t o c o lb a s e do np u b l i ck e yc r y p t o g r a p h y , e x a c t l y d e s c r i b e sa n dp i o v 部t h es e c u r i t yo fi m p r o v e dk c i b e r o sp r o t o c o lb yu s i n gb a nl o g i c ( 5 ) s t u d i e sc l a s s i ce - c o m m e r c ep r o t o c o l s ：n z gp r o t o c o la n di s ip r o t o c o l ，a n a l y z e st h e i r a d v a n t a g e sa n dd i s a d v a n t a g e s ，d e s i g n san e we - c o m n l e r c ep r o t o c o lw h i c hh a ss u c h c h a r a m w s ：s e c u r i t y , n o n - r e p u d i a t i o n ，a n dt i m e l i n e s s ( 6 ) e x t e n d ss v ol o g i ct of o r m a l l ya n a l y z ee - c o m m e r c ep r o t o c o l sb e s i d e si t st i m e l i n e s s ，a n d a n a l y z et h en e we o m m e r c ep r o t o c o lb yu s i n gs p i nt op m v et h a tt h i si m p r o v e m e n ti s s u c c e s s f u l v k e y w o r d s ：e - c o m m e r c ep r o t o c o l ；f o r m a la n a l y s i s ；s v ol o g i c ；t i m e l i n e s s ； m o d e l c h e c k i n g v i 贵州大学硕士论文 原创性声明 本人郑重声明：所呈交的学位论文，是本人在导师的指导下， 独立进行研究所取得的成果。除文中已经注明引用的内容外，本 论文不包含任何其他个人或集体已经发表或撰写过的科研成果。 对本文的研究在做出重要贡献的个人和集体，均已在文中以明确 方式标明。本人完全意识到本声明的法律责任由本人承担。 论文作者签名： 杰丝! l 塞 e l 期： 2q q 2 生 旦 关于学位论文使用授权的声明 本人完全了解贵州大学有关保留、使用学位论文的规定，同 意学校保留或向国家有关部门或机构送交论文的复印件和电子 版，允许论文被查阅和借阅；本人授权贵州大学可以将本学位论 文的全部或部分内容编入有关数据库进行检索，可以采用影印、 缩印或其他复制手段保存论文和汇编本学位论文。 ( 保密论文在解密后应遵守此规定) 论文作者签名：巡导师签名j 翻日期：垫弓盈红 贵州大学硕士论文 1 1 研究背景及意义 1 绪论 随着国际互联网i n t e m e t 的日趋流行，电子商务已经渗透到了社会上的各行各业和人们 的日常生活中。电子商务正在改变着企业和消费者之间就企业的产品和服务供应而进行的交 互方式，它正在为完全崭新的企业风险投资的孕育创造机会，它还促使政府部门重新思考其 一贯作为传统监督者的角色定位。电子商务己经给各种企业、各种职业、消费者、企业家、 投资者以及政府部门造成了巨大的影响。 尽管电子商务的发展前景十分诱人，但是人们对电子商务的安全却普遍心存疑虑。电子 商务活动基于开放的互联网，必然面临各种安全风险，如欺诈、抵赖、信息泄漏或被篡改等 等，如何保证网上信息传播的安全成了人们日益关注的一个重要问题，因为电子商务与人们 日常生活关系密切，它的安全问题就成了最敏感的领域，如果没有安全，根本无法实施任何 电子商务活动。因而在电子商务中，安全是一个至关重要的核心问题。 从目前解决安全问题的方式来看，基于密码技术的安全协议是解决电子商务安全问题最 有效的手段之一。但是，电子商务协议的设计是一项非常复杂而且容易出错的工作，现在比 较成熟的电子商务协议均存在一些漏洞，限制了电子商务的应用。 由此可见，阻碍电子商务向前发展的一个关键问题是电子商务协议的安全性分析问题。 然而，早期的协议安全性分析所采用的是非形式化方法，它是根据己知的各种攻击方法对协 议进行攻击，以攻击是否有效来检验密码协议是否安全。而实际上存在着许多未知的攻击方 法，所以非形式化方法只能分析协议中是否存在已知的缺陷，而不能全面客观地分析密码协 议。因此安全协议的形式化分析方法的的研究对促进电子商务的发展具有重要的意义。为此 作者硕士期间将主要针对电子商务协议的安全特性进行形式化分析与研究。 1 2 国内外研究现状 1 2 1 电子商务协议及其发展现状 电子商务是一种以电子商务协议为构成框架的网络交易系统，其中，电子商务协议的安 全性是决定电子商务发展的关键因素。一个完整的电子商务体系涉及到客户、服务商和银行 等方面【4 】。 2 0 世纪9 0 年代以来，计算机网络技术得到了飞速发展，网络化和全球化成为不可抗拒 的世界潮流。有关机构预计，到2 0 0 7 年，全球b 2 b 电子商务市场的规模将会达到8 3 万亿 美元。 贵州大学硕士论文绪论 电子商务协议是面向电子商务的密码协议，安全的电子商务协议是保证电子商务活动正 常开展的基础，其基本属性包括安全性、保密性、完整性、可认证性、非否认性及公平性 i 划1 1 2 l 【1 3 ) 等。非否认协议的目标有两个：一个是确认发方非否认f 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 fr e c e i p t ) ，亦即非否认协议向发送方提供不可抵赖的证据， 证明接收方己收到了某条消息。同其它密码协议一样，电子商务协议的建模与形式化分析研 究非常重要，对于已有成熟韵密码协议建模分析与验证技术可以直接应用到电子商务协议 中。因此，进行电子商务协议的形式化分析研究具有重大理论意义和现实的应用价值，是顺 利开展电子商务应用的技术保障i 1 】。 典型的电子商务协议有：c h a u m , f i a t & n a o r 协议、d a m g a r d 协议、b r a n d 协议、s s l 协议、 s e t 协议等等【1 。 1 2 2 安全协议形式化分析研究现状 安全协议，是以密码学为基础的消息交换协议，其目的是在网络环境中提供各种安全服 务，实现各自的安全目标，而安全目标又是多种多样的，例如，认证协议的目标是认证参加 协议的主体的身份。此外，许多认证协议还有一个附加的目标。即在主体之间安全地分配密 钥或其他各种秘密。密码协议的主要目的是利用密码技术实现密钥交换、身份认证和安全支 付，在安全领域中协议同密码算法同样重要【1 】o 但是，安全协议的设计极易出错，即使我们只讨论安全协议中最基本的认证协议，其中 参加协议的主体只有两三个，交换的消息也只有有限几条，设计一个正确的、符合认证目标 的、没有冗余的认证协议也是十分困难的【1 ”。因此，2 0 年来，为了应对这一挑战，人们设 计了不同种类的形式化分析方法投入了大量的精力，取得了可喜的成果。 安全协议设计与分析的困难性在于：( 1 ) 安全目标本身的微妙性。例如，表面上十分简单 的“认证目标”，实际上十分微妙。关于认证性的定义，至今存在各种不同的观点；f 2 ) 协议 运行环境的复杂性。实际上，当安全协议运行在一个十分复杂的公开环境时，攻击者处处存 在。我们必须形式化地刻画安全协议的运行环境，这当然是一项艰巨的任务；( 3 ) 攻击者模 型的复杂性。我们必须形式化地描述攻击者的能力，对攻击者和攻击行为进行分类和形式化 的分析；( 4 ) 安全协议本身具有“高并发性”的特点。因此，安全协议的分析变得更加复杂 并具有挑战性【3 j 。 对安全协议用形式化方法分析的工作最初出现在七、八十年代。直到九十年代初，几个 研究者利用形式化方法找到了一些安全协议尚未发现的安全漏洞后，形式化发现安全协议漏 洞的方法才引起人们的极大关注，并逐渐成为信息安全领域中的一个热门方向脚。 安全协议的研究主要包括两方面内容，即安全协议的安全性分析方法研究和各种实用安 全协议的设计与分析研究。安全协议的安全性分析方法主要有两类，一类是攻击检验方法， 一类是形式化分析方法，其中安全协议的形式化分析方法是安全协议研究中最关键的研究问 2 贵州大学硕士论文 绪论 题之一，它的研究始于8 0 年代初，目前正处于百花齐放，充满活力的状态之中。 从大的方面讲，在协议形式化分析方面比较成功的研究思路可以分为三种： 1 ) 逻辑分析方法 逻辑分析方法是迄今为止影响最大，应用最为广泛的协议分析方法。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 逻辑f 1 研，用于描述和验 证密码协议。它成功地对几个著名的协议进行了分析，找出了其中已知和未知的漏洞。 b a n 逻辑的成功极大地激发了密码研究者对密码协议形式化分析的兴趣，并导致许多 密码协议形式化分析方法的产生。b a n 逻辑形式化定义了协议的目标，并且确定了协议初 始时刻各参与者的知识和信任，通过协议中消息的发送和接收步骤产生新的知识，运用推导 规则来得到晟终的信任和知识。如果最终的知识和信任的语句集里不包含所要得到的目标知 识和信任的语句时，就说明协议存在安全缺陷。由于b a n 逻辑简单、直观，便于掌握和使 用，而且可以成功地发现协议中存在的安全缺陷，因此得到了广泛地应用。随后人们在使用 b a n 逻辑分析密码协议时，发现b a n 逻辑存在着缺陷1 s 1 1 2 0 1 2 7 ：初始假设的确定非形式化， 理想化步骤非形式化，缺乏精确定义的语义，无法探测对协议的攻击。为此许多文献对b a n 逻辑进行了某些必要的改进或扩展，这些逻辑分别称为g n y 逻辑阱】、a t 逻辑【“、v o 逻 辑 3 1 】和s v o 逻辑f 3 2 哪驯，人们又把这一类逻辑统称为b a n 类逻辑。但这些改进或扩展的 逻辑都比较复杂，没有最初b a n 逻辑那么简单、实用。 2 ) 模型检测方法 模型检测技术是一种验证有限状态系统的自动化分析工具，如用于硬件电路设计和通信 协议。目前关于模型检测的研究越来越受到人们的关注，因为它对协议的自动验证和工程化 设计具有指导意义。1 9 9 6 年，g a v i nl o w e 首先使用c s p 和模型检测技术对密码协议进行分 析p j ，并首次采用c s p 模型和c s p 模型检测工具f d r 来分析n e e d h a ms c h r o e d e r 公钥协议。 s p i n 系统是基于。符号模型检测”( s y m b o l i c m o d e l c h e c k i n g ) 技术的模型检测工具软件。它 能够检测系统设计的逻辑错误，也能检测异步系统，也用来验证通信协议的正确性。发展到 今天，s p i n 已成为国际上广为流行的分析有限状态系统的常用工具。 目前对于协议分析来讲，模型检测已经证明是一条非常成功的途径，这种方法发现了协 议的许多以前未发现的新的攻击。但模型检测仍然存在着许多问题，最主要的问题在于：模 型检测是用于有限状态系统的分析工具，如何将密码协议说明成有限状态系统，而又没有增 加或减少密码协议的安全性，这将是一个需要深入研究和探索的关键问题。 3 ) 定理证明方法 这是一个新的研究熟点，同证明程序的正确性一样，将协议的证明规约到证明一些循环 不变式。这方面开始于k e m m e r e r 的i m a j o 和i t p 的研究，这个领域中值得一提的还有 b i l i g n a n a 的c o q 证明系统、d u t e r t r e 和s c h n e i d e r 的p v s 证明系统、s n e k k e n e s 的公理证明 器h o l 以及i s a b e l l e 定理证明系统。目前，最为常用的还是p i 演算及其扩展的s p i 演算方 法。 3 贵州大学硕士论文 绪论 近几年来，又出现了两种建立密码协议模型的方法，即归纳方法( 1 n d u c t i em e t h o d ) 和串 空间方法( s t r a n ds p a c em e t h o d ) 。这两种方法与p e t r i 网有密切的联系，其验证过程可由模型 检测工具和定理证明器自动完成，而且正朝着适应于开放式系统的方向发展，因此有着广阔 的发展前景。 到目前为止，还很难找出一种方法把密码协议的各个方面全部包括进去，因此要找出一 种分析方法能够发现或防止密码协议所有可能的漏洞是不可能的，我们只希望在给定合适的 假设条件下保证协议的安全性。应当指出的是，运用形式化分析方法分析密码协议，都只是 保证协议安全性的必要条件，而不是协议安全性的充分条件。 我国科学工作者对国际上已有协议的分析方面做了一些工作，但在实际应用方面与国际 先进水平还有一定的差距【9 j ，因此对安全协议的应用研究同样具有非常重要的意义。 1 3 主要研究内容 ( 1 ) 研究电子商务协议的基本理论和基本性质：安全性、保密性、完整性、可认证性、 非否认性、公平性和时限性等，重点对时限特性进行分析。 ( 2 ) 研究b a n 逻辑的优缺点，并对其公理规则进行部分扩展，使其可以形式化分析改 进的k e r b e r o s 认证协议。 ( 3 ) 研究s v o 逻辑的优缺点，并对其缺点进行部分改进，使其可以分析电子商务协议 的时限性。 ( 4 ) 研究模型检测工具s p i n 的工作原理，学习如何使用p r o m e l a 语言对电子商务协议 进行建模，并编写程序，对p r o m e l a 语言中时间段的设置进行编程模拟。 ( 5 ) 研究电子商务协议：n z g 协议和i s i 协议，并对其各自的优缺点进行分析，根据结 果设计一个新的电子商务协议，使该协议具有不可否认性，匿名性和时限性。 ( 6 ) 使用改进后的s v o 逻辑对新协议的时限性进行证明，并同时使用模型检测工具 s p i n 对新协议时限性进行模型检测。 1 4 本文的组织结构 本论文主要由六个部分组成，具体组织结构如下： 第1 章主要介绍电子商务协议研究现状、安全协议形式化分析研究现状、研究意义以 及文章总体框架。 第2 章主要介绍b a n 类逻辑的发展历史，对各个逻辑的优缺点进行了简要介绍。同 时扩展b a n 逻辑的公理规则，使其可以更加准确的分析证明身份认证协议；另外我们还提 出了s v o 逻辑的改进方案，使s v 0 逻辑可以分析电子商务协议的时限性。 。 第3 章介绍模型检测相关理论及应用，对模型检测工具s p i n 的基本结构、特征以及 p r o m e l a 语言的基本语法做了较详细的阐述。 4 贵州文学硕士论文 绪论 第4 章采用扩展的b a n 逻辑对基于公钥的k e r b e r o s 身份认证协议进行形式化分析证 明，以证明改进后的k e r b e r o s 身份认证协议的安全性是否得到提高。 第5 章分析了n z g 协议和i s i 协议的优缺点，并在二者的基础上提出一个新的具有公 平性、匿名性和时限性的电子商务协议，然后使用改进后的s v o 逻辑对新协议进行时限性 证明，并同时使用模型检测工具s p i n 对新协议时限性进行检钡i ，以此验证s v o 逻辑的改 进是否正确。 第6 章结论与展望。 5 贵州大学硕士论文 基于逻辑的电子商务协议分析方法 2 基于逻辑的电子商务协议分析方法 2 1b a n 逻辑 从1 9 7 8 年到1 9 8 9 年b a n 逻辑嘲冽诞生的十余年中，产生了大量的安全协议。这些协 议中，大多数身份认证协议都含有安全漏洞或者信息冗余。身份认证协议的设计是十分困难 的，很容易出错。有许多原因可能造成错误，例如不熟悉攻击者的行为等，但是最重要的原 因是：没有完善的协议正确性概念，以及没有方便的可用逻辑推理来导出正确或错误结论。 在这样的背景下，。b u r r o w 、a b a d i 和n e e d h a m 共同提出了一种分析认证协议的逻辑( 后 人以他们名字的首字母命名为b a n 逻辑) ，他们的出发点是用这种逻辑对认证协议进行形 式化分析，来研究认证双方是否相信正是认证双方在相互通信而不是入侵者。b a n 逻辑可 以精确地描述各个主体所相信的内容( 称为“信念”) ，并记录导致结果的推理过程。b a n 逻辑定义了这种基于信念的逻辑，用于研究通过认证协议的运行，认证双方通过相互接收和 发送消息来从最初的信念逐渐发展到协议运行最终要达到的目的认证双方的最终信念， 其目的是为分析安全协议提供逻辑工具。b a n 逻辑对被分析的安全协议确立了前提，即协 议采用的密码算法是安全的，不考虑密码算法被攻破的情况。这样就可以集中分析认证协议 的运行所带来的信念结果，这种分析前提成为以后安全协议形式化分析方法所遵循的共同基 本准则。 b a n 逻辑的提出具有划时代意义，它是分析安全协议的一个里程碑，极大地推动了安 全协议的形式化验证这一领域的发展。 2 1 1b a n 逻辑概念 b a n 逻辑建立在模态逻辑基础上，它区分几种对象： 主体( p r i n c i p a l s ) ，即协议参与者，通常用a 、b ，s 表示； 密钥( e n c r y p t i o nk e y s ) ，通常用k n ，k 。、k h 表示两个主体之间的共享密钥，k 、 瓦、k 表示各主体的公钥，k 一、k b 1 、k 4 表示相应的私钥； ( 爹公式( f o r m u l a s ) 或者叫做声明( s t a t e m e n t s ) ，例如用n 、n b 和n 。表示随机数。 p 、q 、r 表示一般意义上的主体，x 、y 表示一般意义上的公式，k 表示一般意义上的 密钥。b a n 逻辑中用逗号表示各部分的连接，连接有类似集合的性质，其元素的顺序可交 换。表示符号如下： 列_ x 或p b e l i e v e s x ：p 相信x ，即p 做出行动时认为x 为真。这种结构在b a n 逻 辑处于中心地位，主体p 所相信内容的集合简称为p 的信条。 6 费州大学硕士论文基于逻辑的电子商务协议分析方法 p q 彳或ps e e s x ：p 看见了x ，有人向p 发送了包含x 的消息，并且p 能够读取和 重复x ( 有可能是在解密运算之后) 。 爿彳或ps a i dx ：p 曾经说过x ，p 在某个时候发出过包含公式x 的消息，虽然不 知道是多久以前发出的消息，但是可以肯定p 发出时p 相信x 。 p | 4 x 或pc o n u o l s x ：p 有权限控制x ，即应该相信“p 对x 有控制权”这个论断。 警( x ) 或f r e s h ( x ) ：公式x 是新鲜的，除了当前这一轮协议的执行，以前任何时候传 送的消息都不包括x 。这对随机数( n o n c e ) 来说通常是正确的，随机数一般包含一个时间 戳( 血 n e s t a m p ) 或者一个一次性使用的数字。 p 山q ：p 和q 使用共享密钥砭通信，k 是安全的，除了p 、q 或他们相信的主体 之外，其它主体无法获得k 。 - p ：k 是p 的公钥，相应的私钥k 1 绝不会被p 或p 信任的主体之外的主体知道。 p x o ：公式x 是仅仅只有p 和o 或者他们信任的主体知道的秘密，只有p 和o 可以使用x 来证明他们的身份。 z ) k ：表示公式x 用密钥k 加密。 ，：表示x 和公式y 联结；y 是秘密，用来证明发出t x 的人的身份。 2 1 2 推理规则 在研究认证协议时，需要关心的是“过去”和“现在”两个时间段的区别。“现在”时 间段起始于当前这一轮协议的开始执行，在这以前发送的所有消息都被认为是“过去”，认 证协议必须很小心地防止“过去”的消息被当作是“现在”的消息而接收。所有“现在”的 信条在整个协议执行阶段都是稳定的，然而“过去”的信条不能直接带到“现在”。区分了 “过去”和“现在”，逻辑的易操作性大为提高。 还需假定加密算法能够保证每个加密部分不能被改变；如果一条消息包含两个独立的加 密部分，它们被视为位于不同的消息中；没有密钥的主体无法理解加密的消息；密钥无法从 已知密文推导出来；每一密文有足够的冗余使得主体解密后可以验证他是否使用了正确的密 钥。 以下是一些主要的规则： ( - - ) 消息含义规则( m e s s a g e - m e a n i n gr u l e s ) ： 处理如何解释消息，从原始消息中提取可相信的内容，对于共享密钥： 7 贵州大学硕士论文 基于逻辑的电子商务协议分析方法 m 1 p l ；p + 上一q ，p 司 z ) 。 一z o i - x 如果主体p 相信他和主体q 共享密钥k ，并且看到了用k 加密的声明x ，则p 相信o 曾经说过x ，成立的前提是要保证p 能够识别自己发过的消息。 类似的，对公钥和共享秘密有： 叫一上_ q ，p 司 石) xp i q _ 三_ p ，p 司 y p | - q 卜zp j s q 卜z ( - - ) 随机数验证规则( n o n c e - v e r i f i c a t i o nr u l e ) ： 随机数验证规则，表示经检验的消息是新鲜的，因此发送者仍然相信它： 纠- # ( x ) ，列toe - x p i - o l - z p 相信x 仅可能是新近产生的，即x 属于“现在”。而0 现在或者过去曾经说过x ，则 p 相信q 相信x 。 ( 三) 管辖权规则( j u r i s d i c t i o nr u l e s ) ： 如果p 相信q 对x 有管辖权，则p 相信q 对x 的判断： j 1 砗t q 一x ，p | t q i - x x x 砷t q p ，斗 p l z x ( 四) 信念联合规则( b e l i e f - c o n c a w n a t i o nr u l e s ) ： 叫- x ，p 1 ；yp | z o l - ( x ，y ) b 1 ：l 二一 b 2 ：l t 一 p | - ( x ，y )尸i ；o l - x b 3 ：纠- o j - ( x , r ) b 4 ：型竺竖：翌 尸| ，o l - xp i - 工 ( 五) 新鲜性联合规则( f i e s h n e s s c o n c a t e n a t i o nr u l e s ) 如果公式的一部分是新鲜的，则整体也是新鲜的： 翻型兰竖2 尸| ；舟( x ，y ) ( 六) 接收规则( r e c e i v i n gr u l e s ) ： r ，：警px 勉：坐毒筝墼司p 司x 贴：生警戤：韭笔笋鲨粥：可p rpq xpq xp4 x 注意：如果p 司x 且p 司y ，并不能得出p , 4 0 ( ，因为x ，y 不是同时产生的。 8 贵州大学硕士论文 基于逻辑的电子商务协议分析方法 2 1 3b a n 逻辑的优缺点 b a n 逻辑是基于知识和信念的认证协议形式化验证逻辑，它通过认证协议运行过程中 的消息接收和发送，一步一步从初始假设逐渐推导出协议运行所要达到的目的。 b a n 逻辑的优点是简单、直观、便于掌握和使用，这使得它得到广泛的应用。 但是b a n 逻辑本身也存在一些缺陷，主要有： f 1 ) 初始假设 在b a n 逻辑中，初始假设难以确定，而假设对分析结论的正确得出至关重要。由于协 议的敏感性，稍微差别的假设就会将一个不安全的协议分析成一个安全的协议。在b a n 逻 辑中，没有形式化的规则来确定假设，从而无法确认和自动验证假设的正确性和有效性。 c 2 ) 理想化步骤 b a n 逻辑的理想化处理由于它的含糊度而受到大量批评。事实上，在形式逻辑分析方 法中，为了能够运用逻辑推理规则，必须将协议翻译成逻辑公式的集台，即理想化。虽然 b a n 逻辑有理想化工作的通常指导。但理想化步骤自身是非形式化的，这就没有形式化的 方法来探究一个理想化的有效性和正确性。 语义 b a n 逻辑缺少一个定义良好的语义，而这样一个语义集对于逻辑的正确性是一个基本 成份。 ( 4 ) 只能验证认证协议 b a n 逻辑只能验证认证协议，不能有效检测出其他对协议的攻击，同时它也无法检查 出协议的并发运行所带来的各类攻击。而安全协议形式分析方法很大程度上是通过证明协议 不存在任何攻击，来证明安全协议的安全性。b a n 逻辑的使用范围和功能是有限的，例如， 它不适于分析电子商务协议，不能分析使用d h 密钥交换算法进行密钥交换的协议。 2 1 4b a n 逻辑的应用 b a n 逻辑在发现某些协议漏洞方面做的很好，特别是关于新鲜性( f r e s h n e s s ) 方面的 漏洞。b a n 逻辑出来以前，许多对协议的攻击都是对协议新鲜性( f r e s h n e s s ) 的攻击，由 于b a n 逻辑的出现，协议设计中这方面的漏洞已经得到了很好的解决。 b a n 逻辑的核心是“高层次简化”，它只关心那些便于定义，并且足以用于在形式化方 法中推理的部分，而忽略掉其它次要部分。逻辑的精髓就是简明、抽象，并且有较强的推演 能力，b a n 逻辑很好地符合了要求。 “高层次简化”是指省略一些细节，以及合并部分概念。协议设计错误的一个重要因素 是存在旧的消息被重新使用的漏洞，攻击者可以从不安全的网络上拷贝旧的消息来破坏协 议。有两种技术可对抗这个问题，一是采用带时间戳的消息，一是要求协议的执行者响应不 9 贵州文学硕士论文 基于逻辑的电子商务协议分析方法 可预知的质询，二者的实现方法完全不同。 b a n 逻辑把它们合并为一个概念“新鲜”，而且只有当涉及的数值“新鲜”时，才可能 做出某种推断。这是极大的简化，只需考虑涉及的主体而不必担心实现的细节不同，这一高 层次简化并未产生不怠后果。 另一有用的抽象是“所有密钥都安全”，这个论断综合了多个概念，它不关心如何产生 和保管好的密钥。还有“管辖权”规则表达了一类有限的信任，相信某些主体在某些方面的 权威是合理的。这些都消除了很多细节问题，使得分析者能够把重点放在协议本身而不是协 议的具体实现上。 b a n 逻辑公布以后立刻引起了各种各样的争论，很多人抱怨它缺乏明确的语法，有 时不能发现协议的漏洞等等。但必须明白的是，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 ( w i t hs h a r e dk e y s ) 协议，k e r b e r o s 等多个著名的协议，得出了许多有意义的结果，找到了协议中已知的和未知的缺陷，并反映 了非形式化分析的许多结果。b a n 逻辑的成功极大地激发了密码学研究者对安全协议形式 分析的兴趣，并导致许多安全协议形式分析方法的产生。这样b a n 逻辑就确立了协议逻辑 形式化分析研究的地位和作用，并开辟了一个崭新的研究方向。 b a n 逻辑不能发现所有的漏洞，有些漏洞它无能为力( 例如：类型漏洞西p ef l a w ) ， 并且，b a n 逻辑的理想化过程和初始化过程很容易出错，这使得验证过程可能出错。建议 把b a n 逻辑作为协议分析的第一步，来验证在b a n 逻辑框架内能够验证的协议漏洞。但 是需要指出的是它不能够检查出所有的漏洞。 b a n 类逻辑为安全协议第一次提供了一整套形式化分析方法，成功地找到安全协议的 许多缺陷及攻击，这无疑极大地推动了安全协议的分析及设计。 2 1 5b a n 逻辑的扩展 为了使b a n 逻辑可以更加准确的描述证明身份认证协议，我们对b a n 逻辑进行了部 分扩展： 扩展( 。) ：型三呈匕兰：! 竺! ! ：璺! = 兰呈 纠一剑一 z ) k 扩展原因：如果p 收到了 x k 这个消息，并且p 相信k 是p 、q 的会话密钥，那么p 就看见消息x ，同时，p 也有理由相信q 发送过消息 石) x ，但是在b a n 逻辑中没有这个 规则，因此需要添加。 贵州大学硕士论文 基于逻辑的电子商务协议分析方法 扩展( 2 ) ：! 生! ! 兰! ：! ! ! 兰! ! ：! ! 三! = 兰= 皇 p 净群( x ) x ) 扩展原因：如果p 看见 x x 这个消息，并且p 相信k 是p 、0 的会话密钥，那么p 就 看见消息x ，同时，p 也相信消息x 是新鲜的，那么p 应该相信 z ) x 也是新鲜的，同样在 b a n 逻辑中没看这个规则，因此需要添加。 扩展。，：生啦坠堡辈掣生! 丝 叫；q 净p 上一q 扩展原因：如果p 相信0 说过 z k 这个消息，且p 相信 x x 这个消息是新鲜的，则 p 有理由相信0 刚刚说过z k ，同时又由于p 相信k 是p 、q 的会话密钥，那么p 就相信 消息x 是由q 加密发送过来的，因此p 应该相信0 也相信k 是p 、q 的会话密钥，同样在 b a n 逻辑中没有这个规则，因此需要添加。 2 2s v o 逻辑 针对b a n 缺陷和不足，s y v e r s o n 和o o r s c h o t 从另一角度提出了s v o 逻辑。s v o 逻辑 综合了b a n 类逻辑中的前四种逻辑，即g n y 逻辑、a t 逻辑i “、v o 逻辑和b a n 逻辑本 身，而且还提出了一种相对于逻辑来说更为合理的理论模型语义和公理化的推导系统。 2 2 1s v o 逻辑概念 依照b a n 逻辑的惯例，p 、q 和r 表示主体变量，k 表示密钥变量，x 和y 表示公式 变量。a 、b 表示两个普通主体。s 是可信服务器。k m 、k 。、k 等表示具体的共享密钥； k 。、瓦、k 。等表示具体的公开密钥；k 、k i l 、1 0 1 等表示相应的秘密密钥；n 、n b 和 n c 等表示临时值；h ( x 滚示x 的单项散列函数。s v o 逻辑所用的记号与b a n 类逻辑相似， 仍用符号l | ，i 一，l 一，b ，4 ，群，- 分别表示相信( b e l i e v e s ) ，接收到( r e c e i v e d ) 、 发送过( s a i d ) 、刚发送过( s a y s ) 、管辖( c o n t r o l s ) 、看到( s e e s ) 、新鲜( f r e s h ) 与等价( e q u i v a l e n t ) 。 ( 1 ) p | ；石或p b e l i e v e sx 表示主体p 相信公式x 是真的。 ( 2 ) p z 石或p r e c e i v e d x ：表示主体p 接收到了包含x 的消息，即存在某主体q 向p 发送了包含x 的消息。 ( 3 ) 爿x 或p s a i dx 表示主体p 曾经发送过包含x 的消息。 1 1 贵州文学硕士论文基于逻辑的电子商务协议分析方法 ( 4 ) 纠一z 或ps a y s x ：表示主体p 刚发送包含x 的消息。 ( 5 ) p f x 或p c o n t r o l s x ：表示p 享有对x 的管辖权。 ( 6 ) p 司x 或p e s x ：表示主体p 看到x 。 f 7 ) 群( z ) 或f r e s h ( x ) ：表示x 是新鲜的，即x 没有在当前回合前作为某消息的一部 分被发送过，这里x 一般为临时值。 ( 8 ) a - 妒：表示公式a 和公式妒等价。 ( 9 ) p 工：表示主体p 拥有x 。 另外s v 0 逻辑系统中所特有的1 2 个符号及其含义如下： ( 1 ) ：表示主体所收到的、不可识别的消息。 ( 2 ) k ：表示密钥k 对应的解密密钥。 ( 3 ) z k ：表示加密消息 工) k ，p 是发送者滞省略) 。 ( 4 ) 【x k ：表示用密钥k 对消息x 签名后所得到的签名消息，即 曙k = 僻， 僻) ) 。) 。 ( 5 ) x r ：表示 y 是x 和y 的合成消息，可以表示成，1 ) ，p 是发送者( 常 省略1 。 ( 6 ) p k t p ( p ，k ) ：表示k 为主体p 的公开加密密钥，只有p 才能理解应用密钥礤加密