- 1、本文档共44页,可阅读全部内容。
- 2、有哪些信誉好的足球投注网站(book118)网站文档一经付费(服务费),不意味着购买了该文档的版权,仅供个人/单位学习、研究之用,不得用于商业用途,未经授权,严禁复制、发行、汇编、翻译或者网络传播等,侵权必究。
- 3、本站所有内容均由合作方或网友上传,本站不对文档的完整性、权威性及其观点立场正确性做任何保证或承诺!文档内容仅供研究参考,付费前请自行鉴别。如您付费,意味着您自己接受本站规则且自行承担风险,本站不退款、不进行额外附加服务;查看《如何避免下载的几个坑》。如果您已付费下载过本站文档,您可以点击 这里二次下载。
- 4、如文档侵犯商业秘密、侵犯著作权、侵犯人身权等,请点击“版权申诉”(推荐),也可以打举报电话:400-050-0827(电话支持时间:9:00-18:30)。
查看更多
博士论文答辩电子商务协议形式化方法及模型检测技术的研究与应用
博士论文答辩电子商务协议形式化方法及模型检测技术的研究与应用 博士生: 文静华 导 师: 李 祥贵州大学计算机软件与理论研究所2006. 5 内容提要 1.论文的背景 2.本文的主要工作与创新点 3.电子商务协议的逻辑分析方法 4.电子商务协议的模型检测技术 5.基于博弈逻辑的电子商务协议形式化分析 6.攻读博士学位期间发表和完成的论文 1.论文的背景 电子商务发展的需要 电子商务协议形式化分析的需要 ……. 2.本文的主要工作与创新点 1、研究电子商务协议的基本理论和基本性质:安全性、必威体育官网网址性、完整性、可认证性、非否认性、公平性、时效性等,并对其中一些重要性质做新的定义,提出电子商务协议设计的基本准则。 2、对当前流行的电子商务协议形式化分析方法进行重点研究,采用当前较新的形式化分析方法对几个典型协议进行分析,找出设计缺陷并提出新的公平非否认性协议。 3、研究电子商务协议的建模方法:有限自动机、Petri网结构等,分别对几个电子商务协议进行分析建模。 4、研究电子商务协议的模型检验方法,采用当前较新的模型检验方法(SMV)对几个典型协议进行分析。 5、研究基于博弈的ATL逻辑及其在电子商务协议形式化分析中的应用,进一步扩展了前人的方法使之在考虑公平性等特性的同时能够分析协议的安全性。同时利用扩展的方法对几个著名电子商务协议进行全面的形式化分析。对ZDB协议(1999)进行分析,发现该协议在非必威体育官网网址通道下存在两个可能的攻击:对Zhou-Gollmann协议(1999)进行分析,发现该协议存在不满足必威体育官网网址性、公平性及适时终止性的缺陷。 3.电子商务协议的逻辑分析方法 BAN逻辑 GNY逻辑 SVO逻辑 Kailar逻辑 周—卿方法 Kailar逻辑的缺陷及卿斯汉教授等人的改进 Kailar逻辑缺陷: 不能分析协议的公平性 非形式化的初始化假设可能导致协议分析的失败 无法理解包含签名密文的协议语句 周—卿方法 初始拥有集合 最终拥有集合 六条推理规则 4个推理步骤 NCP协议及其分析 通信协议 1) 2) 3) 仲裁协议 当接收者B否认收到消息时,发送者A请求C裁决,C根据一定的规则进行裁决 NCP协议的问题 我们认为NCP协议的主要潜在问题在于仲裁协议部分,当通信服务频繁时, 仲裁中心的负荷可能过重,另外仲裁中心保留多少仲裁信息以及保留时间多长都是很难确定的问题。由于通信双方没有主动掌握对方可追究证据,协议的公平性完全依赖于仲裁中心。 改进的协议NCP′ 1) 2) 3) 4) 5) 分析结果 经过使用周—卿方法分析,新的协议满足可追究和公平性原则,且可以工作在不安全和不可靠的信道上。 4.电子商务协议的模型检测技术 模型检测技术 时序逻辑 分枝时序逻辑CTL SMV NuSMV 模型检测的过程 模型检测包括以下几个过程: a) 建模 b) 规格说明 c) 验证 d) 分析 SMV的工作原理 ISI协议分析与验证 ISI支付协议是由Medvinsky和Neuman提出来的,其目的是付款人A向收款人B付款,整个付款过程中付款人A保持匿名。在协议中,除了付款人A和收款人B之外还有双方都信任的货币服务方CS。 协议消息的描述 为了描述ISI协议中的消息,我们构造记录类型message如下: typedef message struct{ messagetype:{Start, m1, m2, m3, m4, m5, m6, End}; key:{ ,,,,,,,,,,,}; Content:{coins,transaction,amount,Tid,date}; POO: ; POR: ; } 其中,POO、POR分别为发方非否认证据和收方非否认证据,Content为消息数据域,messagetype为消息类型域, key为密钥域。 协议的有限状态系统模型 协议的有限状态系统模型 协议的有限状态系统模型 服务机构CS的状态转换图 协议属性的CTL描述 (1)?非否认性 本协议中发方非否认证据和收方非否认证据分别为: POO: POR: 协议满足非否认性即要求:在协议结束时,付款人收到POR而收款人收到POO,用CTL描述为: AF(Payer.A_Rec_POR0),AF(Payee.B_Rec_POO 0)。 (2) 公平性 协议的公平性要求不论协议终止于任何阶段,付款人收到POR必须当且仅当收款人收到POO,收发双方始终处于平等地位,用CTL描述为: AG(Payer
您可能关注的文档
最近下载
- 装饰装修工程施工组织方案设计[技术标].docx
- 2024-2025学年河南省郑州市管城区五年级(上)期末语文试卷(全解析版).docx
- 2024子宫内膜癌分子分型临床应用中国专家共识(完整版) .pdf
- 膀胱癌讲课图文ppt课件.ppt
- 2023-2024学年湖南长沙长郡中学八年级物理第一学期期末教学质量检测试题含解析.pdf VIP
- 2024年重庆高考化学试卷(解析版).docx
- 三星数码相机 SAMSUNG WB110说明书.pdf
- DG∕T J 08-2004A-2014_太阳能热水系统应用技术规程.pdf
- 电动车棚施工协议集合4篇.docx
- 浅析工程造价管理与投资控制.pdf VIP
文档评论(0)