• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Software and systems modeling >Automated anonymity verification of the ThreeBallot and VAV voting systems
【24h】

Automated anonymity verification of the ThreeBallot and VAV voting systems

机译：ThreeBallot和VAV投票系统的自动匿名验证

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

In recent years, a large number of secure voting protocols have been proposed in the literature. Often these protocols contain flaws, but because they are complex protocols, rigorous formal analysis has proven hard to come by. Rivest's ThreeBallot and Vote/Anti-Vote/Vote (VAV) voting systems are important because they aim to provide security (voter anonymity and voter verifiability) without requiring cryptography. In this paper, we construct CSP models of ThreeBallot and VAV, and use them to produce the first automated formal analysis of their anonymity properties. Along the way, we discover that one of the crucial assumptions under which ThreeBallot and VAV (and many other voting systems) operate-the short ballot assumption-is highly ambiguous in the literature. We give various plausible precise interpretations and discover that in each case, the interpretation either is unrealistically strong or else fails to ensure anonymity. We give a revised version of the short ballot assumption for ThreeBallot and VAV that is realistic but still provides a guarantee of anonymity.
机译：近年来，文献中已经提出了大量安全的投票协议。这些协议通常都有缺陷，但是由于它们是复杂的协议，因此很难进行严格的形式分析。 Rivest的ThreeBallot和Vote / Anti-Vote / Vote（VAV）投票系统非常重要，因为它们旨在提供安全性（选民匿名和选民可验证性）而无需加密。在本文中，我们构建ThreeBallot和VAV的CSP模型，并使用它们对它们的匿名属性进行首次自动形式化分析。在此过程中，我们发现在文献中，ThreeBallot和VAV（以及许多其他投票系统）运作的关键假设之一就是简短的投票假设。我们给出了各种可能的精确解释，并发现每种情况下的解释要么不切实际，要么无法确保匿名性。我们给出了ThreeBallot和VAV的简短投票假设的修订版本，该修订版本是现实的，但仍可保证匿名性。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号