一种针对隐私类性质的无界验证方法
密码学与安全
2019-04-09 v3
摘要
本文考虑在符号模型中验证匿名性与不可链接性的问题，其中协议被表示为应用 pi 演算变体中的进程，该演算尤其在 ProVerif 工具中得到使用。现有工具与技术无法直接验证这些以行为等价性表达的属性。我们提出了一种不同的方法：我们为协议设计了两个充分条件以确保匿名性与不可链接性，随后可使用 ProVerif 自动进行有效验证。我们的两个条件对应于两大类针对不可链接性的攻击，即数据泄露与控制流泄露。该理论结果具有足够的普适性，适用于基于多种密码学原语的广泛协议类。特别地，使用我们的工具 UKano，我们提供了诸如 BAC 与 PACE（电子护照）、Hash-Lock（RFID 认证）等协议的首个形式化安全证明。我们的工作还促成了对新攻击的发现，其中包括对先前被声称（在弱意义上）不可链接的 LAK 协议（RFID 认证）的一种攻击。
引用
@article{arxiv.1710.02049,
title = {A method for unbounded verification of privacy-type properties},
author = {Lucca Hirschi and David Baelde and Stéphanie Delaune},
journal= {arXiv preprint arXiv:1710.02049},
year = {2019}
}
备注
Will appear in the Journal of Computer Security (IOS Press)