Machine-Checked Security for Digital Systems at Barkhausen Institut
Research at the Barkhausen Institut focuses on making digital systems provably 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 a significant contribution to this goal.
What is the paper about?
Remote Attestation (RA) is a fundamental protocol used to verify whether a device – such as a laptop, cloud server, or IoT sensor – has been tampered with. It relies 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-checked proofs of its cryptographic security.
In our paper, we developed the first machine-checked cryptographic verification of digital signatures and remote attestation. We demonstrate 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).
What exactly has been developed?
We defined digital signatures and RA within the SSProve framework, with cryptographic operations and state transitions specified through mathematical reasoning. We then proved that if the underlying digital signature scheme is secure (in the strong, cryptographic sense of unforgeability), then the RA protocol can also be secure. Our development represents the first step for RA and can serve to build real-world application use cases.
The entire formal development was carried out using SSProve, a Rocq Prover-based framework for stateful and modular cryptographic proofs. Our proof developments are available as an open-source repository.
What does this mean for us?
This work strengthens the Barkhausen Institut’s mission of building trustworthy digital systems through formal verification. By providing a machine-checked proof of RA security, we give a widely used yet previously unverified cryptographic mechanism a solid foundation. This advances the Verified System Design Automation group’s goal of trustworthiness by design, from theory all the way to real-world systems.
Where can we find out more about this?
Formally-verified Security against Forgery of Remote Attestation using SSProve
Sara Zain, Barkhausen Institut; Jannik Mähn, Stefan Köpsell, Barkhausen Institut; and Sebastian Ertel, Barkhausen Institut.
Link to the paper: https://arxiv.org/pdf/2502.17653