信息学院毕业论文格式

1、贵州财经学院信息学院本科毕业论文（设计） 目 录 摘摘 要要. ABSTRACT. 1 绪论绪论.1 1.1 课题背景.2 1.2 我们的工作与本文的组织结构.6 1.2.1 主要工作 .6 1.2.2 本文的组织结构 .6 2 电子商务协议电子商务协议.8 2.1 密码协议.8 2.1.1 密码协议基本概念 .8 2.1.2 密码协议分类 .9 2.1.3 密码协议的安全性 .11 2.1.4 密码协议的设计规范 .12 2.1.5 密码协议的形式化分析 .13 3 电子商务协议的逻辑分析方法及其在公平非否认协议中的应用电子商务协议的逻辑分析方法及其在公平非否认协议中的应用.24 3.1 一

2、阶逻辑.24 3.1.1 简要介绍.25 3.1.2 语法 .26 3.1.3 语义 .26 3.2 BAN 逻辑.27 3.2.1 BAN 逻辑综述.27 3.2.2 BAN 逻辑.27 3.2.3 BAN 逻辑系统中的构造子.28 3.2.4 BAN 逻辑系统中的基本推理规则 .30 3.2.5 基于 BAN 逻辑的认证协议分析.32 3.2.6 一个新的认证协议及其形式化分析 .34 7 结束语结束语.94 7.1 主要研究工作.94 7.2 下一步工作.94 主要参考文献主要参考文献.96 附录附录 A: XXXXX .103 致致 谢谢.104 贵州财经学院信息学院本科毕业论文（设计

3、） I 摘摘 要要 本文主要对逻辑方法与模型检测技术及其在电子商务协议并形式化分析中的应用进行 了系统研究。总的来说，从理论到实践两个层面上研究了电子商务协议的形式化分析的相 关技术，其工作主要有以下几个方面: 1.对电子商务协议的基本理论和基本性质进行了分析和讨论，包括：安全性、保密性、完 整性、可认证性、非否认性、公平性、时效性等，并对其中一些重要性质做新的定义，提 出电子商务协议设计的基本准则。 2.对当前流行的电子商务协议形式化分析方法进行重点研究，包括 BAN 逻辑、Kailar 逻 辑及周卿方法。采用这些较新的形式化分析方法对几个典型协议进行分析，找出设计缺 陷并提出新的公平非否认

4、性协议。 3.研究了电子商务协议的形式化建模方法：有限自动机、Petri 网、Kripke 结构等，分别 对几个典型电子商务协议进行分析建模。 4.提出利用模型检验工具 SMV 分析验证电子商务协议的安全性、公平性和可追究性等重要 特性的基本框架，对几个典型协议进行了分析验证。 5.研究基于博弈的 ATL 逻辑及其在电子商务协议形式化分析中的应用，进一步扩展了前人 的方法使之在考虑公平性等特性的同时能够分析协议的安全性。同时利用扩展的方法对几 个著名电子商务协议进行全面的形式化分析。 关键词：关键词：电子商务协议，形式化分析，逻辑方法，模型检测，博弈逻辑 贵州财经学院信息学院本科毕业论文（设计

5、） II Abstract The dissertation mainly studies the applications of logic and model checking methods in formal analysis of E-commerce protocols. In general, the author studies the related formal analysis technology of E-commerce protocols from two aspects, theory and applications. The main works and r

6、esults are as follows: 1.Analyzes and discusses the basic theories and characters of E-commerce protocols, includes: security, secrecy, integrity, authentication, non-repudiation, fairness, timeliness and etc. redefine some key significant characters, and bring forward some new rules of E-commerce p

7、rotocols design. 2.Studies the current formal analysis methods for E-commerce protocols: BAN logic、Kailar logic and Zhou-Qing approach. Use the above methods to analyzing some important protocols, find out its limitations and bring forward a new fair non-repudiation protocol. 3.Research the formal m

8、odeling methods of E-commerce protocols: finite state machine, Petri net , Kripke structure and etc. Then analyzed some typical protocols by using these new tools. 4.A new approach was proposed for analyzing the security, non-repudiation and the fairness property of E-commerce protocols, and analyze

9、d some typical protocols from two vital aspects of accountability property and fairness property by using SMV. 5. Discusses ATL(Alternating-time Temporal Logic) logical and its applications in formal analysis of E-commerce protocols, and extend Dr Kremer approach to analyze security of protocols bes

10、ides its fairness. In the end, we stringently formally analyze some typical protocols. Key words: E-commerce Protocols， formal analysis，logic method，Symbolic Model Checking， game logic 贵州财经学院信息学院本科毕业论文（设计） 1 1 绪论绪论 最近几年来，随着计算机与网络技术的飞速发展和广泛应用，使得信息的流通与存取 变得更为快速与便捷。例如:政府积极推进电子政务、企业公司间电子商务(Electronic co

11、mmerce)、个人在线购物(on-line Shopping)、信息家电(Information Appliance)、电 子商务等，这些都是计算机与网络技术的重大应用的结果。因此可以说，在过去的十几年 里，计算机与计算机网络技术带给人类社会的重大影响，不亚于工业革命，意义重大而深 远。 自从美国前总统克林顿发表了“电子商务白皮书”之后，各国都加快步伐来构建电子 商务系统，以迎接全球信息化、网络商业化的到来。冲绳八国集团发表的全球信息化宣言 其核心的内容就是电子商务(Electronic commerce)，据 IDC 公布的数据，全球电子商务 的规模 2003 年已突破 1 万亿美元，20

