We formalise definitions of ballot secrecy and ballot independence by Smyth, JCS'21 as indistinguishability games in the computational model of security. These definitions improve upon Smyth, draft '21 to consider a wider class of voting systems. Both Smyth, JCS'21 and Smyth, draft '21 improve on earlier works by considering a more realistic adversary model wherein they have access to the ballot collection. We prove that ballot secrecy implies ballot independence. We say ballot independence holds if a system has non-malleable ballots. We construct games for ballot secrecy and non-malleability and show that voting schemes with malleable ballots do not preserve ballot secrecy. We demonstrate that Helios does not satisfy our definition of ballot secrecy. Furthermore, the Python framework we constructed for our case study shows that if an attack exists against non-malleability, this attack can be used to break ballot secrecy.

翻译：我们形式化定义了Smyth在JCS'21中提出的选票保密性与选票独立性概念，将其构建为计算安全模型下的不可区分性游戏。相较于Smyth的draft'21版本，这些定义扩展了适用投票系统的范围。Smyth的JCS'21与draft'21均改进了早期工作，通过引入更贴近现实的敌手模型——允许敌手访问选票集合。我们证明选票保密性蕴含选票独立性。若系统具备非可塑性选票特性，则称其满足选票独立性。我们构建了选票保密性与非可塑性安全游戏，并证明采用可塑性选票的投票方案无法保障选票保密性。实验表明Helios系统不符合我们定义的选票保密性要求。此外，我们基于Python框架的案例分析证实：若存在对非可塑性的攻击，该攻击可被用于破坏选票保密性。