（通信与信息系统专业论文）视频支付协议的设计与分析.pdf

独创性( 或创新性) 声明 本人声明所呈交的论文是本人在导师指导下进行的研究工作及取得 的研究成果。尽我所知，除了文中特别加以标注和致谢中所罗列的内容以 外，论文中不包含其他人已经发表或撰写过的研究成果，也不包含为获得 北京邮电大学或其他教育机构的学位或证书而使用过的材料。与我一同工 作的同志对本研究所做的任何贡献均已在论文中作了明确的说明并表示 了谢意。 申请学位论文与资料若有不实之处，本人承担一切相关责任。 本人弛一玉吼加舨n 】f 本人签名：!日期：二：!：一 关于论文使用授权的说明 学位论文作者完全了解北京邮电大学有关保留和使用学位论文的规 定，即：研究生在校攻读学位期间论文工作的知识产权单位属北京邮电大 学。学校有权保留并向国家有关部门或机构送交论文的复印件和磁盘，允 许学位论文被查阅和借阅：学校可以公布学位论文的全部或部分内容，可 以允许采用影印、缩印或其它复制手段保存、汇编学位论文。( 保密的学 位论文在解密后遵守此规定) 保密论文注释：本学位论文属于保密在一年解密后适用本授权书。非保密论文注释：本 学位论文不属于保密范闱，适_ j 本授权j 体。 本人签名： 2 0f 0 弓f 6 日期： ，、。 翩签名：f 垒竺阻日期：圣笪叟：至：! 生 j 一| 入 视频支付协议的设计与分析 摘要 随着计算机网络的普及及其技术的发展，基于网络的视频应用越 来越普遍。在因特网上视频支付服务越来越重要，这一领域应用数 量的不断增长，使得研究如何在因特网上执行公平的在线交易的方法 越来越受关注。由此，公平交易成为一个中心问题，也就是如何以公 平的方式通过网络交易服务，其中，如何保证交易的公平性是基于该 应用的关键。所谓公平性是指在协议执行的任何阶段，参与协议的任 何一方都不占优势。公平性有两层含义：首先，正确的执行完协议后， 应当满足可追究性，保证双方收到非否认证据，即保证发方收至t j e o r 且收方收n e 0 0 。其次，如果协议异常终止，协议应当保证通信双方 都处于同等地位，任何一方不占任何优势。公平交易就是满足公平性 的安全电子商务交易。 本文首先介绍了一些安全电子商务的公平性的知识，并选取了一 种卿斯汉老师提出的比较独特新颖的新形式化逻辑分析方法，对其进 行了介绍，并以此方法分析了三个典型的安全电子商务协议，对其中 所存在的非公平现象的原因提出了一些解决方法，在此基础上对这三 个协议的不足和缺陷做了分析，并且对其做了改进，然后根据这些问 题以及对它们的解决方案，本文提出了两个新的公平交易协议并对其 公平性用新形式化逻辑分析法做了分析。新协议不仅可以满足公平 性，而且在保密性上也十分出色。文章最后也对新协议存在的不足和 缺陷做了讨论。 法 关键词视频安全性非否认性公平性新形式化逻辑分析方 一j d e s i g na n da n a l y s i so fv i d e 0p a y m e n t p r o t o c o l s a b s t r a c t w i t hr a p i dd e v e l o p m e n to fc o m p u t e rn e t w o r kt e c h n o l o g i e s ，v i d e o a p p l i c a t i o n sb a s e do nn e t w o r kh a sb e e nm o r ea n dm o r ec o m m o n v i d e o p a y m e n ts e r v i c e sh a sb e e nm o r ea n dm o r ei m p o r t a n t ，t h eg r o w so f a p p l i c a t i o n si nt h i sa r e al e a dt oa ne f f e c tt h a tr e s e a r c ho nh o wt oc a r r yf a i r o n li n ee x c h a n g ep r o t o c o l so ni n t e r n e th a sb e e nm o r ea n dm o r ea t t r a c t i v e s o ，f a i re x c h a n g eh a sb e e nak e yp o i n t ，t h a ti s ，h o wt oe x c h a n g es e r v i c e s i naf a i r n e s sw a yo ni n t e r n e t ，a m o n gt h e s e ，h o wt om a k ei n s u r a n c eo ft h e f a i r n e s so ft h ee x c h a n g eb u s i n e s si st h ek e yo ft h eu s e f a i r n e s sm e a n s d u r i n ga n yp a r t so ft h ep r o t o c o lp e r f o r m i n g ，a n yo ft h ei n v o l v e dp a r t i e s t a k e sn oa d v a n t a g e so fa n o t h e r f a i r n e s sh a st w om e a n i n g s ：f i r s t ，w h e n p r o t o c o le n d s ，i ts h o u l ds a t i s f yt h ea c c o u n t a b i l i t y , a n de n s u r et h a tt w o p a r t i e sg e tt h e i rn o n - r e p u d i a t i o ne v i d e n c e s ，n a m e l ye n s u r et h a tt h es e n d e r g e t s t h e e o r ( e v i d e n c e o f r e c e i p t ) a n d t h er e c e i v e r g e t s t h e e o o ( e v i d e n c eo fo r i g i n ) ，t h e n ，i ft h ep r o t o c o le n d e da b n o r m a l l y , t h e p r o t o c o ls h o u l de n s u r et h a tt w oi n v o l v e dp a r t i e si nt h ec o m m u n i c a t i o na t ae q u a l l ys t a t u s ，n e i t h e ro ft h e mt a k e sa d v a n t a g e so fa n o t h e r t h ef a i r e x c h a n g eb u s i n e s s i st h e s e c u r i t ye l e c t r o n i ce x c h a n g eb u s i n e s st h a t s a t i s f i e dt h ef a i r n e s s t h i sp a p e rf i r s ti n t r o d u c e st h ef a i r n e s sk n o w l e d g eo fs o m es e c u r i t y e l e c t r o n i ce x c h a n g eb u s i n e s s ，a n ds e l e c tan e w u n i q u ef o r m a l i z a t i o nl o g i c a n a l y z i n gm e t h o dp r o p o s e db yq i ns i h a n ，a n dp r o p o s es o m es o l u t i o nf o r t h e u n f a i r p h e n o m e n o ne x i s t e d i nt h ep r o t o c o l ，a n db a s e t h e s e ，w e a n a l y z et h es h o r t c o m i n g sa n dl i m i t a t i o n so ft h et h r e ep r o t o c o l sm e n t i o n e d a b o v e ，a n dw ei m p r o v et h e m ，t h e nb a s e dt h e s ep r o b l e m sa n dt h e i r s o l u t i o n s ，t h i sp a p e rp r o p o s e dt w on e wf a i re x c h a n g eb u s i n e s sp r o t o c o l a n da n a l y z e si tw i t ht h en e wu n i q u ef o r m a l i z a t i o nl o g i ca n a l y z i n gm e t h o d 入 目录 第一章绪论1 1 1 研究背景1 1 2 研究目的2 1 3 论文主要工作及安排3 第二章视频支付概述及协议设计相关内容4 2 1 几个重要概念4 2 1 1 对称加密体制4 2 1 2 公钥加密体制及公钥加密技术5 2 2 对称加密体制及公钥加密体制的比较6 2 2 1 公平性7 2 2 2 不可否认性7 2 2 3 可追究性7 2 3 公平交易协议与传统安全协议的区别及其设计原则8 2 4 形式化逻辑分析方法9 2 5 新形式化逻辑分析方法1 0 第三章w e b 视频下p p v 协议的分析与改进1 4 3 1w e b 视频下p p v 协议1 4 3 1 1w e b 视频下p p v 协议的概念1 4 3 1 2w e b 视频下p p v 协议的计费模型1 4 3 2w e b 视频下p p v 协议的分析1 7 3 3w e b 视频下p p v 协议的改进1 8 第四章c m p i 协议的分析与优化2 0 4 1c m p i 协议2 0 4 2c m p i 协议的分析2 0 4 3c m p i 协议的优化2 2 第五章w a n gg u i l i n 通用透明o f f l i n et t p 公平非否认协议的分析与改进2 4 5 1w a n gg u i l i n 的通用的透明o f f l i n et t p 公平非否认协议2 4 5 1 1 协议介绍2 4 5 1 2 协议内容2 5 5 2w a n gg u i l i n 的通用的透明o f f l i n et t p 公平非否认协议的分析2 8 5 3w a n gg u i l i n 的通用的透明o f f l i n et t p 公平非否认协议的改进3 8 第六章两个公平交易协议的设计4 l 6 1 移动通信环境下p p v 协议的支付模型4 1 6 2 视频传输公平非否认交易协议4 6 第七章两个公平交易协议的分析5 0 7 1 移动通信环境下p p v 协议的支付协议分析5 0 7 2 视频传输公平非否认交易协议5 1 第八章总结与展望6 6 参考文献6 7 致谢7 1 攻读学位期间发表学术论文目录7 2 北京邮电人学硕士学位论文第1 页共7 2 页 1 1 研究背景 第一章绪论 随着移动通信技术和网络技术的不断发展，通过移动网络提供的视频服务越 来越多。而视频支付协议的研究也成为了现行研究的热点之一，而视频支付协议 较其他支付协议来说有其独特的要求。 针对传统的这些独特的要求，许多学者相继提出了一系列的安全协议设计原 则和要求，试图从协议设计的开始就避免协议可能产生的缺陷，其中一些设计原 则同样适用于公平交易协议。但是由于公平交易协议的运行环境和应用环境与传 统的安全协议有所不同，而且它比传统的安全协议有着更复杂的性质。因此， 在设计公平交易协议时所需要考虑的问题也不完全相同l 。 视频支付，顾名思义就是为视频服务支付费用，如视频点播，视频教学等， 目前来说，现有的协议大都时要求用户预付费的，但是如果因为服务商或者网络 的原因，用户未能享受到良好的服务或者服务被另外黑客窃取，对用户来说就只 能是“损失”，这是一个不对等的交易1 2 j 。当然本身造成的原因，是由于大部分协 议都是服务提供方设计运营的，因此为了保证他们本身的利益，通常会要求用户 做出妥协，而用户的权益就得不到保耐3 1 。 在传统的移动通信环境中( 如2 g ) ，服务接入和服务提供是在用户和电信运 营商签署入网协议时由电信运营商捆绑提供的。电信运营商既提供了电信通信网 络，又是应用服务提供者1 4 j 。2 g 系统采用这样一种垂直的设计原则，它的很多 设计都是为了优化以提供更好的语音服务。这种垂直设计原则就使得如果需要增 加一种新的非语音服务，所耗费的代价将是非常昂贵的。所以在第三代移动电信 系统( 3 g ) 中，比如u m t s ( u n i v e r s a lm o b i l et e l e c o m m u n i c a t i o n ss y s t e m ，通用移动 通信系统) ，就采取了一种水平设计原则，它将接入和通信服务部分及内容与应 用服务部分分离1 5 j 。电信运营商提供接入和通信服务部分，独立的应用服务提供 商和内容提供商可以将服务建立在电信运营商提供的一个平台上，而无须去构建 自己的电信网络，这大大降低了其进入门槛，而使得增值服务提供商( v a s p ) 蓬 勃发展。电信运营商和v a s p 之间业务互相影响牵制很大，所以为这些v a s p 视频支付协议的设计与分析 北京邮电人学硕f ：学位论文第2 页共7 2 页 提供一种怎样的计费模式，就显得非常重要。这也正是移动电子支付所要解决的 问题【6 1 。 电子支付系统的公平性和安全性是电子商务能否得到认可和发展的关键因 素。只有在公平可靠的电子支付系统的基础之上，才能使网上电子商务活动更具 活力。许多密码学者已经提出了大量的电子现金机制，其中主要包括c h a u m 和 p e d e r s e n 的机制l 、g r a m e r 和p e d e r s e n 的机制1 8 j 等。这些机制和其它一些电子现 金机制一样，都包括3 个子协议：取款协议，支付协议和存储协议。其思想为： 在取款协议中，用户可以提取电子现金；在支付协议中，用户将电子现金发送给 商家，商家验证其有效性后送回付款说明；在存款协议中，商家将付款说明和电 子现金发送给银行，银行验证其有效性后，将电子现金存入商家的账户。虽然利 用密码技术提供了很强的安全性，但它们还存在一些不公平性，例如：在支付子 协议中，商家可以先取款，但不送给用户付款说明，这就对用户不公平；假设银 行要求商家必须有用户签字的付款说明才可取款，如果用户收到付款说明后却不 返回对该付款说明的签字，这就对商家不公平而另一种协议，称为小额电子支付 协议，如本文的p p v 协议【9 1 。它的思想是将要支付的现金分成若干单位，用户根 据收到的信息商品逐个单位释放支付信息，将用户和商家的风险都降为一个可容 忍的单位。但是，任何一方被非法者利用，都会给自己造成可观的累加损失1 1 0 l 。 可见，这些协议都存在“谁先提供信息服务，谁就要比对方冒更大的风险”的问题。 这个问题不解决，就不能保证公平的交易，势必会影响电子商务应用的发展。 1 2 研究目的 移动电子支付与互联网上的电子支付相比，既有相同的地方，也有相异之处。 随着3 g 的发展，增值服务提供商大量出现。2 g 和3 g 的一个显著区别就是3 g 中这 些巨量而且数目一直增加的v a s p 的存在，电信运营商和v a s p 之间业务互相影 响牵制很大。在移动电子支付中，三方角色通常是移动用户、v a s p 和电信运营 商，其中电信运营商一般扮演可信第三方的角色，而通常的交易一般发生在移动 用户和v a s p 之间【1 1 l 。例如本文中重点分析得移动终端视频服务，这在3 g 系统中 将是一个炙手可热的业务，但是如何实现移动用户与v a s p 之问的合理计费却一 直没有比较完美的解决方法i l 引。针对这一问题，本文借鉴了互联网上的即看即 付( p a y p e r v i e w ，p p v ) 协议的思路，大胆对其进行了改进，使之适应移动终 端的低计算能力、低存储能力的需求，设计了一个适应移动终端的p p v 协议。该 协议是一个能够实现移动终端安全计费的p p v 协议【1 3 l 。通过分析，该协议不仅从 视频芰付协议的设计与分析 - 、 北京邮电大学硕l 学位论文第3 页共7 2 页 公共参数的存储空间需求和用户端计算负荷上是轻量级的，而且在解决p p v 支付 争端上是有效的。该协议可以保护用户不被错误收费，同时提供防止用户抵赖的 合法证据1 1 4 j 。 因此，我们需要设计一些新的协议，在不伤害服务商的基础上保证用户的利 益，并且做到有效可行。 总之，随着移动增值业务的大量出现，不同的业务可能需要不同的支付机制， 对移动电子支付的研究还有许多工作没有做。我的毕业设计主要针对移动终端的 视频服务的支付做了一定的研究，论文的组织结构如下所述。 1 3 论文主要工作及安排 本文以视频支付环境为基础，分析了3 个著名协议：w e b 视频下p p v 协议， c m p l 协议和w a n gg u i l i n 通用透明o f f - l i n et r p 公平非否认协议，并对他们存 在的不公平性做出了改进，之后在之前工作的基础上，本文提出了2 个新的协议： 移动通信环境下p p v 协议的支付协议和视频传输公平非否认交易协议，并对他 们的公平性进行了分析，以2 者为题的2 篇文章已经分别被e i 检索。 ；： 论文第一章绪论，阐述了论文依据的现实和课题背景，指出了论文研究 的重要意义，引出了本文的研究目的和内容，设计了论文研究的结构和技术路线。 第二章简单介绍了一些相关知识和内容。 第三，四，五章分别对w 曲视频下p p v 协议，c m p l 协议和w a n gg u i l i n 通用透明o f f - l i n e1 曙公平非否认协议进行了分析并对其协议过程中产生的不公 平性提出改进意见。 第六章提出了两个新的基于视频支付环境下的协议。 第七章对两个新协议的公平性进行了分析。 视频支付协议的设计与分析 北京邮电人学硕上学位论文第4 页共7 2 页 第二章视频支付概述及协议设计相关内容 2 1 几个重要概念 2 1 1 对称加密体制 密码学中，常见的2 种体制：一种是对称加密体制，也叫单钥加密体制，另外 一种是非对称密码体制，也叫公钥密码体制1 1 引。本节我们先介绍一下对称加密 体制( 单钥加密体制) ，下一节我们介绍一下公钥加密体制，之后介绍一下2 者的 区别。 对称加密体制指如果一个加密系统的加密密钥和解密密钥相同，或者虽然不 相同但是可由其中的任意一个很容易的推导出另一个，即密钥是双方共享的，则 该系统所采用的就是对称加密体制，形象的说就是一把钥匙开一把锁。我们所知 道的传统密码系统就是以此体制作为加密系统的1 1 6 1 。 图2 1 给出了一般对称加密体制下的信息流程图： 图2 1 对称加密体制下的信息流程图 视频支付协i 义的设计与分析 户、 北京邮电大学硕十学位论文第5 页共7 2 页 图中，m 表示明文；c 表示密文；e 表示加密算法；d 表示解密算法；k 表示密 钥；万表示密码分析员对的分析或猜测；i 表示密码分析员进行密码分析时掌握的 其他相关信息。 很明显，图中安全信道是否真的安全成了对称加密体制最难以解决的问题， 因为它关系到密钥k 是否会被窃听，篡改或滥用。 从图中看出，对称加密是基于共同保守秘密来实现的。采用对称加密技术的 双方必须要保证采用的是相同的密钥，因此要保证彼此密钥的交换安全可靠，同 时还要设定防治密钥泄密和更改密钥的程序。对称密钥的管理和分发工作是意见 具有潜在危险和繁琐的过程，可通过公开密钥的加密技术实现对对称密钥的管 理，使相应的管理变得安全，同时还解决了对称密钥体制中存在的管理，运输的 可靠性问题和鉴别问题。在此就不再赘述了1 1 7 l 。 2 1 2 公钥加密体制及公钥加密技术 1 9 7 6 年，d i f f i e 和h e l l m a n 首次提出公开密钥加密体制，这在密码学的发展史 上具有里程碑的意义。并由r i v e s t ，s h a m i r e 和a d l e m a n 提出了第一个比较完善的 公钥加密体制算法，即著名的r s a 算法。后来陆续出现了e i g a m a l 公钥密码体制， m c e l i e c e 公钥密码算法和椭圆曲线公钥密码( e c c ) 体制等1 1 8 l 。由于本文中只涉及 到公钥加密技术的基本概念，所以仅对这一部分做一些简略的介绍： 图2 2 给出了公开密钥加密体制下的信息流程图： 图2 2 公开密钥密码系统信息流程图 视频支付协议的设计与分析 ，岛) 北京邮电人学硕。i ：学位论文 第6 页共7 2 页 图中，m 表示明文；c 表示密文；e 表示加密算法；d 表示解密算法；足，k ，k 表 示密钥；万表示密码分析员对的分析或猜测；，表示密码分析员进行密码分析时掌 握的其他相关信息。 公钥密码体制指一个加密系统的加密密钥和解密密钥是不一样的，或者说不 能由一个推导出一个。其中一个成为公钥用于加密，是公开的，另一个成为私钥 用于解密，是保密的。其中由公钥计算私钥是难解的，即所谓的不能由一个推导 出另一个。 从定义上看这一体制的最大特点是采用2 个密钥分别用于加密和解密。一个 公丌的作为机密密钥；另一个为用户专用，作为解密密钥，通信双方无需事先交 换密钥就可以进行保密通信了。这就解决了对称密码体制中的密钥管理难题，满 足了开放系统的需求【1 9 1 。 2 2 对称加密体制及公钥加密体制的比较 由上面的分析以及给出的图2 1 图2 2 中可以看出： 由于发送信道往往时不可靠的，所以在对称密码系统中，必须用不同于发送 信息的另外一个安全信道来分发密钥。但是公开密钥密码系统不需要分发密钥的 额外信道。可以公开加密密钥，这样做无损于整个系统的保密性，需要保密的仅 仅时解密密钥【删。 无论是对称加密体制还是公钥加密体制，都要面对密钥保护的问题。一个密 钥系统是否是完善的，有时候取决于能否正常的保护密钥。对称加密体制的致命 弱点就是密钥管理非常困难，因此再很难在实际应用中得到广泛应用。公钥加密 体制的密钥管理相对就简单的多了，因为对于发放来说，只要记住收方的公钥就 可以进行j 下常的信息加密以及对收方发送信息的签名验证。对称加密，就是密钥 是相同的，加密和解密都是同一个密钥；而非对称加密，就是加密的密钥和解密 的密钥不相同，即有私钥和公钥之分1 2 。公钥是公开分发的，而私钥只有自己 拥有。安全的电子邮件定义比较广泛，其中较为常用的是加密与签名。简单的说， 加密是指，用对方的公钥加密，这样就只有对方用他的私钥才能解密，实现加密 的目的；而签名是指，用自己的私钥加密，接受者用公钥解密，达到“签名”的目 的，表示这封邮件是你发的。 视频支付协议的设计与分析 北京邮电大学硕一l ：学位论文 第7 页共7 2 页 2 2 1 公平性 电子商务交易满足安全协议的所有基本属性，如保密性、安全性、认证性、 完整性之外，还必须具有非否认性和公平性两个重要属性。这是因为关于交易的 争论己成为一个普遍的问题，为了解决这种争论需要使用不可否认性。同时，协 议的公平性更是必不可少的。因此，交易中两个重要的性质应该是交换的公平性 和非否认性1 2 2 j 。 所谓公平性是指在协议执行的任何阶段，参与协议的任何一方都不占优势， 并有强公平性与弱公平性的定义之分。( 对公平性的定义可以稍微介绍的详细一 点，另外，对强公平、弱公平的定义，也可以简单介绍一下，那篇博士论文罩有) 对公平性形式化的分析也得到了广泛研究。 2 2 2 不可否认性 不可否认性是电子商务协议的一个重要性质。其目的在于通过通信主体提供 对方参与协议交换的证据来保证其合法利益不受侵害，即协议主体必须对自己的 合法行为负责，不能也无法事后否认。不可否认协议主体的目的在于收集证据， 以便事后能够向仲裁方证明对方主体的确发送或接收了消息1 2 3 1 。证据一般是以 签名消息的形式出现的，从而将消息与消息的发送方和接受方进行绑定。非否认 服务的两个基本目标是提供发送方和接收方非否认依据，即发送方非否认依据 ( e o o ，e v i d e n c eo fo r i g i n ) 和接收方非否认依据( e o r ，e v i d e n c eo fr e c e i p t ) 。 在不可否认协议中，主体目标互不相同。而要达成不可否认这一目标，协议 必须具有证据的正确性及交易的公平性两个特点。在不可否认性之中还可引申出 电子商务一些其他的相关性质，如适时中止性、公平性、可追究性等。 2 2 3 可追究性 可追究性是指电子商务交易发生纠纷时，可通过历史信息获取交易当时的情 况，从而获得解决交易纠纷的能力。另外，还有一些安全属性易于理解，如隐私 性。对于商户以外的参与者，订单信息( 支付金额和产品详细信息) 等应被屏蔽。 设计安全电子商务协议的目标就是保证这些电子商务安全属性在协议执行完毕 时能够得以实现，换言之，评估一个安全电子商务协议是否安全，就是检查其所 欲达到的安全属性是否遭到攻击者的破坏【2 4 l 。 视频支付协议的设计与分析 北京邮电大学硕十学位论文第8 页共7 2 页 2 3 公平交易协议与传统安全协议的区别及其设计原则 公平交易协议属于安全协议的一种，但由于公平交换协议和传统的安全协议 在设计目标上的不同，它们所要满足的安全属性、试图预防的攻击类型和运行环 境又有很大不同，主要表现在以下几个方面1 2 5 1 ： 通信信道要求不同 在传统安全协议中，通常假设协议在不安全的信道上进行，攻击者完全控制 通信，所有在信道上传输的消息都有可能被拦截、篡改、重放。而在公平交换协 议中，需要对信道有更高的要求。1 9 9 9 年，p a g n i n a 和g a r t n e r i i e g q 了若没有可信 第三方( t r u s t e dt h i r dp a r t y ，t t p ) 的存在，就不可能有真币公平的公平交换协议， 如果协议只在不可靠信道上进行，也不可能建立真正的公平交换协测2 6 。否则， 在不可靠信道上发往r r p 的消息可能丢失，这就等同于没有t r p 。 安全目标和攻击者类型不同 传统安全协议中，参与者都诚实，想要通过合作实现共同的目标，通常假设 所有的攻击者具有同样的能力。在公平交换协议中，每一个参与者都知道其他实 体可能不诚实，参与协议的各方没有共同的目标。分析公平交换协议时，除了考 虑外部攻击者以外，还必须考虑协议合法参与者是恶意的情况，恶意参与者可以 独自进行欺骗( 此时他等同于其他攻击者) ，也可以与其他攻击者合谋1 2 7 1 。 协议构成不同 在传统的安全协议中，一般不存在子协议。而在公平交换协议中，往往存在 多个子协议，在协议设计时，任何情况下都能保证执行过程的唯一性尤为重要。 由上述的不同特点，原有的安全协议的设计原则不足以保证设计出更安全的公平 交换协议，必须根据公平交换协议的特点，给出相应的公平交换协议的设计原则。 公平交换协议的设计原则 根据给出的公平交换协议与传统的安全协议的区别，下面给出公平交换协议 的设计应注意的一些原则。 原则1 ：明确公平交换协议要求的通信信道质量 公平交换协议对通信信道的要求比传统的安全协议对信道的要求高。没有可 信第三方的存在，就不可能有真正公平的公平交换协议( 虽然也存在不包括t r p 的公平交换协议，如逐步交换的公平交换协议，但该类协议是建立在协议双方有 相同计算能力的假设基础上的，这种假设常常是不成立的) 。如果协议只在不可 靠信道上进行，也不可能建立真正的公平交换协议。否则，在不可靠信道上 发往t r p 的消息可能丢失，这就等同于没有t t p 。因此，在设计公平交换协议时， 视频支付协议的设计与分析 ，l 北京邮电人学硕：l 学位论文 第9 页共7 2 页 需要明确说明该协议所要求的信道质量。 原贝j j 2 ：明确公平交换协议中可能的攻击者能力 公平交换协议所面临的攻击类型与传统的安全协议所面临的攻击类型有所 不同。在设计公平交换协议时，必须明确该协议所需预防的攻击者模型并对可能 的攻击做出判断。在传统的安全协议中，通常假设协议在敌手可以完全控制的网 络环境中运行，敌手可以进行读取、更改、删除消息。而诚实参与者互相信任， 他们想要通过合作获得共同目标。在公平交换协议中，由第2 节中的( 1 ) 知道，在 有t r p 参与的协议中，攻击者不能完全控制信道。因此，在设计公平交换协议 时，必须根据具体的情况，对所预防的攻击者模型进行适当的修改。此外，在设 计公平交换协议时，不能假设参与协议的各方是相互信任的，因为在公平交换协 议中，参与协议的各方没有共同的利益和目标，每一个参与者都知道其他实体可 能不诚实，在某种意义上，参与者总是在和敌手运行协议。因此，除了考虑外部 入侵者以外，恶意的一方可以是参与协议的实体的其中一个( 在多方协议中，可 能是其中的几个) 。传统的安全协议必须对外部入侵者是安全的，公平交换协议 甚至对恶意的参与者也是安全的。设计公平交换协议时，必须考虑一个或多个协孵 议参与者是恶意的情况。 公平交换协议的攻击类型与传统的安全协议的攻击类型有所差别，例如，传 统的安全协议所要求的秘密性和认证性，在有些公平交换协议中是不必要的，公 平交换协议中单纯的角色欺骗不构成有效攻击，电子合同协议中不需对合同的内 容进行保密等。公平交换协议的设计中，应根据实际情况，尽可能给出所设计协 议要预防的攻击，虽然事先知道所有可能的攻击是不可能的，但对于常见的、已 ； 知的可能攻击，在协议设计时都应该避列2 9 l 。 2 4 形式化逻辑分析方法 通常，人们都是对安全协议进行理论分析，但这种分析只能对已知的缺陷进 行分析，而对于协议中前潜在的漏洞或不足，则要通过严密的形式化逻辑分析来 解决。形式化逻辑分析方法有很多种，而且很多学者也在不断的进行研究之中。 由于本文主要是利用卿斯汉老师改进的k a i l a r 逻辑分析方法对一些协议进行了分 析，下面主要对这一改进的k a i l a r 逻辑分析方法做一介绍。 原k a i l a r 逻辑分析方法可参见相关文酬矧，这里直接介绍一下k a i l a r 逻辑的3 个缺陷： ( 1 ) k a i l a r 逻辑不能分析安全电子商务协议的一个重要安全性质一公平性； ( 2 ) 在应用k a i l a r 逻辑进行逻辑推理前，初始假设的设定过程是非形式化的， 视频支付协议的设计与分析 北京邮电大学硕_ f 学位论文第l o 页共7 2 页 不恰当的引入初始假设可能会导致协议分析失败； ( 3 ) k a i l a r 逻辑在解释和分析协议语句时，只能解释和分析那些签名的明文消 息，没有处理签名的加密消息的安全机制，限制了协议分析的范围。 基于我们所研究的是公平交易协议，其公平性是最为重要的属性，因此我们 不能利用k a i l a r 逻辑来分析和解决问题。而改进后的k a i l a r 逻辑分析方法可以同时 用于分析安全电子商务协议的可追究性和公平性。在改进后的形式化逻辑分析方 法中，每个主题在协议运行前拥有一个初时拥有集合，它由一些公式组成。随着 协议分析的进行，主体拥有的集合不断扩大，到协议运行结束时，每个主体拥有 一个最终拥有集合。 协议的可追究性是通过发送方非否认和接收方非否认两个基本目标实现的。 在新的形式化分析方法中，通过验证e o o 属于接收方的最终拥有集合，并且e o r 属于发送方的最终拥有集合是否成立，验证协议的可追究性。 协议的公平性包含两层含义：首先，协议正常完成后，保证发送方收到e o r 且接受方收至i j e o o ；其次，如果协议异常终止，协议应保证通信双方都处于同等 地位，任何一方都不占优势。或者等价的说，消息接收方接收至j j e o o 当且仅当消 息发送方收到e o r 。在新的形式化分析方法中，当协议在任何一步异常终止时， 验证协议是否满足公平性的方法时e o o 属于接收方拥有集合是否当且仅当e o r 属于发送方的拥有集合。 安全电子商务协议在一个分布式环境中运行，这个环境包含3 类主体：发送方 a ，接收方b 和可信第三方t r p ，其中t r p 可以时一个或多个主体。在这个环境中， a 和b 之间可以直接通信或者通过t t p 进行转发。环境是协议运行的具体环境的 抽象，它只包含协议涉及者和协议分析者考虑的因素。在这里环境包含2 方面的 因素：主体是否诚实和通信信道是否可靠。在这里假设a 和b 是不诚实的，t t p 是 诚实的。通信信道是可靠的也可以是不可靠的。 至于详细的改进的k a i l a r 逻辑分析方法可参见文献1 3 。 2 5 新形式化逻辑分析方法 新形式化逻辑分析方法是在著名的k a i l a r 逻辑的基础上改进而来的，我们直 接分析k a i l a r 逻辑的3 个缺陷- ( 1 ) k a i l a r 逻辑不能分析安全电子商务协议的一个重要安全性质一公平性； ( 2 ) 在应用k a i l a r 逻辑进行逻辑推理前，初时假设的设定过程时非形式化的， 不前当的引入初时假设可能会导致协议分析失败： ( 3 ) k a i l a r 逻辑在解释和分析协议语句时，只能解释和分析那些签名的明文消 视频支付协议的设计与分析 北京邮电大学硕七学位论文 第1 1 页共7 2 页 息，没有处理签名的加密消息的安全机制，限制了协议分析的范围。 基于我们所研究的时公平交易协议，其公平性是最为重要的属性，因此我们 不能利用k a i l a r 逻辑来分析和解决问题。下面我们介绍一种新的形式化逻辑分析 方法，它可以同时用于分析安全电子商务协议的可追究性和公平性。在新的形式 化逻辑分析方法中，每个主题在协议运行前拥有一个初时拥有集合，它由一些公 式组成。随着协议分析的进行，主体拥有的集合不断扩大，到协议运行结束时， 每个主体拥有一个最终拥有集合。 协议的可追究性是通过发送方非否认和接收方非否认两个基本目标实现的。 在新的形式化分析方法中，通过验证e o o 属于接收方的最终拥有集合，并且e o r 属于发送方的最终拥有集合是否成立，验证协议的可追究性。 协议的公平性包含两层含义：首先，协议正常完成后，保证发送方收至i j e o r 且接受访收至u e o o ；其次，如果协议异常终止，协议应保证通信双方都处于同等 地位，任何一方都不占优势。或者等价的说，消息接收方接收至l j e 0 0 当且仅当消 息发送方收至u e o r 。在新的形式化分析方法中，当协议在任何一步异常终止时， 验证协议是否满足公平性的方法时e o o 属于接收方拥有集合是否当且仅当e o r 属于发送方的拥有集合。 安全电子商务协议在一个分布式环境中运行，这个环境包含3 类主体：发送方 a ，接收方b 和可信第三方t t p ，其中t r p 可以时一个或多个主体。在这个环境中， a 和b 之间可以直接通信或者通过订p 进行转发。环境是协议运行的具体环境的 抽象，它只包含协议涉及者和协议分析者考虑的因烈3 甜。在这里环境包含2 方面 的因素：主体是否诚实和通信信道是否可靠。在这里假设a 和b 是不诚实的，r r p 是诚实的。通信信道是可靠的也可以是不可靠的。 假设协议由t l 条协议语句组成。在协议开始前，主体p 的初始拥有集合为o ! ， 它包含环境分配给p 的密钥和p 能证明的共识。当协议的第i ( 1 s i s 以) 条语句执行完 毕后，主体p 的拥有集合为d ：，当协议经过，l 步运行终止时，用o 。记p 的最终拥 有集合。显然， o 。一d ：。 d ： 按如下规则递归生成： ( 1 ) 如果协议的第f 条语句为p q ：m ，那么我们不妨设 m = ( m k ，似。k 。) ，其中 m k ， m 。) 足诺哕1 ，k 够1 ，k 。畴1 ，即m 由 若干个不在畴1 中出现的加密消息如 m k ， m ) 足。( 其中，它们的加密密钥k ， 视频支付协议的设计与分析 北京邮电大学硕 ：学位论文 第1 2 页共7 2 页 k 。在够1 中出现) 和一些其他消息复合而成，那么q = 够1u m ，m 。，肘。 。 ( 2 ) 如果协议的第f 条语句为q t t p p ：m 或p 付t t p ：m 那么 q 一哕1u ( 3 ) 如果协议的第i 条语句为q 一刀甲：m ，或者乃p 呻q ：m ，或者 q 付t t p ：m 那么嘭= 畴1 ( 4 ) 如果( 石，y ) e q ，那么x e 啡且y q 。反之，若z q 且y q ，则 ( x ，y ) e q 。 ( 5 ) 如果 x k 啡且k e 啡i ，那么x e 啡。反之，若x q 且k e q ，则 x ) 置啡。 可追究性值参与通信的双方均r j , - , l 句第三方证明对方对某个消息负责。假设发 送方a 通过环境将消息或电子货物m 发送给接收方b ，可追究性是这样实现的： ( 1 ) 发方非否认是由a 将e 0 0 通过环境发送给b 实现的。e o o 是协议设计者定 义的一个公式，它包含使a 不可抵赖的证据。这个公式由a 产生，或者由a 和t r p 共同产生，通过环境最终发送给b ，并且由e o o e q 可以推导出口 - 4 呻朋。 ( 2 ) 收方非否认是由b 将e o r 通过环境发送给a 实现的。e o r 是协议设计者定 义的一个公式，它包含使b 不可抵赖的证据。这个公式由b 产生，或者l h a 和r r p 共同产生，通过环境最终发送给a ，并且由e o r e d 4 可以推导出a b 呻朋。 协议语句的第一个重要属性是可中断性。如果一个协议语句受环境影响，可 能未被执行或未被正确执行，那么这条语句是可中断的。按照可中断性，协议语 句分为以下3 类： ( 1 ) 协议语句州b 呻b a t t p ：m 是可中断的因为a 或b 是不诚实的，他可能 因对自己有利而不执行这条协议语句。 ( 2 ) 在信道可靠的情况下，协议语句刀甲呻州b ：肘是不可中断的。因为t r p 是诚实的，他肯定会执行这条协议语句，t r p 发送的消息会被a , - 或b 正确的接收。 在信道不可靠的情况下，t t p 发送的消息由可能丢失，第2 类协议语句是可中断 的。 ( 3 ) 协议语句纠bh 刀甲：m 在信道可靠或信道不可靠的条件下均是不可中 视频支付协议的设计与分析 厂 北京邮电大学硕十学位论文 第1 3 页共7 2 页 断的。因为1 r p 是诚实的，他使m 可被f r p 操作得到。a 或b 可以通过这一操作 获得对自己有用的消息，a 或b 不会放弃这一操作。即使在信道不可靠的条件下， a 或b 仍可以通过多次f t p 操作取得m 。 因此，协议的公平性是指协议除了满足可追究性外，还满足以下条件：协议 在任何第f 条语句中断时，e 0 0 磷。1 当且仅当e o r e 谚。 协议在哪些步可能异常终止，取决于具体协议的运行环境7 1 。 视频支付协议的设计与分析 北京邮电人学硕1 ：学位论文第1 4 页共7 2 页 第三章w e b 视频下p p v 协议的分析与改进 3 1w e b 视频下p p v 协议 3 1 1w e b 视频下p p v 协议的概念 p p v ( p a y p e r v i e w ) 协议，是一种即看即付协议，在这种协议下，用户只 需为他们收看的节目付费。p p v 协议的思想是将要支付的现金分成若干单位， 用户根据收到的信息商品逐个单位释放支付信息，将用户和商家的风险都降为一 个可容忍的单位。 3 1 2w e b 视频下p p v 协议的计费模型 图3 1p p v 服务模型 视频支付协议的设计与分析 北京邮电大学硕卜学位论文第1 5 页共7 2 页 p p v 服务系统主要涉及服务提供者s 、用户c 和经纪者b 。服务提供者s 和用户c 在经纪者b 处都维持一帐户，这些帐户和常规的银行帐户相联系，当 用户收看了收费节目时，他的帐户将被扣除适当的量，同时s 的帐户将存入适当 的量。用户的帐户可以从银行补充资金，同时s 帐户里的奖金可以存入银行。 服务提供者在网上公布