Analyzing encryption protocols using formal verification techniques

An approach to analyzing encryption protocols using machine-aided formal verification techniques is presented. The properties that the protocol should preserve are expressed as state invariants, and the theorems that must be proved to guarantee that the cryptographic facility satisfies the invariants are automatically generated by the verification system. A formal specification of an example system is presented, and several weaknesses that were revealed by attempting to verify and test the specification formally are discussed.<>     

Extending NCP for protocols using public keys

One of the greatest obstacles to wide-spread deployment of wireless mobile systems is security. Cryptographically strong protocols and algorithms are required to enable secure communication over links that are easy to monitor and control by an attacker. While good cryptographic algorithms exist, it is difficult to design protocols that are immune to malicious attack. Good analysis techniques are lacking. This paper presents extensions to a technique for specifying and analyzing nonmonotonic cryptographic protocols that use asymmetric keys. We introduce new actions and inference rules, as well as slight modifications to the Update function. An important observation is that reasoning about the origin of messages is quite different when dealing with asymmetric key protocols. We also introduce the notion that keys in certificates should be bound to the principals receiving them. We extend the technique to meet the binding requirements and show how the flaw in the Denning and Sacco public key protocol, which was discovered by Abadi and Needham, is revealed. We demonstrate the extended technique using one protocol of our own and the Needham and Schroeder public key protocol. We also introduce and analyze a fix to a known weakness in Needham and Schroeder’s protocol using our extended technique. Finally, we present several applications of these techniques to protocols for mobile computing over wireless networks. This revised version was published online in June 2006 with corrections to the Cover Date.     

智能化电视网络安全协议的验证方法综述

在有线电视网络领域,安全的网络通信协议是安全的信息传输的保障,那么研究出有效的协议安全性验证方法显得至关重要。当前,随着互联网的普及数字电视的双向化、智能化趋势日益明显,处于互联网中的数字电视将面临严峻的信息安全威胁,必须通过通信协议的安全性验证法选择出安全性更高的通信协议,才能确保双向数字电视传输网络的安全性。目前,关于验证通信协议的方法主要分为逻辑推理分析法、模型模拟检测法、定理归纳证明法以及其它衍生验证法。本文在前期研究的基础上,对近五年提出的典型的协议验证方法进行总结比较,分析各验证方法的优缺点。最后,对协议验证领域存在的问题及未来的发展趋势做以阐述。     

On automating the verification of secure ad-hoc network routing protocols

Ad-hoc networks do not rely on a pre-installed infrastructure, but they are formed by end-user devices in a self-organized manner. A consequence of this principle is that end-user devices must also perform routing functions. However, end-user devices can easily be compromised, and they may not follow the routing protocol faithfully. Such compromised and misbehaving nodes can disrupt routing, and hence, disable the operation of the network. In order to cope with this problem, several secured routing protocols have been proposed for ad-hoc networks. However, many of them have design flaws that still make them vulnerable to attacks mounted by compromised nodes. In this paper, we propose a fully automatic verification method for secure ad-hoc network routing protocols that helps increasing the confidence in a protocol by providing an analysis framework that is more systematic, and hence, less error-prone than the informal analysis. Our method is based on a deductive proof technique and a backward reachability approach. The main novelty of this approach compared to the prior works is that beside providing expressive semantics and syntax for modelling and specifying secure routing protocols, it assumes an arbitrary topology, and a strong attacker model.     

Verification of Secure Network Protocols in Uncertain Environments

In this paper, we present a method for protocol checking and verification using discrete event control. By protocol checking and verification, we mean verifying that a protocol is logically correct, that it does not cause deadlocks, and that it has been defined to respond to uncontrollable events that may occur in a system implementing it. Our approach differs from those previously suggested in two key ways. We extend the elementary theory of discrete event control to allow us to model more complicated protocols, including protocols relying on arbitrary counting models. We then present a maximum probability method for analyzing a protocol’s ability to react to a priori unspecified events. Unlike current protocol modeling, we use a pushdown automata for modeling protocols. This allows us to model protocols with greater fidelity. Our methods are illustrated using a simple two-level hierarchical protocol that defines the behavior of ad hoc wireless network nodes as they attempt to establish a secure connection. As wireless networks become more prevalent throughout the world, the off-line verification of protocols before they are implemented will help ensure that wireless network protocols are robust to security intrusions before they are deployed into the field. This will save time and money in the long run.     

Protocol verification using database technology

A novel application of databases in communications networks, namely, protocol verification on a parallel database machine, is described. An approach to protocol verification that uses database algorithms executing on a commercially available, parallel architecture called a hypercube multicomputer is introduced. The goal is to achieve the high degree of computational parallelism necessary to explore rapidly the global state space of even very complex protocols, significantly reducing the time required to verify a protocol and allowing formal verification to be included as part of the process of protocol design. An overview is provided of the relational model of protocol verification used, and extensions to the model are described. The hypercube multicomputer and the algorithms for relational database operations designed to execute in that environment are then described. Estimates of the performance improvements achievable by parallel executing of verification algorithms in the proposed system are given     

