V2X 撤销协议的形式化分析
密码学与安全
2017-08-08 v2
摘要
车载网络（V2X）安全的研究已产生一系列针对该领域的安全机制与协议，兼顾安全性与隐私性。通常，这些提案的安全性分析在很大程度上是非形式化的。然而，形式化分析可用于暴露缺陷，并最终为协议提供更高水平的保证。本文聚焦于许多提案中 V2X 安全机制的一个特定要素的形式化分析：通过使恶意或行为不当车辆的凭证失效，将其从 V2X 系统中撤销。即便在车辆定期更换假名的情形下，该撤销也需以不可关联的方式执行以保护车辆隐私。Forster 等人提出的 REWIRE 方案及其子方案 BASIC 和 RTOKEN 旨在通过密码学解决方案与可信硬件应对这一挑战。使用 TAMARIN 证明器进行的形式化分析识别出这些方案中某些功能正确性与认证属性的两处缺陷。随后我们提出 Obscure Token (OTOKEN)，作为 REWIRE 的扩展，以隐私保护方式实现撤销。我们的方法通过引入额外的密钥对，解决了功能与认证属性问题，从而在不揭示长期身份的情况下，为车辆的成功撤销提供了更强且可验证的保证。此外，OTOKEN 是首个与形式化模型协同设计的 V2X 撤销协议。
引用
@article{arxiv.1704.07216,
title = {Formal Analysis of V2X Revocation Protocols},
author = {Jorden Whitefield and Liqun Chen and Frank Kargl and Andrew Paverd and Steve Schneider and Helen Treharne and Stephan Wesemeyer},
journal= {arXiv preprint arXiv:1704.07216},
year = {2017}
}
备注
16 pages, 4 figures