基于模型检测的电子商务交易协议形式化分析与验证-李婉璐.docx

《基于模型检测的电子商务交易协议形式化分析与验证-李婉璐.docx》由会员分享，可在线阅读，更多相关《基于模型检测的电子商务交易协议形式化分析与验证-李婉璐.docx（47页珍藏版）》请在得力文库 - 分享文档赚钱的网站上搜索。

1、独 创 性 声 明 本人声明所呈交的论文是我个人在导师指导下进行的研究工作及取得的研究成 果。尽我所知，除了文中特别加以标注和致谢的地方外，论文中不包含其他人己经发 表或撰写过的研究成果，也不包含为获得宁夏大学或其它教育机构的学位或证书而使 用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中作了明确的 说明并表示了谢意。 研究 生 签 名 ： t振 4 时间： t年 S月沽日 关于论文使用授权的说明 本人完全了解宁夏大学有关保留、使用学位论文的规定，即：学校有权保留送交 论文的复印件和磁盘，允许论文被查阅和借阅，可以采用影印、缩印或扫描等复制手 段保存、汇编学位论文。同意宁夏大学

2、可以用不同方式在不同媒体上发表、传播学位 论文的全部或部分内容。 (保密的学位论文在解密后应遵守此协议 ） 研究生签名：令 I减 导师签名 : 时间：年 C月日 时 间 ： 年 JT耳奸曰 摘要 fSfSfll“ 根据 CNNIC(Ctiina fntemet Network information Center， 中国互联网络信息中心 )发布的 “ 第 37次中国互联 W络发展状况统计报告 ” W， 2015年， 42.7%的网民遭遇过网络安全问题。随着网 络购物群体的不断增大，电子商务安全问题引起了消费者的广泛关注。 2015年，我国网络购物 用户规模达到 4.丨 3亿，同时， 16.4%

3、的消费者在网购过程中遭遇到过网络消费欺诈。由此可见， 网络安全问题和交易安全问题是保证电子商务进一步发展的关键之所在。 交易协议是交易安全问题的核心。本文从网络交易安全问题出发，选取主流电子商务 B2C 模式作为研究对象，通过模型检测方法对基于第三方支付平台的交易协议进行了形式化建模、分 析和验证，以保证买家和商户之间完成安全、可靠的交易活动。其主要内容如下： 1. 介绍了课题背景、相关理论基础和采用形式化方法分析安全协议的发展过程以及研究现 状。 2. 对 B2C模式涉及到的电子商务交易协议进行了简要的分析，使用 Promela语言形式化地 描述了电子商务交易协议中涉及到的四个实体：买家、商

4、户网站、第三方支付平台和银 行。 3. 使用模型检测方法对 B2C模式交易协议进行形式化验证，对交易协议进行抽象化建模， 描述了电子商务交易协议的 LTL性质，使用 Spin的 P形界面工具 XSpin得到交易协议 的运行轨迹，在此基础上分析目前 B2C模式交易协议存在的潜在安全隐患。 4. 针对分析结果，提出了一种基于 B2C模式的改进模型，增加了物流方和第三方隐私服务 器两个实体，用于规范交易流程和保护买家隐私。 关键词：形式化方法， Spin,模型检测，电子商务交易协议 ， Promela Abstract n37th Statistical Report on Internet Dev

5、elopment in China“ which issued by CNNIC (China Internet Network Information Center), indicate that 42.7% of Internet users encountered network security issues in China. With the growing population of online shopping people, e-commerce security problems arouse much concern. In China, online shopping

6、 users reached 413 million, at the same time, 16.4% of consumers encountered the network consumer fraud by 2015. Thus, both network security and transaction security are important to ensure the further development of e-commerce. Trade agreements are the key point to transaction security. This articl

7、e focuses on transaction security, and select B2C e-commerce model as a research object. Formal analysis and verification of e-commerce transaction protocols are based on model checking method. In order to ensure the completion of the normal, reliable and secure transactions rules between customers

8、and merchants. Its main content is as follows: Introduce the subject background, theory foundation and the present situation that use of formal methods to analyze security protocol development process and research. Analyze e-coxnmerce transaction protocols of B2C mode briefly. Expounds the design pr

9、inciple of e-commerce transaction agreement, such as anonymity, non-repudiatioiij fairness, safely, etc. Then described buyers, merchant sites, third-party payment platform and bank with Promela language. Formal verification and model the transaction protocols through model checking. Then use LTL fo

10、rmulation to describe the e-commerce transaction protocol properties. According the transaction protocols running trace to analyze the loopholes of the B2C trading agreement. Put forward an improved model to standardize transaction process and protecting the privacy of the buyer. Add two entities to

11、 the current e-commerce transaction model of B2C mode the original model, such as the logistics and privacy proxy server. Keywords: Formal Method, Spin, Model Checking, E-commerce Transaction Protocols, Promela 目录 mw. i 第一章绪论 . 1 1.1选题背景 . 1 1.2国内外研究现状 . 1 1.2.1安全协议的研究与发展 . 1 1.2.2电子商务 B2C模型及交易协议的安全

12、性质 . 2 1.2. 3形式化分析方法的研究和进展 . 3 1.3本文的主要工作 . 4 第二章理论框架 . 5 2. 1形式化方法 . 5 2. 1.1形式化方法的发展 . 5 2. 1.2形式化方法的概念 . 5 2. 1. 3形式化描述语言 . 6 2_ 2额检测 . 7 2.2.1模型检测技术 . 8 2. 2. 2模型检测的应用 . 9 2. 2. 3模型检测工具 . 9 2. 3才莫态逻 $茸 . 10 2.3.1线性时序逻辑 . 10 2.3.2计算树逻辑 . 10 2. 3.3 (I-演算 . II 第三章电子商务交易协议的分析、建模及验证 . 12 3_1 Spin 工具

13、. 12 3. 1. 1 Spin的概述12 3. 1.2 Spin 的特征 . 12 3. 1.3 Spin的主要用途 . 13 3. 1.4 Spin检测的基本过程 . 13 3.2电子商务 B2C模式交易协议 . 14 3. 2.1 B2C 模式 . 14 3. 2. 2 B2C模式的交易协议 . 14 3. . 3对电子商务交易协议进行 Promela建模 . : . 15 3. 3.1 Promela 语言 . 15 3. 3. 2建立电子商务交易协议模型 . 16 3. 3. 3电子商务交易协议的 LTL性质描述及运行轨迹 . 20 3. 3. 4电子商务交易协议的验证 . 21

14、3. 3. 5电子商务交易协议中各实体的状态转换图 . 23 3. . 4电 子商务交易协议模型检测结果分析 . 25 第四章基于传统 B2C模式的改进模型 . 26 4. 1传统的 B2C模式的模型 . . . 26 4. 2改进交易模式的模型 . 27 4.2.1改进模型的基本架构设计 . 27 4. 2*. 2改进交易模式的模型 . 28 4.2.3改进模型的详细设计 . 31 4. 3 31 4.3.1改进模型的适用性 . 31 4.3.2改进模型的协议安全性 . 32 第五章结语 . 33 5. 1全文，關 . 33 5.2进一步的工作 . 33 参考文献 . 34 賺 . .37

15、Mi ilt . 41 个人简介 . 42 第一章绪论 1.1选题背景 2015年，随着 “ 互联网 +” 概念的提出和行动推进，互联网对整体社会将产生新的影响。 2015年上半年，中国网民规模达 6.88亿，互联网普及率为 50.3%。美国著名未来学家阿尔 温 托夫勒 2】 预言：在信息化社会，谁能够控制网络，掌握网络信息，谁就是人类社会的主 宰。随着“ 互联网 +” 概念的提出，电子商务逐步取代电子政务，成为信息化的主要驱动力 量。截止到 2015年 6月，中国电子商务上半年交易额达 7.63万亿元。中国己经超越美国， 成为世界第一电子商务大国。 根据 CNMC(China Interne

16、t Network丨 nformation Center， 中国互联网络信息中心 )发布的 “ 第 37次中国互联网络发展状况统计报告 ” ， 2015年，我国网络购物用户规模达到 4.13 亿，同时， 16.4%的消费者在网购过程中遭遇到过网络消费欺诈。在进行网络购物时，绝大 多数用户最关心问题是：现有的电子商务系统能否保证使用者进行安全、可靠的交易。没有 企业或个人甚至商业机构愿意在一个不安全的网络环境中进行商务交易。不安全的网络交易 不仅会导致个人隐私和商业机密的泄露，甚至可能带来重大的经济损失。所以，如何构筑一 个安全、稳定的电子商务交易环境，成为未来互联网发展的一个重大问题，受到国际

17、社会的 高度关注。 电子商务交易协议是电子商务安全的基础，是保证买家和商户之间完成可安全可靠交易 活动的规范。目前，安全协议的设计理论不够完善，通常协议的出错率较高，不能满足预期 目标。因此需要借助形式化方法来设计和分析安全协议，从而判断它是否符合设计要求，能 否达到预期的安全目标。安全协议本身具有的微妙性、存在环境的复杂性、攻击者模型的复 杂性和高并发行，使得协议的安全性分析具有其理论上和实践上的困难性。 本文选取电子商务 B2C模式作为研究对象，通过对交易协议的形式化建模，使我们能够 更好的明确和理解协议的运作过程和最终目标 ，并且为自动化验证工具提供基本的数据支 持。同时，本文通过模型检

18、测的方法分析指出电子商务 B2C模式交易协议中存在的安全缺陷， 以此作为开发人员改进交易协议的重要依据。在本文最后一章，提出了一种基于传统 B2C模 式的改进模型。本方法对目前主流的电商网站改进电子商务交易协议具有指导作用。 1.2国内外研究现状 1.2.1安全协议的研究与发展 网络世界与现实世界的显著区别在于：现实世界中，交互双方依据彼此的生物特征识别 对方；在网络世界中，相互通信的双方可能未曾谋面，彼此的认证需要建立在密码体制的基 础上。安全协 议 3，也可称为密码协议，是建立在密码学理论基础上的一种消息交换协议。 安全协议被用于在计算机网络或分布式系统中，根据密码算法和数理逻辑，为协议参

19、与者提 供各种安全服务。例如，实现密钥分配、身份认证、电子商务交易等任务的各方约定任务执 行的步骤和执行的规则。 安全协议始于 1978年 R.M.Needham和 M.D.Schroeder发表的 Needham-Schroeder认证协议 (简称 NS认证协议） 。后来的学者以 Needham-Schroeder协议为蓝本 设计出了许多目前仍 广泛使用的认证协议。 从 1978年 Needham-Schroeder协议的诞生算起至今，安全协议经历了多个发展阶段。 根据协议目的将最常用的安全协议分成以下四类 5】 ： (1) 密钥交换协议 。一 般情况下在完成会话密钥的建立过程中使用本类协议

20、。参与协 议的两个或多个实体之间通过公共信道交换一个信息，即可建立一个用于在公共信道上安全 通信的共享秘密。密钥交换本身不提供通讯双方的身份验证服务，因此该协议很容易受到中 间人攻击。 (2) 认证协议。在通信过程中通过认证协议进行实体之间的认证、在实体之间安全地 分配密钥或其他各种秘密、确认发送和接收的消息的非否认性等，用来防止假冒、篡改、否 认等攻击。 (3) 可认证的密钥交换协议。是网络通信中普遍应用的一种安全协议。这类协议将密 钥交换协议和认证协议结合起来，不仅能够使得会话双方计算共享会话密钥而且还能互相认 证对方的身份。协议要求对通信双方进行身份认证，在认证成功后 通信双方分配会话密

21、钥， 保证协议双方进行安全通信目前应用较多的可认证的密钥交换抽，议有：分布认证安全服务 (DASS)协议、互连网密钥交换 （ IKE)协议 6、 Kerberos认证协议 7等。 (4) 电子商 务协议。电子商务协议是电子商务安全的基础。电子商务协议用于规范买 家和商户，保证两者之间完成安全、可靠交易活动。协议主体往往是参与交易的双方，双方 都不能以损害对方利益为手段，获得不应得的利益。 1.2.2电子商务 B2C模型及交易协议的安全性质 电子商务 s将信息网络技术和传统商务活动相结合为手段，指买卖双方通过互联网进行 商品交换。广义的电子商务是指使用通过网络进行商务活动。狭义的电子商务是指电子

22、贸易， 即Electronic Commerce， 简称 EC。 主要指以计算机网络为基础所进行的各种商务活动，包 括买家 (customer)、商户 (merchant)、银行 (bank)和为各方提供担保服务的第 -.方认证机制 (CA) 之间的资金流、信息流和物流的交互关系。各方通过开放的网络环境共享资源、相互联系 9， 使得电子商务面临的各种安全问题越来越突出。 B2C (Business to Customer)是中国最早产生的电子商务模式，以互联网为主要服务提 供手段，实现企业与个人之间开展的电子商务活动的总称，如企业为个人提供在线商品购买、 在线医疗服务等。构成 B2C模式的四个

23、要素为：买家，商户网站，支付系统和物流方。目前 较常见的 B2C商户网站有：天猫商城，亚马逊，京东，当当等等。 早期对电子商务中的安全问题的研究集中在保证网络安全，预防病毒和黑客攻击。随着 形式化方法的发展，现在对电子商务中安全问题的研究集中在设计适当的安全协议和对现有 的交易协议进行形式化分析与改进，来保证交易过程规范、可靠。 电子商务交易协议的安全性质主要包括以下几个方面叫 （ 1)完整性，是指保证协议中各 参与者所接收到的信息没有经过修改、删除或增加 (2)保密性，是指交易过程中产生的数 据只能被授权用户读取或得到。防止交易双方的交易信息被 “ 有心者 ” 窃取。 （ 3)身份认证 性，

