TWC: Small: Functional Reactive Cryptography

加密协议是保护分布式计算机应用程序的基本工具，但也是出了名的难以设计和分析。随着现代计算机应用变得越来越复杂、互联、分布和交互，迫切需要提高研究人员设计和分析协议的能力，这些协议远远超出了传统的安全消息传输问题。这项研究通过研究专门针对安全分析的新的计算数学模型，研究了改进密码协议设计和分析方式的框架。这些方法将允许对更复杂的应用程序进行安全分析，并提高公众对分析本身的信心。这个项目探索了计算模型，在这些模型中，时间只被隐式地处理，通过逻辑依赖。避免显式的时间建模大大简化了密码协议的分析，仍然捕获了与安全属性相关的时间约束。考虑了不同的通信和安全模型，并通过简化将它们在安全保证、它们捕获现实攻击的能力以及描述密码感兴趣的协议的表现力方面相互比较。模型通过举例说明它们在一组典型案例研究中的使用来进行评估，这些案例研究包括不经意传输协议和用于安全多方计算的协议。这些工具和技术将帮助开发人员更容易地对更广泛的应用程序的安全性进行推理，并导致更安全和可靠的软件。

Cryptographic protocols are a fundamental tool to secure distributed computer applications, but also notoriously hard to design and analyze. With modern computer applications becoming increasingly complex, interconnected, distributed and interactive, there is a pressing need to improve the researchers' ability to design and analyze protocols that go well beyond the traditional problem of secure message transmission. This research investigates frameworks to improve the way cryptographic protocols are designed and analyzed, by investigating new mathematical models of computation specifically targeted to security analysis. These methods will allow security analysis of more complex applications, and also to improve public confidence in the analysis itself. This project explores computation models where time is only treated implicitly, through logical dependencies. Avoiding the explicit modeling of time greatly simplifies the analysis of cryptographic protocols, still capturing timing constraints that are relevant to security properties. Different communication and security models are considered, and compared to each other via reductions, with respect to security guarantees, their ability to capture realistic attacks, and expressiveness in describing protocols of cryptographic interest. Models are evaluated by exemplifying their use in the analysis of a set of representative case studies, including Oblivious Transfer protocols, and protocols for secure multiparty computation. These tools and techniques will help developers to more easily reason about the security of a wider range of applications, and lead to more secure and trustworthy software.