基于秘密认证的可验证量子秘密共享协议

该文针对量子秘密共享协议难以抵抗内部成员欺骗攻击的问题，采用秘密认证的方法提出可验证量子秘密共享协议的一般性模型，基于Bell态双粒子变换提出一种新验证算法，并以此给出一个新的可验证量子秘密共享协议。与现有的量子秘密共享协议的验证算法相比，新验证算法既能有效抵抗内部成员欺骗攻击等典型的攻击策略，又可大幅提升协议效率，而且可以与现有量子秘密共享协议相结合，具备很好的可扩展性。     

Bioinspired Security Analysis of Wireless Protocols

Fraglets represent an execution model for communication protocols that resembles the chemical reactions in living organisms. The strong connection between their way of transforming and reacting and formal rewriting systems makes a fraglet program amenable to automatic verification. Grounded on past work, this paper investigates feasibility of adopting fraglets as model for specifying security protocols and analysing their properties. In particular, we give concrete sample analyses over a secure RFID protocol, showing evolution of the protocol run as chemical dynamics and simulating an adversary trying to circumvent the intended steps. The results of our analysis confirm the effectiveness of the cryptofraglets framework for the model and analysis of security properties and eventually show its potential to identify and uncover protocol flaws.     

A survey of light-weight transport protocols for high-speednetworks

A comparative survey is presented of techniques used at the transport layer in eight representative protocols, most of which were designed to improve the protocol processing rate. The protocols are the relevant portions of the APPN, Datakit, Delta-t, NETBLT, OSI/TP4, TCP, VMTP, and XTP architectures. The protocols are described, and the functions under consideration are defined. No distinction is made as to whether these functions are carried out in a LAN, MAN, or WAN environment. The objective is to provide reliable, end-to-end transmission of data. The mechanisms required to support connection management, acknowledgements, flow control, and error handling are examined. Suitable techniques for designing light-weight transport protocols are identified. A discussion is presented as to which technique seems the most promising     

Formal Methods in Communication Protocol Design

While early protocol design efforts had to rely largely on seat-of-the-pants methods, a variety of more rigorous techniques have been developed recently. This paper surveys the formal methods being applied to the problems of protocol specification, verification, and implementation. In the specification area, both the service that a protocol layer provides to its users and the internal operations of the entities that compose the layer must be defined. Verification then consists of a demonstration that the layer will meet its service specification and that each of the components is correctly implemented. Formal methods for accomplishing these tasks are discussed, including state transition models, program verification, symbolic execution, and design rules.     

一种验证非否认协议的新方法

为了描述非否认协议中的各种不确定因素,在Kailar逻辑系统中引入了表示缺省信息的否定词,以及相应的推理机制。提出了安全协议验证的新方法,主要特点是:可以直接对协议的动态运行过程进行推理;推理具有非单调性;避免过多的理想化假设;可以分析含有多个子协议的非否认协议,以及协议的可追究性和公平性。文中以一种基于离线TTP方式的非否认协议为例,验证了该协议在运行一次时具有可追究性,但多次运行时存在攻击。     

Modular specification and verification of XTP

The transfer protocol framework supports the formal specification and verification of data transfer protocols. It consists of generic specification modules and theorems. Compositions of specification module instances result in well-structured specifications which describe a protocol, the medium used, and the service provided by means of TLA formulas. The protocol verification is based on the proof of the logical implication between protocol and service specification. Due to the modular structuring of the specifications, this proof can be decomposed into a set of subimplications which correspond directly to theorems of the framework. Therefore, the development of formal specifications as well as the protocol verification can be reduced to the instantiation and arrangement of framework elements. The flexibility of the framework opens its application for a broad spectrum of data transfer protocols. We outline the principles of the framework and concentrate on its application to the high-speed transfer protocol XTP. Because of the framework support, the formal modeling and analysis of this modern and function-rich protocol was manageable and identifies deficiencies of the current protocol definition clearly.     

Power-One通信电源监控系统通信协议破解

根据数据链路层通信协议的一般格式,对串口监听工具截取的Power-One通信电源监控系统中的通信信息进行了逻辑推理和分析,破解了其通信协议的格式和各种通信命令。实验表明,破解结果正确无误。对于通信电源分布式监控系统通信协议的设计和实现,具有一定的借鉴意义。     

ITPMAP: An Improved Three-Pass Mutual Authentication Protocol for Secure RFID Systems