24、是指要在交易信息的传输过程中为交易参与者提供可靠认证，防止消费欺诈。 （ 4)不可 否认性，即交易双方均不可否认发出的信息。 1.2. 3形式化分析方法的研究和进展 即使只讨论安全协议中最基本的认证协议，设计也是十分困难。设计既要保证协议是正 确的、符合认证目标的，同时要求协议没有冗佘。形式化方法学家设计了不同种类的形式化 分析方法来解决这一难题。目前，对安全协议的形式化分析主要有以下三种方法：模态逻辑 方法，模型检测方法和定理证明方法。 模态逻辑方法 迄今为止最简单、最直接的一种安全协议分析方法是 基于知识与信念推理的模态逻 辑方法。这种方法由命题和推理规则组成，命题表示主体对消息的知识或信

25、念，可以从己知 的知识和信念通过推理规则得到新的知识和信念。 SyverS n_阐述了知识、信念和语义在 安全协议的分析中的关系与相互作用。在这类方法中，最著名的是 BAN类逻辑。 1989年， Abadi , Burrows和 Needham率先以逻辑形式方法提出了 BAN逻辑 11，开 创了描述和验证安全协议的先河。随后，利用 BAN逻辑成功地发现了 CCITTX.509标准間 推荐草案中存在的安全漏洞。许多密码研究者将注意力转移到对安全协议的形式化分析方 向，许多安全协议的形式化分析方法应用而生。 BAN逻辑抽象度高，并且简单、使用，可以用来发现安全协议中的安全缺陷与避免协 议的冗余性。

