基于分层的网络安全协议验证方法

提出了一种新的基于分层的网络安全协议验证方法。首先对要验证的安全属性进行划分,将其分成若干安全子属性;其次对要进行验证的安全协议在安全性等价的条件下进行转换;然后逐步剖分成一个自底向上的多层协议,如果每一层子协议满足所要验证的安全属性的一个子属性,那么这个协议即可被证明是安全的。这种方法相比于传统的验证方法,不但高效,而且完备性更佳。     

Theoretical analysis for communication-induced checkpointingprotocols with rollback-dependency trackability

Rollback-Dependency Trackability (RDT) is a property that states that all rollback dependencies between local checkpoints are on-line trackable by using a transitive dependency vector. In this paper, we address three fundamental issues in the design of communication-induced checkpointing protocols that ensure RDT. First, we prove that the following intuition commonly assumed in the literature is in fact false: If a protocol forces a checkpoint only at a stronger condition, then it must take, at most, as many forced checkpoints as a protocol based on a weaker condition. This result implies that the common approach of sharpening the checkpoint-inducing condition by piggybacking more control information on each message may not always yield a more efficient protocol. Next, we prove that there is no optimal on-line RDT protocol that takes fewer forced checkpoints than any other RDT protocol for all possible communication patterns. Finally, since comparing checkpoint-inducing conditions is not sufficient for comparing protocol performance, we present some formal techniques for comparing the performance of several existing RDT protocols     

基于不变量查找的German协议验证

提出了一种通过查找缓存一致性协议不变量来验证带参协议正确性的新方法.缓存一致性协议验证的难点在于必须证明协议对于任意大小的带参系统都成立.我们通过寻找不变量和协议规则之间的对应关系来计算辅助不变量,从而帮助推导验证缓存一致性协议.我们设计实现了一个不变量查找工具并将该工具应用到German协议上计算它们的辅助不变量并成功地验证了协议的安全性质.     

安全高效的群组密钥协商协议

群组密钥协商(GKA)是保证随后安全通信的重要手段之一。提出了一种新的群组密钥协商协议,在协议中,参与者可以通过一系列算法对其他参与者的真伪进行验证。该协议以较低的计算成本实现参与者安全的会话密钥协商,具备可容错性和长期私钥可重用性的特点。分析表明可抵抗多数常见攻击。     

A simple deniable authentication protocol based on the Diffie–Hellman algorithm

Deniable authentication protocol is a new authentication mechanism in secure computer communication, that not only enables an intended receiver to identify the source of a received message but also prevents a third party from identifying the source of the message. In this paper, based on the Diffie–Hellman algorithm, we propose a new simple deniable authentication protocol from a provably secure simple user authentication scheme. Compared with other deniable authentication protocols, our proposed protocol not only achieves the property of deniable authenticity, but also provides the mutual authentication between the sender and the intended receiver and the confidentiality.     

Deductive verification of the Sliding Window Protocol

We consider the well-known Sliding Window Protocol which provides reliable and efficient transmission of data over unreliable channels. A formal proof of correctness for this protocol faces substantial difficulties, caused by a high degree of parallelism which creates a significant potential for errors. Here we consider a version of the protocol that is based on selective repeat of frames. The specification of the protocol by a state machine and its safety property are represented in the language of the verification system PVS. Using the PVS system, we give an interactive proof of this property of the Sliding Window Protocol.     

一种用于松散耦合的分布式信息系统的身份认证协议

随着计算机网络和信息系统的飞速发展,在现有的异构的信息系统基础上共享信息的要求越来越迫切,本文提出了构造松散耦合的分布式信息系统的方法来解决这个问题,ＬＣＤＩＳ中的一个关键总是就是其安全性。本文首先提出了ＬＣＤＩＳ的概念,并对其进行了形式化的描述。由于ＬＣＩＤＩＳ具有自身的特点,因此不能直接采用 身份认证协议。我们针对其特点,提出了一种专用的身份认证协议。该协议已经成功地用于实际的松散耦合的分布式     

A protocol to achieve independence in constant rounds

