Nonmonotonic Cryptographic Protocols

Abstract

This paper presents a new method for specifying and analyzing cryptographic protocols. Our method offers several advantages over previous approaches. Our technique is the first to allow reasoning about nonmonotonic protocols. These protocols are needed for systems that rely on the deletion of information. There is no idealization step in specifying protocols; we specify at a level that is close to the actual implementation. This avoids errors that might otherwise render a specification that passes the analysis, useless in practice. In our method, knowledge and belief sets for each principal are modified via actions and inference rules. Every message is considered to be broadcast, and we introduce the update function to maintain global knowledge. We show how our method uncovers the known flaw in the Needham and Schroeder protocol, and that the revision by the same authors does not contain this flaw. We also show that our method correctly handles protocols that are trivially insecure, such as Nessett's noted example. We then apply our method to our khat protocol. The analysis reveals a serious, previously undiscovered flaw in our nonmonotonic protocol for long-running jobs; one that seems obvious in hindsight, but escaped the attention of the authors and over 300 USENIX conference attendees. In addition, our analysis reveals a previously unknown vulnerability in phase II of khat. These are stunning confirmations of the importance of tools for analyzing cryptographic protocols.