Achim Brucker a animé un séminaire le 13 septembre 2023

Achim Brucker (University of Exeter, UK) a animé un Seminar@SystemX sur le thème « Verification of Stateful Security Protocols in Isabelle/HOL« , le 13 septembre 2023.

Résumé :

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.

Biographie :

Dr. Achim Brucker is a full Professor in Computer Science (Chair of Cybersecurity) at the University of Exeter, UK and a leading expert in secure software engineering, cyber security, and formal methods. He is the head of the Cybersecurity Group at Exeter and leads the Software Assurance & Security Research Team. From December 2015 to May 2019, he was a Senior Lecturer and Consultant at the Computer Science Department of The University of Sheffield, UK. His current work includes the research on security aspects of distributed, e.g., service-oriented, systems. This includes research in applied security aspects such as access control or business-process modeling as well as in fundamental aspects such as novel techniques in the area of static and dynamic approaches for ensuring the security of applications. Moreover, he is participating in the development of interactive theorem proving environments for Z (HOL-Z) and UML/OCL (HOL-OCL, which is integrated into a formal MDE toolchain) and a model-based test-case generator (HOL-TestGen).

 

Replay du séminaire :

• Pour être informé de nos prochains Seminar@SystemX, rendez-vous ici.