Oh!... is it really you? : using rank functions to verify authentication protocols

• Main Author: Heather, James
• Published: Royal Holloway, University of London 2000
• Subjects: 004.01
• Online Access: http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.394363

A security protocol is a mechanism designed to allow secure communications through an insecure medium, even when that medium is controlled by a hostile attacker. Historically, approaches to analysis of security protocols have fallen into two broad categories: model checking and theorem proving. Each has its strengths, but the weaknesses of each are all too apparent. Model checking suffers from the problem of being able to check only a finite system; theorem proving is difficult to automate and often produces no conclusive results. Schneider's previous work on rank functions provides a formal approach to verification of certain properties of a security protocol. In this thesis, we develop the theory to allow for an arbitrarily large network, and give a clearly defined decision procedure by which one may either construct a rank function, proving correctness of the protocol, or show that no rank function exists. We show how the algorithm may be implemented to give a means of analysing authentication protocols that avoids the inherent limitations of both model checking and theorem proving. We discuss the implications of the absence of a rank function, and the open question of completeness of the rank function theorem.