Abstract
The paper presents a new method for specifying and analyzing cryptographic protocols. The method offers several advantages over previous approaches. The technique is the first to allow reasoning about nonmonotonic protocols, which are needed for systems that rely on the deletion of information. There is no idealization of protocols; we specify at a level that is close to the actual implementation. We show how the method uncovers the known flaw in the Needham and Schroeder protocol (R.M. Needham and M.D. Schroeder, 1978). We then apply the method to the khat protocol (A.D. Rubin, P. Honeyman, 1993). The analysis reveals a serious, previously undiscovered flaw in the nonmonotonic protocol for long-running jobs.<>