资源描述
摘要本文主要对逻辑方法与模型检测技术及其在电子商务协议并形式化分析中的应用进行了系统研究。总的来说，从理论到实践两个层面上研究了电子商务协议的形式化分析的相关技术，其工作主要有以下几个方面:1.对电子商务协议的基本理论和基本性质进行了分析和讨论，包括：安全性、保密性、完整性、可认证性、非否认性、公平性、时效性等，并对其中一些重要性质做新的定义，提出电子商务协议设计的基本准则。五号、宋体、1.5倍行间距2.对当前流行的电子商务协议形式化分析方法进行重点研究，包括BAN逻辑、Kailar逻辑及周卿方法。采用这些较新的形式化分析方法对几个典型协议进行分析，找出设计缺陷并提出新的公平非否认性协议。五号、宋体、用逗号分隔关键词：电子商务协议，形式化分析，逻辑方法，模型检测，博弈逻辑四号、黑体、加粗四号，TimesNewRoman加粗、居中AbstractThe 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 results 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 protocols 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.五号，TimesNewRoman，用逗号分隔开五号，TimesNewRoman加粗Keywords：E-commerce Protocols, formal analysis, logic method, Symbolic Model Checking, game logic目录 摘要IAbstractII1.绪论11.1课题背景12.电子商务协议22.1密码协议27 结束语37.1 主要研究工作37.2 下一步工作3参考文献4致 谢5附录1:参考文献基本格式1附录2:论文目录和页码的设置方法4 一级标题 四号 宋体 加粗1.绪论 正文部分宋体 五号字 1.5倍行距，段首缩进两个字符最近几年来，随着计算机与网络技术的飞速发展和广泛应用，使得信息的流通与存取变得更为快速与便捷。例如:政府积极推进电子政务、企业公司间电子商务(Electronic commerce)、个人在线购物(on-line Shopping)、信息家电(Information Appliance)、电子商务等，这些都是计算机与网络技术的重大应用的结果。因此可以说，在过去的十几年里，计算机与计算机网络技术带给人类社会的重大影响，不亚于工业革命，意义重大而深远。二级标题 宋体 五号 加粗自从美国前总统克林顿发表了“电子商务白皮书”之后，各国都加快步伐来构建电子商务系统，以迎接全球信息化、网络商业化的到来。冲绳八国集团发表的全球信息化宣言其核心的内容就是电子商务(Electronic commerce)，据IDC公布的数据，全球电子商务的规模2003年已突破1万亿美元，2004年已超过7.3万亿美元.“上网的企业不一定能成功，但不上网的企业将会被淘汰出局”这已经成为大多数人的共识。世界上许多大的公司都将电子商务列为主要的发展方向。IBM公司25%的收入来自于电子商务；CISCO公司85%的交易在线完成，电子商务使其销售额增加了500%，而人员仅增加了100%，交货期也由原来的3周变为3天。电子商务在增加卖方的销售机会的同时，也同样增加了买方购买的机会，例如企业采购时利用电子商务可以找到新的供应商和贸易伙伴。另外在电子商务中，讨价和还价的传递也十分快捷。总的看来，美国的电子商务的启动期为1991-1995, 1996-1999为其高速增长期，从2000年开始进入稳定的成长期。我国政府也积极推动电子商务发展，1997年10月，标志着中国政府在电子商务领域实质性突破，1996-1999年为启动期，从1999年开始进入高速增长期，而后随着网络经济的“泡沫”现象，全球的电子商务活动暂时陷入了“寒冬”，现已恢复进入了健康的发展阶段。1.1课题背景密码协议是以密码学为基础的消息交换协议，其目的是在网络环境中提供各种安全服务1。安全目标是多种多样的。例如，认证协议的目标是认证参加协议的主体的身份。此外，许多认证协议还有一个附加的目标，即在主体之间安全地分配密钥或其他各种秘密。密码协议的主要目的是利用密码技术实现密钥交换、身份认证和安全支付，在安全领域中协议同密码算法同样重要。若密码算法十分先进，但密码协议的设计有缺陷，该密码体系仍存在严重的安全隐患。当前关于安全问题的研究热点之一是涉及密钥分布、身份验证、数字签名和公证的密码协议的建模与形式化分析1。 2.电子商务协议2.1密码协议密码协议基本概念密码协议是密码参与者采取的一系列步骤，它包括两方或多方密码参与者，设计它的目的是要完成一项任务。“一系列步骤”意味着协议是从开始到结束的一个序列，每一步必须按严格的规定依次执行，在前一步完成前，后面的步骤都不能执行 ；“包括两方或多方”意味着完成这个协议至少需要两个人，单独的一个人不能构成协议，当然单独的一个人也可采取一系列步骤去完成一个任务，但这不是协议（另外一些人必须完成某件事才构成协议）；最后，“设计它的目的是要完成一项任务”意味着协议必须做一些事。有些东西看起来像协议，但不完成一个任务，那也不是一个完整的协议，只是浪费时间而已2。为了分析方便和书写统一，我们对本书中用到的关于协议形式分析中的符号说明如表2-1所示：表名称位于表格上方 宋体，五号 居中 表2-1 协议形式分析中的符号说明A System principal A ( Alice )B System principal B (Bob)S Trusted ServerAB: m A sending a message m to B m可放箭头上m,n Concatenation of message m and n 可用逗点代逗号Ks Public key of the Trusted Servermk Encrypt m using key kmk Decrypt m using key k Bit-wise exclusive-or operation (XOR) 三级标题 宋体 五号2.1.3 电子商务协议介绍本文只考虑协议的非否认性和公平性，假定协议是安全的，并不引入第三方攻击者模型，因而参与协议的主体集合为：付款人A，收款人B、货币服务方CS 。其中货币服务方CS是诚实公正的，将严格执行协议运行，而A和B则不一定诚实有可能为了自己的利益中断协议执行。协议中三个参与主体在SMV系统中都对应一个FSM, 这三个FSM在同一MODULE之内，每个主体都是这个MODULE的一个实例(Instance),这三个实例分别为Payer，Payee和CoinService。在协议运行的时候，每个主体选择各自相应的自动机运行，其状态转移图分别示于图2-1、图2-2和图2-3（其中，！表示发送消息；？表示接收消息）。图名称位于图示下方 宋体，五号，居中 图2-1 付款人A的状态转换图7 结束语形式化描述方法是连接协议工程各个阶段的纽带，是协议工程中的核心问题。电子商务协议是实现电子商务的重要技术基础，而安全性、公平性和可追究性又是电子商务协议安全中最重要的性质。基于逻辑的形式分析方法已成为目前电子商务协议研究的主要热点，也是设计电子商务协议中值得研究的重要课题。本章将对全文的研究工作及创新点进行总结，并且提出一些需要进一步深入研究的问题。7.1 主要研究工作7.2 下一步工作参考文献1 昂温 G，昂温P S外国出版史M陈生铮，译北京：中国书籍出版社，1988 2 马克思关于工资、价格和利润的报告札记M/马克思，恩格斯马克思恩格斯全集：第44卷北京：人民出版社，1982：505 3 中国地质学会地质论评J1936，1（1）北京：地质出版社，1936四号、黑体、加粗、居中 4 李炳穆理想的图书馆员和信息专家的素质与形象J图书情报工作，2000(2)：5-8 5 姜锡洲一种温热外敷药制备方案：中国，88105607.3P1989-07-26中文采用：五号宋体；英文采用：五号Times NewRoman段落采用1.5倍行距 6 METCALF S W. The Tort Hall air emission study C/OL/ The International Congress on Hazardous Waste, Atlantic Marriott Marquis Hotel, Atlanta, Georgia, June 5-8, 1995: Impact on human and ecological health1998-09-22. http: / atsdrl.astdr.cdc.gov: 8080/Cong95.html.四号、黑体、加粗、居中致 谢 附录1:参考文献基本格式 一、参考文献是对期刊论文引文进行统计和分析的重要信息源之一 ，在本规范中采用 GB 7714推荐的顺序编码制编排。 二、参考文献著录项目 a. 主要责任者 (专著作者、论文集主编、学位申报人、专利申请人、报告撰写人、期刊文章作者、析出文章作者)。多个责任者之间以“，”分隔，注意在本项数据中不得出现缩写点“.”。主要责任者只列姓名，其后不加“著”、“编”、“主编”、“合编”等责任说明。 b. 文献题名及版本(初版省略)。 c. 文献类型及载体类型标识。 d. 出版项(出版地、出版者、出版年)。 e. 文献出处或电子文献的可获得地址。 f. 文献起止页码。 g. 文献标准编号(标准号、专利号)。 三、参考文献类型及其标识 1、根据 GB 3469规定，以单字母方式标识以下各种参考文献类型：参考文献类型专著论文集报纸文章期刊文章学位论文报告标准专利文献类型标识MCNJDRSP注：M（Monograph）,C(Collection),N(Newspaper),J(Journal),D(Dissertation),R(Report), S(Standard),P(Patent).2、对于专著、论文集中的析出文献，其文献类型标识建议采用单字母“A”；对于其他未说明的文献类型，建议采用单字母“Z”。 3、对于数据库 (database) 、计算机程序 (computer program) 及电子公告 (electronic bulletin board)等电子文献类型的参考文献，建议以下列双字母作为标识： 电子参考文献类型数据库计算机程序电子公告电子文献类型标识DBCPEB4、电子文献的载体类型及其标识 对于非纸张型载体的电子文献，当被引用为参考文献时需要在参考文献类型标识中同时标明其载体类型 。本规范建议采用双字母表示电子文献载体类型：磁带(magnetic tape)MT，磁盘(disk)DK，光盘(CD-ROM)CD，联机网络(online)OL，并以下列格式表示包括了文献载体类型的参考文献类型标识： 文献类型标识/载体类型标识 如：DB/OL联机网上数据库(database online) DB/MT磁带数据库(database on magnetic tape) M/CD 光盘图书(monograph on CD-ROM) CP/DK磁盘软件(computer program on disk) J/OL 网上期刊(serial online) EB/OL网上电子公告(electronic bulletin board online) 以纸张为载体的传统文献在引作参考文献时不必注明其载体类型。 四、文后参考文献表编排格式 参考文献按在正文中出现的先后次序列表于文后；表上以 “参考文献：”(左顶格)或 “参考文献” (居中)作为标识；参考文献的序号左顶格，并用数字加方括号表示，如1、2、，以与正文中的指示序号格式一致 。参照ISO 690及ISO 690-2，每一参考文献条目的最后均以“.”结束。各类参考文献条目的编排格式及示例如下： a. 专著、论文集、学位论文、报告序号 主要责任者. 文献题名 文献类型标识. 出版地： 出版者， 出版年. 起止页码(任选). 1刘国钧， 陈绍业，王凤翥. 图书馆目录M. 北京：高等教育出版社，1957. 15-18. 2辛希孟. 信息技术与信息服务国际研讨会论文集：A集C.北京： 中国社会科学出版社，1994. 3张筑生. 微分半动力系统的不变集D. 北京：北京大学数学系数学研究所，1983.4冯西桥. 核反应堆压力管道与压力容器的LBB分析R. 北京 ：清华大学核能技术设计研究院，1997. b. 期刊文章 序号 主要责任者.文献题名J. 刊名，年，卷(期)： 起止页码. 5何龄修. 读顾城南明史J. 中国史研究，1998，(3)：167-173. 6金显贺，王昌长，王忠东，等. 一种用于在线检测局部放电的数字滤波技术 J. 清华大学学报(自然科学版)， 1993， 33(4)： 62-67. c. 论文集中的析出文献序号 析出文献主要责任者. 析出文献题名 A. 原文献主要责任者(任选) . 原文献题名 C. 出版地：出版者，出版年. 析出文献起止页码.7钟文发. 非线性规划在可燃毒物配置中的应用A. 赵玮. 运筹学的理论与应用中国运筹学会第五届大会论文集C. 西安：西安电子科技大学出版社，1996. 468-471. d.报纸文章序号 主要责任者. 文献题名 N. 报纸名，出版日期 (版次). 8 谢希德. 创造学习的新思路N. 人民日报，1998-12-25(10). e. 国际、国家标准 序号 标准编号，标准名称S. 9 GB/T 16159-1996，汉语拼音正词法基本规则S. f.专利 序号 专利所有者. 专利题名 P. 专利国别：专利号，出版日期. 10 姜锡洲. 一种温热外敷药制备方案 P. 中国专利：881056073，1989-07-26. g.电子文献 序号 主要责任者.电子文献题名 电子文献及载体类型标识.电子文献的出处或可获得地址，发表或更新日期/引用日期(任选). 11 王明亮. 关于中国学术期刊标准化数据库系统工程的进展 EB/OL. http:/www. 1998-08-16/1998-10-04. 12万锦坤. 中国大学学报论文文摘(1983-1993). 英文版 DB/CD. 北京:中国大百科全书出版社，1996. h.各种未定义类型的文献 序号 主要责任者.文献题名 Z. 出版地：出版者，出版年. 五、参考文献与注释的区别 参考文献是作者写作论著时所参考的文献书目，一般集中列表于文末；注释是对论著正文中某一特定内容的进一步解释或补充说明 ，一般排印在该页地脚 。参考文献序号用方括号标注，而注释用数字加圆圈标注(如、)。附录2:论文目录和页码的设置方法毕业论文写完后，要设置页码和生成目录。步骤如下：1、 封面封面不设置页码。点击菜单栏的“插入”“页码”取消“首页显示页码”中的绿“确定”。2、 内页的页码设置内页一般包含“致谢”、“中英文摘要”、“中英文关键词”和“目录”。可分别对这四个项目设置页码。光标固定在“致谢”页的“致谢”前或后，点击菜单栏的“文件”“页面设置”“页边距”找到“预览应用于（Y）:”，选择“本节”“确定”；点击菜单栏的“插入”“页码”“格式”“数字格式（F）:”，选择罗马数字找到“页码编排”，点击“起始页码”，显示“确定”“确定”。其他项目的页码设置方法同上。3、 目录的自动生成方法 “致谢”、“中英文摘要”、“中英文关键词”、“目录”、正文中的一级标题使用一级标题，可分别选定“致谢”、“中英文摘要”、“中英文关键词”、“目录”、正文中的各级标题。方法为：首先选定“致谢”，然后点击工具栏中的“样式”，下拉菜单，选择“标题1”，这样“致谢”就设置为标题1了，然后光标指向设置为标题1的“致谢”后，双击工具栏的“格式刷”，再分别对“摘要”、“关键词”、“目录”、正文中的一级标题进行选定，到此，标题1的设置工作完成。二级标题的设置：先选定一个二级标题，然后点击“样式”，下拉菜单，选择“标题2”，这样选定的二级标题就设置为标题2了。光标固定在已设置为标题2的二级标题上，双击“格式刷”，然后分别对所有二级标题一一选定，这样二级标题的设置工作完成。三级标题（如果还有四级标题和五级标题）的设置方法同前。最后，光标回到目录页，固定在“目录”之后或下面，然后点击菜单栏中的“插入”“引用”“索引和目录（D）”“目录”“确定”。这样目录就自动生成了。还可对自动生成的目录进行字体、字号和行距的调整，先选定已自动生成的目录，然后按照需要进行字体、字号和行距的调整。4、 正文页码设置光标固定在正文页第一页的第一个字符前，点击菜单栏的“文件” “页面设置”“页边距”找到“预览应用于（Y）:”，选择“插入点之后”“确定”；然后点击菜单栏的“插入”“页码”“格式”“数字格式（F）:”，选择阿拉伯数字1 2 3找到“页码编排”，点击“起始页码”，显示1“确定”“确定”。这样正文部分的页码自动生成。5、 附录页码设置设置方法同上。
展开阅读全文