An algebraic approach to the verification of a class of Diffie-Hellman protocols

We present a framework for reasoning about secrecy in a class of Diffie-Hellman protocols. The technique, which shares a conceptual origin with the idea of a rank function, uses the notion of a message-template to determine whether a given value is generable by an intruder in a protocol model. Traditionally, the rich algebraic structure of Diffie-Hellman messages has made it difficult to reason about such protocols using formal, rather than complexity-theoretic, techniques. We describe the approach in the context of the MTI protocols, and derive conditions under which each protocol in the suite can be considered secure.     

Probabilistic verification of communication protocols

Complete behavior of a communication protocol can be very large. It is worth investigating whether partial exploration of the behavior generates reasonable results. We present such a procedure which performs partial exploration using most-probable-first search. Some of the ideas used in this procedure are based on a convolutional decoding procedure due to Jelinek and a performance evaluation procedure due to Rudin. Multiple trees of protocol behavior are constructed. Some results on estimating the probability of encountering an unexplored state in a finite run of a protocol are also presented. Nicholas F. Maxemchuk received the B.S.E.E. degree from the City College of New York, NY, and the M.S.E.E. and Ph.D. degrees from the University of Pennsylvania, Philadelphia. He is the Head of the Distributed Systems Research Department at AT & T Bell Laboratories, Murray Hill, NJ, and has been at AT & T Bell Laboratories since 1976. Prior to joining Bell Laboratories he was at the RCA David Sarnoff Research Center in Princeton, NJ for eight years. Dr. Maxemchuk has been on the adjunct faculties of Columbia University and the University of Pennsylvania. He has been an advisor to the United Nations on data networking and has been on networking panels for the US Air Force and DARPA. He has served as the Editor for Data Communications for the IEEE Transactions on Communications, as a Guest Editor for the IEEE Journal on Selected Areas in Communications, and has been on the program committee for numerous conferences and workshops. He was awarded the RCA Laboratories Outstanding Achievement Award, the Bell Laboratories Distinguished Technical Staff Award, and the IEEE's 1985 and 1987 Leonard G. Abraham Prize Paper Award. Krishan Sabnani received a BSEE degree from Indian Institute of Technology, New Delhi, India and a PhD degree from Columbia University, New York, NY. In 1981, he joined AT & T Bell Laboratories after graduating from Columbia University. He is currently working in the Distributed Systems Research Department of AT & T Bell Laboratories. His major area of interest is communication protocols. Dr. Sabnani was a co-chairman of the Eighth International Symposium on Protocol Specification, Testing, and Verification held in Atlantic City, NJ during June 1988. He is currently an editor of the IEEE Transactions on Communications and of the IEEE Transactions on Computers. He has served on the program committees of several conferences. He is also a guest editor of two special issues of the Journal on Selected Areas in Communications (JSAC) and the Computer Networks and ISDN Systems Journal, respectively.     

An autonomic cloud environment for hosting ECG data analysis services

Advances in sensor technology, personal mobile devices, wireless broadband communications, and Cloud computing are enabling real-time collection and dissemination of personal health data to patients and health-care professionals anytime and from anywhere. Personal mobile devices, such as PDAs and mobile phones, are becoming more powerful in terms of processing capabilities and information management and play a major role in peoples daily lives. This technological advancement has led us to design a real-time health monitoring and analysis system that is Scalable and Economical for people who require frequent monitoring of their health. In this paper, we focus on the design aspects of an autonomic Cloud environment that collects peoples health data and disseminates them to a Cloud-based information repository and facilitates analysis on the data using software services hosted in the Cloud. To evaluate the software design we have developed a prototype system that we use as an experimental testbed on a specific use case, namely, the collection of electrocardiogram (ECG) data obtained at real-time from volunteers to perform basic ECG beat analysis.     

An experience report: porting the MG‐RAST rapid metagenomics analysis pipeline to the cloud