Radio frequency identification (RFID) is a wireless technology used in various applications to minimize the complexity of everyday life. However, it opens a large number of security and privacy issues that require to be addressed before its successful deployment. Many RFID authentication protocols are proposed in recent years to address security and privacy issues, and most of them are based on lightweight cryptographic techniques such as pseudo-random number generators (PRNGs), or bitwise logical operations. However, the existing RFID authentication protocols suffer from security weaknesses, and cannot solve most of the security and privacy problems. A new solution is necessary to address security and privacy issues. In this paper, an improved three-pass mutual authentication protocol (ITPMAP) for low-cost RFID tags is proposed to offer an adequate security level for RFID systems. The proposed ITPMAP protocol uses one PRNG on the tag side and heavy-weighted cryptographic techniques (i.e., digital signature and password-based encryption schemes) on the back-end server side instead of lightweight cryptographic techniques to address the security and privacy issues. The ITPMAP protocol is secure against various attacks such as cloning, spoofing, replay, and desynchronization attacks. Furthermore, as a proof of concept, the ITPMAP protocol is adopted to propose the design of three real-life RFID systems; namely: Signing and Verification of Graduation Certificate System, issuing and verification of e-ticketing system, and charging and discharging of prepaid card system. The Unified Modeling Language is used to demonstrate the design of the proposed ITPMAP protocol and systems. Java language is used for the implementation of the proposed systems. In addition, the “Mifare Classic” tags and readers are used as RFID apparatuses for the proposed systems.     

Toward efficient protocol design through protocol profiling and performance assessment: using formal verification in a different context

The most common use of formal verification methods so far has been in identifying whether livelock and/or deadlock situations can occur during protocol execution, process, or system operation. In this work, we aim to show that an additional equally important and useful application of formal verification methods can be in protocol design in terms of performance‐related metrics. This can be achieved by using the methods in a rather different context compared with their traditional use, that is, not only as model checking tools to assess the correctness of a protocol in terms of lack of livelock and deadlock situations but rather as tools capable of building profiles of protocol operations, assessing their performance, and identifying operational patterns and possible bottleneck operations. This process can provide protocol designers with an insight about the protocols’ behavior and guide them toward further optimizations. It can also assist network operators and service providers to assess the protocols’ relative performance and select the most suitable protocol for specific deployment scenarios. We illustrate these principles by showing how formal verification tools can be applied in this protocol profiling and performance assessment context using some existing protocol implementations in mobile and wireless environments as case studies. Copyright © 2011 John Wiley & Sons, Ltd.     

Exploring the design space of reliable multicast protocols for wireless mesh networks

Many important applications in wireless mesh networks require reliable multicast communication, i.e., with 100% packet delivery ratio (PDR). Previously, numerous multicast protocols based on automatic repeat request (ARQ) have been proposed to improve the packet delivery ratio. However, these ARQ-based protocols can lead to excessive control overhead and drastically reduced throughput. In this paper, we present a comprehensive exploration of the design space for developing high-throughput, reliable multicast protocols that achieve 100% PDR.Motivated by the fact that 802.11 MAC layer broadcast, which is used by most wireless multicast protocols, offers no reliability, we first examine if better hop-by-hop reliability provided by unicasting the packets at the MAC layer can help to achieve end-to-end multicast reliability. We then turn to end-to-end solutions at the transport layer. Previously, forward error correction (FEC) techniques have been proved effective for providing reliable multicast in the Internet, by avoiding the control packet implosion and scalability problems of ARQ-based protocols. In this paper, we examine if FEC techniques can be equally effective to support reliable multicast in wireless mesh networks. We integrate four representative reliable schemes (one ARQ, one FEC, and two hybrid) originally developed for the Internet with a representative multicast protocol ODMRP and evaluate their performance.Our experimental results via extensive simulations offer an in-depth understanding of the various choices in the design space. First, compared to broadcast-based unreliable ODMRP, using unicast for per-hop transmission only offers a very small improvement in reliability under low load, but fails to improve the reliability under high load due to the significantly increased capacity requirement which leads to congestion and packet drop. Second, at the transport layer, the use of pure FEC can significantly improve the reliability, increasing PDR up to 100% in many cases, but can be inefficient in terms of the number of redundant packets transmitted. In contrast, a carefully designed ARQ–FEC hybrid protocol, such as RMDP, can also offer 100% reliability while improving the efficiency by up to 38% compared to a pure FEC scheme. To our best knowledge, this is the first in-depth study of high-throughput, reliable multicast protocols that provide 100% PDR for wireless mesh networks.     

密码协议的一种基于组合推理的模型验证

将密码协议与协议中用到的密码算法视为一个系统，基于组合推理技术建立了密码协议系统的形式化模型。采用基于假设／保证的组合推理技术提出了新的假设／保证推理规则和假设／保证推理算法，证明了该规则的正确性，实现了密码协议系统的模型验证，并重点解决了系统分解问题、假设函数的设定问题等难题。以kerberos v5密码协议系统为例，利用该组合推理技术对密码协议系统进行了安全验证。