Independence is a fundamental property needed to achieve security in fault-tolerant distributed computing. In practice, distributed communication networks are neither fully synchronous or fully asynchronous, but rather loosely synchronized. By this, we mean that in a communication protocol, messages at a given round may depend on messages from other players at the same round. These possible dependencies among messages create problems if we need n players to announce independently chosen values. This task is called simultaneous broadcast. In this paper, we present the first constant round protocol for simultaneous broadcast in a reasonable computation model (which includes a common shared random string among the players). The protocol is provably secure under general cryptographic assumptions. In the process, we develop a new and stronger formal definition for this problem. Previously known protocols for this task required either O(log n) or expected constant rounds to complete (depending on the computation model considered)     

使用组合协议逻辑PCL验证

安全协议的形式化分析和验证一直是信息安全领域的一个重要问题。本文介绍了组合式验证方法以及面向安全协议验证的组合式验证工具PCL,并采用PCL对Amended Needham-Schroeder协议进行了验证,证明该协议满足保密性。在验证中将完整的协议划分为三个子协议,对子协议分别做性质描述和验证,最后将三个子协议组合成完整的协议,通过三个子协议之间前置断言和后置断言的一致性,证明了组合之后的协议满足保密性。     

使用组合协议逻辑PCL验证Amended Needham-Schroeder协议

安全协议的形式化分析和验证一直是信息安全领域的一个重要问题。本文介绍了组合式验证方法以及面向安全协议验证的组合式验证工具PCL,并采用PCL对Amended Needham-Schroeder协议进行了验证,证明该协议满足保密性。在验证中将完整的协议划分为三个子协议,对子协议分别做性质描述和验证,最后将三个子协议组合成完整的协议,通过三个子协议之间前置断言和后置断言的一致性,证明了组合之后的协议满足保密性。     

The cost of becoming anonymous: on the participant payload in Crowds

Crowds is a recently proposed protocol for anonymous communication, which is based on the idea of “blending into a crowd”. Thus, each participant of the crowd gets the benefits of anonymity but also serves as a proxy for other participants. An important measure of the protocol is the participant payload in the system, which is measured by the amount of work a participant needs to pay on serving as a proxy for any communication requested by the participants in the system. In this paper, we derive a precise formula for the participant payload in Crowds, which improves the previous results. Moreover, our result shows the first time that the participant payload in Crowds is entirely independent of the size of the crowd. In consequence, Crowds protocol has a very nice scalability property.     

基于椭圆曲线的单轮零知识证明方案

零知识证明在信息安全领域有着很广泛的应用前景。然而传统的零知识证明方案为了保证方案的正确性需要多轮的迭代,大大增加了交互双方的通信量,使得方案往往不适合实际应用。提出了一种单轮零知识证明的方案,在保证方案正确性、完全性和零知识性的同时将方案运行的迭代次数降低到1,最大程度地减少了方案的通信量。同时将零知识证明扩展到了椭圆曲线上的离散对数问题,提高了方案的安全性。最后给出了构造单轮零知识方案的一个必要条件。     

不同PKG环境下AKE协议的安全性分析

介绍不同PKG环境下的AKE协议，分别对M-B协议及不同PKG环境下的AKE协议进行安全性分析，并指出其存在的安全缺陷。对后者进行改进，提出一个新的在不同PKG环境下的AKE协议。通过启发式分析证明改进协议可以抵抗已知所有攻击，同时通过与其他相关协议的比较可以发现，改进协议具有更好的安全属性。     

ESC: An efficient,scalable, and crypto-less solution to secure wireless networks

In this paper we present ESC: an efficient, scalable, and crypto-less solution for the establishment of a secure wireless network (that is, a network where, for any pair of nodes, there exists a path composed of encrypted links).ESC guarantees the security of the 90% of the network scenario in the presence of 4 global eavesdropper adversaries with about 370 local peer-to-peer communications avoiding both pre-shared secrets and cryptographic functions.The founding block of our proposal is inspired by COKE [1], where the bits of the secret key associated to a link are generated via a multi-round protocol that, at each round, leverages just channel anonymity.Starting from this founding block, we further provide several relevant contributions: we devise a theoretical model and prove a lower bound for the probability to establish a safe-link in the presence of a global eavesdropper adversary. Further, we study the emergent property of network security achieved via the local property of safe-link establishment. To characterize this feature, we introduce two intuitive and useful metrics: network safety and largest safe component, both aimed at capturing the security features provided by ESC.The thorough theoretical analysis of our proposal, the security proof (under the Canetti–Krawczyk model) supporting our key establishment protocol, as well as our extensive simulations showing the effectiveness and efficiency of our protocol for a wide range of network configuration parameters, make our proposal a viable solution to enforce the security of real networks, other than paving the way for further research in this field.     

