该论文针对智能交通系统中车辆与基础设施间安全通信的关键需求，聚焦于恶意或异常车辆密码凭证的及时撤销问题。当前标准对撤销处理规定模糊，现有方案在可扩展性和有效性方面存在严重局限。为此，作者提出了一种形式化验证的车辆自撤销机制，该机制利用车辆中的可信处理元素（TPE），但不依赖可信时间源，从而避免了时间同步的脆弱性。方案兼容现有标准化工作，并首次利用Tamarin证明器保证撤销的确定性和可预测的上界，即使在存在现实攻击者（如网络延迟、消息丢失）的情况下也能确保撤销的实效性。作者在虚拟5G-Edge部署场景中模拟了大量车辆通信的真实环境，包括网络故障和延迟，实验结果表明该机制在保持形式化保证的同时，具有低网络开销和良好的可扩展性。该工作对V2X安全基础设施的改进具有重要参考价值。