A Simple Logic for Authentication Protocol Design

In this paper, we describe a simple logic. The logic uses the notion of channels that are generalisations of communication links with various security properties. The abstract nature of channels enables us to treat the protocol at a higher abstraction level than do most of the known logics for authentication, and thus, we can address the higher level functional properties of the system, without having to be concerned with the problems of the actual implementation. The major advantage of the proposed logic is its suitability for the design of authentication protocols. We give a set of synthetic rules that can be used by protocol designers to construct a protocol in a systematic way.