November 28, 2025. Research at the Barkhausen Institute focuses on making digital systems demonstrably more secure and trustworthy. With the paper “Formally-verified Security against Forgery of Remote Attestation using SSProve”, our research group Verified System Design Automation has made an important contribution to this goal.
Categories
Tags
Contact info
Silicon Saxony
Marketing, Kommunikation und Ă–ffentlichkeitsarbeit
Manfred-von-Ardenne-Ring 20 F
Fax: +49 351 8925 889
Contact person:
Remote Attestation (RA) is a basic protocol used to check whether a device – such as a laptop, a cloud server or an IoT sensor – has been tampered with. It is based on digital signatures: the device generates a signed report of its internal state, which a remote verifier can check. Despite its widespread use, RA lacks rigorous, machine-verified proofs of its cryptographic security.
In our paper, we have developed the first machine-verified cryptographic verification of digital signatures and remote attestation. We show that the security of RA is equivalent to the security of the underlying digital signatures. We formalized and proved the results in the SSProve framework using Rocq Prover (formerly Coq).
Flowchart showing the modular specification of RA using the SSProve package composition with labeled boxes and arrows indicating the data flow and functions.
We defined digital signatures and RA within the SSProve framework, specifying cryptographic operations and state transitions through mathematical reasoning. We then proved that the RA protocol is also secure if the underlying digital signature scheme is secure (in the strong, cryptographic sense of unforgeability). Our development represents the first step for RA and can be used to create real-world use cases.
All formal development was done using SSProve, a framework for stateful and modular cryptographic proofs based on Rocq Prover. Our proof developments are available as an open-source repository.
This work strengthens the Barkhausen Institute’s mission to build trustworthy digital systems through formal verification. By providing a machine-verified proof of RA security, we are giving a solid foundation to a widely used but previously unverified cryptographic mechanism. This advances the Verified System Design Automation group’s goal of trustworthiness by design, from theory to real-world systems.
Formalized verified security against remote attestation forgery with SSProve
Sara Zain, Barkhausen Institute; Jannik Mähn, Stefan Köpsell, Barkhausen Institute; and Sebastian Ertel, Barkhausen Institute.
Link to the paper: https://arxiv.org/pdf/2502.17653
– – – – –
👉 www.barkhauseninstitut.org
Photo: Sara Zain
