Speaker: Achim Brucker, Chair of Computer Security, University Exeter, GB
Tuesday May 16 2023, 14:00, Room 1Z61
Communication networks like the Internet form a large distributed system where a huge number of components run in parallel, such as security protocols and distributed web applications. For what concerns security, it is obviously infeasible to verify them all at once as one monolithic entity; rather, one has to verify individual components in isolation.
While many typical components like the security protocol TLS have been studied intensively, there exists much less research on analyzing and ensuring the security of the composition of security protocols. This is a problem since the composition of systems that are secure in isolation can easily be insecure.
The verification of security protocols is one of the success stories of formal methods. There is a wide spectrum of methods available, ranging from fully automated methods to interactive theorem proving with proof assistants like Isabelle/HOL. The latter provide overwhelmingly high assurance of the correctness, which automated methods often cannot: due to their complexity, bugs in such automated verification tools are likely and thus the risk of erroneously verifying a flawed protocol is non-negligible. Still, there are only a few works that try to combine advantages from both ends of the spectrum: a high degree of automation and assurance.
In this talk, I will give a general introduction to security protocols and demonstrate selected attacks on them. After this introduction, I will present our work in developing a highly automated and trustworthy protocol verification approach in Isabelle/HOL that supports the verification of (composable) security protocols with a mutable long-term state. The approach also includes a simple user-friendly transaction-based protocol specification language embedded into Isabelle, and can also leverage several results such as soundness of a typed model.
This is joint work with Andreas Hess (DTU, Denmark), Sebastian Mödersheim (DTU, Denmark), and Anders Schlichtkrull (Aalborg University Copenhagen, Denmark).
Publications:
- Andreas V. Hess, Sebastian A. Mödersheim, Achim D. Brucker, Anders Schlichtkrull: Performing Security Proofs of Stateful Protocols. CSF 2021: 1-16
- Andreas V. Hess, Sebastian A. Mödersheim, and Achim D. Brucker: Stateful Protocol Composition in Isabelle/HOL. In ACM Transactions on Privacy and Security, 2023.