博士论文答辩电子商务协议形式化方法及模型检测技术的研究与应用.ppt

博士论文答辩电子商务协议形式化方法及模型检测技术的研究与应用 博士生： 文静华 导 师： 李 祥贵州大学计算机软件与理论研究所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