26、但是由于 BAN逻辑的抽象级别过高，分析范围过窄，在使用 BAN逻辑分析 安全协议时带来较大的局限性。 BAN逻辑的缺陷在于：不能推理知识。因此只适 用于分析 简单的认证协议。许多文献提出了对 BAN逻辑的改进或延伸逻辑，如 GNY逻辑 13、 AT逻 辑 叫、 VO逻辑 15、 SVO逻辑 叫和 MB逻辑 17等，统称为 BAN类逻辑。 BAN类逻辑只适用于分析简单的认证、密码分配协议，并不适用于电子商务协议的安 全性分析。 Kailar提出 Kailar逻辑 18，是用于分析电子商务协议的新的形式化分析方法。 但 Kailar逻辑也不能够完全适用于分析电子商务协议。 Kailar逻辑对电子

27、商务协议语句的初 始化假设和解释都是非形式化的，而且无法分析协议的公平性，不能处理协议中的密文 叫。 2001年，卿斯汉、周典萃等人提出了一种可用来分析电子商务协议公平性的新方法 M。 模型检测方法 模型检测的研究始于八十年代初，最初用于硬件电路设计。随着形式方法的日益进步和 符号模型检测技术的出现，模型检测的适用范围变得更加广泛。 1996年， Gavinlowe首先 使用 CSP和模型检测技术对密码协议进行分析 CT， 并成功找到 Needham-Schroeder公钥协 议的一个以前从未发现的攻击。目前，模型检测已被用于跟踪分布式 系统设计过程中的逻辑 设计的错误，如操作系统，数据通信协

