TitleThe Logic of Authentication Protocols
Publication TypeConference Proceedings
Year of Publication2001
AuthorsSyverson, P., and I. Cervesato
Conference NameFoundations of Security Analysis and Design --- FOSAD'00
VolumeSpringer-Verlag LNCS 2171
Pagination63-136
Abstract

The rationale of authentication has been a topic of study for about a decade and a half. First attempts at formal analysis of authentication protocols were not using logics per se, but were certainly logical. Millen's Interrogator was a Prolog based tool specifically designed for authentication protocol analysis that functioned essentially as a special purpose model checker. Kemmerer used the general purpose formal specification language Ina Jo and an accompanying symbolic execution tool Inatest to specify and analyze protocols.
We will focus on logics of authentication, beginning with BAN. However, we will not only be discussing logics per se. We will also be looking at the `rhyme and reason' of authentication, the attempts to formalize and define notions of authentication and to apply these. Thus, we will also be considering the logic of authentication in a broader sense.
We will not discuss (except incidentally) other formal methods that have been applied to authentication. In particular, we will not be describing process algebras, automata, automated tools such as theorem provers or model checkers.

Full Text

SyversonCervesato2001.pdf

NRL Publication Release Number

01-1221.1-1283