Cryptographic protocols

We develop principles and rules for achieving secrecy properties insecurity protocols. Our approach is based on traditional classification techniques, and extends those techniques to handle concurrent pro-cesses that use shared-key cryptography. The rules have the form of typing rules for a basic concurrent language with cryptographic primitives, the spi calculus. They guarantee that, if a protocol typechecks, then it does not leak its secret inputs.

We study the verification of secrecy and authenticity properties for cryptographic protocols which rely on symmetric shared keys. The verification can be reduced to check whether a certain parallel program which models the protocol and the specification can reach an erroneous state while interacting with an adversary. Assuming finite principals, we present a decision procedure for the reachability problem which is based on a `symbolic' reduction system.

Keywords: authentication, wireless, link security, mobile

Questions of belief are essential in analyzing protocols for authentication in distributed computing systems. In this paper we motivate, set out, and exemplify a logic specifically designed for this analysis; we show how various protocols differ subtly with respect to the required initial assumptions of the participants and their final beliefs. Our formalism has enabled us to isolate and express these differences with a precision that was not previously possible. It has drawn attention to features of protocols of which we and their authors were previously unaware, and allowed us to suggest improvements to the protocols. The reasoning about some protocols has been mechanically verified. This paper starts with an informal account of the problem, goes on to explain the formalism to be used, and gives examples of its application to protocols from the literature, both with conventional shared-key cryptography and with public-key cryptography. Some of the examples are chosen because of their practical importance, while others serve to illustrate subtle points of the logic and to explain how we use it. We discuss extensions of the logic motivated by actual practice - for example, in order to account for the use of hash functions in signatures. The final sections contain a formal semantics of the logic and some conclusions.

Authentication protocols are the basis of security in many distributed systems, and it is therefore essential to ensure that these protocols function correctly. Unfortunately, their design has been extremely error prone. Most of the protocols found in the literature contain redundancies or security flaws. A simple logic has allowed us to describe the beliefs of trustworthy parties involved in authentication protocols and the evolution of these beliefs as a consequence of communication. We have been able to explain a variety of authentication protocols formally, to discover subtleties and errors in them, and to suggest improvements. In this paper we present the logic and then give the results of our analysis of four published protocols, chosen either because of their practical importance or because they serve to illustrate our method.

Keywords: BAN logic, GNY logic, cryptography, authentication, formal methods

Keywords: Isabelle

We propose a new efficient automatic verification technique, Athena, for the analysis of security protocols. Our approach has several major advantages over the current model checking approaches. First, Athena contains a logic that can express various security properties including authentication, secrecy, and electronic commerce properties. We have developed an automatic procedure for evaluating well-formed formulas in this logic. For a well-formed formula, if the evaluation procedure terminates, it will generate a counterexample if the formula is false, or provide a proof if the formula is true. Thus, we can verify security properties under arbitrary protocol configurations, while almost all the current automatic tools can only reason about the security properties under limited protocol configurations. Second, Athena exploits many state space reduction techniques. We use an extension of the recently proposed Strand Space Model [?] to represent the protocol executions. By capturing the exact causal relation we achieve a much more concise state representation. Together with the backward search and other techniques, Athena naturally avoids the state space explosion problem caused by asynchronous composition and symmetry redundancy. We also allow free variables in the state structure. Thus, a state with free variables can represent a set of concrete states, and a state transition between two states with free variables can represent a set of state transitions between two concrete states. Athena also has the advantage that it can easily borrow results from theorem proving through unreachability theorems to reduce the state space further. As shown in our experiments, these techniques dramatically reduce the state space that needs to be explored, demonstrating that Athena is a promising technique for analyzing complicated security protocols.

In [BAN89] Burrows, Abadi, and Needham presented a logic (BAN) for analyzing cryptographic protocols in terms of belief. This logic is quite useful in uncovering flaws in protocols; however, it also has produced confusion and controversy. Much of the confusion was cleared up when Abadi and Tuttle provided a semantics for a version of that logic (AT) in [AT91]. In this paper we present a protocol to show that both BAN and AT are not expressive enough to capture all of the kinds of flaws that appear to be within their scope. We then present a logic that adds temporal formalisms to AT and that is rich enough to reveal the flaws in the presented protocol; nonetheless, this logic is sound with respect to the same semantics that was given in [AT91]. Finally, we argue that any approach of this type is inadequate by itself to demonstrate the absence of such flaws. We must supplement the formal logic with semantic analysis techniques.