28、议，铁路信号协议，航天器的控制软件等。 模型检测技术对协议的自动验证和工程化设计具有指导意义。但是，模型检测同时也存 在缺陷：模型检测只适用于分析有限状态系统，而无法对状态爆炸的系统进行建模和分析。 定理证明方法 定理证明方法通过证明一些循环不变式来证明协议，主要可分为两类 22:推理构造方法 和证明构造方法。推理构造方法的代表有 Meadows的 NRL协议分析器方法 23i、 Cervesato 等学者的基于线性逻辑的协议验证方法 p4和 Millen等学者的基于逻辑规则的协议验证方法 25。本类方法的优点是能够发现攻击，并证明协议在多次运行下的正确性，缺点是不能自动 化地解决状态爆炸问题

29、。证明构造方法的典型代表是 Kemmerer的 InaJo和 ITP的研究 M。 证明构造方法的优点是不限制主体参与协议运行的回合，而且可以分析状态无限多的协 议。但是它的缺点是不能完全自动化。 随着技术的发展，整体网络安全形势日渐紧迫。我国的网络安全技术防护能力较弱，协 议安全性分析的起步较晚，很难找出一种方法全面的分 析方法。通过形式化分析方法只能在 给定的假设条件下保证协议的安全性。形式化分析方法不是保证协议安全性的充分条件，而 是必要条件。 1.3本文的主要工作 论文将首先在第一章从电子商务的安全性出发，介绍了论文的选题背景、安全协议的发 展现状，电子商务 B2C模式和交易协议的安全性

