...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of computer security >A method for unbounded verification of privacy-type properties
【24h】

A method for unbounded verification of privacy-type properties

机译：一种无限制验证隐私类型属性的方法

获取原文
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

In this paper, we consider the problem of verifying anonymity and unlinkability in the symbolic model, where protocols are represented as processes in a variant of the applied pi calculus, notably used in the ProVerif  tool. Existing tools and techniques do not allow to verify directly these properties, expressed as behavioral equivalences. We propose a different approach: we design two conditions on protocols which are sufficient to ensure anonymity and unlinkability, and which can then be effectively checked automatically using ProVerif . Our two conditions correspond to two broad classes of attacks on unlinkability, i.e.  data and control-flow leaks. This theoretical result is general enough that it applies to a wide class of protocols based on a variety of cryptographic primitives. In particular, using our tool, UKano , we provide the first formal security proofs of protocols such as BAC and PACE (e-passport), Hash-Lock (RFID authentication), etc. Our work has also lead to the discovery of new attacks, including one on the LAK protocol (RFID authentication) which was previously claimed to be unlinkable (in a weak sense).
机译：在本文中，我们考虑了在符号模型中验证匿名性和不可链接性的问题，其中协议表示为所应用pi演算的变体中的过程，特别是在ProVerif工具中使用。现有的工具和技术不允许直接验证这些特性，以行为等效性表​​示。我们提出一种不同的方法：我们在协议上设计两个条件，这些条件足以确保匿名性和不可链接性，然后可以使用ProVerif有效地对其进行自动检查。我们的两个条件对应于针对不可链接性的两大类攻击，即数据和控制流泄漏。该理论结果足够概括，可以应用于基于各种密码原语的多种协议。特别是，使用我们的工具UKano，我们提供了BAC和PACE（电子护照），Hash-Lock（RFID身份验证）等协议的第一批正式安全证明。我们的工作还导致了新攻击的发现。 ，其中包括一个LAK协议（RFID身份验证），该协议以前被认为是不可链接的（意义不大）。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号