SECURITY PROTOCOLS

Security Protocols

A Survey on Design and Analysis of Security Protocols

1. Abstract

Security protocols aim to allow two or more principals to establish a secure communication over a hostile network, such as the Internet. The design of security protocols is particularly error-prone; because it is difficult to anticipate what an intruder may achieve interacting through a number of protocol runs, claiming to be an honest participant. Thus, the verification of security protocols has attracted a lot of interest in the formal methods community and as a result lots of verification techniques/tools, as well as good practices for protocol design, have appeared in the two last decades. In this paper, we describe the state of the art in automated tools that support security protocol development. This mainly involves tools for protocol verification and, to a lesser extent, for protocol synthesis and protocol diagnosis and repair. Also, we give an overview of the most significant principles for the design of security protocols and of the major problems that still need to be addressed in order to ease the development of security protocols.

2. Methodology

This survey main aim is how to design and analysis of security protocols. When software is safety critical, the use of rigorous, mathematical models to software development becomes recommendable but sometimes mandatory. By using mathematical models, software problems are identified at earlier stages, prior to construction. There exists two approaches to the verification of security protocols, one is based on the complexity and the probability of breaking the cryptographic primitives of a protocol, and the other on what can be learned from interacting with several principals engaged in an arbitrary number of protocol runs. These two approaches differ mainly in how they model cryptographic primitives.

3. Literature Review

Meadows's method One of the first attempts at using automated theorem proving to security protocol analysis was due to Meadows. In 1996, she presented the NRL Protocol Analyzer (NPA) [Meadows 1996], a special-purpose tool, written in Prolog. Notably, NP A could be used to verify if a protocol was up to satisfy principal authentication or key distribution. Meadows's work extended Dolev and Yao's in two main respects. First, the spy attempts more than just finding out a secret. The spy may try, for example, to convince an agent that a message has certain properties that it does not. Second, NPA's method was a general, term-rewriting proof procedure, instead of an ad-hoc one (c.f. Dolev and Yao's approach).

NPA aims to prove that a collection of user-specified protocol states are umeachable. Using this strategy, it found two previously unknown attacks, one on Simmons's Selective Broadcast Protocol and the other on Burns Mitchell's Resource Sharing Protocol. NPA also identified hidden assumptions in two protocols: the Neuman Stubblebine re-authentication protocol and the Aziz- Diffie wireless communication protocol. NP A however is highly interactive, much in the same way a theorem prover is, relying on the user to guide the search for a proof. It is not guaranteed to terminate and has no means of converting a protocol description into ...