30、质以及采用形式化方法分析安全协议的研 究现状 .。第二章在形式化方法的大背景下，介绍了模型检测和模态逻辑。论文通过对几种模 型检测工具进行比较，体现出使用 Spin模型检测工具和使用线性时序逻辑描述系统的特点。 三章是本论文的核心，首先剖析了 Spin工具的原理，重点介绍 Spin的图形界面工具 XSpin 的使用过程。本论文以电子商务 B2C模式为例， 介绍了 B2C模式中涉及到的 4个实体，包 括买家，商户，银行和第三方支付平台；通过形式化描述语言 Promela描述购物流程中不同 实体之间的交互方式，对交易流程中不同实体涉及到的不同交易协议进行形式化分析；用 Spin/Promela对交

31、易流程的 4个模块进行形式化建模，描述了电子商务交易协议的 LTL性质， 并用 XSpin模型 检测工具进行检测，得到了系统中每个实体的状态转移图，在此基础上验证 了电子商务交易协议的可行性和正确性 ，最后通过对交易实体的建模和协议验证结果分析出 电子商务 B2C模式领域潜在的安全隐患。在论文第四章中针对第三章的分析结果提出了一 种基于传统 B2C模式的改进模型，在第三章建立的模型的基础上添加了物流方和第三方隐 私服务器两个实体，进一步规范交易流程、保护用户隐私。最后，第五章对本文的研究工作 进行总结和回顾，并指出未来的进一步工作和尚需完善的研究内容。 第二章理 论框架 2.1形式化方法 2.

32、 1.1形式化方法的发展 形式化方法是数学的长期发展而产生的，通常作为开发软件或硬件系统的数学工具。 20 世纪 60年代末期， Floyd、 Hoare和 Manna等人采用数学方法证明计算机程序正确性的研究 被认为是形式化方法研究领域的开端。 80年代末期， IBM在做 CICS (CustomerInformation Control System)系统更新和升级过程中，利用形式化方法取得了影响广泛的成果。随后， 形式化方法在硬件设计领域取得大量成果，引起了学术研究领域和工业应用领域的高度关 注。这时出现了大量基于形式化方法的相关理论和方法。 90年代开始，形式化方法引起了 计算机教育界

33、的广泛关注。90年代中期，美国在顶尖的 35所大学的计算机学科实施了形式 化方法教育实践。 2001年在欧洲成立了专门的形式化方法教育研究分会。 2004年 5月 “ 软 件工程的形式化方法 ” 被列为一门核心课程。 2004年 11月欧洲形式化方法协会发布了对 11 个国家、 58所高等院校中 的 117门肜式化方法教育相关课程的调研报告 2009年 10 月，微软在北京组织了 Verified Software研讨会，要求工程开发的软件都要用一些基于理论 的工具检查。近年来特别是各种安全攸关和生命攸关的系统许多采用形式化方法支持软件开 发。如交通工具的控制系统、交通指挥调度控制系统、自动化

34、运输系统以及核电站控制系统。 经过近几十年的研究和发展，如今在形式化方法研究领域取得了大量令人嘱目的研究成 果。从早期的一阶谓词演算方法到今天基于代数、进程代数、逻辑、状态机等的多种形式方 法。形式化方法随着研究的深入和支持工具的增多，适用性范围也在逐渐增大。但形式化方 法不是万能的，当前的形式化方法还远远没有发挥出其应有的潜力。 2. 1. 2形式化方法的概念 形式化方法是基于数学和逻辑的方法来规范和验证目标软件系统及其性质。形式 化方法的基本思想是：用无直观内容的抽象符号表示目标软件系统中的任意对象，用由抽象 符号组成的抽象关系表示目标软件系统中任意关系，同时这些对象和关系都只满足公理系统 所描述的逻辑关系。验证过程中只依赖这种逻辑关系而不依赖这些符号的直观含义。把几何 对象和他们的直观意义脱离 ，从而保证了数学推理过程的正确性，能够极大地提高软件的安 全性和可靠性。 形式化方法广义上是指计算机应用系统设计、实现及维护的工程方法。狭义的形式化方 法是指将计算机学科的数学基础理论和计算机应用系统开发结合起来 ,指导工程化地开发计 算机应用系统的方法和技术。运用形式化方法对安全协议的描述和开发过程如图 2-1所示：