TitleInvariant Generation Techniques in Cryptographic Protocol Analysis
Publication TypeConference Paper
Year of Publication2000
AuthorsMeadows, C.
Conference Name13th Computer Security Foundations Workshop
PublisherIEEE Computer Society Press
Abstract

The growing interest in the application of formal methods of cryptographic protocol analysis has led to the development of a number of different techniques for generating and describing invariants that are defined in terms of what messages an intruder can and cannot learn. These invariants, which can be used to prove authentication as well as secrecy results, appear to be central to many different tools and techniques. However, since they are usually developed independently for different systems, it is often not easy to see what they have in common with each other, or to tell whether or not they can be used in systems other than the ones for which they were developed. In this paper we attempt to remedy this situation by giving an overview of several of these techniques, discussing their relationships to each other, and developing a simple taxonomy. We also discuss some of the implications for future research.

Full Text

Meadows2000c.pdf

NRL Publication Release Number

00-1221.1-1147