共查询到20条相似文献,搜索用时 125 毫秒
1.
给出了一种离线TTP公平非否认协议的分析方法,离线TTP公平非否认协议得到了广泛的研究,针对离线TTP公平非否认协议的分析并不是那么广泛.针对离线TTP公平非否认协议具有协议簇的特点,将协议实例化,实例化后可以对单个协议实例的非否认性和有效性进行分析;通过扩展Kailar逻辑,增加时间相关限定词来表述协议的执行序列,用协议执行序列来表达和分析协议的公平性和时效性.利用该方法,对两种公平非否认协议进行分析,分析的结果表明CCD不符合公平性,而ZG的时效性不能够得到满足. 相似文献
2.
崔楠 《计算机与信息技术》2009,(5)
非否认性是考量电子商务协议的重要方面。SVO逻辑以其简洁的特点在协议的安全性验证方面被广泛应用。本文通过对SVO逻辑分析推理规则进行扩展,将其运用到对电子商务协议的非否认性的验证上,对CMP1进行了形式化分析。形式化分析的结果表明CMP1满足非否认性。 相似文献
3.
不可否认协议时限性的形式化分析 总被引:8,自引:0,他引:8
虽然SVO逻辑由于其简单性在对不可否认协议的形式化分析中得到了广泛的应用,但它在时间描述能力上的不足使得它无法分析不可否认协议的时限性.通过向SVO逻辑添加一种简单的时间表达和分析方法扩展了SVO逻辑,并使用扩展后的逻辑对Zhou和Gollmann于1996年提出的一个公平不可否认协议及其一个改进协议进行了分析.分析结果表明,原协议不具有时限性,而改进协议具有时限性,因此也说明了扩展后的新逻辑能够分析不可否认协议的时限性.另外,新逻辑还能用来分析一般密码协议中的时间相关性质. 相似文献
4.
为了将密码协议的非否认性和公平性统一在一个框架之下更好地进行分析,提出了一套适用于分析非否认性和公平性的一阶逻辑语法和语义。在此基础上建立了一个用于分析非否认性和公平性的一阶逻辑模型,并以Fair ZG非否认协议为例进行了分析,发现了该协议的一个已知攻击,证明了模型的有效性和正确性。 相似文献
5.
一种新型的非否认协议 总被引:16,自引:3,他引:16
在克服一种非否认协议草案的缺陷的基础上,提出一种新的非否认协议.新的协议可以在不安 全和不可靠的信道上工作,并能对付各种欺骗行为.此外,还对SVO逻辑进行扩充,引进一些新 的概念和方法,并用扩展后的SVO逻辑分析与证明新的非否认协议. 相似文献
6.
7.
8.
UCSA(Universally Composable Symbolic Analysis)框架结合了形式化分析方法和UC框架。在前人的基础上继续扩展UCSA框架的适用范围。为了使该框架能够分析发送者非否认协议,提出发送者非否认性的理想功能和形式化定义,利用分析执行序列和构造模拟进程的方法分析两者在UCSA框架下的可靠性和完备性。结果表明两者在UCSA框架下是等价的。 相似文献
9.
在介绍Kim公平非否认协议的基础上,分析了LSG协议,指出协议中存在因消息重放而导致不公平的情况,提出了一个改进后的协议,并用新的Kailar逻辑对新协议的公平性和可追究性进行了分析。 相似文献
10.
11.
不可否认协议必须满足存活性、不可否认性、公平性和时限性,但当前大多数形式化方法只能分析该类协议的部分性质,证明或证伪协议逻辑的部分正确性.本文通过向ZQZ逻辑添加时间表达式,提出了一种适用于不可否认协议建模与分析的扩展ZQZ逻辑方法,包括推理规则和安全性质模型.展示新方法的应用时,使用其分析了ZG和KPB这两个局部逻辑正确性已知的两方不可否认协议,以及YLL这个逻辑正确性尚在讨论的基于区块链的多方不可否认协议.实验显示,对前两个协议的分析结果与既有事实相符,对第三个协议的分析发现其无法为收方提供设计者所宣称的时限性.以上结论从逆向工程角度佐证了扩展ZQZ逻辑方法是一种行之有效的不可否认协议分析新方法. 相似文献
12.
13.
一种分析Timed-Release公钥协议的扩展逻辑 总被引:6,自引:0,他引:6
在Coffey和Saidha提出的CS逻辑(CS逻辑将时间与逻辑结构相结合,可用于形式化分析Timed-release公钥协议的时间相关性秘密的安全性)的基础上,提出了CS逻辑的扩展逻辑,它更好地反映了Timed-release公钥协议的特性,并对一个协议实例进行了有效的形式化分析. 相似文献
14.
15.
移动电子商务协议的形式化分析和验证是近年来移动电子商务协议的一个重要研究热点。以一个支付网关为中心的匿名的移动电子商务支付协议PCMS为研究对象,建立了PCMS协议的时间自动机模型,并用计算树逻辑CTL公式描述PCMS协议的部分性质,最后利用模型检测工具UPPAAL对PCMS协议的无死锁、时效性、有效性和钱原子性进行检测验证。验证结果表明,以支付网关为中心的匿名的安全支付协议PCMS满足无死锁、时效性、有效性和钱原子性。 相似文献
16.
多方不可否认协议需要满足不可否认性、公平性和时限性三大安全目标,但是现有的对多方不可否认协议的形式化分析方法大多是对两方协议分析方法的简单扩展,单一方法不能完整覆盖所有的安全目标分析;同时,对单一安全目标的分析能力有限,分析结果不可靠。首先,综合比较现有的分析技术,选定SVO逻辑进行扩展,显式引入时间因素,给出对应的语法定义和时间演算公理。然后,对改进逻辑的语义模型进行介绍,并证明了逻辑系统的可靠性,使得改进后的逻辑系统支持对多方不可否认协议三大安全目标的分析。最后,选取一个典型的多方不可否认协议,分别对其时限性和公平性进行分析,发现了其中存在的时限性和公平性缺陷,并给出了对应的攻击方法。其中,公平性缺陷是首次被发现。 相似文献
17.
18.
SU Kaile Xiao Yinyin Chen Qingliang Lin Han 《Frontiers of Computer Science in China》2007,1(2):191-199
The formal methods for security protocols guarantee the security properties of protocols. Instantiation Space Logic is a new
security protocol logic, which has a strong expressive power. Compositional Logic is also a useful security protocol logic.
This paper analyzes the relationship between these two logics, and interprets the semantics of Compositional Logic in Instantiation
Space model. Through our work, the interpreted Compositional Logic can be extended more easily. Moreover, those security protocols
described in Compositional Logic can be automatically verified by the verifier of Instantiation Space. The paper also proves
that the expressive power of Instantiation Space Logic, which can not be completely interpreted by Compositional Logic, is
stronger than Compositional Logic. 相似文献
19.
Along with advancement of communication systems, the demand for fault-tolerance and real-time performance for communication protocols continues to increase. Communication protocols which perform recovery from any abnormal state to a normal state are called self-stabilizing protocols. However, in these protocols, real-time recovery is not taken into consideration. This paper discusses verification of communication protocols which have self-stabilizing and timeliness properties, which are called responsive protocols.Gouda et al. proposed a mathematical method to prove whether a given protocol specification satisfies the self-stabilizing property. However, this method is not automated and does not verify the timeliness property. This paper thus proposes an automated method for verification of responsive protocols. In this method, communication protocols are modeled by extended finite state machines and their states are represented by predicates. The self-stabilizing property is proven by verifying that sequences of such states which start from an arbitrary abnormal state converge in a normal state. Also, the timeliness property is proven by verifying that the convergence is done within a priori given time. 相似文献
20.
In certified email (CEM) protocols, trusted third party (TTP) transparency is an important security requirement which helps to avoid bad publicity as well as protecting individual users’ privacy. Cederquist et al. proposed an optimistic certified email protocol, which employs key chains to reduce the storage requirement of the TTP. We extend their protocol to satisfy the property of TTP transparency, using existing verifiably encrypted signature schemes. An implementation with the scheme based on bilinear pairing makes our extension one of the most efficient CEM protocols satisfying strong fairness, timeliness, and TTP transparency. We formally verify the security requirements of the extended protocol. The properties of fairness, timeliness and effectiveness are checked in the model checker Mocha, and TTP transparency is formalised and analysed using the toolsets µCRL and CADP. 相似文献