Formal Methods for the Analysis of Authentication Protocols

[peter honeyman <honey@citi.umich.edu>]

avi rubin and i recently completed a survey paper that may be of interest
to cpunx.  it is available via anonymous ftp from citi.umich.edu:

/afs/umich.edu/group/itd/citi/public/techreports/PS.Z/citi-tr-93-7.ps.Z

i have attached the abstract to this message.

	peter

=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

Formal Methods for the Analysis of Authentication Protocols

A D. Rubin
P. Honeyman

Center for Information Technology Integration
University of Michigan
Ann Arbor


In this paper, we examine current approaches and the state of the art
in the application of formal methods to the analysis of cryptographic
protocols.  We use Meadows' classification of analysis techniques into
four types.

The Type I approach models and verifies a protocol using specification
languages and verification tools not specifically developed for the
analysis of cryptographic protocols.  In the Type II approach, a
protocol designer develops expert systems to create and examine
different scenarios, from which she may draw conclusions about the
security of the protocols being studied.  The Type III approach models
the requirements of a protocol family using logics developed
specifically for the analysis of knowledge and belief.  Finally, the
Type IV approach develops a formal model based on the algebraic
term-rewriting properties of cryptographic systems.

The majority of research and the most interesting results are in the
Type III approach, including reasoning systems such as the BAN logic;
we present these systems and compare their relative merits.  While each
approach has its benefits, no current method is able to provide a
rigorous proof that a protocol is secure.