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.