On the security of fair non-repudiation protocols

We analyzed two non-repudiation protocols and found some new attacks on the fairness and termination property of these protocols. Our attacks are enabled by several inherent design weaknesses, which also apply to other non-repudiation protocols. To prevent these attacks, we propose generic countermeasures that considerably strengthen the design and implementation of non-repudiation protocols. The application of these countermeasures is finally shown by our construction of a new fair non-repudiation protocol.     

基于多比特全同态加密的安全多方计算

本文中,我们首先证明了李增鹏等人提出的多比特多密钥全同态加密方案(MFHE)满足密钥同态性质,利用此性质,可以通过门限解密得到最终解密结果.使用该方案,我们设计了一个在CRS模型下和半恶意攻击者模型下安全的三轮多方计算协议(MPC).该安全多方计算协议的安全性是基于容错学习问题(LWE)的两个变种问题Ferr LWE和Some are errorless.LWE,而且,通过非交互的零知识证明,我们可以把半恶意攻击者模型下安全的三轮多方计算协议转变为在恶意模型下安全的三轮多方计算协议.     

A novel key agreement protocol based on chaotic maps

Based on the semi-group property of Chebyshev chaotic map and some effective improvements of our original protocol, we propose a novel chaotic maps-based key agreement protocol which is proved to be secure, feasible and extensible.     

Connection-oriented multi-channel MAC protocol for ad-hoc networks

This work proposes an on-demand connection-oriented multi-channel MAC protocol for ad-hoc networks. The major features of the proposed protocol are as follows: (a) each mobile node is equipped with only two network interfaces; (b) MAC layer broadcast primitive is supported; and (c) no time synchronization is required. Compared with other multi-channel MAC protocols, the proposed protocol reduces the cost of channel negotiation by considering the property that a connection typically generates multiple packets for transmitting. The NS-2 is used to evaluate the performance of the proposed protocol. Simulation results indicate that the proposed protocol can reduce the cost of channel negotiation and increase the network throughput.     

A routing protocol for anycast messages

An anycast packet is one that should be delivered to one member in a group of designated recipients. Using anycast services may considerably simplify some applications. Little work has been done on routing anycast packets. In this paper, we propose and analyze a routing protocol for anycast message. It is composed of two subprotocols: the routing table establishment subprotocol and the packet forwarding subprotocol. In the routing table establishment subprotocol, we propose four methods (SSP, MIN-D, SET, and GET) for enforcing an order among routers for the purpose of loop prevention. These methods differ from each other on information used to maintain orders, the impact on QoS, and the compatibility to the existing routing protocols. In the packet forwarding subprotocol, we propose a Weighted-Random Selection (WRS) approach for multiple path selection in order to balance network traffic. In particular, the fixed and adaptive methods are proposed to determine the weights. Both of them explicitly take into account the characteristics of distribution of anycast recipient group while the adaptive method uses the dynamic information of the anycast traffic as well. Correctness property of the protocol is formally proven. Extensive simulation is performed to evaluate our newly designed protocol. Performance data shows that the loop-prevention methods and the WRS approaches have great impact on the performance in terms of average end-to-end packet delay. In particular, the protocol using the SET or CBT loop-prevention methods and the adaptive WRS approach performs very close to a dynamic optimal routing protocol in most cases     

优先级顶协议的形式化验证

优先级顶协议是一种优先级驱动的抢占式调度协议,它具有无死锁和单阻塞的性质.Dang Van Hung 和Philip Chan在文献[6]中形式地规范和验证了这两个性质.但他们没有对状态函数HiPripcp明确定义,这使得验证的细节较难理解.为了解决这个问题,提出了一种新的方法来验证优先级顶协议单阻塞的性质.通过时段演算的方法,对优先级顶协议进行了规范,并给出了状态函数HiPripcp的明确定义.根据优先级顶协议的规范,形式地验证了该协议的单阻塞性质.采用的验证方法更少地依赖于HiPripcp,这使得验证的细节更易于理解.此外,提出的验证方法可被应用于实时数据库系统中类似协议的形式化验证.