On 27 and 28 March, the EuroProofNet Tutorial on 'Usable Formal Methods for Security of Systems' will take place at TU Dresden. The BI will participate with the following two contributions:

Our scientist Dr.-Ing. Carsten Weinhold is going to talk about a novel communication protocol that establishes a secure connection to a remote device and simultaneously verifies that the expected software is running on this device. For this purpose, Carsten and his colleague Dr.-Ing Michael Roitzsch combined the existing techniques Transport Layer Security (TLS) and Remote Attestation in such a way that their security properties add up. Both are of the opinion that none of the combinations of these protocols proposed in related work achieves this and would like to discuss this idea with the other participants. The talk will also cover how this research fits into the broader concept of a modular trust anchor that protects the application that use this protocol.

BI-Scientist Jannik Mähn examines the communication protocol just described from a formal perspective. This means that he and his colleague Sebastian Ertel translated the protocol and its properties into the SSProve tool, based on the "Coq theorem-prover". Then he carried out the proofs in SSProve, which were previously carried out by hand in "pen-and-paper" style. In this way, he could prove the security properties of this protocol with computer support in such a way that sources of error and bugs are avoided as far as possible. This allows to guarantee a higher level of security for the protocol.

More information: https://europroofnet.github.io/wg3-dresden24/

The key idea of this event is to bring together industry designers and formal methods research community to share ideas and experiences on how to improve the tools to reduce the barrier to adoption.