(1) Computer Science Department, University of California, 93106 Santa Barbara, CA, USA;(2) U.S. Naval Research Laboratory, 4555 Overlook Avenue, SW, 20375 Washington, DC, USA;(3) The MITRE Corporation, 01730 Bedford, MA, USA
Abstract:
Three experimental methods have been developed to help apply formal methods to the security verification of cryptographic protocols of the sort used for key distribution and authentication. Two of these methods are based on Prolog programs, and one is based on a general-purpose specification and verification system. All three combine algebraic with state-transition approaches. For purposes of comparison, they were used to analyze the same example protocol with a known flaw.