Existing applications in computational biology typically favor a local cluster based integrated computational platform. We present a lessons learned type report for scaling up an existing metagenomics application that outgrew the available local cluster hardware. In our example, removing a number of assumptions linked to tight integration allowed to expand beyond one administrative domain, increase the number and type of machines available for the application, and also improved scaling properties of the application. The assumptions made in designing the computational client make it well suitable for deployment as a virtual machine inside a cloud. This paper discusses the decision process and describes the suitability of deploying various bioinformatics computations to distributed heterogeneous machines. Copyright © 2011 John Wiley & Sons, Ltd.     

Formal verification of mobile robot protocols

Mobile robot networks emerged in the past few years as a promising distributed computing model. Existing work in the literature typically ensures the correctness of mobile robot protocols via ad hoc handwritten proofs, which, in the case of asynchronous execution models, are both cumbersome and error-prone. Our contribution is twofold. We first propose a formal model to describe mobile robot protocols operating in a discrete space i.e., with a finite set of possible robot positions, under synchrony and asynchrony assumptions. We translate this formal model into the DVE language, which is the input format of the model-checkers DiVinE and ITS tools, and formally prove the equivalence of the two models. We then verify several instances of two existing protocols for variants of the ring exploration in an asynchronous setting: exploration with stop and perpetual exclusive exploration. For the first protocol we refine the correctness bounds and for the second one, we exhibit a counter-example. This protocol is then modified and we establish the correctness of the new version with an inductive proof.     

Formal verification of dependable distributed protocols

Dependable distributed systems often employ a hierarchy of protocols to provide timely and reliable services. Such protocols have both dependability and real-time attributes, and the verification of such composite services is a problem of growing complexity even when using formal approaches. Our intention in this paper is to exploit the modular design aspects appearing in most dependable distributed protocols to provide formal level of assurance for their correctness. We highlight the capability of our approach through a case study in formal modular specification and tool-assisted verification of a timestamp-based checkpointing protocol. Furthermore, during the process of verification, insights gained in such a stack of protocols have assisted in validating some additional properties those dealing with failure recovery.     

An experience report on the personal software process

Individual developers can use quality analysis and management techniques that many consider applicable only to projects and organizations. One of the authors, a software practitioner, explains how the personal software process (PSP) gave him the training he needed. The software industry's demand to achieve predictability and consistency in the face of rapid change is significant. The PSP framework helps an individual to meet these demands. Using the PSP has provided the author with several benefits. His estimation accuracy has improved significantly. However, adding more data to his historical database will help further improve his estimating skills. As it is said: “there is no substitute for hard work to be successful”. Similarly, “there is no substitute for more data to improve an individual's personal processes”. The author's current goal is to narrow the percentage error in his estimates to within roughly 5%. He also plans to focus on improving early defect removal through more effective reviews and preventing defects by improving skills and practices     

An autonomic approach for P2P/cloud collaborative environments

The rise of Cloud Computing has progressively dimmed the interest in volunteer and peer-to-peer computing, in general. However, efficient and cost-effective large scale distributed collaborative environments cannot be achieved leveraging upon the Cloud alone. In this paper, we propose a novel hybrid P2P/cloud approach where components and protocols are autonomically configured according to specific target goals, such as cost-effectiveness, reliability and availability. The proposed approach is based on the Networked Autonomic Machine (NAM) framework, which allows distributed system designers to include different kinds of cost and performance constraints. As an example, we show how the NAM-based approach can be used to design collaborative storage systems, enabling the definition of an autonomic policy to decide, according to cost minimization and data availability goals, how to part data chunks among peer nodes and Cloud, based on the local perception of the P2P network.     

基于RSA的零知识水印验证协议

提出了一种基于RSA公钥密码体制的零知识水印验证协议,以解决通常的水印检测方案泄漏与水印相关的敏感信息的问题。协议利用公钥加密对水印及水印嵌入位置的水印化数据进行盲化处理,通过判断它们之间相关性的方法实现了版权水印的公开验证。同时,对如何抵抗骗局攻击进行了研究,提出了在协议执行过程中限制证明者P、验证者V对外通信的方法抵抗该类攻击。     

