Safely composing security protocols

Security protocols are small programs that are executed in hostile environments. Many results and tools have been developed to formally analyze the security of a protocol in the presence of an active attacker that may block, intercept and send new messages. However even when a protocol has been proved secure, there is absolutely no guarantee if the protocol is executed in an environment where other protocols are executed, possibly sharing some common keys like public keys or long-term symmetric keys. In this paper, we show that security of protocols can be easily composed. More precisely, we show that whenever a protocol is secure, it remains secure even in an environment where arbitrary protocols satisfying a reasonable (syntactic) condition are executed. This result holds for a large class of security properties that encompasses secrecy and various formulations of authentication. This work has been partly supported by the RNTL project POSé and the ARA SSIA Formacrypt.     

Automated verification and refinement for physical-layer protocols

This paper demonstrates how to use a satisfiability modulo theories (SMT) solver together with a bounded model checker to verify properties of real-time physical layer protocols. The method is first used to verify the Biphase Mark protocol, a protocol that has been verified numerous times previously, allowing for a comparison of results. The techniques are extended to the 8N1 protocol used in universal asynchronous receiver transmitters. We then demonstrate the use of temporal refinement to link a finite state specification of 8N1 with its real-time implementation. This refinement relationship relieves a significant disadvantage of SMT approaches—their inability to scale to large problems. Finally, capturing the impact of metastability on timing requirements is a key issue in modeling physical-layer protocols. Rather than model metastability directly, a contribution of our models is treating its effect as a constraint on non-determinism.     

An intelligent agent-based collaborative information security framework

In this paper we proposed a framework for collaborative intelligent agents in a distributed environment to execute sound security strategies for protecting information resources. First, the intelligent agent-based Duty Reliable Center (DRC) in the model uses the group decision method to determine a global information threat level. With the threat level, local agent employs the Bayes’ decision procedure to calculate the expected loss of its all-possible actions, and then chooses an action among them with the minimum expected loss to protect its information resources. The proposed framework enables an agent to choose among alternatives in an optimal fashion, taking into account the worth of acquiring prior information to reduce uncertainty. Because system operations are distributed, hackers are unlikely to wreck the whole system. Thus, it is expected to yield information security cost-effective solutions.     

A cooperative agent-based model for active security systems

This paper presents a multi-agent model for implementing active security concepts. In this model, a group of agents can carry out their tasks cooperatively in order to achieve an ultimate security goal. Thus a low-level module of the proposed model reads the values of interesting data items of the relevant current network events and passes them to a relational database. Comparing these measurements against predefined values in an intruder signature database may point to a particular attack.The proposed model consists of two parts. (1) A multiagent Intrusion Detection System (MIDS) for detecting attacks. (2) An Active Security Mechanism (ASM) for taking active, network-wide, response against attackers. The proposed approach provides a customizable host environment built from various systems software components to allow an optimal match between the intrusion circumstances and the underlying security architecture. Thus, different frameworks can support alternative responses of existing security services. In addition, the ASM can take rapid response against attacks by making use of sensible sharing of attack intelligence. System agents communicate with each other on different hosts using an agent communication language through a message router.     

Information based reasoning about security protocols

We propose a notion of information based abstraction for the logical study of security protocols and study how protocol actions update agents' information. We show that interesting security properties of Needham-Schroeder like protocols can be verified automatically.     

Invariant-based reasoning about parameterized security protocols

We explore the applicability of the programming method of Feijen and van Gasteren to the domain of security protocols. This method addresses the derivation of concurrent programs from a formal specification, and it is based on common notions like invariants and pre- and post-conditions. We show that fundamental security concepts like secrecy and authentication can nicely be specified in this way. Using some small extensions, the style of formal reasoning from this method can be applied to the security domain. To demonstrate our approach, we discuss an authentication protocol and a public-key distribution protocol, and we deal with their composition. By focussing on a general setting where agents run the protocols multiple times, the nonce concept turns out to pop-up naturally. Although this work does not contain any new protocols, it does offer a new view on reasoning about security protocols.     

密码协议安全性质研究

针对密码协议安全性质研究存在的问题,基于协议的运行过程--协议运行迹研究了一般秘密性、猜测攻击,强秘密性、完美前向秘密性、已知密钥攻击、新鲜性和完整性.分析了各个安全性质的具体含义,并对其进行了形式化定义,指出了为保证这些安全性质协议运行迹需满足的条件,并分析了不同秘密性之间的关系.最后实例研究结果表明,定义是正确且有效的.     

