（计算机软件与理论专业论文）基于模型检测的电子商务协议形式化验证方法研究.pdf

郑州大学硕士学位论文 摘要 安全的电子商务协议是保证电子商务活动正常开展的基础。一个貌似安全的 协议往往存存安全上的漏洞。模型检测是一种常见的形式化分析方法，在验证电 子商务协议时，它的逻辑推理能力比较弱。此外，随着网络的大规模应用，需要 分析安全的电子商务协议存不可靠环境下并发运行时是否仍然保持安全性。本文 主要结果如下： 1 基于消息转换的验证模型。定义了一个扩展的有限状态自动机、一些新 的逻辑转换规则，并给出了详细的分析步骤。用扩展的f s a 根据消息为协议建模， 不仅可动态显示各个参与者并发执行协议的过程，而且增强了自动机的逻辑分析 能力。利用该方法分析匿名原子交易协议，可知当交易主体诚实时，该协议满足 可追究性、公平性、原子性等；对协议模型抽象后，借助模型检测工具u p p a a l 验证了协议的活性。 2 基于动作转换的验证模型。定义了一个信任矩阵和一个动作集合，并将 它们和逻辑规则一起引入有限状态自动机为协议参与者建模。信任矩阵形式化了 协议参与者之间的信任关系，从而无需初始化假设；动作集合将加密、签名等动 作明确地表示出来，从而在规范协议时无需理想化过程。利用该方法分析匿名原 子交易协议，可知当交易主体彳i 诚实时，该协议不满足可追究性；通过搜索参与 者进程的模型，找到了性质不满足的原因，从而对原协议进行了修改；对修改后 的协议进一步分析，发现其满足可追究性、公平性、原子性等。 3 用模型检测方法分析了不可靠环境下协议的安全性质。验证结果表明， 一个安全的电子商务协议在不可靠环境下由多对参与者同时执行时，有可能不再 满足安全性质；当安全性质违背时，可借助模型检测工具( 本文用模型检测工具 u p 脚a l ) 生成的消息序列对协议进行改进。 关键词：电子商务协议，模型检测，k a i l a r 逻辑，多轮执行，小可靠环境，u p 队a l 塑! ! ! 查兰堡主堂竺丝苎 a b s t r a c t t h es e c l l r ee c o m m e r c ep r o t o c o l sa r ef h n d a m e n t a lt oe - c o m m e r c e b u t ，b e c a u s eo f s u b t l e t i e si n v o l v e di nt h e i rd e s i 弘，m a n yo fm e mh a v eb e e ns h o w nt oh a v en a w s t o a v o i dt h e s es u b t l em i s c o n c 印t i o n s ，s e v e m lf o h n a lm e t h o d sf o ra i l a l y z i n ge c o m m e r c e 口r o t o c o l sh a v eb e e nd e v i s e d m o d e lc h e c k i n gh a sb e e np r o v e dt ob ev e r yu s e 砌f o r t h i sp u r p o s e ，a l t h o u 曲i th a sap o o ra b i l i t yo fi l l “o n m e a n w h i l e ，w i t ht h eg m w i n g p o p u l a r i t yo f t h ei n t e m e t ，“i sn e c e s s a r yt oa n a l y z em u l t i p l en l n so f 也ep m t o c o l i n t h ep r e s e n c eo fs i t co rc o m m u n i c a t i o nf a i l u r e t h i sp 叩e r sm a i nc o n t r i b u t i o n i n c h l c l e s ： 1 p r e s e n t i n gaf r a m e w o r kb a s e do nt h ep r o t o c o lm e s s a g ee x c h a n g e s w ed e f i n ea n e x t e n d e df i n i t es t a t ea u t o m a t o n ，s o m en e w1 0 9 i cm l e sa n das e to fa n a l y s i ss t e p s m o d e l i n gt h ep r o t o c o lb ys u c haf s a ，w ec a nn o to n l yd i s p l a yd y n 锄i c a l l yh o w e a c h p a r t i c i p a n te x e c u t e st h ep r o t o c o lc o c u r r e n t l y ，b u ti m p r o v et h ea b i l i t yo fi l l a t i o no f t h ef s a ，w h i c he n a b l eu st oa n a l y z es i g n a t u r ea n dc i p h e r t e x ti nt h ee c o m m e r c e p m t o c o l s w et a k ea n o n ”n o u sa t o m i ct r a n s a c t i o n sp r o t o c o la sa ne x a m p l e ，a n df i n d s u c hp m p e n i e sa sa c c o u n t a b i l i 吼f a i m e s sa n da t o m i c i t ya r es a t i s f i e di n 血i sp r o t o c o l g i v e nt h a t m e p r i n c i p a l s a r eh o n e s t a 盘e r 曲s t r a c t i n gt h em o d e l ，w eu s ea m o d e l c h e c k i n gt o o lu p p 从l t ov e r i f yw h e l e rt h et i m eo ft h ep r o t o c o lv i o l a t e so r n o t 2 p r e s e n t i n ga 疗a m e w o r kb a s e do nt h ep n c i p a i s a c t i o ne x c h a n g e s w ee x t e n d f i n i t cs t a t ea u t o m a t aw i ll o g i cr u l e s ，t m s tm a 啪xa n da c t i o n so fp r i n c i p a l st oa n a l y z e e c o m m e r c ep r o t o c o l s t b e 衄l s tm a 缸xd e s c r i b e st h er c l i a b l er e l a t i o n s h i pb e m e e n t t l ep r i n c i p a l sf o 肌a l l ys ot h a tt h ei n i t i a ls t a t ea s s u m p t i o ni sl 儿1 n e c e s s a r y t h es e to f a c d o 船l e a d su st om o d e lm ep m t o c o lw i t h o u ti d e a l i z a t i o np r o c e s s ，a n dt h es e to f i n f b r e n c em l e si sp m v i d e df o rr e d u c t j o na n da n a l y s i so fs i 印a m r ea f l dc j p h e n e x t a s a i le x a m p l e ，a c c o u n 协i l i t yi sf o u n dn o tt ob es a t i s f i e di nt h ea a t pw h e nt h e p a n i c i p a n t sa r ed i s h o n e s t f a t e l y ，w ec a nf i n dt h er e 器o no fv i o l a t i o na c c o r d i n g t om ep r i n c i p a l s m o d e l s a f 【e r o p t i m i z i n g t h e p r o t o c o l ， w ec a ns h o wt h e a c c o u n t a b i l i t y ，f a i m e s sa n da t o m i c i t ya r es “s f i e d 丁 郑州大学硕士学位论文 3 f a i l u r ea n a l y s i so fe c o m m e r c ep r o t o c o lu s i n gm o d e lc h e c k i n g o u rc o n c l u s i o ni s l a t ，m es e c u r ep r o p e r t i e so fa i le c o m m e r c ep r o t o c o lm a yb e “o l a t e dw h e n 也e p m t o c o li se x e c u t e db yan 珊曲e ro fp r i n c j p a l sc 叩c u e n t l yi nt h ep r c s e n c eo fs i t eo r c o m m u n i c a t i o nf a i l u r e w ee v a l u a t ew h i c hf a i l u r e sc a u s et h ev i o l a t i o no fo n eo rm o r e o ft h ep r 叩e r t i e sa c c o r d i n gt ot h ec o u m e rc x a m p l ew h i c hi sp r o d u c e db ym o d e l c b e c l ( i n gt o o ( u p p a a li n 也i sp a p e r ) k e y w o r d s ：e c o m m e r c ep r o t o c o l ，m o d e lc h e c k i n k a i l a rl o g i c ，m u l t i p l en l n s ，f a i l u r c 柚a l y s i s ，u p 队a l i 郑捌客学预士学挺论文 圈裘豳聚 餐l ，l 邀子商务簇鍪1 蓬3 1 黼家避稳m 。2 0 图3 。2 顾客进程c 2 l 嚣3 3 银行透纛嚣。 蹬3 。4 变鼹目惑进程b 2 2 图3 ，5 抽象后鞠协议参与者模型2 3 鋈3 。淤黢a 己验逶辫审獒羹象2 辱 图4 1 顾释迸穰3 l 霆4 ，2 褥寨述程3 l 匿4 ，3 敬避岳麓矮窖避程3 碡 图5 iw 嚣环硫下参与者模型。嬲 墅5 ，2 糇客运 i 环境不可靠时参与港模溅一4 0 溪5 3 鬻家运嚣舔壤不可靠薅参与誊攘鍪毒 强5 。4 端兰方远行环蟪誉可靠孵与卷模型碡z 图6 1w 靠环境下单轮协议参与者搂烈4 6 餮越哥靠骂壤下多轮秘蔽参与誊模鍪然 图6 3 不可靠环境下澎轮协议务与者模型5 0 郑重声明 y9 7 6 7 本人的学位论文是在导师的指导下独立撰写并完成的，学位论文没有剽 窃、抄袭等违反学术道德、学术规范的侵权行为，否则，本人愿意承担由此 产生的一切法律责任和法律后果，特此郑重声明。 学位论文作者 务竿 枷年6 月7 日 郑州大学硕士学位论文 第一章引言 1 1 研究背景 电子商务是客户( c u s t o m e r ) 、商家( m e r c h a n t ) 和各方所信任的第三方认证机构 ( c a ) 之间的信息流、资金流和物流的交互关系，各方通过遍及全球的、开放的但 不安全的i n t e n l e t 相互联系峨如图1 所示。 。一；怠档 8 一芦 刨苜”一“ l 并，1 c2 银仃b3 曲冢m 4 第二万认| 止机构c a 图| l 电子商务模型 在电子商务模型中，四方三流交互关系必须有规可循，以保证各方利益和安 全，并能控制风险，这就是各种协议( p r o t o c 0 1 ) 。协议是两个或两个以上的参与 者为完成某项特定任务而采取的按顺序定义的通信序列和计算步骤。每个通信步 骤将消息从一个主体传给另一个主体，计算步骤用于更新主体的内部状态。电子 商务协议正是为了完成电子商务活动而设计的协议。 电子商务由于方便、快捷而开展得如火如荼。据不完全统计，2 0 0 5 年我国电 子商务交易额达7 4 0 0 亿元，比上年增长5 0 ；网上购物用户数量达2 2 0 0 万户，比 上年增加6 0 0 万户。但电子商务的安全问题也越来越突出。万事达信用卡集团于 2 0 0 5 年6 月1 7 日称，大约4 0 0 0 万信用卡顾客账户被一名黑客利用电脑病毒侵入， 黑客可能将用户账号信息用作欺诈行为，而且多家银行的顾客账户都遭到了入 侵。信用卡账户等信息的泄漏，将带给人们最直接的损失。此外，a c 尼尔森公 司的调查表明：安全性是网上购物者用信用卡支付的主要顾虑。 安全的电子商务协议是保证电子商务活动正常开展的基础。电子商务中的客 户之间必须通过安全的、可信赖的协议才能建立起相互之间的信任关系。协议的 缺陷可能会使客户间传送的数据遭到恶意修改而不被客户发现，从而使客户受到 严重损失。因此，电子商务协议的安全性是电子商务安全的重要环节，也是电子 商务发展的瓶颈。 安全的电子商务协议不但应当具备传统的安全协议所具备的全部功能，还必 郑州大学硕士学位论文 须具备一些特殊的性质来确保交易的有效性。例如，电子商务协议必须保证货币 在交易过程中守恒；顾客和商家能够出示证据显示交易商品的内容；在交易过程 中不泄漏主体的身份；参与协议的主体不能否认曾经参加过会话，等等。但电子 商务协议在并行环境中运行，非常复杂且容易出错。经过精心设计的协议往往存 在安全上的漏洞，仅凭人的直觉判断很难把错误找出来。如：k e r b e r o s 协议及基 础n e e d h a ms c h r o e d e f 协议起初被认为是安全的，1 7 年后才被证实有可怕的漏洞 口j 。因此对电子商务协议安全性的分析是个重要的问题。 分析电子商务协议的困难性存于 3 】：( 1 ) 安全目标本身的微妙性；( 2 ) 协议 运行环境的复杂性。当协议运行在一个十分复杂的公开环境时，攻击者处处存在。 必须形式化地刻画协议的运行环境，这是一项艰巨的任务；( 3 ) 攻击者模型的复 杂性。必须形式化地描述攻击者的能力，对攻击者和攻击行为进行分类和形式化 分析；( 4 ) 协议本身具有“高并发性”的特点。因此，个电子商务协议在设计出 来之后，需要从多方面对其各种性质进行分析，协议分析正是揭示电子商务协议 是否存在缺陷的重要途径。为此，本文对电子商务协议安全性质的分析进行了初 步的研究和探讨。 1 2 研究现状 近年来，国内外研究人员利用形式化方法分析安全协议并取得了。一系列成 果。如在定理证明方面，m e a d o w s 的n r l 协议分析器 4 1 发现了许多已知的和未知 的安全协议漏洞；p a u l s o n 提出了基于归纳的定理证明方法【5 】，他研制的定理证明 器i s a b e l l e 可用归纳的方法分析安全协议；文献 6 】用归纳证明的方法分析了s e t 协议的安全性质。在逻辑分析方面，主要有b a n 逻辑【”、b a n 类逻辑( 如g n y 逻辑、a u t l o g 逻辑、a t 逻辑) 以及s v o 逻辑 8 】等，其中后者可用于分析电子 商务协议的币可否认性【9 1 ；后来，k a i l a r 在b a n 逻辑基础上提出了用于分析电子 商务协议可追究性的k a i l 砌翌辑，白硕等提出了非单调动态逻辑n dl 1 ”，周典 翠等提出了一种分析电子商务协议的新工具，文献【1 3 将k a i l a r 逻辑和l p c 结 合来分析电子商务协议，等等。 d o l e v 和y a o 等人最早应用模型检测方法来分析安全协议。但该模型只针 对保密性进行建模处理，表达能力非常有限。文献【1 5 对d o l e v - y a o 模型进行了 改进，但验证过程中对用户的依赖性很大，且不保证最后收敛。 郑州大学硕十学位论文 t h a y e r ，h e r z o g 和g u t t l n a l l 1 卅提出的串空间( s t r a n d s p a c e ) 模型是一种结合定理 证明和协议迹的混合方法。s o n g 应用串空间模型，结合定理证明和模型检测技术， 研制出安全协议自动检验工具a 也e n a 。串空间模型的时间和空间效率比较 高，但描述协议属性时不及逻辑方法自然、丰富。 在模型检测方面使用最广的是c s p 理论。1 9 9 6 年l o w e 首先采用c s p ( 通信顺 序进程) 方法和模型校验技术对安全协议进行形式化分析。他应用c s p 模型和c s p r 1 模型校验工具f d r 分析n s p k 协议，发现了一个近1 7 年来未知的攻击1 。之后， r o s c o e 提出c s p + f d r 是形式化分析安全协议的一条新途径，可用于分析不可靠 环境下电子商务协议的确认发送原子性、原子性【1 9 1 及可追究性。 另外，s t a n d f j r d 大学的m i t c h e l l 等人【2 0 1 使用m u r p h i 分析了一些复杂协议，如 k e r b e m s 协议、s s l 协议等。文献【2 l 】用模型检测工具s m v 分析了d 罾c a s h 协议和 n e t b i l l 协议的原子性。文献 2 2 】用自动验证工具u p p a a l 验证了带时间约束的简 单网络支付协议的原子性，文献 2 3 用u p p a a l 验证了t l s 握手协议，等等。 1 3 研究内容 上述方法都能较好地分析协议的某些属性，但也有一定的局限性。如文献 6 用基于归纳的方法分析s e t 协议，证明过程较为繁琐；b a n 逻辑可对交易主体的 消息和信仰建模，但不能对行为建模；k a i l a r 逻辑可对交易主体的消息和责任建 模，从而可分析可追究性，但需要初始假设及对协议进行理想化，而这正是k a i l a r 逻辑的最大缺陷f 2 ”；文献【1 2 ，1 3 有较强的逻辑分析能力，但不能动态显示协议的 执行过程：文献 2 2 虽可实现自动验证，但不具备逻辑推理能力，等等。 在常见的三种形式化分析方法中，定理证明对协议参加者数量和消息数量没 有限制，但难以实现自动验证。逻辑分析中的证明构造简洁，容易完成，但不能 对交易主体的行为建模，且有时还需要初始假设及对协议进行理想化2 4 ，2 5 】。本文 主要用模型检测分析电子商务协议的安全性质。这是因为：( 1 ) 模型检测简洁明 了，可动态显示协议的执行过程，且可借助模型检测工具实现自动验证，验证速 度比其他方法( 如定理证明2 印) 快；( 2 ) 如果性质不满足，可借助模型检测工具 产生的反例查找原因；( 3 1 模型检测技术己成功地用于分析安全协议【2 】。但在分 析电子商务协议时，模型检测的逻辑推理能力较弱。 此外，当用模型检测方法分析协议的安全性质时，目前的大多数文献都假设 郑州大学硕上学位论文 只有一对协议参与者在可靠环境下执行协议。随着网络的大规模应用，越来越多 的协议在不可靠环境下并发执行，因此下列问题也应运而生：在可靠环境下安全 的协议运行在不可靠环境下时，是否仍然保持原来的安全性质1 8 】：在单轮情况 下安全的协议，一旦有多对参与者并发执行，是否仍然保持原来的安全性质；当 一一个主体同时执行多个协议时，原本相互独立的、安全的协议是否仍然保持原来 的安全性质2 7 1 ，等等。 针对上述问题，本文主要工作如下： ( 1 ) 基于消息转换的验证模型。该方法定义了一个扩展的有限状态自动机， 并给出了一些新的逻辑转换规则和详细的分析步骤。用扩展的f s a 为协议建模， 刁i 仅可动态显示各个参与者并发执行协议的过程，而且增强了自动机的逻辑分析 能力，可分析带有加密、签名消息的电子商务协议的安全性质。利用该方法分析 匿名原子交易协议，可知当交易主体诚实时，该协议满足可追究性、公平性、原 子性；对协议模型抽象后，我们借助模型检测工具u p 队a l 验证了协议的时效 性。 ( 2 ) 基于动作转换的验证模型。定义了一个信任矩阵和一个动作集合，并将 它们和逻辑规则一起引入有限状态自动机为协议参与者建模。信任矩阵形式化了 协议参与者之间的信任关系，从而无需初始化假设；动作集合将加密、签名等动 作明确地表示出来，从而在规范协议时无需理想化过程。此外，动作集合的引入 还减少了逻辑规则的使用，使得分析过程更为直观明了。利用该方法分析匿名原 子交易协议，可知当交易主体不诚实时，该协议不满足可追究性；通过分析参与 者进程的模型，我们找到了性质不满足的原因，并对原协议进行修改；对修改后 的协议进一步分析，发现其满足可追究性、公平性、原子性。 ( 3 ) 用模型检测方法分析了在升i 可靠环境下协议的安全性质。结果表明，一 个安全的电子商务协议在不可靠环境下由多对参与者同时执行时，有可能不再满 足安全性质；当安全性质违背时，可借助模型检测工具( 本文用模型检测工具 u p p a a l ) 生成的消息序列对协议进行改进。 1 4 本文结构 本文是如下组织的： 第一章引言，介绍研究背景、现状和主要研究内容及意义。 4 郑州大学硕士学位论文 第二章介绍电子商务协议的基本知识，并简单介绍模型检测工具u p p a a l 。 第三章具体介绍基于消息的有限状态自动机与逻辑相结合的分析方法。 第四章具体介绍基于动作的有限状态自动机与逻辑相结合的分析方法。 第五章验证不可靠环境下电子商务协议的安全性质。 第六章验证不可靠环境下多轮协议的安全性质。 第七章总结全文，展望未来的工作。 郑州大学硕士学位论文 第二章预备知识 本章前两节介绍电子商务协议的基本概念及安全性，第三节介绍模型检测的 基础知识及模型检测工具u p p a a l 。鉴于本文所用到的逻辑规则是建立在k a i l a r 逻辑和卿周逻辑基础之上，第四节简单介绍这两种逻辑。 2 1 电子商务协议的基本概念 2 1 1 电子商务协议的基本结构 电子商务协议的基本结构雎明如下。参与协议的主体有3 个： 用户：安全地从服务提供方获得服务，然后通过金融机构安全地向服务提供 方付费。 服务提供方：安全地向用户提供服务，并通过金融机构安全地向用户索取费 用。 金融机构：负责向用户和服务提供方提供证据，然后从用户方帐户安全地提 取资金，并将资金安全地支付给服务提供方帐户。 电子商务协议主要由以下3 个步骤组成。 确定价格：用户和服务提供方通过执行协议，协商并确定价格。 提供服务：服务提供方向用户安全地提供服务。 传递证据：金融机构向交易双方传递一个消息，表明已经从用户帐户安全地 提取资金，并将资金安全地支付给服务提供方帐户。 2 1 2 电子商务协议的运行环境及语义 电子商务协议存一个分布式环境中运行，这个环境包含3 类主体：发送方a 、 接收方b 和可信第三方t t p ，其中t t p 可以是一个或多个主体。在这个环境中，a 和b 之间可以直接通信，也可通过t t p 转发。环境包含两方面：交易实体是否诚 实和通信信道是否可靠”】。协议的各种属性与运行环境密切相关。 假设通信信道不可靠，电子商务协议语句根据中断性可分为三判1 2 】： ( 1 ) a l b b 川t t p ：m 若a ，b 都是诚实的日通信信道是可靠的，则是不可中 断的；否则是可中断的。 ( 2 ) 在信道可靠的情况下，t t p b 恤：m 是不可中断的。 6 郑州大学顿十学位论文 ( 3 ) a 旧一t t p ：m 在信道可靠或= i j | i 可靠的条件下都是不可中断的。 2 ，1 3 常见的电子商务协议 常见的电子商务协议有：安全套接层协议s s l ( s c c l l r es o c k e tl a y e r ) 2 9 1 ，安全 电子交易协议s e t ( s e c u r ee l e c t r o n i c 仃a n s a c t i o n ) 【3 0 1 ，匿名原子交易协议 ( a n o n y m o u sa t o m i c 廿锄s a c t i o np m t o c 0 1 ) 【3 l 】，f r a n k l i n 瓜e i t e i ，卧议【3 2 】，自动解决争论 的公平交换协议 3 3 等。下面简单介绍其中几个，它们是本文进行形式化分析的“试 验床”。 1 匿名原子交易协议 匿名原子交易协议( a n o n y m o u sa t o m i ct r a n s a c t i o n s ) 是由j c 锄p 和j d t y g a r 于1 9 9 6 年提出的，首次解决了电子商务协议中原子性与匿名性之间的矛盾，对推 动电子商务发展起着至关重要的作用。该协议描述如下： 1 c - m ：o r d e r ； 2 m _ c ：( n ，c o n 仃a c t ，( g o o d s ) k ) 川； 3 - c + b ：( 聆，t i m e o u t ，m ，l ，c o i n ) k j ：4 - b + m ：( 珂，t i m e o u t ，m ，l ，v a l u e ) 叫。 5 m _ l ：( n ，t i m e o u t ，叼i 5 6 - c h l ：( c o m m i t ，丘n ) ； 7 b 寸l ：( c o m m i t ，胛) k - ；8 m l ：( c o m m i t ，聆) i 一。 顾客发送商品订单给商家，商家收到后，发送已签名的交易号胛、商品描述 c o n t m c t 及用对称密钥励口密的g o o d s 给顾客。顾客在第三步向银行发送签过名的 消息，银行检验c o i n 是否有效及是否被重用；在第四步银行通知商家准备提交， 商家确认”、l 、t i m e o u t ( v a l u e 为c o i n 的币值) 。第五步中商家向交易日志l 发送 足、t i m e o u t 和n 进行提交，l 验证是否超时。第六、七、八步中，c 、b 、m 分别通 过助操作从l 处获得提交成功的证据。 2 自动解决争论的公平交换协议 自动解决争论的公平交换协议是一个重要的公平交换协议，主要用于数字产 品的电子交易，协议描述如下： 1 t p c ：d o w n l o a do f p r o d u c te n c r y p t e d w “h k e y k l ； 2 c _ m ：p u r c h a s eo r d e r ； 3 m 子c ：p r o d u c te n c i 卯t e d w i t has e c o n d k e y k 2 ； 4 m _ t p ：m ed e c r y p t i n gk e y “kf o rt h ep r o d u c ta 1 1 dm e 印p r o v e dp u r c h a s e 7 郑卅1 人学硕士学位论文 o r d e r ： 5 c _ t p ：t h ep a y m e n tt o k e na n dc o p yo f t h ep u r c h a s eo r d e r ； 6 t p 手c ：m ed e c r y p t i n gk e y ： 7 t p _ m ：p a y m e n tt o k e n 。 顾客从第三方下载加密产品后，在第二步给商家发送一个购买序号。商家收 到后，在三、四步分别给顾客发送加密产品，给第三方发送产品的解密密钥。顾 客将刚收到的加密产品与下载的加密产品进行比较，若相同，则在第五步将购物 代币以及购买序号的副本发给第三方。第三方检查购物代币，若不合法，取消协 议；否则将解密密钥转发给顾客，将购物代币转发给商家。 3 f 删【l k l i n 瓜e i t e r 协议 f r a n k l i n 瓜e i t e r 协议也是一个重要的公平交换协议，它存参与者x 和y 之间通 过第三方z 交换秘密。协议描述如下： 1 x 一 y ：x s e c r e t l ： 2 y 一 x ：y s e c r e “： 3 x 一 z ：x s e c r e t 2 c o r r e c t 或x s e c r c t 2 i n c o r r e c t ； 4 y 一 z ：y s e c r e t 2 c o r r e c t 或y s e c r e t 2 i n c o 盯e c t ： 5 z 一 x ：y s e c r e t 2 c o r r e c t 或e x c h a n g e a b o n ； 6 z 一 y ：x s e c r e t 2 c o r r e c t 或e x c h a n g e a b o n 。 在该协议中，参与者x 与y 相互交换秘密，第三方z 控制两个参与者或者接收 或者均得不到彼此的秘密。x 、y 把各自的秘密分为两部分。第一二步，两者各 自把秘密的第一部分传给对方；三四步中，各自把秘密的第二部分传给第三方z 。 在实际的f r 协议的第四步之后，z 对x 和y 秘密的第二部分进行基于h a s h 函数的 检验。之后，z 要么把秘密的第二部分正确传送，要么通知x 、y 交换失败。 2 2 电子商务协议的安全性 2 2 1 常见的电子商务协议的安全| 生质 电子商务协议验证就是验证协议的安全属性能否得到保证。常见的属性主要 有保密性、完整性、认证性、非否认性、可追究性、公平性、原子性、匿名性、 隐私性、时效性等。下面介绍本文用到的几个重要的安全属性。 郑州大学硕士学位论文 ( 1 ) 非否认性( n o n r e p u d i a t i o n ) ：会话结束后，会话各方都没有能力否认其参 加会话的事实。 ( 2 ) 可追究性( a c c o l i n t 曲i l i 呦：指协议主体应当对自己的行为负责，在发生纠 纷时，主体可以提供必要的证据保护自身的利益。可追究性通过发方非否认证据 ( e o o ) 和收方非否认证据( e o r ) 实现，即正确执行完后，应当保证发送方收到e o r 且接收方收到e 0 0 。 ( 3 ) 公平性( f a i m e s s ) ：保证参加协议的各方在协议执行的任何阶段都处于同 等地位，当协议执行完后或者各方得到各自所需的或者什么也得不到。它包含两 层含义：首先，正确地执行完协议后保证发送方收到e o r 日接收方收到e 0 0 ；其 次，如果协议异常终止，协议应保证通信双方都处于同等地位，任何一方都不占 优势。 ( 4 ) 原子性3 4 1 。原予性分为三级，呈向上兼容，后者包含前者。 货币原子性( m o n e y a t o m i c i t y ) ：电子商务交易发生前后资金守恒，资金在电 子支付中既不会创生也不会消失，顾客货币的减少等于商家货币的增加。 商品原子性( g o o d sa t o m i c i t y ) ：协议一定满足货币原子性日保证顾客收到商 品当日仅当对应商家获得付款。 确认发送原子性( c e r t m e dd e l i v e r y ) ：首先，协议一定满足货币原子性和商品 原子性；其次，需对顾客从商家购得的商品和商家付给顾客的商品分别确认，保 证客户得到他所订购的商品。如有争议，拥有仲裁依据证实交易商品的内容。 ( 5 ) 时效性：协议参与者在规定时间内收到消息或电子货物。时间一般由交 易的一方制定，其他参与者有权否决。 2 2 2 电子商务协议的分析前提 在分析电子商务协议时，通常做以下基本假设： ( 1 ) 协议所采用的加密算法足够强壮； ( 2 ) 密码系统是完善的( p e 疵c t ) ，即只有掌握密钥的主体才能理解密文消息； ( 3 ) 无加密项冲突； ( 4 ) 哈希函数是抗碰撞的； ( 5 ) 诚实的主体遵循协议规定执行协议，不诚实的主体不会完全遵守协议。 9 郑州大学硕士学位论文 2 2 3 电子商务协议的设计准则 文献 2 8 】归纳了l o 条安全协议的设计准则，它们同样适用于电子商务协议： ( 1 1 设计目标明确，无二义性； ( 2 ) 最好应用描述协议的形式语言，对安全协议本身进行形式化描述； ( 3 ) 通过形式化分析方法证明电子商务协议实现了设计目标； ( 4 ) 安全性与具体采用的密码算法无关； ( 5 ) 保证临时值和会话秘钥等重要消息的新鲜性，防止重放攻击； ( 6 ) 尽量采用异步认证方式，避免采用同步时钟( 时戳) 的认证方式； ( 7 ) 具有抵抗常见攻击，特别是防止重放攻击的能力； ( 8 ) 进行运行环境的风险分析，作尽可能少的初始安全假设： f 9 1 实用性强，可用于各种网络的不同协议层： ( 1 0 ) 尽可能减少密码运算，降低成本，扩大应用范围。 第( 7 ) 条十分重要。“永远不低估攻击者的能力”，这是设计安全协议时应当时 刻牢记的一条重要原则。 2 2 4 电子商务协议分析方法简介 目前电子商务协议的分析方法主要有非形式化方法和形式化方法。 非形式化方法主要包括直观检测和实际攻击。直观检测必须在协议实现之后 才能实行，有可能导致人力物力的巨大浪费；实际攻击利用现在已知的攻击方法 对协议进行攻击，以攻击是否有效判断协议是否安全。由于实际中还存在许多未 知的攻击方法，因此无法检测在未知攻击下协议是否存在缺陷。 形式化方法主要包括定理证明、模型检测和逻辑分析。它能全面深刻地检测 到协议中的细小漏洞，并能发现现有的攻击手段对协议造成的威胁，甚至能发现 新的攻击方法。通过对电子商务协议进行形式化分析，可以反过来指导其设计， 使其更完善。因此形式化验证以其严谨、简洁的特点而成为验证协议的重要方法， 是电子商务领域研究的热点。 为了用形式化方法分析电子商务协议，首先要对协议及其必须满足的性质进 行形式化描述，然后用某种方法( 定理证明、模型检测或逻辑分析) 分析协议。 需要指出的是：用形式化方法分析电子商务协议，只是保证协议安全性的必要条 1 0 郑州大学硕士学位论文 件而非充分条件。本文主要用模型检测方法分析电子商务协议的安全性质，下面 简单介绍该方法。 2 3 模型检测 2 - 3 1 模型检测简介 模型检测【3 5 1 是对有穷状态系统的一种形式化确认( v a l i d a t i o n ) 方法，它的基本 思想是通过状态空间搜索来确认系统是否具有某些性质。即给定一个系统p 和规 约、l ，生成对应于系统的模型m ，然后证明m ，即规约、l ，在檬型m 中成立，从 而证明了系统p 满足规约、l ，。若、l ，成立，模型检测工具应加以确认，否则给出反例 说明、l ，不成立的情况，供调试使用。 模型检测的一个严重缺陷是“状态爆炸( s t a t ee x p l o s i o n ) 问题”，即随着所要检 测的系统的规模增大，模型检测算法所需的时间空间开销往往呈指数增长。解 决该问题的途径有两个：一是将模型检测与定理证明相结合，如斯坦福大学的 s t e p 时态证明器。二是引入符引溪型检测方法。其他方法还有o n t h e n y 算法、 抽象归纳、偏序方法和对称归约、局部状态空间( 法) 等。 目前的模型检测工具主要有：c o s p a n f o r m a lc h e c k 、m u r p h y 、s p 、 s m v 、u p p a a l 、v i s 等。本文主要用模型检测工具u p 队a l 验证协议性质， 后面我们将简单介绍u p p a a l 。 2 3 2 利用模型检测方法分析协议的过程 用模型检测方法分析协议有以下4 个过程：( 1 ) 建立协议模型：( 2 ) 将协议 模型转化为某种特定模型检钡4 语言支持的协议模型；( 3 ) 用这种特定模型检测工 具所支持的逻辑对待检验的性质进行描述；( 4 ) 运行并判断协议是否满足要求。 当模型检测工具判断出协议不符合要求时，需要考虑的问题是：上述过程的 前3 步是否出错误，或是协议的确升i 满足其必须具备的性质。 2 _ 3 3 u p 队a l 简介 u p p a a l 是由瑞典的u p p s a l a 大学与丹麦的a a l b o 昭大学联合研发的、基 于时间自动机的一种自动验证工具，己成功用于通信协议和实时控制器的验证。 u p p a a l 有一个易于用户操作和使用的集成环境，它的图形用户主界面主要 郑州大学硕十学位论文 由一个系统编辑器( s y s t e me d i t o r ) 、一个模拟器( s i m u l a t o r ) 和一个验证器( v e r i f i e r ) 组成。使用该工具时，首先在系统编辑器中将要验证的协议用自动机建模，之后 可在模拟器中检查所建模型可能的执行是否有错，以便存验证前发现一些错误； 最后在验证器中将要验证的协议性质用b n f 语法来描述，通过快速搜索系统的 状态空间来检查协议的性质是否满足。如果性质不满足，u p 队a l 会自动生成一 个诊断序列以便设计者修改协议。另外，模板带有参数，给模板传递刁i 同的参数 可得到不同的进程，因此通过设计模板可以描述结构相同的多个进程。这一点对 第六章多轮协议的建模至关重要。 u p p a a l 提供了一种b n f 语法，p m p ：= a 】p i e p ie 】p l a p 。 其中： e p 表示p o s s i b l e ，e q 表示l e a d t o ，等价于a 【 ( p i m p l y a q ) 。 在验证中常用的两类安全性质是e p 和a 【 p ，e - x ：主体p 能够证明公式z ： p x ：主体p 对公式x 负有责任； 生_ p ：秘钥世，可以用于验证主体p 的身份。 存卿周逻辑中，每个主体在协议运行前拥有一个初始拥有集合，它由一些 公式组成。随着分析的进行，主体的拥有集合不断扩大，到协议运行结束时，每 个主体拥有一个最终拥有集合。假设协议由”条语句组成。在协议开始之前，主 体p 的初始拥有集合记为o ：，它包含环境分配给p 的密钥和p 能证明的公式。当 协议的第涤语句执行完毕后，主体p 的拥有集合记为o ：。当协议经过n 步运行终 止时，用0 。记p 的最终拥有集合。 卿周逻辑共有6 条推理规则： r 签溯u ：竿筹。 如果主体p 拥有用j 1 签名的公式x ，并日p 能够证明丘可用于验证主体q 的 身份，那么p 可以证明q 对公式x 负有责任。 r ，连接规则： ! 三望三f ! ! 羔2 ，! 三堡! 羔! ! 垒! ! ， 。 尸 一q j ；尸卜q yp 卜q ( j ，y ) p 卜x ；，卜，p - ( 工，y ) p 卜( 聋，y )尸卜x ；p _ y 如果主体尸能够证明主体q 对某一公式的连接或并负有责任，那么尸能够证明 q 对这个公式的各个部分负有责任。反之，若p 能够证明9 对几个公式负有责任， 那么p 能够证明q 对这几个公式的连接或并负有责任。 r ，密文理解规则：! 三堡兰 型! ：! 三堡! 丝。 。 ， _ q o 这条规则是新引入的，用于理解签名的加密消息。如果主体p 能够证明主体 9 对某个用对称密钥砌口密的公式z 负有责任，并_ 且p 能够证明q 拥有加密密钥 蜓也是解密密钥) ，那么p 能够证明q 对公式x 负有责任。 1 4 郑州大学硕士学位论文 r 。拥有删：蒜a 如果主体p 的初始拥有集合中包含某个公式x ，那么任何主体q 能证明p 拥有 这个公式x 。 r ；传递删：筹，筹。 第二条子规则是新引入的，假设主体爿和占是通信双方，爿与b 通过t t p 交换 消息 扎如果通信的一方a 或者b 能够证明t t p 对消息肘负责，那么他能够证咀对 方历戈者爿拥有这个消息。 ， r 。电子证书规则：! 三! ：! 茎z ：望l” p 卜二q 0 这条