ITR: Simplifying Design and Analysis of Cryptographic Protocols

ITR：简化加密协议的设计和分析

• 批准号: 0326277
• 负责人: Silvio Micali
• 金额: $ 131万
• 依托单位: Massachusetts Institute of Technology
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2003
• 资助国家: 美国
• 起止时间: 2003-09-01 至 2009-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0326277&HistoricalAwards=false
• 关键词: ITR; Simplifying; Design; Analysis; Cryptographic

As Internet usage increasingly penetrates all aspects of society,security concerns increasingly rise in importance. As one moves frommerely hosting web sites to supporting electronic commerce, banking,auctions, health-care, and voting, the ability to prevent maliciousoutsiders, or even malicious insiders, from gaining confidentialinformation or manipulating the system becomes increasingly critical.Looking to the future, one can expect the evolution of even more complexsystems, such as digital rights management systems and elaborate singlesign-on web services, with correspondingly complex securityrequirements.Cryptography is an essential tool for implementing secure distributedsystems over the Internet: no other technology provides the requiredconfidentiality, authentication, or other security properties.Yet using cryptography effectively is surprisingly difficult. Whilethere are good candidates for the underlying basic cryptographicoperations (encryption, digital signatures, etc.), such cryptographicprimitives by themselves are not sufficient: they need to be utilizedwithin a larger framework---a cryptographic protocol---specifyingexactly how they are to be used in a multi-party distributed system. Theability to design and prove secure a cryptographic protocol for a givenpurpose is essential to the secure evolution of our Internet-basedsociety; yet our tools for doing so are still surprisingly awkward andlimited.At the highest level of description, this proposal aims to remedy thissituation by providing tools and techniques that facilitate the easydesign and analysis of secure cryptographic protocols.Today, there are two major approaches to protocol design. The first isa formal approach pioneered by Dolev and Yao, based on theorem-provingand model-checking. This approach offers surprisingly good designtools, but at present this approach has a very limited domain ofapplicability, and furthermore the limitations on what an adversary isallowed to do in this approach make the analysis only suggestive, ratherthan conclusive, in practice. (That is, a ``proof of security'' for aprotocol in this formal model doesn't necessarily imply that theprotocol will be secure in practice.) The second approach is based oncomputational complexity; this approach offers solid conclusions, sincethe adversary is not unreasonably restricted, but is very difficult touse.Intellectual merit of proposed research: The most significant researchdirection proposed here is to build strong effective relationshipsbetween these two approaches, greatly expanding upon earlier seminalwork 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 formalmethods to design and analyze cryptographic protocols, with theconfidence that the result will be secure in the real world (that is,when realistic computational models and assumptions apply). The formalmethods will be enlarged to handle many of the important ``details''ordinarily not considered by formal methods, such as error handling andalgebraic 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 withinthe formal model to be implemented securely in the ``real world'' (thatis, within the computational model).This research program is challenging; it requires an interdisciplinaryapproach as it crosses boundaries normally respected. Furthermore, developing ``generic'' techniques that apply to any protocol isnecessarily more challenging than the usual procedure of working onprotocols individually.Broad impact: The results of this research will not only advance theacademic state of the art, but will also provide practitioners witheffective tools and technology for making Internet-based societyincreasingly secure. The simplifications resulting from the proposedresearch will also enable cryptographic protocols to be taught in aneffective and secure manner to a larger circle of students andimplementers.

随着互联网的使用日益渗透到社会的各个方面，安全问题的重要性日益上升。 随着人们从仅仅托管网站转向支持电子商务、银行、拍卖、医疗保健和投票，防止恶意外部人员甚至恶意内部人员获取机密信息或操纵系统的能力变得越来越重要。展望未来，人们可以期待更复杂系统的发展，如数字版权管理系统和精心设计的单点登录Web服务，密码学是在Internet上实现安全分布式系统的基本工具：没有其他技术提供所需的机密性、认证或其他安全属性。然而，有效地使用密码学是令人惊讶的困难。 虽然对于底层的基本密码操作（加密、数字签名等）有很好的候选者，这样的密码原语本身是不够的：它们需要在一个更大的框架-密码协议-中被利用，该框架确切地规定了它们如何在多方分布式系统中被使用。设计和证明一个密码协议的安全性对于我们基于Internet的社会的安全发展是必不可少的，然而我们这样做的工具仍然令人惊讶地笨拙和有限。在最高级别的描述中，这个建议旨在通过提供工具和技术来改善这种情况，这些工具和技术有助于安全密码协议的简单设计和分析。今天，有两种主要的协议设计方法。 第一种伊萨由Dolev和Yao开创的形式化方法，基于定理证明和模型检查。 这种方法提供了令人惊讶的好的设计工具，但目前这种方法具有非常有限的适用范围，而且在这种方法中允许对手做什么的限制使得分析在实践中仅具有建议性，而不是结论性的。 (That在这个正式模型中，协议的“安全性证明”并不一定意味着协议在实践中是安全的。 第二种方法是基于计算复杂性;这种方法提供了坚实的结论，因为对手不是不合理的限制，但很难使用。拟议研究的智力价值：这里提出的最重要的研究方向是在这两种方法之间建立强有力的有效关系，大大扩展了阿巴迪和罗加维的早期研究工作，以及最近的赫尔佐格，然后赫尔佐格，米卡利，我们的目标是提供一种方法，使人们可以使用简化的形式化方法来设计和分析密码协议，并确信其结果在真实的世界中是安全的（即，当现实的计算模型和假设适用时）。 形式方法将被扩展到处理许多通常不被形式方法考虑的重要“细节”，如错误处理和代数恒等式。 密码技术将被用来“迫使”一个现实世界的对手不比他的“正式”对手更强大。 这项研究将通过开发"编译“技术来进行，这种技术使任何在形式模型中被证明是安全的协议能够在"真实的世界”中安全地实现（即在计算模型中）。这项研究计划是具有挑战性的，它需要一种跨学科的方法，因为它跨越了通常受到尊重的边界。 此外，开发适用于任何协议的“通用”技术必然比单独研究协议的通常过程更具挑战性。广泛影响：这项研究的结果不仅将推动学术界的最新发展，而且还将为实践者提供有效的工具和技术，使基于Internet的社会越来越安全。 从拟议的研究中得到的简化也将使密码协议能够以有效和安全的方式教授给更大范围的学生和实施者。