ITR: Simplifying Design and Analysis of Cryptographic Protocols

Massachusetts Institute Of Technology, Cambridge MA

Investigators

Abstract

As Internet usage increasingly penetrates all aspects of society, security concerns increasingly rise in importance. As one moves from merely hosting web sites to supporting electronic commerce, banking, auctions, health-care, and voting, the ability to prevent malicious outsiders, or even malicious insiders, from gaining confidential information or manipulating the system becomes increasingly critical. Looking to the future, one can expect the evolution of even more complex systems, such as digital rights management systems and elaborate single sign-on web services, with correspondingly complex security requirements. Cryptography is an essential tool for implementing secure distributed systems over the Internet: no other technology provides the required confidentiality, authentication, or other security properties. Yet using cryptography effectively is surprisingly difficult. While there are good candidates for the underlying basic cryptographic operations (encryption, digital signatures, etc.), such cryptographic primitives by themselves are not sufficient: they need to be utilized within a larger framework---a cryptographic protocol---specifying exactly how they are to be used in a multi-party distributed system. The ability to design and prove secure a cryptographic protocol for a given purpose is essential to the secure evolution of our Internet-based society; yet our tools for doing so are still surprisingly awkward and limited. At the highest level of description, this proposal aims to remedy this situation by providing tools and techniques that facilitate the easy design and analysis of secure cryptographic protocols. Today, there are two major approaches to protocol design. The first is a formal approach pioneered by Dolev and Yao, based on theorem-proving and model-checking. This approach offers surprisingly good design tools, but at present this approach has a very limited domain of applicability, and furthermore the limitations on what an adversary is allowed to do in this approach make the analysis only suggestive, rather than conclusive, in practice. (That is, a ``proof of security'' for a protocol in this formal model doesn't necessarily imply that the protocol will be secure in practice.) The second approach is based on computational complexity; this approach offers solid conclusions, since the adversary is not unreasonably restricted, but is very difficult to use. Intellectual merit of proposed research: The most significant research direction proposed here is to build strong effective relationships between these two approaches, greatly expanding upon earlier seminal work by Abadi and Rogaway, and more recently by Herzog, and then Herzog, Micali, and Liskov. The goal is to provide methods so that one may use simplified formal methods to design and analyze cryptographic protocols, with the confidence that the result will be secure in the real world (that is, when realistic computational models and assumptions apply). The formal methods will be enlarged to handle many of the important ``details'' ordinarily not considered by formal methods, such as error handling and algebraic identities. Cryptographic techniques will be used to ``force'' a real-world adversary to be no more powerful than his ``formal'' counterpart. The research will proceed by develping ``compilation'' techniques that enable any protocol proven secure within the formal model to be implemented securely in the ``real world'' (that is, within the computational model). This research program is challenging; it requires an interdisciplinary approach as it crosses boundaries normally respected. Furthermore, developing ``generic'' techniques that apply to any protocol is necessarily more challenging than the usual procedure of working on protocols individually. Broad impact: The results of this research will not only advance the academic state of the art, but will also provide practitioners with effective tools and technology for making Internet-based society increasingly secure. The simplifications resulting from the proposed research will also enable cryptographic protocols to be taught in an effective and secure manner to a larger circle of students and implementers.