12、04 年已超过 7.3 万亿美元.“上网的企业不一定能 成功，但不上网的企业将会被淘汰出局”这已经成为大多数人的共识。世界上许多大的公 司都将电子商务列为主要的发展方向。IBM 公司 25%的收入来自于电子商务；CISCO 公司 85%的交易在线完成，电子商务使其销售额增加了 500%，而人员仅增加了 100%，交货期也 由原来的 3 周变为 3 天。电子商务在增加卖方的销售机会的同时，也同样增加了买方购买 的机会，例如企业采购时利用电子商务可以找到新的供应商和贸易伙伴。另外在电子商务 中，讨价和还价的传递也十分快捷。总的看来，美国的电子商务的启动期为 1991-1995, 1996-1999

13、 为其高速增长期，从 2000 年开始进入稳定的成长期。我国政府也积极推动电 子商务发展，1997 年 10 月，标志着中国政府在电子商务领域实质性突破的“中国商品交 易网”正式开通.中国人民银行己建成了全国认证中心。可以这样认为，1996-1999 年为 启动期，从 1999 年开始进入高速增长期，而后随着网络经济的“泡沫”现象，全球的电 子商务活动暂时陷入了“寒冬” ，现已恢复进入了健康的发展阶段。 1.1 课题背景 密码协议是以密码学为基础的消息交换协议，其目的是在网络环境中提供各种安全服 务1。安全目标是多种多样的。例如，认证协议的目标是认证参加协议的主体的身份。此 外，许多认证协议还

14、有一个附加的目标，即在主体之间安全地分配密钥或其他各种秘密。 密码协议的主要目的是利用密码技术实现密钥交换、身份认证和安全支付，在安全领域中 贵州财经学院信息学院本科毕业论文（设计） 协议同密码算法同样重要。若密码算法十分先进，但密码协议的设计有缺陷，该密码体系 仍存在严重的安全隐患。当前关于安全问题的研究热点之一是涉及密钥分布、身份验证、 数字签名和公证的密码协议的建模与形式化分析1。 2 2 电子商务协议电子商务协议 2.1 密码协议 2.1.1密码协议基本概念 密码协议是密码参与者采取的一系列步骤，它包括两方或多方密码参与者，设计它的目 的是要完成一项任务。 “一系列步骤”意味着协议是从

15、开始到结束的一个序列，每一步必须 按严格的规定依次执行，在前一步完成前，后面的步骤都不能执行 ；“包括两方或多方” 意味着完成这个协议至少需要两个人，单独的一个人不能构成协议，当然单独的一个人也可 采取一系列步骤去完成一个任务，但这不是协议（另外一些人必须完成某件事才构成协议） ； 最后， “设计它的目的是要完成一项任务”意味着协议必须做一些事。有些东西看起来像协 议，但不完成一个任务，那也不是一个完整的协议，只是浪费时间而已2。 为了分析方便和书写统一，我们对本书中用到的关于协议形式分析中的符号说明如表 2-1 所示： 表表 2-1 协议形式分析中的符号说明协议形式分析中的符号说明 A Sy

16、stem principal A ( Alice ) B System principal B (Bob) S Trusted Server AB: m A sending a message m to B m 可放箭头 上 m,n Concatenation of message m and n 可用逗点代 逗号 Ks Public key of the Trusted Server mk Encrypt m using key k mk Decrypt m using key k Bit-wise exclusive-or operation (XOR) 贵州财经学院信息学院本科毕业论文（

17、设计） 2.1.3电子商务协议介绍 本文只考虑协议的非否认性和公平性，假定协议是安全的，并不引入第三方攻击者模型， 因而参与协议的主体集合为：付款人 A，收款人 B、货币服务方 CS 。其中货币服务方 CS 是诚实公正的，将严格执行协议运行，而 A 和 B 则不一定诚实有可能为了自己的利益中断协 议执行。协议中三个参与主体在 SMV 系统中都对应一个 FSM, 这三个 FSM 在同一 MODULE 之内， 每个主体都是这个 MODULE 的一个实例(Instance),这三个实例分别为 Payer，Payee 和 CoinService。在协议运行的时候，每个主体选择各自相应的自动机运行，其状

18、态转移图分 别示于图 2-1、图 2-2 和图 2-3（其中，！表示发送消息；？表示接收消息） 。 图 2-1 付款人 A 的状态转换图 7 7 结束语结束语 形式化描述方法是连接协议工程各个阶段的纽带，是协议工程中的核心问题。电子商务 协议是实现电子商务的重要技术基础，而安全性、公平性和可追究性又是电子商务协议安全 中最重要的性质。基于逻辑的形式分析方法已成为目前电子商务协议研究的主要热点，也是 设计电子商务协议中值得研究的重要课题。 本章将对全文的研究工作及创新点进行总结，并且提出一些需要进一步深入研究的问题。 7.1 主要研究工作 7.2 下一步工作 贵州财经学院信息学院本科毕业论文（设

19、计） 参考文献 1 Bruce Schneier. Applied Cryptography: Protocols, Algorithms, and Source Code in C, Second Edition. John Wiley Communications of the ACM, 21(12), 1978, 993-999; reprinted in Advances in computer security, Ed. R. Turn, Dedham, MA: Artech House, 1988. 4 卿斯汉.安全协议 20 年研究进展J.软件学报,2003,14(10):1740-1752. 5 卿斯汉.信息系统的安全M.北京:科学出版社,2003:47-67. 6 J.Zhou and D.G