Formal methods for the verification and design of modern cryptographic applications

现代密码应用验证和设计的形式化方法

• 批准号: 94209379
• 负责人: Professor Dr. Matteo Maffei, Ph.D.
• 金额: --
• 依托单位: Institut für Informationssysteme
• 依托单位国家: 德国
• 项目类别: Independent Junior Research Groups
• 财政年份: 2009
• 资助国家: 德国
• 起止时间: 2008-12-31 至 2016-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/94209379?language=en
• 关键词: Formal; methods; verification; design; modern

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.

设计安全协议长期以来一直被认为是容易出错的，并且这种协议的安全性证明对于人类来说很难。最近提出了几种基于形式化方法的自动化协议验证技术。尽管有这些令人鼓舞的结果，现代密码应用程序的验证仍然是一个悬而未决的问题。首先，现代协议依赖于复杂的密码原语，并实现了现有工具大多不支持的复杂安全属性，在某些情况下，甚至没有形式化。第二，当前的自动化分析技术不提供端到端的安全保证，因为它们关注于协议的逻辑，并从其实现中抽象出来。该提案旨在为现代密码协议的验证和设计开发新的形式化方法，如匿名，信任和电子投票协议。这就要求我们研究现代密码原语的新抽象，提出新的形式化的广泛的安全属性，并开发自动验证技术。为了提供端到端的安全保证，我们还打算解决协议实现的安全属性的验证，目标是源代码和汇编代码。最后，我们打算将正式的方法应用到分布式系统的设计中，特别关注部分受损系统和对等网络中的安全保证。