基于 SSProve 的远程信任度认证伪造攻击形式化验证
密码学与安全
2025-07-15 v2
摘要
远程信任度认证（RA）是云环境中受信任执行环境以及操作系统中受信任设备驱动器 onboarding 的基础。然而，RA 在最强模型（即语义模型）中缺乏其安全属性的严格机械化定义。这种机械化需要状态分离证明（StateSeparating Proofs, SSP）的概念。然而，SSP 仅最近在 Rocq Prover 中作为基础框架得到实现。基于该框架，本文提出了 RA 基本安全属性的首个机械化形式化化构建。我们的 Rocq Prover 开发首先定义数字签名，并在强存在主义攻击模型中形式化验证其防伪造安全性。基于这些结果，我们定义 RA 并将 RA 的安全性归约到数字签名的安全性。我们的构建提供了 RA 协议防伪造安全性的证据。此外，我们将我们的推理扩展到 RA 的基本原语，并将其安全性归约到数字签名基本原语的安全性。
引用
@article{arxiv.2502.17653,
title = {Formally-verified Security against Forgery of Remote Attestation using SSProve},
author = {Sara Zain and Jannik Mähn and Stefan Köpsell and Sebastian Ertel},
journal= {arXiv preprint arXiv:2502.17653},
year = {2025}
}