Formal Methods for the Analysis of Authentication Protocols

Abstract

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.