2025/02/24 by Zain, Sara, Jannik Mähn, Mähn, Jannik +4
Computer Science · #Advanced Malware Detection Techniques #Cloud Data Security Solutions #Cryptography and Security (cs.CR) #FOS: Computer and information sciences #Security and Verification in Computing
paper · pdf · doi:10.48550/arxiv.2502.17653
openalex publication_date 2025/02/24 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Remote attestation (RA) is the foundation for trusted execution environments in the cloud and trusted device driver onboarding in operating systems. However, RA misses a rigorous mechanized definition of its security properties in one of the strongest models, i.e., the semantic model. Such a mechanization requires the concept of StateSeparating Proofs (SSP). However, SSP was only recently implemented as a foundational framework in the Rocq Prover. Based on this framework, this paper presents the first mechanized formalization of the fundamental security properties of RA. Our Rocq Prover development first defines digital signatures and formally verifies security against forgery in the strong existential attack model. Based on these results, we define RA and reduce the security of RA to the security of digital signatures. Our development provides evidence that the RA protocol is secure against forgery. Additionally, we extend our reasoning to the primitives of RA and reduce their security to the security of the primitives of the digital signatures.