On automatic verification of self-stabilizing population protocols

The population protocol model has emerged as an elegant computation paradigm for describing mobile ad hoc networks, consisting of a number of mobile nodes that interact with each other to carry out a computation. The interactions of nodes are subject to a fairness constraint. One essential property of population protocols is that all nodes must eventually converge to the correct output value (or configuration). In this paper, we aim to automatically verify self-stabilizing population protocols for leader election and token circulation in the Spin model checker. We report our verification results and discuss the issue of modeling strong fairness constraints in Spin.     

安全协议状态空间的束动作偏序约简算法*

目前安全协议分析的偏序归约算法较为复杂、不易实现,限制了其适用范围,且以动作为基础,粒度较小,对减少状态空间的作用有限。针对该问题提出了一种束动作偏序约简算法,将同一会话中的动作序列看做一个束动作,根据攻击者截获的消息与攻击者知识集间的关系,判断迹等价的束动作迁移所到达的后继状态是否为冗余节点,以约简状态空间。该算法思想简单、易于实现;实例表明它有效地约简了安全协议的状态空间。     

An interactive tool for design,simulation, verification,and synthesis of protocols

We have developed a user-friendly CAD graphical tool for the design, verification, simulation, and synthesis of protocols based on an interactive tool for Petri net and state diagram designs. Special features of this tool are: the capability of modeling both control and data flows, reduction and analysis, simulation of network behavior and performance, coding (parametrized protocols and automatic implementation), synthesis (two party protocol and ordinary Petri nets), animation and flexible design. Since it is Petri-net based, it allows simulation during all design phases and has extensive applications such as parallel debugging and simulation, expert systems, etc. Future enhancements of this tool are also discussed.     

Knowledge structure approach to verification of authentication protocols

~~Knowledge structure approach to verification of authentication protocols1. Hintikka, J., Knowledge and Belief, Ithaca, NY. Cornell University Press, 1962. 2. Fagin, R., Halpern, J., Moses, Y. et al.,Reasoning About Knowledge, Cambridge, MA. MIT Press, 1995. 3. Halpern, I., Zuck, L., A little knowledge goes a long way. Simple knowledge based derivations and correctness proofs for a family of protocols. Journal of the ACM, 1992, 39(3): 449-478. 4. Stulp, F., Verbrugge, …     

Efficient verification of security protocols using partial-order reductions

In this paper we explore how partial-order reduction can make the task of verifying security protocols more efficient. These reduction techniques have been implemented in our tool Brutus. Partial-order reductions have proved very useful in the domain of model checking reactive systems. These reductions are not directly applicable in our context because of additional complications caused by tracking knowledge of various agents. We present partial-order reductions in the context of verifying security protocols and prove their correctness. Experimental results demonstrating the effectiveness of this reduction technique are also presented. Published online: 24 January 2003     

Security policy verification for multi-domains in cloud systems

The cloud is a modern computing paradigm with the ability to support a business model by providing multi-tenancy, scalability, elasticity, pay as you go and self-provisioning of resources by using broad network access. Yet, cloud systems are mostly bounded to single domains, and collaboration among different cloud systems is an active area of research. Over time, such collaboration schemas are becoming of vital importance since they allow companies to diversify their services on multiple cloud systems to increase both uptime and usage of services. The existence of an efficient management process for the enforcement of security policies among the participating cloud systems would facilitate the adoption of multi-domain cloud systems. An important issue in collaborative environments is secure inter-operation. Stemmed from the absence of relevant work in the area of cloud computing, we define a model checking technique that can be used as a management service/tool for the verification of multi-domain cloud policies. Our proposal is based on NIST’s (National Institute of Standards and Technology) generic model checking technique and has been enriched with RBAC reasoning. Current approaches, in Grid systems, are capable of verifying and detect only conflicts and redundancies between two policies. However, the latter cannot overcome the risk of privileged user access in multi-domain cloud systems. In this paper, we provide the formal definition of the proposed technique and security properties that have to be verified in multi-domain cloud systems. Furthermore, an evaluation of the technique through a series of performance tests is provided.     

