A simple logic for authentication protocol design

The authors 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 one to treat the protocol at a higher abstraction level than do most of the known logics for authentication, and thus, one 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. They give a set of synthetic rules that can be used by protocol designers to construct a protocol in a systematic way