Year

1997

Degree Name

Doctor of Philosophy

Department

School of Information Technology and Computer Science

Abstract

An authentication protocol essentially provides a mechanism for verifying the identities of nodes in an insecure network, and for the safe distribution of secrets. The subject of authentication protocols is enormously subtle. It is surprisingly easy to design incorrect protocols. A typical authentication protocol consists of an exchange of just a few messages, may appear intuitively correct, and still not work as intended. It is common to find examples of published protocols in the literature which have subsequently been found to contain flaws. As a result, methods for verifying the correctness of protocols have proliferated. A pioneering work in this area is a modal logic of Burrows, Abadi and Needham. Their work has led to the development of a substantial number of logics of a similar kind, often referred to as "authentication logics". If authentication logics are to be used to verify the correctness of protocols, then there is a need to verify the correctness of the logics themselves. The latter is the metalogical problem of obtaining assurance about the soundness of a logic. A meaningful solution to this problem requires the development of an independently motivated semantics for the logic. However, as compared to the formalisms in which authentication logics are couched, the development of semantics for such logics has generally lagged behind. Indeed, despite some notable previous work in the latter direction, it is rare to find a rigorous proof of soundness for an existing authentication logic.

There are several other interesting areas in the study of protocols besides authentication logics. These include alternative methods for analyzing protocols, and models for analyzing protocol efficiency.

This thesis makes some contributions to the areas of authentication logics and protocol analysis; the contributions made are summarized below.

1. Authentication logics

(a) A critical appraisal of an authentication logic of Gong, Needham and Yahalom: It is shown that the above logic exhibits several undesirable features, including instances of unsoundness, incompleteness, and redundancy. These observations are used to highlight the need for a semantic basis for authentication logics.

(b) A modification to the logic of Gong, Needham and Yahalom for automatic analysis of protocols: The proposed modification lends to a simple technique for automating deductions in the modified logic. Not only does the automation provided serve as an aid in analyzing protocols, but it also proves useful in confirming some of the difficulties in using the original logic.

(c) A computational model for authentication logics: The proposed model decouples the syntax and semantics of notions that are central to existing authentication logics. The import of the resulting model is that it provides a solid foundation for devising such logics.

(d) An authentication logic and its proof of soundness: The model developed above is used to devise a new authentication logic and to establish a soundness theorem for the logic in a rigorous manner.

2. Protocol analysis

A model for reasoning about lower bounds on rounds: The proposed model is primarily motivated by the need to verify the correctness of some informal bounds found in the literature. It provides a precise definition of the metric number of rounds and a theorem which relates lower bounds on rounds with security requirements.

The thesis is organized as follows. Chapter 1 is an introductory survey on authentication logics. The Chapters 2, 3, 4, and 5 cover parts (l)(a)-(d) above, respectively. Chapter 6 covers part 2. Chapter 7 contains our conclusions.

Download

Share

COinS
 

Unless otherwise indicated, the views expressed in this thesis are those of the author and do not necessarily represent the views of the University of Wollongong.