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.