Formal methods for the verification and design of modern cryptographic applications

长期以来，人们都知道设计安全协议是容易出错的，而且这种协议的安全证明对人类来说是很尴尬的。最近提出了几种基于形式化方法的技术来实现协议验证的自动化。尽管有这些有希望的结果，现代密码学应用的验证仍然是一个悬而未决的问题。首先，现代协议依赖于复杂的加密原语，并实现了现有工具大多不支持的复杂安全属性，在某些情况下甚至没有形式化。其次，当前的自动化分析技术不提供端到端的安全保证，因为它们关注协议的逻辑，而远离协议的实现。该提案旨在开发新的形式化方法来验证和设计现代加密协议，如匿名、信任和电子投票协议。这要求我们研究现代密码原语的新颖抽象，提出各种安全属性的新形式化，并开发其自动验证的技术。为了提供端到端的安全保证，我们还打算针对源代码和汇编代码，对协议实现的安全属性进行验证。最后，我们打算将形式化方法应用于分布式系统的设计，特别关注部分受损系统和点对点网络中的安全保证。

Designing security protocols has long been known to be error-prone and security proofs of such protocols are awkward to make for humans. Several techniques based on formal methods were recently proposed to automate protocol verification. Despite these promising results, the verification of modern cryptographic applications is still an open issue. First, modern protocols rely on complex cryptographic primitives and achieve sophisticated security properties that are mostly not supported by existing tools and, in some cases, not even formalized. Second, current automated analysis techniques do not provide end-to-end security guarantees, since they focus on the logic of the protocol and abstract away from its implementation. This proposal aims at developing new formal methods for the verification and design of modern cryptographic protocols, such as anonymity, trust, and electronic voting protocols. This requires us to study novel abstractions of modern cryptographic primitives, to propose new formalizations of a wide range of security properties, and to develop techniques for their automated verification. In order to provide end-to-end security guarantees, we additionally intend address the verification of security properties on protocol implementations, targeting both source code and assembly code. Finally, we intend to apply formal methods to the design of distributed systems, with a specific focus on security guarantees in partially compromised systems and in peer-to-peer networks.