An energy-aware virtual machines consolidation method for cloud computing: Simulation and verification

Cloud systems have become an essential part of our daily lives owing to various Internet-based services. Consequently, their energy utilization has also become a necessary concern in cloud computing systems increasingly. Live migration, including several virtual machines (VMs) packed on in minimal physical machines (PMs) as virtual machines consolidation (VMC) technique, is an approach to optimize power consumption. In this article, we have proposed an energy-aware method for the VMC problem, which is called energy-aware virtual machines consolidation (EVMC), to optimize the energy consumption regarding the quality of service guarantee, which comprises: (1) the support vector machine classification method based on the utilization rate of all resource of PMs that is used for PM detection in terms of the amount' load; (2) the modified minimization of migration approach which is used for VM selection; (3) the modified particle swarm optimization which is implemented for VM placement. Also, the evaluation of the functional requirements of the method is presented by the formal method and the non-functional requirements by simulation. Finally, in contrast to the standard greedy algorithms such as modified best fit decreasing, the EVMC decreases the active PMs and migration of VMs, respectively, 30%, 50% on average. Also, it is more efficient for the energy 30% on average, resources and the balance degree 15% on average in the cloud.     

A new approach for the verification of cache coherence protocols

We introduce a cache protocol verification technique based on a symbolic state expansion procedure. A global Finite State Machine (FSM) model characterizing the protocol behavior is built and protocol verification becomes equivalent to finding whether or not the global FSM may enter erroneous states. In order to reduce the complexity of the state expansion process, all the caches in the same state are grouped into an equivalence class and the number of caches in the class is symbolically represented by a repetition constructor. This symbolic representation is partly justified by the symmetry and homogeneity of cache-based systems. However, the key idea behind the representation is to exploit a unique property of cache coherence protocols: the fact that protocol correctness is not dependent on the exact number of cached copies. Rather, symbolic states only need to keep track of whether the caches have 0, 1, or multiple copies. The resulting symbolic state expansion process only takes a few steps and verifies the protocol for any system size. Therefore, it is more efficient and reliable than current approaches. The verification procedure is first applied to the verification of five existing protocols under the assumption of atomic protocol transitions. A simple snooping protocol on a split-transaction shared bus is also verified to illustrate the extension of our approach to protocols with nonatomic transitions     

云存储系统中数据完整性验证协议

在云存储网络环境中,数据的安全性和完整性是用户最关心的问题之一。综合考虑云存储网络环境中的安全需求,设计了云存储数据完整性验证(CS-DIV)协议。客户端把数据文件和校验标签上传到云存储服务器后随机抽查,服务器返回验证证据并由客户端判断文件的完整性。协议可以有效地验证云存储数据的完整性,并抵抗恶意服务器欺骗和恶意客户端攻击,从而提高整个云存储系统的可靠性和稳定性。仿真实验数据表明,所提协议以较低的存储、通信及时间开销实现了数据的完整性保护。     

Formal verification of secure group communication protocols modelled in UML

The paper discusses an experience in using Unified Modelling Language and two complementary verification tools in the framework of SAFECAST, a project on secured group communication systems design. AVISPA enabled detecting and fixing security flaws. The TURTLE toolkit enabled saving development time by eliminating design solutions with inappropriate temporal parameters.     

基于ATL的公平交换协议的形式化验证

如何对电子商务协议进行分析与验证一直是研究的热点,基于ATL（交替时态逻辑）对电子商务协议中的公平交换协议（Fair Exchange Protocols）进行形式化分析与验证,并选取了其中的一个电子合同签署协议进行形式化验证。用ATL语言来形式化描述公平交换协议,并使用ATS（Alternating Transition Systems,交替转移系统）来为公平交换协议进行形式化建模,再用形式化验证工具MOCHA对公平交换协议的公平性（Fairness）、及时性（Timeliness）和不可滥用性（Abuse-Freeness）进行有效的验证;对验证结果进行分析与讨论,发现了该协议不满足公平性和不可滥用性,不符合设计的要求。