Implementation-Level Analysis of E-Voting Systems

电子投票系统（e-voting systems）是最具挑战性的安全关键系统之一，它们必须满足丰富的复杂安全要求。例如，除了保持个人选民的投票隐私（投票隐私），他们还应该允许选民检查他们的选票是否被正确计算（可验证性），同时防止买票和选民胁迫（抵制）。这些和其他安全需求已经在电子投票系统的协议设计层面上得到了形式化的描述和分析，然而，在电子投票系统的实现层面上如何保证这些特性仍然是一个悬而未决的问题。因此，本项目的目标是设计一般的方法和技术，用于电子投票系统的健全实施层面的分析，并证明这些方法和技术对具体系统的适用性，包括作为项目内案例研究提供的电子投票系统的原型实施。在该项目中，基于语言的信息流安全的技术和方法，特别是基于语言的不干扰，将与加密协议分析的技术和方法相结合。这将推动对基于语言的不干涉的研究，也超越电子投票领域。在该项目中开发的原型和取得的成果可作为优先方案内其他项目的案例研究。

Systems for electronic voting (e-voting systems) are among the most challenging security-critical systems, with a rich set of intricate security requirements they have to fulfill. For example, besides keeping the votes of individual voters private (privacy of votes), they should also allow voters to check that their votes were counted correctly (verifiability), while at the same time prevent vote buying and voter coercion (coercion-resistance). These and other security requirements have been formalized and analyzed on the protocol design level of e-voting systems.However, ensuring such properties on the implementation-level of e-voting systems is still an openproblem. The goal of this project is therefore to devise general methods and techniques for the soundimplementation-level analysis of e-voting systems and to demonstrate the applicability of these methods and techniques for concrete systems, including a prototypical implementation of an e-voting system provided as a case study within the project. In the project, techniques and methods for language-based information flow security, in particular language-based non-interference, will be combined with techniques and methods for cryptographic protocol analysis. This will advance research on language-based non-interference also beyond the domain of e-voting. Prototypes developed and results obtained within the project can serve as case studies for other projects withinthe Priority Programme.