On the secure implementation of security protocols

We consider the problem of implementing a security protocol in such a manner that secrecy of sensitive data is not jeopardized. Implementation is assumed to take place in the context of an API that provides standard cryptography and communication services. Given a dependency specification, stating how API methods can produce and consume secret information, we propose an information flow property based on the idea of invariance under perturbation, relating observable changes in output to corresponding changes in input. Besides the information flow condition itself, the main contributions of the paper are results relating the admissibility property to a direct flow property in the special case of programs which branch on secrets only in cases permitted by the dependency rules. These results are used to derive an unwinding theorem, reducing a behavioural correctness check (strong bisimulation) to an invariant.     

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.     

Analysis of security protocols based on challenge-response

Security protocol is specified as the procedure of challenge-response, which uses applied cryptography to confirm the existence of other principals and fulfill some data negotiation such as session keys. Most of the existing analysis methods, which either adopt theorem proving techniques such as state exploration or logic reasoning techniques such as authentication logic, face the conflicts between analysis power and operability. To solve the problem, a new efficient method is proposed that provides SSM semantics-based definition of secrecy and authenti- cation goals and applies authentication logic as fundamental analysis techniques, in which secrecy analysis is split into two parts: Explicit-Information-Leakage and Implicit-Information-Leakage, and correspondence analysis is concluded as the analysis of the existence relationship of Strands and the agreement of Strand parameters. This new method owns both the power of the Strand Space Model and concision of authentication logic.     

Integrating manufacturing systems through knowledge exchange protocols within an agent-based Knowledge Network

Manufacturing enterprises need the ability to respond to rapid changes in the market more than ever before. Besides, they are forced to constantly modify their culture and internal organization structures because of change and intense competition in the market. This obviously requires industrial organizations to manage the different components of their organizations by integrating and coordinating them into a highly efficient, effective, and responsive system in order to maintain and improve their competitiveness. This paper presents a knowledge exchange procedure for creating an integrated intelligent manufacturing system. The basic features of the proposed scheme are introduced and the approach is supported through a case study.     

Framework for evaluating security protocols in a banking environment

This paper presents an evaluation framework for security protocols that can be used to secure a bank's system. The framework firstly distinguishes between different bank applications, such as securing electronic transactions, securing message exchanges between remote parties, and securing the bank's system resources. Furthermore, the framework evaluates the security services and the level of the services provided by a protocol. It also evaluates the architectural layer on which the services are provided.     

安全协议攻击序列重构技术

攻击者攻击序列在安全协议形式化分析技术中用于描述攻击者对安全漏洞的攻击步骤.目前,攻击序列重构技术是安全协议形式化分析研究的热点与难点.对国际流行的方法进行了介绍和总结,重点分析和比较了基于模型检测的方法、基于定理证明的方法、基于逻辑程序的方法等能够进行攻击序列重构的各种方法,指出了各自的优缺点及技术手段、技术特点,最后给出了该领域的进一步研究方向.     

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     

Scalable RFID security protocols supporting tag ownership transfer

We identify privacy, security and performance requirements for radio frequency identification (RFID) protocols, as well as additional functional requirements such as tag ownership transfer. Many previously proposed protocols suffer from scalability issues because they require a linear search to identify or authenticate a tag. In support of scalability, some RFID protocols, however, only require constant time for tag identification, but, unfortunately, all previously proposed schemes of this type have serious shortcomings. We propose a novel scalable RFID authentication protocol based on the scheme presented in Song and Mitchell (2009) [1], that takes constant time to authenticate a tag. We also propose secret update protocols for tag ownership and authorisation transfer. The proposed protocols possess the identified privacy, security and performance properties and meet the requirements for secure ownership transfer identified here.     

Algebra model and security analysis for cryptographic protocols

With the rapid growth of the Internet and the World Wide Web a large number of cryptographic protocols have been deployed in distributed systems for various application requirements, and security problems of distributed systems have become very important issues. There are some natural problems: does the protocol have the right properties as dictated by the requirements of the system? Is it still secure that multiple secure cryptographic protocols are concurrently executed? How shall we analy…